--- a/src/ZF/Cardinal.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/Cardinal.thy Sun Jul 14 19:59:55 2002 +0200
@@ -9,11 +9,6 @@
theory Cardinal = OrderType + Finite + Nat + Sum:
-(*** The following really belong in upair ***)
-
-lemma eq_imp_not_mem: "a=A ==> a ~: A"
-by (blast intro: elim: mem_irrefl)
-
constdefs
(*least ordinal operator*)
@@ -44,7 +39,8 @@
"lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50)
"LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
-subsection{*The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 *}
+subsection{*The Schroeder-Bernstein Theorem*}
+text{*See Davey and Priestly, page 106*}
(** Lemma: Banach's Decomposition Theorem **)
--- a/src/ZF/Epsilon.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/Epsilon.thy Sun Jul 14 19:59:55 2002 +0200
@@ -7,7 +7,7 @@
header{*Epsilon Induction and Recursion*}
-theory Epsilon = Nat + mono:
+theory Epsilon = Nat:
constdefs
eclose :: "i=>i"
--- a/src/ZF/Inductive.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/Inductive.thy Sun Jul 14 19:59:55 2002 +0200
@@ -7,7 +7,7 @@
header{*Inductive and Coinductive Definitions*}
-theory Inductive = Fixedpt + mono + QPair
+theory Inductive = Fixedpt + QPair
files
"ind_syntax.ML"
"Tools/cartprod.ML"
--- a/src/ZF/IsaMakefile Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/IsaMakefile Sun Jul 14 19:59:55 2002 +0200
@@ -45,7 +45,7 @@
Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
Trancl.thy Univ.thy \
WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \
- ind_syntax.ML mono.thy pair.thy simpdata.ML \
+ ind_syntax.ML pair.thy simpdata.ML \
thy_syntax.ML upair.thy
@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
--- a/src/ZF/Nat.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/Nat.thy Sun Jul 14 19:59:55 2002 +0200
@@ -7,7 +7,7 @@
header{*The Natural numbers As a Least Fixed Point*}
-theory Nat = OrdQuant + Bool + mono:
+theory Nat = OrdQuant + Bool:
constdefs
nat :: i
--- a/src/ZF/Perm.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/Perm.thy Sun Jul 14 19:59:55 2002 +0200
@@ -11,7 +11,7 @@
header{*Injections, Surjections, Bijections, Composition*}
-theory Perm = mono + func:
+theory Perm = func:
constdefs
--- a/src/ZF/QPair.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/QPair.thy Sun Jul 14 19:59:55 2002 +0200
@@ -11,7 +11,7 @@
header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
-theory QPair = Sum + mono:
+theory QPair = Sum + func:
text{*For non-well-founded data
structures in ZF. Does not precisely follow Quine's construction. Thanks
--- a/src/ZF/QUniv.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/QUniv.thy Sun Jul 14 19:59:55 2002 +0200
@@ -7,7 +7,7 @@
header{*A Small Universe for Lazy Recursive Types*}
-theory QUniv = Univ + QPair + mono + equalities:
+theory QUniv = Univ + QPair:
(*Disjoint sums as a datatype*)
rep_datatype
--- a/src/ZF/Trancl.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/Trancl.thy Sun Jul 14 19:59:55 2002 +0200
@@ -7,7 +7,7 @@
header{*Relations: Their General Properties and Transitive Closure*}
-theory Trancl = Fixedpt + Perm + mono:
+theory Trancl = Fixedpt + Perm:
constdefs
refl :: "[i,i]=>o"
--- a/src/ZF/WF.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/WF.thy Sun Jul 14 19:59:55 2002 +0200
@@ -17,7 +17,7 @@
header{*Well-Founded Recursion*}
-theory WF = Trancl + mono + equalities:
+theory WF = Trancl:
constdefs
wf :: "i=>o"
--- a/src/ZF/equalities.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/equalities.thy Sun Jul 14 19:59:55 2002 +0200
@@ -20,10 +20,6 @@
lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
by blast
-(*FIXME: move to upair once it's Isar format*)
-lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
-by blast
-
(** Monotonicity of implications -- some could go to FOL **)
lemma in_mono: "A<=B ==> x:A --> x:B"
--- a/src/ZF/func.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/func.thy Sun Jul 14 19:59:55 2002 +0200
@@ -7,7 +7,7 @@
header{*Functions, Function Spaces, Lambda-Abstraction*}
-theory func = equalities:
+theory func = equalities + Sum:
subsection{*The Pi Operator: Dependent Function Space*}
@@ -486,6 +486,108 @@
done
+subsection{*Monotonicity Theorems*}
+
+subsubsection{*Replacement in its Various Forms*}
+
+(*Not easy to express monotonicity in P, since any "bigger" predicate
+ would have to be single-valued*)
+lemma Replace_mono: "A<=B ==> Replace(A,P) <= Replace(B,P)"
+by (blast elim!: ReplaceE)
+
+lemma RepFun_mono: "A<=B ==> {f(x). x:A} <= {f(x). x:B}"
+by blast
+
+lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
+by blast
+
+lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
+by blast
+
+lemma UN_mono:
+ "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"
+by blast
+
+(*Intersection is ANTI-monotonic. There are TWO premises! *)
+lemma Inter_anti_mono: "[| A<=B; a:A |] ==> Inter(B) <= Inter(A)"
+by blast
+
+lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)"
+by blast
+
+lemma Un_mono: "[| A<=C; B<=D |] ==> A Un B <= C Un D"
+by blast
+
+lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D"
+by blast
+
+lemma Diff_mono: "[| A<=C; D<=B |] ==> A-B <= C-D"
+by blast
+
+subsubsection{*Standard Products, Sums and Function Spaces *}
+
+lemma Sigma_mono [rule_format]:
+ "[| A<=C; !!x. x:A --> B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)"
+by blast
+
+lemma sum_mono: "[| A<=C; B<=D |] ==> A+B <= C+D"
+by (unfold sum_def, blast)
+
+(*Note that B->A and C->A are typically disjoint!*)
+lemma Pi_mono: "B<=C ==> A->B <= A->C"
+by (blast intro: lam_type elim: Pi_lamE)
+
+lemma lam_mono: "A<=B ==> Lambda(A,c) <= Lambda(B,c)"
+apply (unfold lam_def)
+apply (erule RepFun_mono)
+done
+
+subsubsection{*Converse, Domain, Range, Field*}
+
+lemma converse_mono: "r<=s ==> converse(r) <= converse(s)"
+by blast
+
+lemma domain_mono: "r<=s ==> domain(r)<=domain(s)"
+by blast
+
+lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset]
+
+lemma range_mono: "r<=s ==> range(r)<=range(s)"
+by blast
+
+lemmas range_rel_subset = subset_trans [OF range_mono range_subset]
+
+lemma field_mono: "r<=s ==> field(r)<=field(s)"
+by blast
+
+lemma field_rel_subset: "r <= A*A ==> field(r) <= A"
+by (erule field_mono [THEN subset_trans], blast)
+
+
+subsubsection{*Images*}
+
+lemma image_pair_mono:
+ "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B"
+by blast
+
+lemma vimage_pair_mono:
+ "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B"
+by blast
+
+lemma image_mono: "[| r<=s; A<=B |] ==> r``A <= s``B"
+by blast
+
+lemma vimage_mono: "[| r<=s; A<=B |] ==> r-``A <= s-``B"
+by blast
+
+lemma Collect_mono:
+ "[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"
+by blast
+
+(*Used in intr_elim.ML and in individual datatype definitions*)
+lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono
+ Collect_mono Part_mono in_mono
+
ML
{*
val Pi_iff = thm "Pi_iff";
@@ -565,6 +667,35 @@
val update_idem = thm "update_idem";
val domain_update = thm "domain_update";
val update_type = thm "update_type";
+
+val Replace_mono = thm "Replace_mono";
+val RepFun_mono = thm "RepFun_mono";
+val Pow_mono = thm "Pow_mono";
+val Union_mono = thm "Union_mono";
+val UN_mono = thm "UN_mono";
+val Inter_anti_mono = thm "Inter_anti_mono";
+val cons_mono = thm "cons_mono";
+val Un_mono = thm "Un_mono";
+val Int_mono = thm "Int_mono";
+val Diff_mono = thm "Diff_mono";
+val Sigma_mono = thm "Sigma_mono";
+val sum_mono = thm "sum_mono";
+val Pi_mono = thm "Pi_mono";
+val lam_mono = thm "lam_mono";
+val converse_mono = thm "converse_mono";
+val domain_mono = thm "domain_mono";
+val domain_rel_subset = thm "domain_rel_subset";
+val range_mono = thm "range_mono";
+val range_rel_subset = thm "range_rel_subset";
+val field_mono = thm "field_mono";
+val field_rel_subset = thm "field_rel_subset";
+val image_pair_mono = thm "image_pair_mono";
+val vimage_pair_mono = thm "vimage_pair_mono";
+val image_mono = thm "image_mono";
+val vimage_mono = thm "vimage_mono";
+val Collect_mono = thm "Collect_mono";
+
+val basic_monos = thms "basic_monos";
*}
end
--- a/src/ZF/mono.thy Sun Jul 14 15:14:43 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,143 +0,0 @@
-(* Title: ZF/mono
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Monotonicity of various operations
-*)
-
-theory mono = Sum + func:
-
-(** Replacement, in its various formulations **)
-
-(*Not easy to express monotonicity in P, since any "bigger" predicate
- would have to be single-valued*)
-lemma Replace_mono: "A<=B ==> Replace(A,P) <= Replace(B,P)"
-by (blast elim!: ReplaceE)
-
-lemma RepFun_mono: "A<=B ==> {f(x). x:A} <= {f(x). x:B}"
-by blast
-
-lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
-by blast
-
-lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
-by blast
-
-lemma UN_mono:
- "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"
-by blast
-
-(*Intersection is ANTI-monotonic. There are TWO premises! *)
-lemma Inter_anti_mono: "[| A<=B; a:A |] ==> Inter(B) <= Inter(A)"
-by blast
-
-lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)"
-by blast
-
-lemma Un_mono: "[| A<=C; B<=D |] ==> A Un B <= C Un D"
-by blast
-
-lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D"
-by blast
-
-lemma Diff_mono: "[| A<=C; D<=B |] ==> A-B <= C-D"
-by blast
-
-(** Standard products, sums and function spaces **)
-
-lemma Sigma_mono [rule_format]:
- "[| A<=C; !!x. x:A --> B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)"
-by blast
-
-lemma sum_mono: "[| A<=C; B<=D |] ==> A+B <= C+D"
-by (unfold sum_def, blast)
-
-(*Note that B->A and C->A are typically disjoint!*)
-lemma Pi_mono: "B<=C ==> A->B <= A->C"
-by (blast intro: lam_type elim: Pi_lamE)
-
-lemma lam_mono: "A<=B ==> Lambda(A,c) <= Lambda(B,c)"
-apply (unfold lam_def)
-apply (erule RepFun_mono)
-done
-
-(** Converse, domain, range, field **)
-
-lemma converse_mono: "r<=s ==> converse(r) <= converse(s)"
-by blast
-
-lemma domain_mono: "r<=s ==> domain(r)<=domain(s)"
-by blast
-
-lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset]
-
-lemma range_mono: "r<=s ==> range(r)<=range(s)"
-by blast
-
-lemmas range_rel_subset = subset_trans [OF range_mono range_subset]
-
-lemma field_mono: "r<=s ==> field(r)<=field(s)"
-by blast
-
-lemma field_rel_subset: "r <= A*A ==> field(r) <= A"
-by (erule field_mono [THEN subset_trans], blast)
-
-
-(** Images **)
-
-lemma image_pair_mono:
- "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B"
-by blast
-
-lemma vimage_pair_mono:
- "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B"
-by blast
-
-lemma image_mono: "[| r<=s; A<=B |] ==> r``A <= s``B"
-by blast
-
-lemma vimage_mono: "[| r<=s; A<=B |] ==> r-``A <= s-``B"
-by blast
-
-lemma Collect_mono:
- "[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"
-by blast
-
-(*Used in intr_elim.ML and in individual datatype definitions*)
-lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono
- Collect_mono Part_mono in_mono
-
-ML
-{*
-val Replace_mono = thm "Replace_mono";
-val RepFun_mono = thm "RepFun_mono";
-val Pow_mono = thm "Pow_mono";
-val Union_mono = thm "Union_mono";
-val UN_mono = thm "UN_mono";
-val Inter_anti_mono = thm "Inter_anti_mono";
-val cons_mono = thm "cons_mono";
-val Un_mono = thm "Un_mono";
-val Int_mono = thm "Int_mono";
-val Diff_mono = thm "Diff_mono";
-val Sigma_mono = thm "Sigma_mono";
-val sum_mono = thm "sum_mono";
-val Pi_mono = thm "Pi_mono";
-val lam_mono = thm "lam_mono";
-val converse_mono = thm "converse_mono";
-val domain_mono = thm "domain_mono";
-val domain_rel_subset = thm "domain_rel_subset";
-val range_mono = thm "range_mono";
-val range_rel_subset = thm "range_rel_subset";
-val field_mono = thm "field_mono";
-val field_rel_subset = thm "field_rel_subset";
-val image_pair_mono = thm "image_pair_mono";
-val vimage_pair_mono = thm "vimage_pair_mono";
-val image_mono = thm "image_mono";
-val vimage_mono = thm "vimage_mono";
-val Collect_mono = thm "Collect_mono";
-
-val basic_monos = thms "basic_monos";
-*}
-
-end
--- a/src/ZF/pair.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/pair.thy Sun Jul 14 19:59:55 2002 +0200
@@ -3,9 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Ordered pairs in Zermelo-Fraenkel Set Theory
*)
+header{*Ordered Pairs*}
+
theory pair = upair
files "simpdata.ML":
@@ -49,8 +50,9 @@
done
-(*** Sigma: Disjoint union of a family of sets
- Generalizes Cartesian product ***)
+subsection{*Sigma: Disjoint Union of a Family of Sets*}
+
+text{*Generalizes Cartesian product*}
lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
by (simp add: Sigma_def)
@@ -66,15 +68,13 @@
"[| c: Sigma(A,B);
!!x y.[| x:A; y:B(x); c=<x,y> |] ==> P
|] ==> P"
-apply (unfold Sigma_def, blast)
-done
+by (unfold Sigma_def, blast)
lemma SigmaE2 [elim!]:
"[| <a,b> : Sigma(A,B);
[| a:A; b:B(a) |] ==> P
|] ==> P"
-apply (unfold Sigma_def, blast)
-done
+by (unfold Sigma_def, blast)
lemma Sigma_cong:
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==>
@@ -95,7 +95,7 @@
by blast
-(*** Projections: fst, snd ***)
+subsection{*Projections @{term fst} and @{term snd}*}
lemma fst_conv [simp]: "fst(<a,b>) = a"
by (simp add: fst_def, blast)
@@ -113,7 +113,7 @@
by auto
-(*** Eliminator - split ***)
+subsection{*The Eliminator, @{term split}*}
(*A META-equality, so that it applies to higher types as well...*)
lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
@@ -133,7 +133,7 @@
done
-(*** split for predicates: result type o ***)
+subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
lemma splitI: "R(a,b) ==> split(R, <a,b>)"
by (simp add: split_def)
--- a/src/ZF/upair.thy Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/upair.thy Sun Jul 14 19:59:55 2002 +0200
@@ -3,8 +3,6 @@
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
Copyright 1993 University of Cambridge
-UNORDERED pairs in Zermelo-Fraenkel Set Theory
-
Observe the order of dependence:
Upair is defined in terms of Replace
Un is defined in terms of Upair and Union (similarly for Int)
@@ -12,6 +10,8 @@
Ordered pairs and descriptions are defined using cons ("set notation")
*)
+header{*Unordered Pairs*}
+
theory upair = ZF
files "Tools/typechk":
@@ -21,13 +21,11 @@
(*belongs to theory ZF*)
declare bspec [dest?]
-(*** Lemmas about power sets ***)
-
lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *)
-(*** Unordered pairs - Upair ***)
+subsection{*Unordered Pairs: constant @{term Upair}*}
lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)"
by (unfold Upair_def, blast)
@@ -44,7 +42,7 @@
apply blast
done
-(*** Rules for binary union -- Un -- defined via Upair ***)
+subsection{*Rules for Binary Union, Defined via @{term Upair}*}
lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)"
apply (simp add: Un_def)
@@ -57,7 +55,6 @@
lemma UnI2: "c : B ==> c : A Un B"
by simp
-(*belongs to theory upair*)
declare UnI1 [elim?] UnI2 [elim?]
lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
@@ -78,7 +75,7 @@
done
-(*** Rules for small intersection -- Int -- defined via Upair ***)
+subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)"
apply (unfold Int_def)
@@ -98,7 +95,7 @@
by simp
-(*** Rules for set difference -- defined via Upair ***)
+subsection{*Rules for Set Difference, Defined via @{term Upair}*}
lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)"
by (unfold Diff_def, blast)
@@ -116,7 +113,7 @@
by simp
-(*** Rules for cons -- defined via Un and Upair ***)
+subsection{*Rules for @{term cons}*}
lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)"
apply (unfold cons_def)
@@ -159,7 +156,7 @@
declare cons_not_0 [THEN not_sym, simp]
-(*** Singletons - using cons ***)
+subsection{*Singletons*}
lemma singleton_iff: "a : {b} <-> a=b"
by simp
@@ -170,7 +167,7 @@
lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
-(*** Rules for Descriptions ***)
+subsection{*Rules for Descriptions*}
lemma the_equality [intro]:
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
@@ -210,7 +207,10 @@
apply (erule the_0 [THEN subst], assumption)
done
-(*** if -- a conditional expression for formulae ***)
+lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
+by blast
+
+subsection{*Conditional Terms: @{text "if-then-else"}*}
lemma if_true [simp]: "(if True then a else b) = a"
by (unfold if_def, blast)
@@ -263,7 +263,7 @@
by (simp split add: split_if)
-(*** Foundation lemmas ***)
+subsection{*Consequences of Foundation*}
(*was called mem_anti_sym*)
lemma mem_asym: "[| a:b; ~P ==> b:a |] ==> P"
@@ -288,7 +288,10 @@
lemma mem_imp_not_eq: "a:A ==> a ~= A"
by (blast elim!: mem_irrefl)
-(*** Rules for succ ***)
+lemma eq_imp_not_mem: "a=A ==> a ~: A"
+by (blast intro: elim: mem_irrefl)
+
+subsection{*Rules for Successor*}
lemma succ_iff: "i : succ(j) <-> i=j | i:j"
by (unfold succ_def, blast)