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" sorry \ \-------------------------------\ text \True\ lemma TrueI: "True" sorry text \side track: Equality\ lemma sym: "s = t \ t = s" thm subst sorry lemma fun_cong: "f = g \ f x = g x" thm subst sorry thm mp thm iff lemma iffI: assumes PQ: "P \ Q" assumes QP: "Q \ P" shows "P = Q" sorry lemma iffD1: "Q = P \ Q \ P" sorry lemma iffD2: "P = Q \ Q \ P" thm sym sorry text \back to True\ lemma eqTrueI: "P \ P = True" sorry lemma eqTrueE: "P = True \ P" thm iffD2 sorry \ \-------------------------------\ text \Universal Quantifier\ lemma allI: assumes P: "\x. P x" shows "\x. P x" sorry lemma spec: "\x. P x \ P x" sorry lemma allE: assumes all: "\x. P x" assumes R: "P x \ R" shows "R" sorry \ \-------------------------------\ text \False\ lemma FalseE: "False \ P" sorry lemma False_neq_True: "False = True \ P" thm eqTrueE sorry \ \-------------------------------\ text \Negation\ lemma notI: assumes P: "P \ False" shows "\P" sorry lemma notE: "\ \P; P \ \ R" sorry lemma False_not_True: "False \ True" sorry \ \-------------------------------\ text \Existential Quantifier\ lemma exI: "P x \ \x. P x" sorry lemma exE: assumes ex: "\x. P x" assumes R: "\x. P x \ R" shows "R" sorry \ \-------------------------------\ text \Conjunction\ lemma conjI: "\ P; Q \ \ P \ Q" sorry lemma conjE: assumes PQ: "P \ Q" assumes R: "\ P; Q \ \ R" shows R sorry \ \-------------------------------\ text \Disjunction\ lemma disjI1: "P \ P \ Q" sorry lemma disjI2: "Q \ P \ Q" sorry lemma disjE: assumes PQ: "P \ Q" assumes P: "P \ R" assumes Q: "Q \ R" shows "R" sorry \ \-------------------------------\ text \Classical Logic\ lemma classical: assumes P: "\P \ P" shows P sorry lemma notnotD: "\\P \ P" sorry lemma disjCI: assumes P: "\Q \ P" shows "P \ Q" sorry lemma tertium_non_datur: "P \ \P" sorry \ \-------------------------------\ text \Choice\ lemma someI_ex: "\x. P x \ P (SOME x. P x)" sorry lemma someI2: assumes a: "P a" assumes PQ: "\x. P x \ Q x" shows "Q (SOME x. P x)" sorry lemma some_equality: assumes a: "P a" assumes P: "\x. P x \ x=a" shows "(SOME x. P x) = a" sorry lemma some_eq_ex: "P (SOME x. P x) = (\x. P x)" sorry \ \-------------------------------\ text \if-then-else\ lemma if_True: "(if True then s else t) = s" sorry lemma if_False: "(if False then s else t) = t" sorry end