header {* Very Simple Propositional Logic *}
theory VSPL
imports CPure
begin

typedecl o

judgment
  Trueprop  :: "o => prop"                  ("(_)" 5)

consts
  False   :: o
  And     :: "[o, o] => o"                (infixr "&" 35)
  Implies :: "[o, o] => o"                (infixr "-->" 25)
 
axioms
  conjI:  "[| P;  Q |] ==> P&Q"
  conjE1: "[| P&Q |] ==> P"
  conjE2: "[| P&Q |] ==> Q"

  impI:   "(P ==> Q) ==> P -->Q"
  impE:   "[| P-->Q ; P|] ==> Q"

  False:  "[| False |] ==> P"
  Raa:    "[| P--> False ==> False |] ==> P"

lemma conj_comm: "P & Q --> Q & P"
  apply (rule impI)
  apply (rule conjI)
  apply (erule conjE2)
  apply (erule conjE1)
  done

lemma tafelbeweis: "(A --> (B--> C))--> (A & B --> C)"
  apply (rule impI)
  apply (rule impI)
  apply (rule impE [where P="B"]) 
  apply (erule impE [where P="A"])
  apply (erule conjE1)
  apply (erule conjE2)
  done

lemma doubleneg: "((P --> False)--> False)--> P"
  apply (rule impI)
  apply (rule Raa)
  apply (rule impE [where P="P--> False"])
  apply (assumption)
  apply (assumption)
  done

constdefs
  Not    :: "o => o"                     ("~ _" [40] 40)
  "~P    == P-->False"

lemma notnot: "~~ P--> P"
  apply (unfold Not_def)
  apply (rule doubleneg)
  done

lemma notnot2: "P --> ~~P"
  apply (unfold Not_def)
  apply (rule impI)
  apply (rule impI)
  apply (erule impE)
  apply (assumption)
  done

lemma notI: "[| P ==> False |] ==> ~P"
  apply (unfold Not_def)
  apply (drule impI) 
  apply (assumption)
  done

lemma notE: "[| ~P; P |] ==> False"
  apply (unfold Not_def)
  apply (erule impE)
  apply (assumption)
  done

lemmas Raa' = Raa [folded Not_def]

constdefs
  Or  :: "[o, o] => o"                (infixr "|" 30)
  "P | Q == ~(~P & ~Q)"

lemma disjI1: "P ==> P | Q"
  apply (unfold Or_def)
  apply (rule notI)
  apply (rule notE [where P="P"])
  apply (erule conjE1) 
  apply (assumption)
  done

lemma disjI2: "Q ==> P | Q"
  apply (unfold Or_def)
  apply (rule notI)
  apply (rule notE [where P="Q"])
  apply (erule conjE2) 
  apply (assumption)
  done

text{* disjE left as an exercise *}
lemma disjE: "[| P | Q; P==> R; Q ==> R |] ==> R"
  apply (unfold Or_def)
  apply (rule Raa')
  apply (rule notE [where P="~P & ~Q"])
  apply (assumption)
  apply (thin_tac "~ (~ P & ~ Q)") 
  apply (rule conjI)
  apply (rule notI)
  apply (erule notE)
  apply (drule impI)
  apply (drule impE)
  apply (assumption, assumption)
  apply (rule notI)
  apply (erule notE)
  apply (drule impI [where P="Q"])
  apply (drule impE)
  apply (assumption, assumption)
  done

constdefs
  Iff :: "[o, o] => o"               (infixr "<-->" 20)
  "P <--> Q == ((P --> Q) & (Q --> P))"

lemma iffI: "[| P--> Q; Q --> P |] ==> P <--> Q"
  apply (unfold Iff_def)
  apply (rule conjI)
  apply (assumption)
  apply (assumption)
  done

lemma iffE1: "[| P <--> Q |] ==> (P --> Q)"
  apply (unfold Iff_def)
  apply (erule conjE1)
  done

lemma iffE2: "[| P <--> Q |] ==> (Q --> P)"
  apply (unfold Iff_def)
  apply (erule conjE2)
  done

lemma iff_notnot: "~~ P <--> P"
  apply (rule iffI)
  apply (rule notnot)
  apply (rule notnot2)
  done

lemma imp_refl: "P --> P"
  apply (rule impI)
  apply (assumption)
  done


lemma iff_refl: "P <--> P"
  apply (rule iffI)
  apply (rule imp_refl)
  apply (rule imp_refl)
  done


constdefs
  True    :: o
  "True   == ~ False"

lemma trueI: "True"
  apply (unfold True_def)
  apply (rule notI)
  apply (assumption) 
  done

lemma trueE: "[| True --> P |] ==> P"
  apply (rule impE [where P= "True"])
  apply (assumption)
  apply (rule trueI)
  done

end