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

header {*  Propositional part of the intuitionistic Gentzen style Calculus G4 *}

theory G4ip
imports Sequents

begin

global

classes "term"
defaultsort "term"

consts

 Trueprop :: "single_seqi"

  True       :: o     
  False      :: o    
  "="        :: "['a,'a] =>  o "  (infixl 50)
  Not        :: "o => o"         ("~_"  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"  ::  "single_seqe" ("((_)/ |- (_))" [6,6] 5)
  "_not_equal" ::  "['a,'a] => o"   (infixl "~=" 50)


parse_translation {* [("@Trueprop", single_tr "Trueprop")] *} 
print_translation {* [("Trueprop", single_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 ; A, $H |- C |] ==> $H |- C"

 (*Propositional Rules*)

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

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

  disjL: "[| $G,  A, $H |- C ; $G,  B, $H |- C |] ==> $G, A | B, $H |- C"
  disjR1: "$H |- A ==> $H |- A | B"
  disjR2: "$H |- B ==> $H |- A | B"

  impR: "A, $H |- B ==> $H |- A --> B"

  iff: " $F |-  (A --> B) & (B --> A)  ==> $F |- (A <-> B)"
 
  (* NEED TO REPLACE impL WITH THE FOUR RULES OF G4ip *)
  impLconj: "$G, A --> B --> C, $H |- D ==> $G, (A & B) --> C, $H |- D"
  impLdisj: "$G, A --> B, C --> B, $H |- D ==> $G, (A | C) --> B, $H |- D"
  impLimp: "[| $G, C --> A, $H |- B --> C ; $G, A, $H |- D |] ==> $G, (B --> C) --> A, $H |- D"
  impLatom: "B, P, $F, $G, $H |- D ==> $F,P --> B, $G,  P, $H |- D"

 
  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)"


(* constdefs
 If :: "[o, 'a, 'a] \<Rightarrow> 'a"  ("(if (_)/ then (_)/ else (_))" 10)
 "If(P,x,y) == THE z::'a. (P \<supset> z=x) \<and> (\<not>P \<supset> z=y)" *)

ML {* val G4ip_SOLVE = DEPTH_SOLVE (FIRST [rtac (thm "impR") 1, rtac (thm "conjL") 1, rtac (thm "iff") 1, rtac (thm "impLconj") 1, rtac (thm "impLdisj") 1, rtac (thm "impLatom") 1, rtac (thm "conjR") 1, rtac (thm "disjL") 1, rtac (thm "impLimp") 1 ,rtac (thm "false") 1, rtac (thm "basic") 1, (rtac (thm "disjR1") 1 APPEND rtac (thm "disjR2") 1)]); *}


end