Theory Export

section ‹Export›

theory Export imports Prover begin

definition ‹prove_sequent ≡ i.mkTree eff rules›
definition ‹prove ≡ λp. prove_sequent ([], [p])›

declare Stream.smember_code [code del]
lemma [code]: ‹Stream.smember x (y ## s) = (x = y ∨ Stream.smember x s)›
  unfolding Stream.smember_def by auto

code_printing
  constant the ⇀ (Haskell) "(\\x -> case x of { Just y -> y })"
  | constant Option.is_none ⇀ (Haskell) "(\\x -> case x of { Just y -> False; Nothing -> True })"

code_identifier
  code_module Product_Type ⇀ (Haskell) Arith
  | code_module Orderings ⇀ (Haskell) Arith
  | code_module Arith ⇀ (Haskell) Prover
  | code_module MaybeExt ⇀ (Haskell) Prover
  | code_module List ⇀ (Haskell) Prover
  | code_module Nat_Bijection ⇀ (Haskell) Prover
  | code_module Syntax ⇀ (Haskell) Prover
  | code_module Encoding ⇀ (Haskell) Prover
  | code_module HOL ⇀ (Haskell) Prover
  | code_module Set ⇀ (Haskell) Prover
  | code_module FSet ⇀ (Haskell) Prover
  | code_module Stream ⇀ (Haskell) Prover
  | code_module Fair_Stream ⇀ (Haskell) Prover
  | code_module Sum_Type ⇀ (Haskell) Prover
  | code_module Abstract_Completeness ⇀ (Haskell) Prover
  | code_module Export ⇀ (Haskell) Prover

export_code open prove in Haskell

text ‹
To export the Haskell code run:
\begin{verbatim}
  > isabelle build -e -D .
\end{verbatim}

To compile the exported code run:
\begin{verbatim}
  > ghc -O2 -i./program Main.hs
\end{verbatim}

To prove a formula, supply it using raw constructor names, e.g.:
\begin{verbatim}
  > ./Main "Imp (Pre 0 []) (Imp (Pre 1 []) (Pre 0 []))"
  |- (P) --> ((Q) --> (P))
  + ImpR on P and (Q) --> (P)
  P |- (Q) --> (P)
  + ImpR on Q and P
  Q, P |- P
 + Axiom on P
\end{verbatim}

The output is pretty-printed.
›

end