# 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 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

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