(* Title:   G3cp.thy
   Author:  Peter Chapman, Department of Computer Science, University of St Andrews
   
*)

header {*  Propositional part of the classical Gentzen style Calculus G3 *}

theory G3cp
imports Sequents

begin

global

classes "term"
defaultsort "term"

consts

 Trueprop :: "two_seqi"

  True       :: o     
  False      :: o    
  "="        :: "['a,'a] =>  o "  (infixl 50)
  Not        :: "o => o"         ("~ _"  [40] 40)
  "&"        :: "[o,o] => o"     (infixr 35)
  "|"       :: "[o,o] => o"      (infixr 30) 
  "-->"       :: "[o,o] => o"      (infixr 25)
  "<->"      :: "[o,o] => o "     (infixr 25)
  The       :: "('a => o ) => 'a"  (binder "THE " 10)


syntax
  "@Trueprop"  ::  "two_seqe" ("((_)/ |- (_))" [6,6] 5)
  "_not_equal" ::  "['a,'a] => o"   (infixl "~=" 50)


parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *} 
print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}

syntax (xsymbols)
  True      :: o        ("\<top>")
  False     :: o        ("\<bottom>")
  Not       :: "o => o"        ("\<not> _" [40] 40)
  "op &"    :: "[o,o] \<Rightarrow>  o"   (infixr "\<and>" 35)
  "op |"    :: "[o,o] \<Rightarrow>  o"   (infixr "\<or>" 30)
  "op -->"  :: "[o,o] \<Rightarrow> o"    (infixr "\<supset>" 25)
  "op <->"   :: "[o,o] \<Rightarrow> o"    (infixr "\<leftrightarrow>" 20)

local

axioms

  cut: "[|  $H |- A, $G ; A, $H |- $F |] ==> $H |- $F"
  exchangeL: "$H, $G |- $F ==> $G, $H |- $F"
  exchangeR: "$F |- $H, $G ==> $F |- $G, $H"
  iff: " $F |- $G, (A --> B) & (B --> A), $H  ==> $F |- $G ,(A <-> B), $H"

   notL: "A, $H |- $F,$G ==> $H |- $F, ~A, $G"  
  notR: "$F,$G |- A, $H ==> $F, ~A, $G |- $H"

 (*Propositional Rules*)

  basic: "$H, P, $G  |- $F, P, $E"
  false:  "$H, False, $G |- $F"

  conjL: "A, B, $H, $G |- $F ==> $G, A & B, $H |- $F"
  conjR: "[| $H |- $G, A, $F ; $H |- $G, B, $F |] ==> $H |- $G, A & B, $F"

  disjL: "[|  A, $H, $G |- $F ; B, $H, $G |- $F |] ==> $G, A | B, $H |- $F"
  disjR: "$H |- A, B, $G, $F ==> $H |- $G, A | B, $F"

  impR: "A, $H |- B, $G, $F ==> $H |- $G, A --> B, $F"
  impL: "[| $G, $F |- $H, A ; B, $G, $F |- $H |] ==> $G, A --> B, $F |- $H"

  True_def: "True == False --> False "
  iff_def: "P <-> Q == (P --> Q) & (Q --> P)"


  (* Equality *)

  refl: "$H |- a=a"
  subst: "$H(a), $G(a) |- E(a) ==> $H(b), a=b, $G(b) |- E(b)"


  (* Reflection *)

  eq_reflection: "|- x=y ==> (x==y)"
  iff_reflection: "|- P <-> Q ==> (P == Q)"

ML {* val G3cp_SOLVE =  REPEAT (FIRST [rtac (thm "impR") 1, rtac (thm "conjL") 1, rtac (thm "disjR") 1, rtac (thm "notR") 1, rtac (thm "notL") 1, rtac (thm "iff") 1, rtac (thm "conjR") 1, rtac (thm "disjL") 1, rtac (thm "impL") 1,rtac (thm "false") 1, rtac (thm "basic") 1]); *}

end