# HG changeset patch # User wenzelm # Date 1331932925 -3600 # Node ID ef6fc1a0884d8df78c0e61d820c990eba780759f # Parent bdec4a6016c269c1f0cd710112a15abfa9fe838a modernized axiomatization; eliminated odd 'finalconsts'; diff -r bdec4a6016c2 -r ef6fc1a0884d src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Fri Mar 16 21:59:19 2012 +0100 +++ b/src/FOL/IFOL.thy Fri Mar 16 22:22:05 2012 +0100 @@ -36,30 +36,68 @@ judgment Trueprop :: "o => prop" ("(_)" 5) -consts - True :: o - False :: o - (* Connectives *) - - eq :: "['a, 'a] => o" (infixl "=" 50) +subsubsection {* Equality *} - Not :: "o => o" ("~ _" [40] 40) - conj :: "[o, o] => o" (infixr "&" 35) - disj :: "[o, o] => o" (infixr "|" 30) - imp :: "[o, o] => o" (infixr "-->" 25) - iff :: "[o, o] => o" (infixr "<->" 25) - - (* Quantifiers *) - - All :: "('a => o) => o" (binder "ALL " 10) - Ex :: "('a => o) => o" (binder "EX " 10) - Ex1 :: "('a => o) => o" (binder "EX! " 10) +axiomatization + eq :: "['a, 'a] => o" (infixl "=" 50) +where + refl: "a=a" and + subst: "a=b \ P(a) \ P(b)" -abbreviation - not_equal :: "['a, 'a] => o" (infixl "~=" 50) where - "x ~= y == ~ (x = y)" +subsubsection {* Propositional logic *} + +axiomatization + False :: o and + conj :: "[o, o] => o" (infixr "&" 35) and + disj :: "[o, o] => o" (infixr "|" 30) and + imp :: "[o, o] => o" (infixr "-->" 25) +where + conjI: "[| P; Q |] ==> P&Q" and + conjunct1: "P&Q ==> P" and + conjunct2: "P&Q ==> Q" and + + disjI1: "P ==> P|Q" and + disjI2: "Q ==> P|Q" and + disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and + + impI: "(P ==> Q) ==> P-->Q" and + mp: "[| P-->Q; P |] ==> Q" and + + FalseE: "False ==> P" + + +subsubsection {* Quantifiers *} + +axiomatization + All :: "('a => o) => o" (binder "ALL " 10) and + Ex :: "('a => o) => o" (binder "EX " 10) +where + allI: "(!!x. P(x)) ==> (ALL x. P(x))" and + spec: "(ALL x. P(x)) ==> P(x)" and + exI: "P(x) ==> (EX x. P(x))" and + exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" + + +subsubsection {* Definitions *} + +definition "True == False-->False" +definition Not ("~ _" [40] 40) where not_def: "~P == P-->False" +definition iff (infixr "<->" 25) where "P<->Q == (P-->Q) & (Q-->P)" + +definition Ex1 :: "('a => o) => o" (binder "EX! " 10) + where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" + +axiomatization where -- {* Reflection, admissible *} + eq_reflection: "(x=y) ==> (x==y)" and + iff_reflection: "(P<->Q) ==> (P==Q)" + + +subsubsection {* Additional notation *} + +abbreviation not_equal :: "['a, 'a] => o" (infixl "~=" 50) + where "x ~= y == ~ (x = y)" notation (xsymbols) not_equal (infixl "\" 50) @@ -68,79 +106,28 @@ not_equal (infixl "\" 50) notation (xsymbols) - Not ("\ _" [40] 40) and - conj (infixr "\" 35) and - disj (infixr "\" 30) and - All (binder "\" 10) and - Ex (binder "\" 10) and - Ex1 (binder "\!" 10) and - imp (infixr "\" 25) and - iff (infixr "\" 25) + Not ("\ _" [40] 40) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) and + imp (infixr "\" 25) and + iff (infixr "\" 25) notation (HTML output) - Not ("\ _" [40] 40) and - conj (infixr "\" 35) and - disj (infixr "\" 30) and - All (binder "\" 10) and - Ex (binder "\" 10) and - Ex1 (binder "\!" 10) - -finalconsts - False All Ex eq conj disj imp - -axiomatization where - (* Equality *) - refl: "a=a" and - subst: "a=b \ P(a) \ P(b)" - - -axiomatization where - (* Propositional logic *) - conjI: "[| P; Q |] ==> P&Q" and - conjunct1: "P&Q ==> P" and - conjunct2: "P&Q ==> Q" and - - disjI1: "P ==> P|Q" and - disjI2: "Q ==> P|Q" and - disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and - - impI: "(P ==> Q) ==> P-->Q" and - mp: "[| P-->Q; P |] ==> Q" and - - FalseE: "False ==> P" - -axiomatization where - (* Quantifiers *) - allI: "(!!x. P(x)) ==> (ALL x. P(x))" and - spec: "(ALL x. P(x)) ==> P(x)" and - - exI: "P(x) ==> (EX x. P(x))" and - exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" - - -axiomatization where - (* Reflection, admissible *) - eq_reflection: "(x=y) ==> (x==y)" and - iff_reflection: "(P<->Q) ==> (P==Q)" - - -lemmas strip = impI allI - - -defs - (* Definitions *) - - True_def: "True == False-->False" - not_def: "~P == P-->False" - iff_def: "P<->Q == (P-->Q) & (Q-->P)" - - (* Unique existence *) - - ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)" + Not ("\ _" [40] 40) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) subsection {* Lemmas and proof tools *} +lemmas strip = impI allI + lemma TrueI: True unfolding True_def by (rule impI) diff -r bdec4a6016c2 -r ef6fc1a0884d src/ZF/ZF.thy --- a/src/ZF/ZF.thy Fri Mar 16 21:59:19 2012 +0100 +++ b/src/ZF/ZF.thy Fri Mar 16 22:22:05 2012 +0100 @@ -14,11 +14,10 @@ typedecl i arities i :: "term" -consts - - zero :: "i" ("0") --{*the empty set*} - Pow :: "i => i" --{*power sets*} - Inf :: "i" --{*infinite set*} +axiomatization + zero :: "i" ("0") --{*the empty set*} and + Pow :: "i => i" --{*power sets*} and + Inf :: "i" --{*infinite set*} text {*Bounded Quantifiers *} consts @@ -26,13 +25,12 @@ Bex :: "[i, i => o] => o" text {*General Union and Intersection *} -consts - Union :: "i => i" - Inter :: "i => i" +axiomatization Union :: "i => i" +consts Inter :: "i => i" text {*Variations on Replacement *} +axiomatization PrimReplace :: "[i, [i, i] => o] => i" consts - PrimReplace :: "[i, [i, i] => o] => i" Replace :: "[i, [i, i] => o] => i" RepFun :: "[i, i => i] => i" Collect :: "[i, i => o] => i" @@ -196,9 +194,6 @@ "_pattern" :: "patterns => pttrn" ("\_\") -finalconsts - 0 Pow Inf Union PrimReplace mem - defs (* Bounded Quantifiers *) Ball_def: "Ball(A, P) == \x. x\A \ P(x)" Bex_def: "Bex(A, P) == \x. x\A & P(x)"