theory Demo5 imports CPure begin

text {* Defining HOL *}

text {* Technical Setup, introducing a new logic *}

classes type 
defaultsort type
typedecl bool 
typedecl ind
arities
  bool :: type
  ind :: type
  "fun" :: (type, type) type

judgment
  Trueprop      :: "bool \<Rightarrow> prop"  ("(_)" 5)

-- ---------------------------------

consts
  Eq            :: "'a \<Rightarrow> 'a \<Rightarrow> bool"      (infixl "=" 50)
  Imp           :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixr "\<longrightarrow>" 25)
  Eps           :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"    (binder "SOME " 10)

consts
  Not           :: "bool \<Rightarrow> bool"           ("\<not> _" [40] 40)
  True          :: bool
  False         :: bool
  If            :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" 10)
  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"   (binder "\<forall>" 10)
  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"   (binder "\<exists>" 10)
  And           :: "bool \<Rightarrow> bool \<Rightarrow> bool"   (infixr "\<and>" 35)
  Or            :: "bool \<Rightarrow> bool \<Rightarrow> bool"   (infixr "\<or>" 30)
  inj           :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
  surj          :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"

text {* Additional concrete syntax *}
syntax
  "_not_equal"  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<noteq>" 50)
translations
  "x \<noteq> y"  == "\<not>(x = y)"



text {* Axioms and basic definitions *}

axioms
  refl:  "t = t"
  subst: "\<lbrakk> s = t; P s \<rbrakk> \<Longrightarrow> P t"
  ext:   "(\<And>x. f x = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)"
  impI:  "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q"
  mp:    "\<lbrakk> P\<longrightarrow>Q;  P \<rbrakk> \<Longrightarrow> Q"
  iff:   "(P\<longrightarrow>Q) \<longrightarrow> (Q\<longrightarrow>P) \<longrightarrow> (P=Q)"
  someI: "P x \<Longrightarrow> P (SOME x. P x)"
  True_or_False: "(P=True) \<or> (P=False)"
  infinity: "\<exists>f :: ind \<Rightarrow> ind. inj f \<and> \<not>surj f"


defs
  True_def:  "True   \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
  All_def:   "All P  \<equiv> (P = (\<lambda>x. True))"
  Ex_def:    "Ex P   \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
  False_def: "False  \<equiv> (\<forall>P. P)"
  not_def:   "\<not> P    \<equiv> P \<longrightarrow> False"
  and_def:   "P \<and> Q  \<equiv> \<forall>R. (P\<longrightarrow>Q\<longrightarrow>R) \<longrightarrow> R"
  or_def:    "P \<or> Q  \<equiv> \<forall>R. (P\<longrightarrow>R) \<longrightarrow> (Q\<longrightarrow>R) \<longrightarrow> R"
  if_def:    "If P x y \<equiv> SOME z. (P=True \<longrightarrow> z=x) \<and> (P=False \<longrightarrow> z=y)"
  inj_def:   "inj f  \<equiv> \<forall>x y. f x = f y \<longrightarrow> x = y"
  surj_def:  "surj f \<equiv> \<forall>y. \<exists>x. y = f x"


text {* Deriving the standard proof rules in HOL *}


text {* Implication *}

-- {* we want to show @{text "\<lbrakk> P \<longrightarrow> Q; P; Q \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"} *}
lemma impE:
  assumes PQ: "P \<longrightarrow> Q"
  assumes P: "P"
  assumes R: "Q \<Longrightarrow> R"
  shows "R"
  apply (rule R)
  apply (insert PQ)
  apply (drule mp)
   apply (rule P)
  apply assumption
  done


-- -------------------------------

text {* True *}

lemma TrueI: "True"
  apply (unfold True_def)
  apply (rule refl)
  done


text {* side track: Equality *}

lemma sym: "s = t \<Longrightarrow> t = s"
  apply (erule subst)
  apply (rule refl)
  done

lemma fun_cong: "f = g \<Longrightarrow> f x = g x"
  apply (erule subst)
  apply (rule refl)
  done

lemma iffI:
  assumes PQ: "P \<Longrightarrow> Q"
  assumes QP: "Q \<Longrightarrow> P"
  shows "P = Q"
  apply (rule mp)
   apply (rule mp)
    apply (insert iff [where P=P and Q=Q])  
    apply assumption
   apply (rule impI)
   apply (rule PQ)
   apply assumption
  apply (rule impI)
  apply (rule QP)
  apply assumption
  done

lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P"
  apply (rule subst)
   apply assumption
  apply assumption
  done

lemma iffD2: "P = Q \<Longrightarrow> Q \<Longrightarrow> P"
  apply (drule sym)
  apply (drule iffD1)
   apply assumption
  apply assumption
  done


text {* back to True *}

lemma eqTrueI: "P \<Longrightarrow> P = True" 
  apply (rule iffI)
   apply (rule TrueI)
  apply assumption
  done

lemma eqTrueE: "P = True \<Longrightarrow> P"
  apply (drule iffD2)
   apply (rule TrueI)
  apply assumption
  done


-- -------------------------------

text {* Universial Quantifier *}

lemma allI: 
  assumes P: "\<And>x. P x"
  shows "\<forall>x. P x"
  apply (unfold All_def)
  apply (rule ext)
  apply (rule eqTrueI)
  apply (rule P)
  done

lemma spec: "\<forall>x. P x \<Longrightarrow> P x"
  apply (unfold All_def)
  apply (rule eqTrueE)
  apply (drule fun_cong)
  apply assumption
  done
 
lemma allE:
  assumes all: "\<forall>x. P x" 
  assumes R: "P x \<Longrightarrow> R" 
  shows "R"
  apply (rule R)
  apply (rule spec, assumption)
  done

-- -------------------------------

