# HG changeset patch # User paulson # Date 1026669595 -7200 # Node ID 6f54e992777ed49625e7d16eb2c43b6758daa0c6 # Parent c9cfe1638bf2bee9f023617aa5574b0059abccd6 Removal of mono.thy diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/Cardinal.thy --- 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 "\" 50) "LEAST " :: "[pttrn, o] => i" ("(3\_./ _)" [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 **) diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/Epsilon.thy --- 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" diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/Inductive.thy --- 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" diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/IsaMakefile --- 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 diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/Nat.thy --- 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 diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/Perm.thy --- 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 diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/QPair.thy --- 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 diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/QUniv.thy --- 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 diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/Trancl.thy --- 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" diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/WF.thy --- 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" diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/equalities.thy --- 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" diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/func.thy --- 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. :r ==> :s; A<=B |] ==> r``A <= s``B" +by blast + +lemma vimage_pair_mono: + "[| !! x y. :r ==> :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 diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/mono.thy --- 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. :r ==> :s; A<=B |] ==> r``A <= s``B" -by blast - -lemma vimage_pair_mono: - "[| !! x y. :r ==> :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 diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/pair.thy --- 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]: ": 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= |] ==> P |] ==> P" -apply (unfold Sigma_def, blast) -done +by (unfold Sigma_def, blast) lemma SigmaE2 [elim!]: "[| : 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" 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), ) == 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, )" by (simp add: split_def) diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/upair.thy --- 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)