Removal of mono.thy
authorpaulson
Sun Jul 14 19:59:55 2002 +0200 (2002-07-14)
changeset 133576f54e992777e
parent 13356 c9cfe1638bf2
child 13358 c837ba4cfb62
Removal of mono.thy
src/ZF/Cardinal.thy
src/ZF/Epsilon.thy
src/ZF/Inductive.thy
src/ZF/IsaMakefile
src/ZF/Nat.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Trancl.thy
src/ZF/WF.thy
src/ZF/equalities.thy
src/ZF/func.thy
src/ZF/mono.thy
src/ZF/pair.thy
src/ZF/upair.thy
     1.1 --- a/src/ZF/Cardinal.thy	Sun Jul 14 15:14:43 2002 +0200
     1.2 +++ b/src/ZF/Cardinal.thy	Sun Jul 14 19:59:55 2002 +0200
     1.3 @@ -9,11 +9,6 @@
     1.4  
     1.5  theory Cardinal = OrderType + Finite + Nat + Sum:
     1.6  
     1.7 -(*** The following really belong in upair ***)
     1.8 -
     1.9 -lemma eq_imp_not_mem: "a=A ==> a ~: A"
    1.10 -by (blast intro: elim: mem_irrefl)
    1.11 -
    1.12  constdefs
    1.13  
    1.14    (*least ordinal operator*)
    1.15 @@ -44,7 +39,8 @@
    1.16    "lesspoll"    :: "[i,i] => o"       (infixl "\<prec>" 50)
    1.17    "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
    1.18  
    1.19 -subsection{*The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 *}
    1.20 +subsection{*The Schroeder-Bernstein Theorem*}
    1.21 +text{*See Davey and Priestly, page 106*}
    1.22  
    1.23  (** Lemma: Banach's Decomposition Theorem **)
    1.24  
     2.1 --- a/src/ZF/Epsilon.thy	Sun Jul 14 15:14:43 2002 +0200
     2.2 +++ b/src/ZF/Epsilon.thy	Sun Jul 14 19:59:55 2002 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  header{*Epsilon Induction and Recursion*}
     2.6  
     2.7 -theory Epsilon = Nat + mono:
     2.8 +theory Epsilon = Nat:
     2.9  
    2.10  constdefs
    2.11    eclose    :: "i=>i"
     3.1 --- a/src/ZF/Inductive.thy	Sun Jul 14 15:14:43 2002 +0200
     3.2 +++ b/src/ZF/Inductive.thy	Sun Jul 14 19:59:55 2002 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  header{*Inductive and Coinductive Definitions*}
     3.6  
     3.7 -theory Inductive = Fixedpt + mono + QPair
     3.8 +theory Inductive = Fixedpt + QPair
     3.9    files
    3.10      "ind_syntax.ML"
    3.11      "Tools/cartprod.ML"
     4.1 --- a/src/ZF/IsaMakefile	Sun Jul 14 15:14:43 2002 +0200
     4.2 +++ b/src/ZF/IsaMakefile	Sun Jul 14 19:59:55 2002 +0200
     4.3 @@ -45,7 +45,7 @@
     4.4    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
     4.5    Trancl.thy Univ.thy \
     4.6    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
     4.7 -  ind_syntax.ML mono.thy pair.thy simpdata.ML		\
     4.8 +  ind_syntax.ML pair.thy simpdata.ML		\
     4.9    thy_syntax.ML upair.thy
    4.10  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
    4.11  
     5.1 --- a/src/ZF/Nat.thy	Sun Jul 14 15:14:43 2002 +0200
     5.2 +++ b/src/ZF/Nat.thy	Sun Jul 14 19:59:55 2002 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  header{*The Natural numbers As a Least Fixed Point*}
     5.6  
     5.7 -theory Nat = OrdQuant + Bool + mono:
     5.8 +theory Nat = OrdQuant + Bool:
     5.9  
    5.10  constdefs
    5.11    nat :: i
     6.1 --- a/src/ZF/Perm.thy	Sun Jul 14 15:14:43 2002 +0200
     6.2 +++ b/src/ZF/Perm.thy	Sun Jul 14 19:59:55 2002 +0200
     6.3 @@ -11,7 +11,7 @@
     6.4  
     6.5  header{*Injections, Surjections, Bijections, Composition*}
     6.6  
     6.7 -theory Perm = mono + func:
     6.8 +theory Perm = func:
     6.9  
    6.10  constdefs
    6.11  
     7.1 --- a/src/ZF/QPair.thy	Sun Jul 14 15:14:43 2002 +0200
     7.2 +++ b/src/ZF/QPair.thy	Sun Jul 14 19:59:55 2002 +0200
     7.3 @@ -11,7 +11,7 @@
     7.4  
     7.5  header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
     7.6  
     7.7 -theory QPair = Sum + mono:
     7.8 +theory QPair = Sum + func:
     7.9  
    7.10  text{*For non-well-founded data
    7.11  structures in ZF.  Does not precisely follow Quine's construction.  Thanks
     8.1 --- a/src/ZF/QUniv.thy	Sun Jul 14 15:14:43 2002 +0200
     8.2 +++ b/src/ZF/QUniv.thy	Sun Jul 14 19:59:55 2002 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  
     8.5  header{*A Small Universe for Lazy Recursive Types*}
     8.6  
     8.7 -theory QUniv = Univ + QPair + mono + equalities:
     8.8 +theory QUniv = Univ + QPair:
     8.9  
    8.10  (*Disjoint sums as a datatype*)
    8.11  rep_datatype 
     9.1 --- a/src/ZF/Trancl.thy	Sun Jul 14 15:14:43 2002 +0200
     9.2 +++ b/src/ZF/Trancl.thy	Sun Jul 14 19:59:55 2002 +0200
     9.3 @@ -7,7 +7,7 @@
     9.4  
     9.5  header{*Relations: Their General Properties and Transitive Closure*}
     9.6  
     9.7 -theory Trancl = Fixedpt + Perm + mono:
     9.8 +theory Trancl = Fixedpt + Perm:
     9.9  
    9.10  constdefs
    9.11    refl     :: "[i,i]=>o"
    10.1 --- a/src/ZF/WF.thy	Sun Jul 14 15:14:43 2002 +0200
    10.2 +++ b/src/ZF/WF.thy	Sun Jul 14 19:59:55 2002 +0200
    10.3 @@ -17,7 +17,7 @@
    10.4  
    10.5  header{*Well-Founded Recursion*}
    10.6  
    10.7 -theory WF = Trancl + mono + equalities:
    10.8 +theory WF = Trancl:
    10.9  
   10.10  constdefs
   10.11    wf           :: "i=>o"
    11.1 --- a/src/ZF/equalities.thy	Sun Jul 14 15:14:43 2002 +0200
    11.2 +++ b/src/ZF/equalities.thy	Sun Jul 14 19:59:55 2002 +0200
    11.3 @@ -20,10 +20,6 @@
    11.4  lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
    11.5  by blast
    11.6  
    11.7 -(*FIXME: move to upair once it's Isar format*)
    11.8 -lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
    11.9 -by blast
   11.10 -
   11.11  (** Monotonicity of implications -- some could go to FOL **)
   11.12  
   11.13  lemma in_mono: "A<=B ==> x:A --> x:B"
    12.1 --- a/src/ZF/func.thy	Sun Jul 14 15:14:43 2002 +0200
    12.2 +++ b/src/ZF/func.thy	Sun Jul 14 19:59:55 2002 +0200
    12.3 @@ -7,7 +7,7 @@
    12.4  
    12.5  header{*Functions, Function Spaces, Lambda-Abstraction*}
    12.6  
    12.7 -theory func = equalities:
    12.8 +theory func = equalities + Sum:
    12.9  
   12.10  subsection{*The Pi Operator: Dependent Function Space*}
   12.11  
   12.12 @@ -486,6 +486,108 @@
   12.13  done
   12.14  
   12.15  
   12.16 +subsection{*Monotonicity Theorems*}
   12.17 +
   12.18 +subsubsection{*Replacement in its Various Forms*}
   12.19 +
   12.20 +(*Not easy to express monotonicity in P, since any "bigger" predicate
   12.21 +  would have to be single-valued*)
   12.22 +lemma Replace_mono: "A<=B ==> Replace(A,P) <= Replace(B,P)"
   12.23 +by (blast elim!: ReplaceE)
   12.24 +
   12.25 +lemma RepFun_mono: "A<=B ==> {f(x). x:A} <= {f(x). x:B}"
   12.26 +by blast
   12.27 +
   12.28 +lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
   12.29 +by blast
   12.30 +
   12.31 +lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
   12.32 +by blast
   12.33 +
   12.34 +lemma UN_mono:
   12.35 +    "[| A<=C;  !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"
   12.36 +by blast  
   12.37 +
   12.38 +(*Intersection is ANTI-monotonic.  There are TWO premises! *)
   12.39 +lemma Inter_anti_mono: "[| A<=B;  a:A |] ==> Inter(B) <= Inter(A)"
   12.40 +by blast
   12.41 +
   12.42 +lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)"
   12.43 +by blast
   12.44 +
   12.45 +lemma Un_mono: "[| A<=C;  B<=D |] ==> A Un B <= C Un D"
   12.46 +by blast
   12.47 +
   12.48 +lemma Int_mono: "[| A<=C;  B<=D |] ==> A Int B <= C Int D"
   12.49 +by blast
   12.50 +
   12.51 +lemma Diff_mono: "[| A<=C;  D<=B |] ==> A-B <= C-D"
   12.52 +by blast
   12.53 +
   12.54 +subsubsection{*Standard Products, Sums and Function Spaces *}
   12.55 +
   12.56 +lemma Sigma_mono [rule_format]:
   12.57 +     "[| A<=C;  !!x. x:A --> B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)"
   12.58 +by blast
   12.59 +
   12.60 +lemma sum_mono: "[| A<=C;  B<=D |] ==> A+B <= C+D"
   12.61 +by (unfold sum_def, blast)
   12.62 +
   12.63 +(*Note that B->A and C->A are typically disjoint!*)
   12.64 +lemma Pi_mono: "B<=C ==> A->B <= A->C"
   12.65 +by (blast intro: lam_type elim: Pi_lamE)
   12.66 +
   12.67 +lemma lam_mono: "A<=B ==> Lambda(A,c) <= Lambda(B,c)"
   12.68 +apply (unfold lam_def)
   12.69 +apply (erule RepFun_mono)
   12.70 +done
   12.71 +
   12.72 +subsubsection{*Converse, Domain, Range, Field*}
   12.73 +
   12.74 +lemma converse_mono: "r<=s ==> converse(r) <= converse(s)"
   12.75 +by blast
   12.76 +
   12.77 +lemma domain_mono: "r<=s ==> domain(r)<=domain(s)"
   12.78 +by blast
   12.79 +
   12.80 +lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset]
   12.81 +
   12.82 +lemma range_mono: "r<=s ==> range(r)<=range(s)"
   12.83 +by blast
   12.84 +
   12.85 +lemmas range_rel_subset = subset_trans [OF range_mono range_subset]
   12.86 +
   12.87 +lemma field_mono: "r<=s ==> field(r)<=field(s)"
   12.88 +by blast
   12.89 +
   12.90 +lemma field_rel_subset: "r <= A*A ==> field(r) <= A"
   12.91 +by (erule field_mono [THEN subset_trans], blast)
   12.92 +
   12.93 +
   12.94 +subsubsection{*Images*}
   12.95 +
   12.96 +lemma image_pair_mono:
   12.97 +    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A <= s``B"
   12.98 +by blast 
   12.99 +
  12.100 +lemma vimage_pair_mono:
  12.101 +    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A <= s-``B"
  12.102 +by blast 
  12.103 +
  12.104 +lemma image_mono: "[| r<=s;  A<=B |] ==> r``A <= s``B"
  12.105 +by blast
  12.106 +
  12.107 +lemma vimage_mono: "[| r<=s;  A<=B |] ==> r-``A <= s-``B"
  12.108 +by blast
  12.109 +
  12.110 +lemma Collect_mono:
  12.111 +    "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"
  12.112 +by blast
  12.113 +
  12.114 +(*Used in intr_elim.ML and in individual datatype definitions*)
  12.115 +lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono 
  12.116 +                     Collect_mono Part_mono in_mono
  12.117 +
  12.118  ML
  12.119  {*
  12.120  val Pi_iff = thm "Pi_iff";
  12.121 @@ -565,6 +667,35 @@
  12.122  val update_idem = thm "update_idem";
  12.123  val domain_update = thm "domain_update";
  12.124  val update_type = thm "update_type";
  12.125 +
  12.126 +val Replace_mono = thm "Replace_mono";
  12.127 +val RepFun_mono = thm "RepFun_mono";
  12.128 +val Pow_mono = thm "Pow_mono";
  12.129 +val Union_mono = thm "Union_mono";
  12.130 +val UN_mono = thm "UN_mono";
  12.131 +val Inter_anti_mono = thm "Inter_anti_mono";
  12.132 +val cons_mono = thm "cons_mono";
  12.133 +val Un_mono = thm "Un_mono";
  12.134 +val Int_mono = thm "Int_mono";
  12.135 +val Diff_mono = thm "Diff_mono";
  12.136 +val Sigma_mono = thm "Sigma_mono";
  12.137 +val sum_mono = thm "sum_mono";
  12.138 +val Pi_mono = thm "Pi_mono";
  12.139 +val lam_mono = thm "lam_mono";
  12.140 +val converse_mono = thm "converse_mono";
  12.141 +val domain_mono = thm "domain_mono";
  12.142 +val domain_rel_subset = thm "domain_rel_subset";
  12.143 +val range_mono = thm "range_mono";
  12.144 +val range_rel_subset = thm "range_rel_subset";
  12.145 +val field_mono = thm "field_mono";
  12.146 +val field_rel_subset = thm "field_rel_subset";
  12.147 +val image_pair_mono = thm "image_pair_mono";
  12.148 +val vimage_pair_mono = thm "vimage_pair_mono";
  12.149 +val image_mono = thm "image_mono";
  12.150 +val vimage_mono = thm "vimage_mono";
  12.151 +val Collect_mono = thm "Collect_mono";
  12.152 +
  12.153 +val basic_monos = thms "basic_monos";
  12.154  *}
  12.155  
  12.156  end
    13.1 --- a/src/ZF/mono.thy	Sun Jul 14 15:14:43 2002 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,143 +0,0 @@
    13.4 -(*  Title:      ZF/mono
    13.5 -    ID:         $Id$
    13.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 -    Copyright   1993  University of Cambridge
    13.8 -
    13.9 -Monotonicity of various operations
   13.10 -*)
   13.11 -
   13.12 -theory mono = Sum + func:
   13.13 -
   13.14 -(** Replacement, in its various formulations **)
   13.15 -
   13.16 -(*Not easy to express monotonicity in P, since any "bigger" predicate
   13.17 -  would have to be single-valued*)
   13.18 -lemma Replace_mono: "A<=B ==> Replace(A,P) <= Replace(B,P)"
   13.19 -by (blast elim!: ReplaceE)
   13.20 -
   13.21 -lemma RepFun_mono: "A<=B ==> {f(x). x:A} <= {f(x). x:B}"
   13.22 -by blast
   13.23 -
   13.24 -lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
   13.25 -by blast
   13.26 -
   13.27 -lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
   13.28 -by blast
   13.29 -
   13.30 -lemma UN_mono:
   13.31 -    "[| A<=C;  !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"
   13.32 -by blast  
   13.33 -
   13.34 -(*Intersection is ANTI-monotonic.  There are TWO premises! *)
   13.35 -lemma Inter_anti_mono: "[| A<=B;  a:A |] ==> Inter(B) <= Inter(A)"
   13.36 -by blast
   13.37 -
   13.38 -lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)"
   13.39 -by blast
   13.40 -
   13.41 -lemma Un_mono: "[| A<=C;  B<=D |] ==> A Un B <= C Un D"
   13.42 -by blast
   13.43 -
   13.44 -lemma Int_mono: "[| A<=C;  B<=D |] ==> A Int B <= C Int D"
   13.45 -by blast
   13.46 -
   13.47 -lemma Diff_mono: "[| A<=C;  D<=B |] ==> A-B <= C-D"
   13.48 -by blast
   13.49 -
   13.50 -(** Standard products, sums and function spaces **)
   13.51 -
   13.52 -lemma Sigma_mono [rule_format]:
   13.53 -     "[| A<=C;  !!x. x:A --> B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)"
   13.54 -by blast
   13.55 -
   13.56 -lemma sum_mono: "[| A<=C;  B<=D |] ==> A+B <= C+D"
   13.57 -by (unfold sum_def, blast)
   13.58 -
   13.59 -(*Note that B->A and C->A are typically disjoint!*)
   13.60 -lemma Pi_mono: "B<=C ==> A->B <= A->C"
   13.61 -by (blast intro: lam_type elim: Pi_lamE)
   13.62 -
   13.63 -lemma lam_mono: "A<=B ==> Lambda(A,c) <= Lambda(B,c)"
   13.64 -apply (unfold lam_def)
   13.65 -apply (erule RepFun_mono)
   13.66 -done
   13.67 -
   13.68 -(** Converse, domain, range, field **)
   13.69 -
   13.70 -lemma converse_mono: "r<=s ==> converse(r) <= converse(s)"
   13.71 -by blast
   13.72 -
   13.73 -lemma domain_mono: "r<=s ==> domain(r)<=domain(s)"
   13.74 -by blast
   13.75 -
   13.76 -lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset]
   13.77 -
   13.78 -lemma range_mono: "r<=s ==> range(r)<=range(s)"
   13.79 -by blast
   13.80 -
   13.81 -lemmas range_rel_subset = subset_trans [OF range_mono range_subset]
   13.82 -
   13.83 -lemma field_mono: "r<=s ==> field(r)<=field(s)"
   13.84 -by blast
   13.85 -
   13.86 -lemma field_rel_subset: "r <= A*A ==> field(r) <= A"
   13.87 -by (erule field_mono [THEN subset_trans], blast)
   13.88 -
   13.89 -
   13.90 -(** Images **)
   13.91 -
   13.92 -lemma image_pair_mono:
   13.93 -    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A <= s``B"
   13.94 -by blast 
   13.95 -
   13.96 -lemma vimage_pair_mono:
   13.97 -    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A <= s-``B"
   13.98 -by blast 
   13.99 -
  13.100 -lemma image_mono: "[| r<=s;  A<=B |] ==> r``A <= s``B"
  13.101 -by blast
  13.102 -
  13.103 -lemma vimage_mono: "[| r<=s;  A<=B |] ==> r-``A <= s-``B"
  13.104 -by blast
  13.105 -
  13.106 -lemma Collect_mono:
  13.107 -    "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"
  13.108 -by blast
  13.109 -
  13.110 -(*Used in intr_elim.ML and in individual datatype definitions*)
  13.111 -lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono 
  13.112 -                     Collect_mono Part_mono in_mono
  13.113 -
  13.114 -ML
  13.115 -{*
  13.116 -val Replace_mono = thm "Replace_mono";
  13.117 -val RepFun_mono = thm "RepFun_mono";
  13.118 -val Pow_mono = thm "Pow_mono";
  13.119 -val Union_mono = thm "Union_mono";
  13.120 -val UN_mono = thm "UN_mono";
  13.121 -val Inter_anti_mono = thm "Inter_anti_mono";
  13.122 -val cons_mono = thm "cons_mono";
  13.123 -val Un_mono = thm "Un_mono";
  13.124 -val Int_mono = thm "Int_mono";
  13.125 -val Diff_mono = thm "Diff_mono";
  13.126 -val Sigma_mono = thm "Sigma_mono";
  13.127 -val sum_mono = thm "sum_mono";
  13.128 -val Pi_mono = thm "Pi_mono";
  13.129 -val lam_mono = thm "lam_mono";
  13.130 -val converse_mono = thm "converse_mono";
  13.131 -val domain_mono = thm "domain_mono";
  13.132 -val domain_rel_subset = thm "domain_rel_subset";
  13.133 -val range_mono = thm "range_mono";
  13.134 -val range_rel_subset = thm "range_rel_subset";
  13.135 -val field_mono = thm "field_mono";
  13.136 -val field_rel_subset = thm "field_rel_subset";
  13.137 -val image_pair_mono = thm "image_pair_mono";
  13.138 -val vimage_pair_mono = thm "vimage_pair_mono";
  13.139 -val image_mono = thm "image_mono";
  13.140 -val vimage_mono = thm "vimage_mono";
  13.141 -val Collect_mono = thm "Collect_mono";
  13.142 -
  13.143 -val basic_monos = thms "basic_monos";
  13.144 -*}
  13.145 -
  13.146 -end
    14.1 --- a/src/ZF/pair.thy	Sun Jul 14 15:14:43 2002 +0200
    14.2 +++ b/src/ZF/pair.thy	Sun Jul 14 19:59:55 2002 +0200
    14.3 @@ -3,9 +3,10 @@
    14.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.5      Copyright   1992  University of Cambridge
    14.6  
    14.7 -Ordered pairs in Zermelo-Fraenkel Set Theory 
    14.8  *)
    14.9  
   14.10 +header{*Ordered Pairs*}
   14.11 +
   14.12  theory pair = upair
   14.13  files "simpdata.ML":
   14.14  
   14.15 @@ -49,8 +50,9 @@
   14.16  done
   14.17  
   14.18  
   14.19 -(*** Sigma: Disjoint union of a family of sets
   14.20 -     Generalizes Cartesian product ***)
   14.21 +subsection{*Sigma: Disjoint Union of a Family of Sets*}
   14.22 +
   14.23 +text{*Generalizes Cartesian product*}
   14.24  
   14.25  lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
   14.26  by (simp add: Sigma_def)
   14.27 @@ -66,15 +68,13 @@
   14.28      "[| c: Sigma(A,B);   
   14.29          !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P  
   14.30       |] ==> P"
   14.31 -apply (unfold Sigma_def, blast) 
   14.32 -done
   14.33 +by (unfold Sigma_def, blast) 
   14.34  
   14.35  lemma SigmaE2 [elim!]:
   14.36      "[| <a,b> : Sigma(A,B);     
   14.37          [| a:A;  b:B(a) |] ==> P    
   14.38       |] ==> P"
   14.39 -apply (unfold Sigma_def, blast) 
   14.40 -done
   14.41 +by (unfold Sigma_def, blast) 
   14.42  
   14.43  lemma Sigma_cong:
   14.44      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
   14.45 @@ -95,7 +95,7 @@
   14.46  by blast
   14.47  
   14.48  
   14.49 -(*** Projections: fst, snd ***)
   14.50 +subsection{*Projections @{term fst} and @{term snd}*}
   14.51  
   14.52  lemma fst_conv [simp]: "fst(<a,b>) = a"
   14.53  by (simp add: fst_def, blast)
   14.54 @@ -113,7 +113,7 @@
   14.55  by auto
   14.56  
   14.57  
   14.58 -(*** Eliminator - split ***)
   14.59 +subsection{*The Eliminator, @{term split}*}
   14.60  
   14.61  (*A META-equality, so that it applies to higher types as well...*)
   14.62  lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
   14.63 @@ -133,7 +133,7 @@
   14.64  done
   14.65  
   14.66  
   14.67 -(*** split for predicates: result type o ***)
   14.68 +subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
   14.69  
   14.70  lemma splitI: "R(a,b) ==> split(R, <a,b>)"
   14.71  by (simp add: split_def)
    15.1 --- a/src/ZF/upair.thy	Sun Jul 14 15:14:43 2002 +0200
    15.2 +++ b/src/ZF/upair.thy	Sun Jul 14 19:59:55 2002 +0200
    15.3 @@ -3,8 +3,6 @@
    15.4      Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    15.5      Copyright   1993  University of Cambridge
    15.6  
    15.7 -UNORDERED pairs in Zermelo-Fraenkel Set Theory 
    15.8 -
    15.9  Observe the order of dependence:
   15.10      Upair is defined in terms of Replace
   15.11      Un is defined in terms of Upair and Union (similarly for Int)
   15.12 @@ -12,6 +10,8 @@
   15.13      Ordered pairs and descriptions are defined using cons ("set notation")
   15.14  *)
   15.15  
   15.16 +header{*Unordered Pairs*}
   15.17 +
   15.18  theory upair = ZF
   15.19  files "Tools/typechk":
   15.20  
   15.21 @@ -21,13 +21,11 @@
   15.22  (*belongs to theory ZF*)
   15.23  declare bspec [dest?]
   15.24  
   15.25 -(*** Lemmas about power sets  ***)
   15.26 -
   15.27  lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
   15.28  lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *)
   15.29  
   15.30  
   15.31 -(*** Unordered pairs - Upair ***)
   15.32 +subsection{*Unordered Pairs: constant @{term Upair}*}
   15.33  
   15.34  lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)"
   15.35  by (unfold Upair_def, blast)
   15.36 @@ -44,7 +42,7 @@
   15.37  apply blast 
   15.38  done
   15.39  
   15.40 -(*** Rules for binary union -- Un -- defined via Upair ***)
   15.41 +subsection{*Rules for Binary Union, Defined via @{term Upair}*}
   15.42  
   15.43  lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)"
   15.44  apply (simp add: Un_def)
   15.45 @@ -57,7 +55,6 @@
   15.46  lemma UnI2: "c : B ==> c : A Un B"
   15.47  by simp
   15.48  
   15.49 -(*belongs to theory upair*)
   15.50  declare UnI1 [elim?]  UnI2 [elim?]
   15.51  
   15.52  lemma UnE [elim!]: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
   15.53 @@ -78,7 +75,7 @@
   15.54  done
   15.55  
   15.56  
   15.57 -(*** Rules for small intersection -- Int -- defined via Upair ***)
   15.58 +subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
   15.59  
   15.60  lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)"
   15.61  apply (unfold Int_def)
   15.62 @@ -98,7 +95,7 @@
   15.63  by simp
   15.64  
   15.65  
   15.66 -(*** Rules for set difference -- defined via Upair ***)
   15.67 +subsection{*Rules for Set Difference, Defined via @{term Upair}*}
   15.68  
   15.69  lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)"
   15.70  by (unfold Diff_def, blast)
   15.71 @@ -116,7 +113,7 @@
   15.72  by simp
   15.73  
   15.74  
   15.75 -(*** Rules for cons -- defined via Un and Upair ***)
   15.76 +subsection{*Rules for @{term cons}*}
   15.77  
   15.78  lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)"
   15.79  apply (unfold cons_def)
   15.80 @@ -159,7 +156,7 @@
   15.81  declare cons_not_0 [THEN not_sym, simp]
   15.82  
   15.83  
   15.84 -(*** Singletons - using cons ***)
   15.85 +subsection{*Singletons*}
   15.86  
   15.87  lemma singleton_iff: "a : {b} <-> a=b"
   15.88  by simp
   15.89 @@ -170,7 +167,7 @@
   15.90  lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
   15.91  
   15.92  
   15.93 -(*** Rules for Descriptions ***)
   15.94 +subsection{*Rules for Descriptions*}
   15.95  
   15.96  lemma the_equality [intro]:
   15.97      "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
   15.98 @@ -210,7 +207,10 @@
   15.99  apply (erule the_0 [THEN subst], assumption)
  15.100  done
  15.101  
  15.102 -(*** if -- a conditional expression for formulae ***)
  15.103 +lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
  15.104 +by blast
  15.105 +
  15.106 +subsection{*Conditional Terms: @{text "if-then-else"}*}
  15.107  
  15.108  lemma if_true [simp]: "(if True then a else b) = a"
  15.109  by (unfold if_def, blast)
  15.110 @@ -263,7 +263,7 @@
  15.111  by (simp split add: split_if)
  15.112  
  15.113  
  15.114 -(*** Foundation lemmas ***)
  15.115 +subsection{*Consequences of Foundation*}
  15.116  
  15.117  (*was called mem_anti_sym*)
  15.118  lemma mem_asym: "[| a:b;  ~P ==> b:a |] ==> P"
  15.119 @@ -288,7 +288,10 @@
  15.120  lemma mem_imp_not_eq: "a:A ==> a ~= A"
  15.121  by (blast elim!: mem_irrefl)
  15.122  
  15.123 -(*** Rules for succ ***)
  15.124 +lemma eq_imp_not_mem: "a=A ==> a ~: A"
  15.125 +by (blast intro: elim: mem_irrefl)
  15.126 +
  15.127 +subsection{*Rules for Successor*}
  15.128  
  15.129  lemma succ_iff: "i : succ(j) <-> i=j | i:j"
  15.130  by (unfold succ_def, blast)