theory week03A_demo_HOL imports Pure begin

text \<open>Defining HOL\<close>

text \<open>Technical Setup, introducing a new logic\<close>

class type
default_sort type

typedecl bool
typedecl ind

axiomatization where bool_arity: "OFCLASS(bool, type_class)"
instance "bool" :: type by (rule bool_arity)

axiomatization where ind_arity: "OFCLASS(ind, type_class)"
instance "ind" :: type by (rule ind_arity)

axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
instance "fun" :: (type, type) type by (rule fun_arity)

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

\<comment> \<open>---------------------------------\<close>

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

definition True :: bool where
  "True \<equiv> (\<lambda>x::bool. x) = (\<lambda>x. x)"

definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>" 10) where
  "All P \<equiv> P = (\<lambda>x. True)"

definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>" 10) where
  "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"

definition False :: bool where
  "False \<equiv> \<forall>P. P"

definition Not :: "bool \<Rightarrow> bool"  ("\<not> _" [40] 40) where
  "\<not> P \<equiv> P \<longrightarrow> False"

definition And :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<and>" 35) where
  "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"

definition Or :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30) where
  "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"

definition If:: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" 10) where
  "If P x y \<equiv> SOME z. (P=True \<longrightarrow> z=x) \<and> (P=False \<longrightarrow> z=y)"

definition inj:: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where
  "inj f  \<equiv> \<forall>x y. f x = f y \<longrightarrow> x = y"

definition  surj:: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where
  "surj f \<equiv> \<forall>y. \<exists>x. y = f x"




text \<open>Additional concrete syntax\<close>

abbreviation
  "not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<noteq>" 50) where
  "x \<noteq> y \<equiv> \<not>(x = y)"


text \<open>Axioms and basic definitions\<close>

axiomatization where
  refl:  "t = t" and
  subst: "\<lbrakk> s = t; P s \<rbrakk> \<Longrightarrow> P t" and
  ext:   "(\<And>x. f x = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)" 
  for t::'a and f :: "'b \<Rightarrow> 'c"

axiomatization where
  impI:  "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
  mp:    "\<lbrakk> P\<longrightarrow>Q; P \<rbrakk> \<Longrightarrow> Q" and
  iff:   "(P\<longrightarrow>Q) \<longrightarrow> (Q\<longrightarrow>P) \<longrightarrow> (P=Q)" and
  True_or_False: "(P=True) \<or> (P=False)" and
  infinity: "\<exists>f :: ind \<Rightarrow> ind. inj f \<and> \<not>surj f"

axiomatization where
  someI: "P x \<Longrightarrow> P (SOME x. P x)" for x :: 'a


text \<open>Deriving the standard proof rules in HOL\<close>


text \<open>Implication\<close>

thm mp

\<comment> \<open>we want to show @{text "\<lbrakk> P \<longrightarrow> Q; P; Q \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"}\<close>
lemma impE:
  assumes PQ: "P \<longrightarrow> Q"
  assumes P: "P"
  assumes QR: "Q \<Longrightarrow> R"
  shows "R"
  sorry

\<comment> \<open>-------------------------------\<close>

text \<open>True\<close>

lemma TrueI: "True"
  sorry

text \<open>side track: Equality\<close>

lemma sym: "s = t \<Longrightarrow> t = s" thm subst
  sorry

lemma fun_cong: "f = g \<Longrightarrow> f x = g x" thm subst
  sorry

thm mp
thm iff
lemma iffI:
  assumes PQ: "P \<Longrightarrow> Q"
  assumes QP: "Q \<Longrightarrow> P"
  shows "P = Q"
  sorry

lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P"
  sorry

lemma iffD2: "P = Q \<Longrightarrow> Q \<Longrightarrow> P" thm sym
  sorry


text \<open>back to True\<close>

lemma eqTrueI: "P \<Longrightarrow> P = True"
  sorry

lemma eqTrueE: "P = True \<Longrightarrow> P" thm iffD2
  sorry


\<comment> \<open>-------------------------------\<close>

text \<open>Universal Quantifier\<close>

lemma allI:
  assumes P: "\<And>x. P x"
  shows "\<forall>x. P x"
  sorry

lemma spec: "\<forall>x. P x \<Longrightarrow> P x"
  sorry

lemma allE:
  assumes all: "\<forall>x. P x"
  assumes R: "P x \<Longrightarrow> R"
  shows "R"
  sorry

\<comment> \<open>-------------------------------\<close>

text \<open>False\<close>

lemma FalseE:
  "False \<Longrightarrow> P"
  sorry

lemma False_neq_True:
  "False = True \<Longrightarrow> P"  thm eqTrueE
  sorry


\<comment> \<open>-------------------------------\<close>

text \<open>Negation\<close>

lemma notI:
  assumes P: "P \<Longrightarrow> False"
  shows "\<not>P"
  sorry

lemma notE: "\<lbrakk> \<not>P; P \<rbrakk> \<Longrightarrow> R"
  sorry

lemma False_not_True: "False \<noteq> True"
  sorry


\<comment> \<open>-------------------------------\<close>

text \<open>Existential Quantifier\<close>

lemma exI:
  "P x \<Longrightarrow> \<exists>x. P x"
  sorry

lemma exE:
  assumes ex: "\<exists>x. P x"
  assumes R: "\<And>x. P x \<Longrightarrow> R"
  shows "R"
  sorry


\<comment> \<open>-------------------------------\<close>

text \<open>Conjunction\<close>

lemma conjI: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> Q"
  sorry

lemma conjE:
  assumes PQ: "P \<and> Q"
  assumes R: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> R"
  shows R
  sorry

\<comment> \<open>-------------------------------\<close>

text \<open>Disjunction\<close>

lemma disjI1:
  "P \<Longrightarrow> P \<or> Q"
  sorry

lemma disjI2:
  "Q \<Longrightarrow> P \<or> Q"
  sorry

lemma disjE:
  assumes PQ: "P \<or> Q"
  assumes P: "P \<Longrightarrow> R"
  assumes Q: "Q \<Longrightarrow> R"
  shows "R"
  sorry


\<comment> \<open>-------------------------------\<close>

text \<open>Classical Logic\<close>

lemma classical:
  assumes P: "\<not>P \<Longrightarrow> P"
  shows P
  sorry


lemma notnotD:
  "\<not>\<not>P \<Longrightarrow> P"
  sorry

lemma disjCI:
  assumes P: "\<not>Q \<Longrightarrow> P"
  shows "P \<or> Q"
  sorry

lemma tertium_non_datur:
  "P \<or> \<not>P"
  sorry


\<comment> \<open>-------------------------------\<close>

text \<open>Choice\<close>

lemma someI_ex: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)"
  sorry

lemma someI2:
  assumes a: "P a"
  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
  shows "Q (SOME x. P x)"
  sorry

lemma some_equality:
  assumes a: "P a"
  assumes P: "\<And>x. P x \<Longrightarrow> x=a"
  shows "(SOME x. P x) = a"
  sorry

lemma some_eq_ex:
  "P (SOME x. P x) = (\<exists>x. P x)"
  sorry


\<comment> \<open>-------------------------------\<close>

text \<open>if-then-else\<close>

lemma if_True:
  "(if True then s else t) = s"
  sorry

lemma if_False:
  "(if False then s else t) = t"
  sorry

end
