1.1 --- a/src/FOL/IFOL.thy Fri Mar 16 21:59:19 2012 +0100
1.2 +++ b/src/FOL/IFOL.thy Fri Mar 16 22:22:05 2012 +0100
1.3 @@ -36,30 +36,68 @@
1.4 judgment
1.5 Trueprop :: "o => prop" ("(_)" 5)
1.6
1.7 -consts
1.8 - True :: o
1.9 - False :: o
1.10
1.11 - (* Connectives *)
1.12 +subsubsection {* Equality *}
1.13
1.14 - eq :: "['a, 'a] => o" (infixl "=" 50)
1.15 +axiomatization
1.16 + eq :: "['a, 'a] => o" (infixl "=" 50)
1.17 +where
1.18 + refl: "a=a" and
1.19 + subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
1.20
1.21 - Not :: "o => o" ("~ _" [40] 40)
1.22 - conj :: "[o, o] => o" (infixr "&" 35)
1.23 - disj :: "[o, o] => o" (infixr "|" 30)
1.24 - imp :: "[o, o] => o" (infixr "-->" 25)
1.25 - iff :: "[o, o] => o" (infixr "<->" 25)
1.26
1.27 - (* Quantifiers *)
1.28 +subsubsection {* Propositional logic *}
1.29
1.30 - All :: "('a => o) => o" (binder "ALL " 10)
1.31 - Ex :: "('a => o) => o" (binder "EX " 10)
1.32 - Ex1 :: "('a => o) => o" (binder "EX! " 10)
1.33 +axiomatization
1.34 + False :: o and
1.35 + conj :: "[o, o] => o" (infixr "&" 35) and
1.36 + disj :: "[o, o] => o" (infixr "|" 30) and
1.37 + imp :: "[o, o] => o" (infixr "-->" 25)
1.38 +where
1.39 + conjI: "[| P; Q |] ==> P&Q" and
1.40 + conjunct1: "P&Q ==> P" and
1.41 + conjunct2: "P&Q ==> Q" and
1.42
1.43 + disjI1: "P ==> P|Q" and
1.44 + disjI2: "Q ==> P|Q" and
1.45 + disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and
1.46
1.47 -abbreviation
1.48 - not_equal :: "['a, 'a] => o" (infixl "~=" 50) where
1.49 - "x ~= y == ~ (x = y)"
1.50 + impI: "(P ==> Q) ==> P-->Q" and
1.51 + mp: "[| P-->Q; P |] ==> Q" and
1.52 +
1.53 + FalseE: "False ==> P"
1.54 +
1.55 +
1.56 +subsubsection {* Quantifiers *}
1.57 +
1.58 +axiomatization
1.59 + All :: "('a => o) => o" (binder "ALL " 10) and
1.60 + Ex :: "('a => o) => o" (binder "EX " 10)
1.61 +where
1.62 + allI: "(!!x. P(x)) ==> (ALL x. P(x))" and
1.63 + spec: "(ALL x. P(x)) ==> P(x)" and
1.64 + exI: "P(x) ==> (EX x. P(x))" and
1.65 + exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
1.66 +
1.67 +
1.68 +subsubsection {* Definitions *}
1.69 +
1.70 +definition "True == False-->False"
1.71 +definition Not ("~ _" [40] 40) where not_def: "~P == P-->False"
1.72 +definition iff (infixr "<->" 25) where "P<->Q == (P-->Q) & (Q-->P)"
1.73 +
1.74 +definition Ex1 :: "('a => o) => o" (binder "EX! " 10)
1.75 + where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
1.76 +
1.77 +axiomatization where -- {* Reflection, admissible *}
1.78 + eq_reflection: "(x=y) ==> (x==y)" and
1.79 + iff_reflection: "(P<->Q) ==> (P==Q)"
1.80 +
1.81 +
1.82 +subsubsection {* Additional notation *}
1.83 +
1.84 +abbreviation not_equal :: "['a, 'a] => o" (infixl "~=" 50)
1.85 + where "x ~= y == ~ (x = y)"
1.86
1.87 notation (xsymbols)
1.88 not_equal (infixl "\<noteq>" 50)
1.89 @@ -68,79 +106,28 @@
1.90 not_equal (infixl "\<noteq>" 50)
1.91
1.92 notation (xsymbols)
1.93 - Not ("\<not> _" [40] 40) and
1.94 - conj (infixr "\<and>" 35) and
1.95 - disj (infixr "\<or>" 30) and
1.96 - All (binder "\<forall>" 10) and
1.97 - Ex (binder "\<exists>" 10) and
1.98 - Ex1 (binder "\<exists>!" 10) and
1.99 - imp (infixr "\<longrightarrow>" 25) and
1.100 - iff (infixr "\<longleftrightarrow>" 25)
1.101 + Not ("\<not> _" [40] 40) and
1.102 + conj (infixr "\<and>" 35) and
1.103 + disj (infixr "\<or>" 30) and
1.104 + All (binder "\<forall>" 10) and
1.105 + Ex (binder "\<exists>" 10) and
1.106 + Ex1 (binder "\<exists>!" 10) and
1.107 + imp (infixr "\<longrightarrow>" 25) and
1.108 + iff (infixr "\<longleftrightarrow>" 25)
1.109
1.110 notation (HTML output)
1.111 - Not ("\<not> _" [40] 40) and
1.112 - conj (infixr "\<and>" 35) and
1.113 - disj (infixr "\<or>" 30) and
1.114 - All (binder "\<forall>" 10) and
1.115 - Ex (binder "\<exists>" 10) and
1.116 - Ex1 (binder "\<exists>!" 10)
1.117 + Not ("\<not> _" [40] 40) and
1.118 + conj (infixr "\<and>" 35) and
1.119 + disj (infixr "\<or>" 30) and
1.120 + All (binder "\<forall>" 10) and
1.121 + Ex (binder "\<exists>" 10) and
1.122 + Ex1 (binder "\<exists>!" 10)
1.123
1.124 -finalconsts
1.125 - False All Ex eq conj disj imp
1.126
1.127 -axiomatization where
1.128 - (* Equality *)
1.129 - refl: "a=a" and
1.130 - subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
1.131 -
1.132 -
1.133 -axiomatization where
1.134 - (* Propositional logic *)
1.135 - conjI: "[| P; Q |] ==> P&Q" and
1.136 - conjunct1: "P&Q ==> P" and
1.137 - conjunct2: "P&Q ==> Q" and
1.138 -
1.139 - disjI1: "P ==> P|Q" and
1.140 - disjI2: "Q ==> P|Q" and
1.141 - disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and
1.142 -
1.143 - impI: "(P ==> Q) ==> P-->Q" and
1.144 - mp: "[| P-->Q; P |] ==> Q" and
1.145 -
1.146 - FalseE: "False ==> P"
1.147 -
1.148 -axiomatization where
1.149 - (* Quantifiers *)
1.150 - allI: "(!!x. P(x)) ==> (ALL x. P(x))" and
1.151 - spec: "(ALL x. P(x)) ==> P(x)" and
1.152 -
1.153 - exI: "P(x) ==> (EX x. P(x))" and
1.154 - exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
1.155 -
1.156 -
1.157 -axiomatization where
1.158 - (* Reflection, admissible *)
1.159 - eq_reflection: "(x=y) ==> (x==y)" and
1.160 - iff_reflection: "(P<->Q) ==> (P==Q)"
1.161 -
1.162 +subsection {* Lemmas and proof tools *}
1.163
1.164 lemmas strip = impI allI
1.165
1.166 -
1.167 -defs
1.168 - (* Definitions *)
1.169 -
1.170 - True_def: "True == False-->False"
1.171 - not_def: "~P == P-->False"
1.172 - iff_def: "P<->Q == (P-->Q) & (Q-->P)"
1.173 -
1.174 - (* Unique existence *)
1.175 -
1.176 - ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
1.177 -
1.178 -
1.179 -subsection {* Lemmas and proof tools *}
1.180 -
1.181 lemma TrueI: True
1.182 unfolding True_def by (rule impI)
1.183
2.1 --- a/src/ZF/ZF.thy Fri Mar 16 21:59:19 2012 +0100
2.2 +++ b/src/ZF/ZF.thy Fri Mar 16 22:22:05 2012 +0100
2.3 @@ -14,11 +14,10 @@
2.4 typedecl i
2.5 arities i :: "term"
2.6
2.7 -consts
2.8 -
2.9 - zero :: "i" ("0") --{*the empty set*}
2.10 - Pow :: "i => i" --{*power sets*}
2.11 - Inf :: "i" --{*infinite set*}
2.12 +axiomatization
2.13 + zero :: "i" ("0") --{*the empty set*} and
2.14 + Pow :: "i => i" --{*power sets*} and
2.15 + Inf :: "i" --{*infinite set*}
2.16
2.17 text {*Bounded Quantifiers *}
2.18 consts
2.19 @@ -26,13 +25,12 @@
2.20 Bex :: "[i, i => o] => o"
2.21
2.22 text {*General Union and Intersection *}
2.23 -consts
2.24 - Union :: "i => i"
2.25 - Inter :: "i => i"
2.26 +axiomatization Union :: "i => i"
2.27 +consts Inter :: "i => i"
2.28
2.29 text {*Variations on Replacement *}
2.30 +axiomatization PrimReplace :: "[i, [i, i] => o] => i"
2.31 consts
2.32 - PrimReplace :: "[i, [i, i] => o] => i"
2.33 Replace :: "[i, [i, i] => o] => i"
2.34 RepFun :: "[i, i => i] => i"
2.35 Collect :: "[i, i => o] => i"
2.36 @@ -196,9 +194,6 @@
2.37 "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
2.38
2.39
2.40 -finalconsts
2.41 - 0 Pow Inf Union PrimReplace mem
2.42 -
2.43 defs (* Bounded Quantifiers *)
2.44 Ball_def: "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
2.45 Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)"