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

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

theory G3ip
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: "A, B, $H, $G |- C ==> $G, A & B, $H |- C"
  conjR: "[| $H |- A ; $H |- B |] ==> $H |- A & B"

  disjL: "[|  A, $H, $G |- C ; B, $H, $G |- 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"
  impL: "[| A --> B, $H, $G |- A ; B, $H,$G |- C |] ==> $G ,A --> B, $H |- C"

  iff: " $F |-  (A --> B) & (B --> A)  ==> $F |- (A <-> B)"

  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 G3ip_SOLVE = DEPTH_SOLVE (CHANGED (FIRST [rtac (thm "basic") 1, rtac (thm "false") 1,rtac (thm "impR") 1, rtac (thm "conjL") 1, rtac (thm "iff") 1, rtac (thm "conjR") 1, rtac (thm "disjL") 1, rtac (thm "impL") 1 THEN distinct_subgoals_tac,rtac (thm "false") 1, rtac (thm "basic") 1, (rtac (thm "disjR1") 1 APPEND rtac (thm "disjR2") 1), distinct_subgoals_tac])); *}

end