(* Title: HOL/HOL.thy ID: $Id: HOL_BASIC.thy,v 1.6 2007/12/18 12:35:14 smaus Exp $ Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson *) header {* The basis of Higher-Order Logic *} theory HOL_BASIC imports CPure (*Jan Smaus removed some calls to files here that contain lemmas that are subject of the exercises *) begin subsection {* Primitive logic *} subsubsection {* Core syntax *} classes type defaultsort type global typedecl bool arities bool :: type fun :: (type, type) type judgment Trueprop :: "bool => prop" ("(_)" 5) consts Not :: "bool => bool" ("~ _" [40] 40) True :: bool False :: bool arbitrary :: 'a The :: "('a => bool) => 'a" Eps :: "('a => bool) => 'a" All :: "('a => bool) => bool" (binder "ALL " 10) Ex :: "('a => bool) => bool" (binder "EX " 10) Ex1 :: "('a => bool) => bool" (binder "EX! " 10) Let :: "['a, 'a => 'b] => 'b" "=" :: "['a, 'a] => bool" (infixl 50) & :: "[bool, bool] => bool" (infixr 35) "|" :: "[bool, bool] => bool" (infixr 30) --> :: "[bool, bool] => bool" (infixr 25) local consts If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) subsubsection {* Additional concrete syntax *} nonterminals letbinds letbind case_syn cases_syn syntax "_not_equal" :: "['a, 'a] => bool" (infixl "~=" 50) "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) "" :: "letbind => letbinds" ("_") "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) "_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" ("_/ | _") translations "x ~= y" == "~ (x = y)" "THE x. P" == "The (%x. P)" "SOME x. P" == "Eps (%x. P)" "_Let (_binds b bs) e" == "_Let b (_Let bs e)" "let x = a in e" == "Let a (%x. e)" print_translation {* (* To avoid eta-contraction of body: *) [("The", fn [Abs abs] => let val (x,t) = atomic_abs_tr' abs in Syntax.const "_The" $ x $ t end)] *} syntax (output) "=" :: "['a, 'a] => bool" (infix 50) "_not_equal" :: "['a, 'a] => bool" (infix "~=" 50) syntax (xsymbols) Not :: "bool => bool" ("\\ _" [40] 40) "op &" :: "[bool, bool] => bool" (infixr "\\" 35) "op |" :: "[bool, bool] => bool" (infixr "\\" 30) "op -->" :: "[bool, bool] => bool" (infixr "\\" 25) (*Jan Smaus: above there was "-->" instead of "?"*) "_not_equal" :: "['a, 'a] => bool" (infix "\\" 50) "ALL " :: "[idts, bool] => bool" ("(3\\_./ _)" [0, 10] 10) "EX " :: "[idts, bool] => bool" ("(3\\_./ _)" [0, 10] 10) "EX! " :: "[idts, bool] => bool" ("(3\\!_./ _)" [0, 10] 10) "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) (*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \ _")*) syntax (xsymbols output) "_not_equal" :: "['a, 'a] => bool" (infix "\\" 50) syntax (HTML output) "_not_equal" :: "['a, 'a] => bool" (infix "≠" 50) Not :: "bool => bool" ("\\ _" [40] 40) "op &" :: "[bool, bool] => bool" (infixr "∧" 35) "op |" :: "[bool, bool] => bool" (infixr "∨" 30) "_not_equal" :: "['a, 'a] => bool" (infix "≠" 50) "ALL " :: "[idts, bool] => bool" ("(3∀_./ _)" [0, 10] 10) "EX " :: "[idts, bool] => bool" ("(3∃_./ _)" [0, 10] 10) "EX! " :: "[idts, bool] => bool" ("(3∃!_./ _)" [0, 10] 10) syntax (HOL) "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) subsubsection {* Axioms and basic definitions *} axioms eq_reflection: "(x=y) ==> (x==y)" refl: "t = (t::'a)" subst: "[| s = t; P(s) |] ==> P(t::'a)" 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*} someI: "P (x::'a) ==> P (SOME x. P x)" the_eq_trivial: "(THE x. x = a) = (a::'a)" impI: "(P ==> Q) ==> (P-->Q)" mp: "[| P-->Q; P |] ==> Q" defs True_def: "True == ((%x::bool. x) = (%x. x))" All_def: "All(P) == (P = (%x. True))" Ex_def: "Ex(P) == P (SOME x. P x)" 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" axioms iff: "(P-->Q) --> (Q-->P) --> (P=Q)" True_or_False: "(P=True) | (P=False)" defs Let_def: "Let s f == f(s)" if_def: "If P x y == SOME z::'a. (P=True --> z=x) & (P=False --> z=y)" finalconsts "op =" "op -->" The arbitrary subsubsection {* Generic algebraic operations *} axclass zero < type axclass one < type axclass plus < type axclass minus < type axclass times < type axclass inverse < type global consts "0" :: "'a::zero" ("0") "1" :: "'a::one" ("1") "+" :: "['a::plus, 'a] => 'a" (infixl 65) - :: "['a::minus, 'a] => 'a" (infixl 65) uminus :: "['a::minus] => 'a" ("- _" [81] 80) * :: "['a::times, 'a] => 'a" (infixl 70) syntax "_index1" :: index ("1") local typed_print_translation {* let fun tr' c = (c, fn show_sorts => fn T => fn ts => if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); in [tr' "0", tr' "1"] end; *} -- {* show types that are presumably too general *} consts abs :: "'a::minus => 'a" inverse :: "'a::inverse => 'a" divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) syntax (xsymbols) abs :: "'a::minus => 'a" ("?_?") syntax (HTML output) abs :: "'a::minus => 'a" ("?_?") subsection {* Theory and package setup *} ML {* val eq_reflection = thm "eq_reflection" val refl = thm "refl" val subst = thm "subst" val ext = thm "ext" val someI = thm "someI" val impI = thm "impI" val mp = thm "mp" val True_def = thm "True_def" val All_def = thm "All_def" val Ex_def = thm "Ex_def" val False_def = thm "False_def" val not_def = thm "not_def" val and_def = thm "and_def" val or_def = thm "or_def" val iff = thm "iff" val True_or_False = thm "True_or_False" val Let_def = thm "Let_def" val if_def = thm "if_def" *} end