Quelle  Export.thy

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 ‹
  export the Haskell code run:
 begin{verbatim}
 > isabelle build -e -D .
 end{verbatim}

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

  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}

  output is pretty-printed.
 ›

end