(* Title: HOL/HOL.thy Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson *) header {* The basis of Higher-Order Logic *} theory HOL_BASIC imports Pure keywords "try" "solve_direct" "quickcheck" "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and "quickcheck_params" :: thy_decl begin subsection {* Primitive logic *} subsubsection {* Core syntax *} classes type default_sort type setup {* Object_Logic.add_base_sort @{sort type} *} arities "fun" :: (type, type) type itself :: (type) type typedecl bool judgment Trueprop :: "bool => prop" ("(_)" 5) axiomatization implies :: "[bool, bool] => bool" (infixr "-->" 25) and eq :: "['a, 'a] => bool" (infixl "=" 50) and The :: "('a => bool) => 'a" consts True :: bool False :: bool Not :: "bool => bool" ("~ _" [40] 40) conj :: "[bool, bool] => bool" (infixr "&" 35) disj :: "[bool, bool] => bool" (infixr "|" 30) All :: "('a => bool) => bool" (binder "ALL " 10) Ex :: "('a => bool) => bool" (binder "EX " 10) Ex1 :: "('a => bool) => bool" (binder "EX! " 10) subsubsection {* Additional concrete syntax *} notation (output) eq (infix "=" 50) abbreviation not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where "x ~= y == ~ (x = y)" notation (output) not_equal (infix "~=" 50) notation (xsymbols) Not ("\ _" [40] 40) and conj (infixr "\" 35) and disj (infixr "\" 30) and implies (infixr "\" 25) and not_equal (infixl "\" 50) notation (xsymbols output) not_equal (infix "\" 50) notation (HTML output) Not ("\ _" [40] 40) and conj (infixr "\" 35) and disj (infixr "\" 30) and not_equal (infix "\" 50) abbreviation (iff) iff :: "[bool, bool] => bool" (infixr "<->" 25) where "A <-> B == A = B" notation (xsymbols) iff (infixr "\" 25) syntax "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) translations "THE x. P" == "CONST The (%x. P)" print_translation {* [(@{const_syntax The}, fn [Abs abs] => let val (x, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const @{syntax_const "_The"} $ x $ t end)] *} -- {* To avoid eta-contraction of body *} nonterminal letbinds and letbind syntax "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) "" :: "letbind => letbinds" ("_") "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10) nonterminal case_syn and cases_syn syntax "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) "" :: "case_syn => cases_syn" ("_") "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") syntax (xsymbols) "_case1" :: "['a, 'b] => case_syn" ("(2_ \/ _)" 10) notation (xsymbols) All (binder "\" 10) and Ex (binder "\" 10) and Ex1 (binder "\!" 10) notation (HTML output) All (binder "\" 10) and Ex (binder "\" 10) and Ex1 (binder "\!" 10) notation (HOL) All (binder "! " 10) and Ex (binder "? " 10) and Ex1 (binder "?! " 10) subsubsection {* Axioms and basic definitions *} axiomatization where refl: "t = (t::'a)" and subst: "s = t \ P s \ P t" and ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" -- {*Extensionality is built into the meta-logic, and this rule expresses a related property. It is an eta-expanded version of the traditional rule, and similar to the ABS rule of HOL*} and the_eq_trivial: "(THE x. x = a) = (a::'a)" 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)" defs True_def: "True == ((%x::bool. x) = (%x. x))" All_def: "All(P) == (P = (%x. True))" Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" False_def: "False == (!P. P)" not_def: "~ P == P-->False" and_def: "P & Q == !R. (P-->Q-->R) --> R" or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" definition If :: "bool \ 'a \ 'a \ 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where "If P x y \ (THE z::'a. (P=True --> z=x) & (P=False --> z=y))" definition Let :: "'a \ ('a \ 'b) \ 'b" where "Let s f \ f s" translations "_Let (_binds b bs) e" == "_Let b (_Let bs e)" "let x = a in e" == "CONST Let a (%x. e)" axiomatization undefined :: 'a class default = fixes default :: 'a subsubsection {* Atomizing meta-level connectives *} axiomatization where eq_reflection: "x = y \ x \ y" (*admissible axiom*) (* from Hilbert_Choice.thy *) subsection {* Hilbert's epsilon *} axiomatization Eps :: "('a => bool) => 'a" where someI: "P x ==> P (Eps P)" syntax (epsilon) "_Eps" :: "[pttrn, bool] => 'a" ("(3\_./ _)" [0, 10] 10) syntax (HOL) "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) syntax "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) translations "SOME x. P" == "CONST Eps (%x. P)" print_translation {* [(@{const_syntax Eps}, fn [Abs abs] => let val (x, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const @{syntax_const "_Eps"} $ x $ t end)] *} -- {* to avoid eta-contraction of body *} (* Own definitions of old exists *) consts EXold :: "('a => bool) => bool" (binder "Exold " 10) defs EXold_def: "EXold(P) == P (Eps P)" end