--- 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 \<Longrightarrow> P(a) \<Longrightarrow> 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 "\<noteq>" 50)
@@ -68,79 +106,28 @@
not_equal (infixl "\<noteq>" 50)
notation (xsymbols)
- Not ("\<not> _" [40] 40) and
- conj (infixr "\<and>" 35) and
- disj (infixr "\<or>" 30) and
- All (binder "\<forall>" 10) and
- Ex (binder "\<exists>" 10) and
- Ex1 (binder "\<exists>!" 10) and
- imp (infixr "\<longrightarrow>" 25) and
- iff (infixr "\<longleftrightarrow>" 25)
+ Not ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ Ex1 (binder "\<exists>!" 10) and
+ imp (infixr "\<longrightarrow>" 25) and
+ iff (infixr "\<longleftrightarrow>" 25)
notation (HTML output)
- Not ("\<not> _" [40] 40) and
- conj (infixr "\<and>" 35) and
- disj (infixr "\<or>" 30) and
- All (binder "\<forall>" 10) and
- Ex (binder "\<exists>" 10) and
- Ex1 (binder "\<exists>!" 10)
-
-finalconsts
- False All Ex eq conj disj imp
-
-axiomatization where
- (* Equality *)
- refl: "a=a" and
- subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> 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 ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ Ex1 (binder "\<exists>!" 10)
subsection {* Lemmas and proof tools *}
+lemmas strip = impI allI
+
lemma TrueI: True
unfolding True_def by (rule impI)
--- 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" ("\<langle>_\<rangle>")
-finalconsts
- 0 Pow Inf Union PrimReplace mem
-
defs (* Bounded Quantifiers *)
Ball_def: "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)"