text {* False *}

lemma FalseE:
  "False \<Longrightarrow> P"
  apply (unfold False_def)
  apply (erule allE)
  apply assumption
  done

lemma False_neq_True:
  "False = True \<Longrightarrow> P"
  apply (drule eqTrueE)
  apply (erule FalseE)
  done
  

-- -------------------------------

text {* Negation *}

lemma notI:
  assumes P: "P \<Longrightarrow> False"
  shows "\<not>P"
  apply (unfold not_def)
  apply (rule impI)
  apply (rule P)
  apply assumption
  done

lemma notE: "\<lbrakk> \<not>P; P \<rbrakk> \<Longrightarrow> R"
  apply (unfold not_def)
  apply (erule impE)
   apply assumption
  apply (erule FalseE)
  done

lemma False_not_True: "False \<noteq> True"
  apply (rule notI)
  apply (erule False_neq_True)
  done


-- -------------------------------

text {* Existential Quantifier *}

lemma exI:
  "P x \<Longrightarrow> \<exists>x. P x"
  apply (unfold Ex_def)
  apply (rule allI)
  apply (rule impI)
  apply (erule allE)
  apply (erule impE)
   apply assumption
  apply assumption
  done
  
lemma exE:
  assumes ex: "\<exists>x. P x"
  assumes R: "\<And>x. P x \<Longrightarrow> R"
  shows "R"
  apply (insert ex)
  apply (unfold Ex_def)
  apply (drule spec)
  apply (drule mp)
   apply (rule allI)
   apply (rule impI)
   apply (rule R)
   apply assumption
  apply assumption
  done


-- -------------------------------

text {* Conjunction *}

lemma conjI: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> Q"
  apply (unfold and_def)
  apply (rule allI)
  apply (rule impI)
  apply (erule impE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply assumption
  done

lemma conjE:
  assumes PQ: "P \<and> Q"
  assumes R: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> R"
  shows R
  apply (insert PQ)
  apply (unfold and_def)
  apply (erule allE)
  apply (erule impE)
   apply (rule impI)
   apply (rule impI)
   apply (rule R)
    apply assumption
   apply assumption
  apply assumption
  done


-- -------------------------------

text {* Disjunction *}

lemma disjI1:
  "P \<Longrightarrow> P \<or> Q"
  apply (unfold or_def)
  apply (rule allI)
  apply (rule impI)
  apply (rule impI)
  apply (erule impE)
   apply assumption
  apply assumption
  done

lemma disjI2:
  "Q \<Longrightarrow> P \<or> Q"
  apply (unfold or_def)
  apply (rule allI)
  apply (rule impI)
  apply (rule impI)
  apply (erule impE, assumption, assumption)
  done

lemma disjE:
  assumes PQ: "P \<or> Q"
  assumes P: "P \<Longrightarrow> R"
  assumes Q: "Q \<Longrightarrow> R"
  shows "R"
  apply (insert PQ)
  apply (unfold or_def)
  apply (erule allE)
  apply (erule impE)
   apply (rule impI)
   apply (rule P)
   apply assumption
  apply (erule impE)
   apply (rule impI)
   apply (rule Q)
   apply assumption
  apply assumption
  done


-- -------------------------------

text {* Classical Logic *}

lemma classical:
  assumes P: "\<not>P \<Longrightarrow> P"
  shows P
  apply (insert True_or_False [where P=P])
  apply (erule disjE)
   apply (erule eqTrueE)
  apply (rule P)
  apply (rule notI)
  apply (rule subst)
   apply assumption
  apply assumption
  done


lemma notnotD:
  "\<not>\<not>P \<Longrightarrow> P"
  apply (rule classical)
  apply (erule notE)
  apply assumption
  done

lemma disjCI:
  assumes P: "\<not>Q \<Longrightarrow> P"
  shows "P \<or> Q"
  apply (rule classical)
  apply (rule disjI1)
  apply (rule P)
  apply (rule notI)
  apply (erule notE)
  apply (rule disjI2)
  apply assumption
  done

lemma tertium_non_datur: 
  "P \<or> \<not>P"
  apply (rule disjCI)
  apply (drule notnotD)
  apply assumption
  done


-- -------------------------------

text {* Choice *}

lemma someI_ex: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)"
  apply (erule exE)
  apply (erule someI)
  done

lemma someI2:
  assumes a: "P a" 
  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x" 
  shows "Q (SOME x. P x)"
  apply (insert a) 
  apply (drule someI, drule PQ)
  apply assumption
  done

lemma some_equality:
  assumes a: "P a"
  assumes P: "\<And>x. P x \<Longrightarrow> x=a"
  shows "(SOME x. P x) = a"
  apply (rule someI2)
   apply (rule a)
  apply (rule P)
  apply assumption
  done

lemma some_eq_ex: 
  "P (SOME x. P x) = (\<exists>x. P x)"
  apply (rule iffI)
   apply (rule exI)
   apply assumption
  apply (erule someI_ex)
  done


-- -------------------------------

text {* if-then-else *}

lemma if_True:
  "(if True then s else t) = s"
  apply (unfold if_def)
  apply (rule some_equality)
   apply (rule conjI)
    apply (rule impI)
    apply (rule refl)
   apply (rule impI)
   apply (drule sym)
   apply (erule False_neq_True)
  apply (erule conjE)
  apply (erule impE)
   apply (rule refl)
  apply assumption
  done

lemma if_False:
  "(if False then s else t) = t"
  apply (unfold if_def)
  apply (rule some_equality)
   apply (rule conjI)
    apply (rule impI)
    apply (erule False_neq_True)
   apply (rule impI)
   apply (rule refl)
  apply (erule conjE)
  apply (erule impE, rule refl)
  apply assumption
  done
  
  
end
