theory week03A_demo_HOL imports Pure begin text \Defining HOL\ text \Technical Setup, introducing a new logic\ 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 \ 'b, type_class)" instance "fun" :: (type, type) type by (rule fun_arity) judgment Trueprop :: "bool \ prop" ("(_)" 5) \ \---------------------------------\ axiomatization Eq :: "'a \ 'a \ bool" (infixl "=" 50) and Imp :: "bool \ bool \ bool" (infixr "\" 25) and Eps :: "('a \ bool) \ 'a" (binder "SOME" 10) definition True :: bool where "True \ (\x::bool. x) = (\x. x)" definition All :: "('a \ bool) \ bool" (binder "\" 10) where "All P \ P = (\x. True)" definition Ex :: "('a \ bool) \ bool" (binder "\" 10) where "Ex P \ \Q. (\x. P x \ Q) \ Q" definition False :: bool where "False \ \P. P" definition Not :: "bool \ bool" ("\ _" [40] 40) where "\ P \ P \ False" definition And :: "[bool, bool] \ bool" (infixr "\" 35) where "P \ Q \ \R. (P \ Q \ R) \ R" definition Or :: "[bool, bool] \ bool" (infixr "\" 30) where "P \ Q \ \R. (P \ R) \ (Q \ R) \ R" definition If:: "bool \ 'a \ 'a \ 'a" ("(if (_)/ then (_)/ else (_))" 10) where "If P x y \ SOME z. (P=True \ z=x) \ (P=False \ z=y)" definition inj:: "('a \ 'b) \ bool" where "inj f \ \x y. f x = f y \ x = y" definition surj:: "('a \ 'b) \ bool" where "surj f \ \y. \x. y = f x" text \Additional concrete syntax\ abbreviation "not_equal" :: "'a \ 'a \ bool" (infixl "\" 50) where "x \ y \ \(x = y)" text \Axioms and basic definitions\ axiomatization where refl: "t = t" and subst: "\ s = t; P s \ \ P t" and ext: "(\x. f x = g x) \ (\x. f x) = (\x. g x)" for t::'a and f :: "'b \ 'c" axiomatization where impI: "(P \ Q) \ P \ Q" and mp: "\ P\Q; P \ \ Q" and iff: "(P\Q) \ (Q\P) \ (P=Q)" and True_or_False: "(P=True) \ (P=False)" and infinity: "\f :: ind \ ind. inj f \ \surj f" axiomatization where someI: "P x \ P (SOME x. P x)" for x :: 'a text \Deriving the standard proof rules in HOL\ text \Implication\ thm mp \ \we want to show @{text "\ P \ Q; P; Q \ R \ \ R"}\ lemma impE: assumes PQ: "P \ Q" assumes P: "P" assumes QR: "Q \ R" shows "R" apply (rule QR) 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 \ t = s" thm subst apply (erule subst) apply (rule refl) done lemma fun_cong: "f = g \ f x = g x" thm subst apply (erule subst) apply (rule refl) done thm mp thm iff lemma iffI: assumes PQ: "P \ Q" assumes QP: "Q \ 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 \ Q \ P" apply (rule subst) apply assumption apply assumption done lemma iffD2: "P = Q \ Q \ P" thm sym apply (drule sym) apply (erule iffD1) apply assumption done text \back to True\ lemma eqTrueI: "P \ P = True" apply (rule iffI) apply (rule TrueI) apply assumption done lemma eqTrueE: "P = True \ P" thm iffD2 apply (drule iffD2) apply (rule TrueI) apply assumption done \ \-------------------------------\ text \Universal Quantifier\ lemma allI: assumes P: "\x. P x" shows "\x. P x" apply (unfold All_def) apply (rule ext) thm eqTrueI apply (rule eqTrueI) apply (rule P) done lemma spec: "\x. P x \ P x" apply (unfold All_def) thm eqTrueE apply (rule eqTrueE) thm fun_cong apply (drule fun_cong) apply assumption done lemma allE: assumes all: "\x. P x" assumes R: "P x \ R" shows "R" apply (rule R) apply (insert all) apply (erule spec) done \ \-------------------------------\ text \False\ lemma FalseE: "False \ P" apply (unfold False_def) apply (erule_tac x=P in allE) apply assumption done lemma False_neq_True: "False = True \ P" thm eqTrueE apply (drule eqTrueE) apply (erule FalseE) done \ \-------------------------------\ text \Negation\ lemma notI: assumes P: "P \ False" shows "\P" apply (unfold Not_def) apply (rule impI) apply (rule P) apply assumption done lemma notE: "\ \P; P \ \ R" apply (unfold Not_def) apply (erule impE) apply assumption apply (erule FalseE) done lemma False_not_True: "False \ True" apply (rule notI) thm False_neq_True apply (erule False_neq_True) done \ \-------------------------------\ text \Existential Quantifier\ lemma exI: "P x \ \x. P x" apply (unfold Ex_def) apply (rule allI) apply (rule impI) apply (erule_tac x=x in allE) apply (erule impE) apply assumption apply assumption done lemma exE: assumes ex: "\x. P x" assumes R: "\x. P x \ R" shows "R" apply (insert ex) apply (unfold Ex_def) thm spec apply (drule spec) thm mp apply (drule mp) apply (rule allI) apply (rule impI) apply (rule R) apply assumption apply assumption done \ \-------------------------------\ text \Conjunction\ lemma conjI: "\ P; Q \ \ P \ 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 \ Q" assumes R: "\ P; Q \ \ 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 \ P \ 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 \ P \ 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 \ Q" assumes P: "P \ R" assumes Q: "Q \ 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: "\P \ 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: "\\P \ P" apply (rule classical) apply (erule notE) apply assumption done lemma disjCI: assumes P: "\Q \ P" shows "P \ 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 \ \P" apply (rule disjCI) apply (drule notnotD) apply assumption done \ \-------------------------------\ text \Choice\ lemma someI_ex: "\x. P x \ P (SOME x. P x)" apply (erule exE) apply (erule someI) done lemma someI2: assumes a: "P a" assumes PQ: "\x. P x \ 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: "\x. P x \ 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) = (\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) thm some_equality 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