improved presentation markup
authorpaulson
Sun Jul 14 15:14:43 2002 +0200 (2002-07-14)
changeset 13356c9cfe1638bf2
parent 13355 d19cdbd8b559
child 13357 6f54e992777e
improved presentation markup
src/ZF/Arith.thy
src/ZF/ArithSimp.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Epsilon.thy
src/ZF/Finite.thy
src/ZF/Fixedpt.thy
src/ZF/Inductive.thy
src/ZF/InfDatatype.thy
src/ZF/IsaMakefile
src/ZF/List.thy
src/ZF/Main.thy
src/ZF/Nat.thy
src/ZF/Order.thy
src/ZF/OrderArith.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/ZF.ML
src/ZF/Zorn.thy
src/ZF/equalities.thy
src/ZF/upair.thy
     1.1 --- a/src/ZF/Arith.thy	Sun Jul 14 15:11:21 2002 +0200
     1.2 +++ b/src/ZF/Arith.thy	Sun Jul 14 15:14:43 2002 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
     1.5  
     1.6  
     1.7 -(** natify: coercion to "nat" **)
     1.8 +subsection{*@{text natify}, the Coercion to @{term nat}*}
     1.9  
    1.10  lemma pred_succ_eq [simp]: "pred(succ(y)) = y"
    1.11  by (unfold pred_def, auto)
    1.12 @@ -163,7 +163,7 @@
    1.13  by (simp add: div_def)
    1.14  
    1.15  
    1.16 -(*** Typing rules ***)
    1.17 +subsection{*Typing rules*}
    1.18  
    1.19  (** Addition **)
    1.20  
    1.21 @@ -218,7 +218,7 @@
    1.22  done
    1.23  
    1.24  
    1.25 -(*** Addition ***)
    1.26 +subsection{*Addition*}
    1.27  
    1.28  (*Natify has weakened this law, compared with the older approach*)
    1.29  lemma add_0_natify [simp]: "0 #+ m = natify(m)"
    1.30 @@ -308,7 +308,7 @@
    1.31  by (drule add_lt_elim1_natify, auto)
    1.32  
    1.33  
    1.34 -(*** Monotonicity of Addition ***)
    1.35 +subsection{*Monotonicity of Addition*}
    1.36  
    1.37  (*strict, in 1st argument; proof is by rule induction on 'less than'.
    1.38    Still need j:nat, for consider j = omega.  Then we can have i<omega,
    1.39 @@ -402,7 +402,7 @@
    1.40  by auto
    1.41  
    1.42  
    1.43 -(*** Multiplication [the simprocs need these laws] ***)
    1.44 +subsection{*Multiplication*}
    1.45  
    1.46  lemma mult_0 [simp]: "0 #* m = 0"
    1.47  by (simp add: mult_def)
     2.1 --- a/src/ZF/ArithSimp.thy	Sun Jul 14 15:11:21 2002 +0200
     2.2 +++ b/src/ZF/ArithSimp.thy	Sun Jul 14 15:14:43 2002 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  theory ArithSimp = Arith
     2.5  files "arith_data.ML":
     2.6  
     2.7 -(*** Difference ***)
     2.8 +subsection{*Difference*}
     2.9  
    2.10  lemma diff_self_eq_0: "m #- m = 0"
    2.11  apply (subgoal_tac "natify (m) #- natify (m) = 0")
    2.12 @@ -60,7 +60,7 @@
    2.13  done
    2.14  
    2.15  
    2.16 -(*** Remainder ***)
    2.17 +subsection{*Remainder*}
    2.18  
    2.19  (*We need m:nat even with natify*)
    2.20  lemma div_termination: "[| 0<n;  n le m;  m:nat |] ==> m #- n < m"
    2.21 @@ -131,7 +131,7 @@
    2.22  done
    2.23  
    2.24  
    2.25 -(*** Division ***)
    2.26 +subsection{*Division*}
    2.27  
    2.28  lemma raw_div_type: "[| m:nat;  n:nat |] ==> raw_div (m, n) : nat"
    2.29  apply (unfold raw_div_def)
    2.30 @@ -196,7 +196,9 @@
    2.31  done
    2.32  
    2.33  
    2.34 -(*** Further facts about mod (mainly for mutilated chess board) ***)
    2.35 +subsection{*Further Facts about Remainder*}
    2.36 +
    2.37 +text{*(mainly for mutilated chess board)*}
    2.38  
    2.39  lemma mod_succ_lemma:
    2.40       "[| 0<n;  m:nat;  n:nat |]  
    2.41 @@ -258,7 +260,7 @@
    2.42  by (cut_tac n = "0" in mod2_add_more, auto)
    2.43  
    2.44  
    2.45 -(**** Additional theorems about "le" ****)
    2.46 +subsection{*Additional theorems about @{text "\<le>"}*}
    2.47  
    2.48  lemma add_le_self: "m:nat ==> m le (m #+ n)"
    2.49  apply (simp (no_asm_simp))
    2.50 @@ -333,7 +335,7 @@
    2.51  done
    2.52  
    2.53  
    2.54 -(** Cancellation laws for common factors in comparisons **)
    2.55 +subsection{*Cancellation Laws for Common Factors in Comparisons*}
    2.56  
    2.57  lemma mult_less_cancel_lemma:
    2.58       "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)"
    2.59 @@ -408,7 +410,7 @@
    2.60  done
    2.61  
    2.62  
    2.63 -(** Distributive law for remainder (mod) **)
    2.64 +subsection{*More Lemmas about Remainder*}
    2.65  
    2.66  lemma mult_mod_distrib_raw:
    2.67       "[| k:nat; m:nat; n:nat |] ==> (k#*m) mod (k#*n) = k #* (m mod n)"
    2.68 @@ -492,7 +494,8 @@
    2.69       "[| m: nat; n: nat |] ==> (m<n) <-> (EX k: nat. n = succ(m#+k))"
    2.70  by (auto intro: less_imp_succ_add)
    2.71  
    2.72 -(* on nat *)
    2.73 +
    2.74 +subsubsection{*More Lemmas About Difference*}
    2.75  
    2.76  lemma diff_is_0_lemma:
    2.77       "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n"
     3.1 --- a/src/ZF/Bool.thy	Sun Jul 14 15:11:21 2002 +0200
     3.2 +++ b/src/ZF/Bool.thy	Sun Jul 14 15:14:43 2002 +0200
     3.3 @@ -112,7 +112,7 @@
     3.4  lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
     3.5                           or_type xor_type
     3.6  
     3.7 -(*** Laws for 'not' ***)
     3.8 +subsection{*Laws About 'not' *}
     3.9  
    3.10  lemma not_not [simp]: "a:bool ==> not(not(a)) = a"
    3.11  by (elim boolE, auto)
    3.12 @@ -123,7 +123,7 @@
    3.13  lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"
    3.14  by (elim boolE, auto)
    3.15  
    3.16 -(*** Laws about 'and' ***)
    3.17 +subsection{*Laws About 'and' *}
    3.18  
    3.19  lemma and_absorb [simp]: "a: bool ==> a and a = a"
    3.20  by (elim boolE, auto)
    3.21 @@ -138,7 +138,7 @@
    3.22         (a or b) and c  =  (a and c) or (b and c)"
    3.23  by (elim boolE, auto)
    3.24  
    3.25 -(** binary 'or' **)
    3.26 +subsection{*Laws About 'or' *}
    3.27  
    3.28  lemma or_absorb [simp]: "a: bool ==> a or a = a"
    3.29  by (elim boolE, auto)
     4.1 --- a/src/ZF/Cardinal.thy	Sun Jul 14 15:11:21 2002 +0200
     4.2 +++ b/src/ZF/Cardinal.thy	Sun Jul 14 15:14:43 2002 +0200
     4.3 @@ -44,7 +44,7 @@
     4.4    "lesspoll"    :: "[i,i] => o"       (infixl "\<prec>" 50)
     4.5    "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
     4.6  
     4.7 -(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
     4.8 +subsection{*The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 *}
     4.9  
    4.10  (** Lemma: Banach's Decomposition Theorem **)
    4.11  
    4.12 @@ -168,7 +168,7 @@
    4.13  done
    4.14  
    4.15  
    4.16 -(*** lesspoll: contributions by Krzysztof Grabczewski ***)
    4.17 +subsection{*lesspoll: contributions by Krzysztof Grabczewski *}
    4.18  
    4.19  lemma lesspoll_not_refl: "~ (i \<prec> i)"
    4.20  by (simp add: lesspoll_def) 
    4.21 @@ -270,7 +270,7 @@
    4.22  apply (rule the_0, blast)
    4.23  done
    4.24  
    4.25 -lemma Ord_Least: "Ord(LEAST x. P(x))"
    4.26 +lemma Ord_Least [intro,simp,TC]: "Ord(LEAST x. P(x))"
    4.27  apply (rule_tac P = "EX i. Ord(i) & P(i)" in case_split_thm)  
    4.28      (*case_tac method not available yet; needs "inductive"*)
    4.29  apply safe
    4.30 @@ -466,7 +466,7 @@
    4.31  done
    4.32  
    4.33  
    4.34 -(*** The finite cardinals ***)
    4.35 +subsection{*The finite cardinals *}
    4.36  
    4.37  lemma cons_lepoll_consD: 
    4.38   "[| cons(u,A) \<lesssim> cons(v,B);  u~:A;  v~:B |] ==> A \<lesssim> B"
    4.39 @@ -585,7 +585,7 @@
    4.40  done
    4.41  
    4.42  
    4.43 -(*** The first infinite cardinal: Omega, or nat ***)
    4.44 +subsection{*The first infinite cardinal: Omega, or nat *}
    4.45  
    4.46  (*This implies Kunen's Lemma 10.6*)
    4.47  lemma lt_not_lepoll: "[| n<i;  n:nat |] ==> ~ i \<lesssim> n"
    4.48 @@ -622,7 +622,7 @@
    4.49  done
    4.50  
    4.51  
    4.52 -(*** Towards Cardinal Arithmetic ***)
    4.53 +subsection{*Towards Cardinal Arithmetic *}
    4.54  (** Congruence laws for successor, cardinal addition and multiplication **)
    4.55  
    4.56  (*Congruence law for  cons  under equipollence*)
    4.57 @@ -699,8 +699,9 @@
    4.58  done
    4.59  
    4.60  
    4.61 -(*** Lemmas by Krzysztof Grabczewski.  New proofs using cons_lepoll_cons.
    4.62 -     Could easily generalise from succ to cons. ***)
    4.63 +subsection{*Lemmas by Krzysztof Grabczewski*}
    4.64 +
    4.65 +(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*)
    4.66  
    4.67  (*If A has at most n+1 elements and a:A then A-{a} has at most n.*)
    4.68  lemma Diff_sing_lepoll: 
    4.69 @@ -903,6 +904,8 @@
    4.70  apply (blast intro: Fin_into_Finite)+
    4.71  done
    4.72  
    4.73 +lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
    4.74 +
    4.75  (*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
    4.76  lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
    4.77  apply (unfold Finite_def)
     5.1 --- a/src/ZF/CardinalArith.thy	Sun Jul 14 15:11:21 2002 +0200
     5.2 +++ b/src/ZF/CardinalArith.thy	Sun Jul 14 15:14:43 2002 +0200
     5.3 @@ -88,7 +88,7 @@
     5.4  done
     5.5  
     5.6  
     5.7 -(*** Cardinal addition ***)
     5.8 +subsection{*Cardinal addition*}
     5.9  
    5.10  text{*Note: Could omit proving the algebraic laws for cardinal addition and
    5.11  multiplication.  On finite cardinals these operations coincide with
    5.12 @@ -214,7 +214,7 @@
    5.13  done
    5.14  
    5.15  
    5.16 -(*** Cardinal multiplication ***)
    5.17 +subsection{*Cardinal multiplication*}
    5.18  
    5.19  (** Cardinal multiplication is commutative **)
    5.20  
    5.21 @@ -301,7 +301,7 @@
    5.22  apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
    5.23  done
    5.24  
    5.25 -(*** Some inequalities for multiplication ***)
    5.26 +subsection{*Some inequalities for multiplication*}
    5.27  
    5.28  lemma prod_square_lepoll: "A \<lesssim> A*A"
    5.29  apply (unfold lepoll_def inj_def)
    5.30 @@ -356,7 +356,7 @@
    5.31  apply (blast intro: prod_lepoll_mono subset_imp_lepoll)
    5.32  done
    5.33  
    5.34 -(*** Multiplication of finite cardinals is "ordinary" multiplication ***)
    5.35 +subsection{*Multiplication of finite cardinals is "ordinary" multiplication*}
    5.36  
    5.37  lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B"
    5.38  apply (unfold eqpoll_def)
    5.39 @@ -396,7 +396,7 @@
    5.40  by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
    5.41  
    5.42  
    5.43 -(*** Infinite Cardinals are Limit Ordinals ***)
    5.44 +subsection{*Infinite Cardinals are Limit Ordinals*}
    5.45  
    5.46  (*This proof is modelled upon one assuming nat<=A, with injection
    5.47    lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z
    5.48 @@ -623,6 +623,15 @@
    5.49  apply (simp add: cmult_def [symmetric] InfCard_csquare_eq)
    5.50  done
    5.51  
    5.52 +lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K"
    5.53 +apply (rule well_ord_InfCard_square_eq)  
    5.54 + apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) 
    5.55 +apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) 
    5.56 +done
    5.57 +
    5.58 +lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
    5.59 +by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord])
    5.60 +
    5.61  (** Toward's Kunen's Corollary 10.13 (1) **)
    5.62  
    5.63  lemma InfCard_le_cmult_eq: "[| InfCard(K);  L le K;  0<L |] ==> K |*| L = K"
    5.64 @@ -672,8 +681,9 @@
    5.65    might be  InfCard(K) ==> |list(K)| = K.
    5.66  *)
    5.67  
    5.68 -(*** For every cardinal number there exists a greater one
    5.69 -     [Kunen's Theorem 10.16, which would be trivial using AC] ***)
    5.70 +subsection{*For Every Cardinal Number There Exists A Greater One}
    5.71 +
    5.72 +text{*This result is Kunen's Theorem 10.16, which would be trivial using AC*}
    5.73  
    5.74  lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))"
    5.75  apply (unfold jump_cardinal_def)
    5.76 @@ -730,7 +740,7 @@
    5.77  apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl])
    5.78  done
    5.79  
    5.80 -(*** Basic properties of successor cardinals ***)
    5.81 +subsection{*Basic Properties of Successor Cardinals*}
    5.82  
    5.83  lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)"
    5.84  apply (unfold csucc_def)
     6.1 --- a/src/ZF/Cardinal_AC.thy	Sun Jul 14 15:11:21 2002 +0200
     6.2 +++ b/src/ZF/Cardinal_AC.thy	Sun Jul 14 15:14:43 2002 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  
     6.5  theory Cardinal_AC = CardinalArith + Zorn:
     6.6  
     6.7 -(*** Strengthened versions of existing theorems about cardinals ***)
     6.8 +subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
     6.9  
    6.10  lemma cardinal_eqpoll: "|A| eqpoll A"
    6.11  apply (rule AC_well_ord [THEN exE])
    6.12 @@ -65,7 +65,7 @@
    6.13  done
    6.14  
    6.15  
    6.16 -(*** Other applications of AC ***)
    6.17 +subsection{*Other Applications of AC*}
    6.18  
    6.19  lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B"
    6.20  apply (rule cardinal_eqpoll
     7.1 --- a/src/ZF/Epsilon.thy	Sun Jul 14 15:11:21 2002 +0200
     7.2 +++ b/src/ZF/Epsilon.thy	Sun Jul 14 15:14:43 2002 +0200
     7.3 @@ -34,7 +34,7 @@
     7.4      "rec(k,a,b) == recursor(a,b,k)"
     7.5  
     7.6  
     7.7 -(*** Basic closure properties ***)
     7.8 +subsection{*Basic Closure Properties*}
     7.9  
    7.10  lemma arg_subset_eclose: "A <= eclose(A)"
    7.11  apply (unfold eclose_def)
    7.12 @@ -77,7 +77,7 @@
    7.13  by (rule arg_in_eclose_sing [THEN eclose_induct], blast) 
    7.14  
    7.15  
    7.16 -(*** Leastness of eclose ***)
    7.17 +subsection{*Leastness of @{term eclose}*}
    7.18  
    7.19  (** eclose(A) is the least transitive set including A as a subset. **)
    7.20  
    7.21 @@ -117,7 +117,7 @@
    7.22  done
    7.23  
    7.24  
    7.25 -(*** Epsilon recursion ***)
    7.26 +subsection{*Epsilon Recursion*}
    7.27  
    7.28  (*Unused...*)
    7.29  lemma mem_eclose_trans: "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)"
    7.30 @@ -205,7 +205,7 @@
    7.31               dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
    7.32  done
    7.33  
    7.34 -(*** Rank ***)
    7.35 +subsection{*Rank*}
    7.36  
    7.37  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    7.38  lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
    7.39 @@ -309,7 +309,7 @@
    7.40  done
    7.41  
    7.42  
    7.43 -(*** Corollaries of leastness ***)
    7.44 +subsection{*Corollaries of Leastness*}
    7.45  
    7.46  lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)"
    7.47  apply (rule Transset_eclose [THEN eclose_least])
     8.1 --- a/src/ZF/Finite.thy	Sun Jul 14 15:11:21 2002 +0200
     8.2 +++ b/src/ZF/Finite.thy	Sun Jul 14 15:14:43 2002 +0200
     8.3 @@ -41,7 +41,7 @@
     8.4    type_intros Fin.intros
     8.5  
     8.6  
     8.7 -subsection {* Finite powerset operator *}
     8.8 +subsection {* Finite Powerset Operator *}
     8.9  
    8.10  lemma Fin_mono: "A<=B ==> Fin(A) <= Fin(B)"
    8.11  apply (unfold Fin.defs)
    8.12 @@ -132,7 +132,7 @@
    8.13  done
    8.14  
    8.15  
    8.16 -(*** Finite function space ***)
    8.17 +subsection{*Finite Function Space*}
    8.18  
    8.19  lemma FiniteFun_mono:
    8.20      "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D"
     9.1 --- a/src/ZF/Fixedpt.thy	Sun Jul 14 15:11:21 2002 +0200
     9.2 +++ b/src/ZF/Fixedpt.thy	Sun Jul 14 15:14:43 2002 +0200
     9.3 @@ -3,11 +3,11 @@
     9.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.5      Copyright   1992  University of Cambridge
     9.6  
     9.7 -Least and greatest fixed points; the Knaster-Tarski Theorem
     9.8 -
     9.9  Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
    9.10  *)
    9.11  
    9.12 +header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
    9.13 +
    9.14  theory Fixedpt = equalities:
    9.15  
    9.16  constdefs
    9.17 @@ -23,7 +23,7 @@
    9.18       "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
    9.19  
    9.20  
    9.21 -(*** Monotone operators ***)
    9.22 +subsection{*Monotone Operators*}
    9.23  
    9.24  lemma bnd_monoI:
    9.25      "[| h(D)<=D;   
    9.26 @@ -124,7 +124,7 @@
    9.27  apply (erule lfp_unfold)
    9.28  done
    9.29  
    9.30 -(*** General induction rule for least fixedpoints ***)
    9.31 +subsection{*General Induction Rule for Least Fixedpoints*}
    9.32  
    9.33  lemma Collect_is_pre_fixedpt:
    9.34      "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |]
    9.35 @@ -243,7 +243,7 @@
    9.36  done
    9.37  
    9.38  
    9.39 -(*** Coinduction rules for greatest fixed points ***)
    9.40 +subsection{*Coinduction Rules for Greatest Fixed Points*}
    9.41  
    9.42  (*weak version*)
    9.43  lemma weak_coinduct: "[| a: X;  X <= h(X);  X <= D |] ==> a : gfp(D,h)"
    10.1 --- a/src/ZF/Inductive.thy	Sun Jul 14 15:11:21 2002 +0200
    10.2 +++ b/src/ZF/Inductive.thy	Sun Jul 14 15:14:43 2002 +0200
    10.3 @@ -3,9 +3,10 @@
    10.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.5      Copyright   1993  University of Cambridge
    10.6  
    10.7 -(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
    10.8  *)
    10.9  
   10.10 +header{*Inductive and Coinductive Definitions*}
   10.11 +
   10.12  theory Inductive = Fixedpt + mono + QPair
   10.13    files
   10.14      "ind_syntax.ML"
   10.15 @@ -18,11 +19,4 @@
   10.16  setup IndCases.setup
   10.17  setup DatatypeTactics.setup
   10.18  
   10.19 -
   10.20 -(*belongs to theory ZF*)
   10.21 -declare bspec [dest?]
   10.22 -
   10.23 -(*belongs to theory upair*)
   10.24 -declare UnI1 [elim?]  UnI2 [elim?]
   10.25 -
   10.26  end
    11.1 --- a/src/ZF/InfDatatype.thy	Sun Jul 14 15:11:21 2002 +0200
    11.2 +++ b/src/ZF/InfDatatype.thy	Sun Jul 14 15:14:43 2002 +0200
    11.3 @@ -3,9 +3,10 @@
    11.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.5      Copyright   1994  University of Cambridge
    11.6  
    11.7 -Infinite-branching datatype definitions
    11.8  *)
    11.9  
   11.10 +header{*Infinite-Branching Datatype Definitions*}
   11.11 +
   11.12  theory InfDatatype = Datatype + Univ + Finite + Cardinal_AC:
   11.13  
   11.14  lemmas fun_Limit_VfromE = 
    12.1 --- a/src/ZF/IsaMakefile	Sun Jul 14 15:11:21 2002 +0200
    12.2 +++ b/src/ZF/IsaMakefile	Sun Jul 14 15:14:43 2002 +0200
    12.3 @@ -43,7 +43,7 @@
    12.4    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    12.5    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
    12.6    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
    12.7 -  Trancl.thy Univ.thy Update.thy \
    12.8 +  Trancl.thy Univ.thy \
    12.9    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
   12.10    ind_syntax.ML mono.thy pair.thy simpdata.ML		\
   12.11    thy_syntax.ML upair.thy
    13.1 --- a/src/ZF/List.thy	Sun Jul 14 15:11:21 2002 +0200
    13.2 +++ b/src/ZF/List.thy	Sun Jul 14 15:14:43 2002 +0200
    13.3 @@ -439,6 +439,8 @@
    13.4  apply (erule rev_type [THEN list.induct], simp_all)
    13.5  done
    13.6  
    13.7 +lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
    13.8 +
    13.9  
   13.10  (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
   13.11  
    14.1 --- a/src/ZF/Main.thy	Sun Jul 14 15:11:21 2002 +0200
    14.2 +++ b/src/ZF/Main.thy	Sun Jul 14 15:14:43 2002 +0200
    14.3 @@ -1,15 +1,8 @@
    14.4 -(*$Id$
    14.5 -  theory Main includes everything except AC*)
    14.6 -
    14.7 -theory Main = Update + List + EquivClass + IntDiv + CardinalArith:
    14.8 +(*$Id$*)
    14.9  
   14.10 -(* belongs to theory Trancl *)
   14.11 -lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl]
   14.12 -  and trancl_induct = trancl_induct [case_names initial step, induct set: trancl]
   14.13 -  and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1]
   14.14 -  and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1]
   14.15 +header{*Theory Main: Everything Except AC*}
   14.16  
   14.17 -
   14.18 +theory Main = List + IntDiv + CardinalArith:
   14.19  
   14.20  (*The theory of "iterates" logically belongs to Nat, but can't go there because
   14.21    primrec isn't available into after Datatype.  The only theories defined
   14.22 @@ -48,29 +41,9 @@
   14.23  by (induct n rule: nat_induct, simp_all)
   14.24  
   14.25  
   14.26 -(* belongs to theory Cardinal *)
   14.27 -declare Ord_Least [intro,simp,TC]
   14.28 -
   14.29 -
   14.30 -(* belongs to theory List *)
   14.31 -lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
   14.32 -
   14.33  (* belongs to theory IntDiv *)
   14.34  lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
   14.35    and negDivAlg_induct = negDivAlg_induct [consumes 2]
   14.36  
   14.37  
   14.38 -(* belongs to theory CardinalArith *)
   14.39 -
   14.40 -lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
   14.41 -
   14.42 -lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K"
   14.43 -apply (rule well_ord_InfCard_square_eq)  
   14.44 - apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) 
   14.45 -apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) 
   14.46 -done
   14.47 -
   14.48 -lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
   14.49 -by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord])
   14.50 -
   14.51  end
    15.1 --- a/src/ZF/Nat.thy	Sun Jul 14 15:11:21 2002 +0200
    15.2 +++ b/src/ZF/Nat.thy	Sun Jul 14 15:14:43 2002 +0200
    15.3 @@ -3,9 +3,10 @@
    15.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.5      Copyright   1994  University of Cambridge
    15.6  
    15.7 -Natural numbers in Zermelo-Fraenkel Set Theory 
    15.8  *)
    15.9  
   15.10 +header{*The Natural numbers As a Least Fixed Point*}
   15.11 +
   15.12  theory Nat = OrdQuant + Bool + mono:
   15.13  
   15.14  constdefs
   15.15 @@ -75,7 +76,7 @@
   15.16  lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard]
   15.17  
   15.18  
   15.19 -(** Injectivity properties and induction **)
   15.20 +subsection{*Injectivity Properties and Induction*}
   15.21  
   15.22  (*Mathematical induction*)
   15.23  lemma nat_induct:
   15.24 @@ -139,7 +140,7 @@
   15.25  by (blast dest!: lt_nat_in_nat)
   15.26  
   15.27  
   15.28 -(** Variations on mathematical induction **)
   15.29 +subsection{*Variations on Mathematical Induction*}
   15.30  
   15.31  (*complete induction*)
   15.32  
   15.33 @@ -226,8 +227,7 @@
   15.34  
   15.35  lemma nat_cases:
   15.36       "[|k=0 ==> P;  !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P"
   15.37 -apply (insert nat_cases_disj [of k], blast) 
   15.38 -done
   15.39 +by (insert nat_cases_disj [of k], blast) 
   15.40  
   15.41  (** nat_case **)
   15.42  
   15.43 @@ -250,9 +250,10 @@
   15.44  done
   15.45  
   15.46  
   15.47 +subsection{*Recursion on the Natural Numbers*}
   15.48  
   15.49 -(** nat_rec -- used to define eclose and transrec, then obsolete
   15.50 -    rec, from arith.ML, has fewer typing conditions **)
   15.51 +(** nat_rec is used to define eclose and transrec, then becomes obsolete.
   15.52 +    The operator rec, from arith.thy, has fewer typing conditions **)
   15.53  
   15.54  lemma nat_rec_0: "nat_rec(0,a,b) = a"
   15.55  apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
    16.1 --- a/src/ZF/Order.thy	Sun Jul 14 15:11:21 2002 +0200
    16.2 +++ b/src/ZF/Order.thy	Sun Jul 14 15:14:43 2002 +0200
    16.3 @@ -3,12 +3,12 @@
    16.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.5      Copyright   1994  University of Cambridge
    16.6  
    16.7 -Orders in Zermelo-Fraenkel Set Theory
    16.8 -
    16.9  Results from the book "Set Theory: an Introduction to Independence Proofs"
   16.10          by Kenneth Kunen.  Chapter 1, section 6.
   16.11  *)
   16.12  
   16.13 +header{*Partial and Total Orderings: Basic Definitions and Properties*}
   16.14 +
   16.15  theory Order = WF + Perm:
   16.16  
   16.17  constdefs
   16.18 @@ -48,9 +48,8 @@
   16.19      ord_iso :: "[i,i,i,i]=>i"      ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
   16.20  
   16.21  
   16.22 -(** Basic properties of the definitions **)
   16.23 +subsection{*Immediate Consequences of the Definitions*}
   16.24  
   16.25 -(*needed?*)
   16.26  lemma part_ord_Imp_asym:
   16.27      "part_ord(A,r) ==> asym(r Int A*A)"
   16.28  by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
   16.29 @@ -109,6 +108,8 @@
   16.30  by (unfold trans_on_def pred_def, blast)
   16.31  
   16.32  
   16.33 +subsection{*Restricting an Ordering's Domain*}
   16.34 +
   16.35  (** The ordering's properties hold over all subsets of its domain
   16.36      [including initial segments of the form pred(A,x,r) **)
   16.37  
   16.38 @@ -165,6 +166,8 @@
   16.39  done
   16.40  
   16.41  
   16.42 +subsection{*Empty and Unit Domains*}
   16.43 +
   16.44  (** Relations over the Empty Set **)
   16.45  
   16.46  lemma irrefl_0: "irrefl(0,r)"
   16.47 @@ -209,6 +212,10 @@
   16.48  done
   16.49  
   16.50  
   16.51 +subsection{*Order-Isomorphisms*}
   16.52 +
   16.53 +text{*Suppes calls them "similarities"*}
   16.54 +
   16.55  (** Order-preserving (monotone) maps **)
   16.56  
   16.57  lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
   16.58 @@ -221,9 +228,6 @@
   16.59  apply (force intro: apply_type dest: wf_on_not_refl)+
   16.60  done
   16.61  
   16.62 -
   16.63 -(** Order-isomorphisms -- or similarities, as Suppes calls them **)
   16.64 -
   16.65  lemma ord_isoI:
   16.66      "[| f: bij(A, B);
   16.67          !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s |]
   16.68 @@ -342,7 +346,7 @@
   16.69  done
   16.70  
   16.71  
   16.72 -(*** Main results of Kunen, Chapter 1 section 6 ***)
   16.73 +subsection{*Main results of Kunen, Chapter 1 section 6*}
   16.74  
   16.75  (*Inductive argument for Kunen's Lemma 6.1, etc.
   16.76    Simple proof from Halmos, page 72*)
   16.77 @@ -456,7 +460,7 @@
   16.78                      well_ord_is_linear well_ord_ord_iso ord_iso_sym)
   16.79  done
   16.80  
   16.81 -(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
   16.82 +subsection{*Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation*}
   16.83  
   16.84  lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B"
   16.85  by (unfold ord_iso_map_def, blast)
   16.86 @@ -564,8 +568,8 @@
   16.87  apply (simp add: domain_ord_iso_map_cases)
   16.88  done
   16.89  
   16.90 -(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
   16.91 -lemma well_ord_trichotomy:
   16.92 +text{*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*}
   16.93 +theorem well_ord_trichotomy:
   16.94     "[| well_ord(A,r);  well_ord(B,s) |]
   16.95      ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |
   16.96          (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) |
   16.97 @@ -585,7 +589,9 @@
   16.98  done
   16.99  
  16.100  
  16.101 -(*** Properties of converse(r), by Krzysztof Grabczewski ***)
  16.102 +subsection{*Miscellaneous Results by Krzysztof Grabczewski*}
  16.103 +
  16.104 +(** Properties of converse(r) **)
  16.105  
  16.106  lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
  16.107  by (unfold irrefl_def, blast)
    17.1 --- a/src/ZF/OrderArith.thy	Sun Jul 14 15:11:21 2002 +0200
    17.2 +++ b/src/ZF/OrderArith.thy	Sun Jul 14 15:14:43 2002 +0200
    17.3 @@ -3,9 +3,10 @@
    17.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.5      Copyright   1994  University of Cambridge
    17.6  
    17.7 -Towards ordinal arithmetic.  Also useful with wfrec.
    17.8  *)
    17.9  
   17.10 +header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
   17.11 +
   17.12  theory OrderArith = Order + Sum + Ordinal:
   17.13  constdefs
   17.14  
   17.15 @@ -32,29 +33,25 @@
   17.16      "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
   17.17  
   17.18  
   17.19 -(**** Addition of relations -- disjoint sum ****)
   17.20 +subsection{*Addition of Relations -- Disjoint Sum*}
   17.21  
   17.22  (** Rewrite rules.  Can be used to obtain introduction rules **)
   17.23  
   17.24  lemma radd_Inl_Inr_iff [iff]: 
   17.25      "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B"
   17.26 -apply (unfold radd_def, blast)
   17.27 -done
   17.28 +by (unfold radd_def, blast)
   17.29  
   17.30  lemma radd_Inl_iff [iff]: 
   17.31      "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
   17.32 -apply (unfold radd_def, blast)
   17.33 -done
   17.34 +by (unfold radd_def, blast)
   17.35  
   17.36  lemma radd_Inr_iff [iff]: 
   17.37      "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
   17.38 -apply (unfold radd_def, blast)
   17.39 -done
   17.40 +by (unfold radd_def, blast)
   17.41  
   17.42  lemma radd_Inr_Inl_iff [iff]: 
   17.43      "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
   17.44 -apply (unfold radd_def, blast)
   17.45 -done
   17.46 +by (unfold radd_def, blast)
   17.47  
   17.48  (** Elimination Rule **)
   17.49  
   17.50 @@ -64,8 +61,7 @@
   17.51          !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;  
   17.52          !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q   
   17.53       |] ==> Q"
   17.54 -apply (unfold radd_def, blast) 
   17.55 -done
   17.56 +by (unfold radd_def, blast) 
   17.57  
   17.58  (** Type checking **)
   17.59  
   17.60 @@ -80,8 +76,7 @@
   17.61  
   17.62  lemma linear_radd: 
   17.63      "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
   17.64 -apply (unfold linear_def, blast) 
   17.65 -done
   17.66 +by (unfold linear_def, blast) 
   17.67  
   17.68  
   17.69  (** Well-foundedness **)
   17.70 @@ -119,7 +114,8 @@
   17.71  lemma sum_bij:
   17.72       "[| f: bij(A,C);  g: bij(B,D) |]
   17.73        ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"
   17.74 -apply (rule_tac d = "case (%x. Inl (converse (f) `x), %y. Inr (converse (g) `y))" in lam_bijective)
   17.75 +apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))" 
   17.76 +       in lam_bijective)
   17.77  apply (typecheck add: bij_is_inj inj_is_fun) 
   17.78  apply (auto simp add: left_inverse_bij right_inverse_bij) 
   17.79  done
   17.80 @@ -156,11 +152,10 @@
   17.81       "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
   17.82        : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),     
   17.83                  A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
   17.84 -apply (rule sum_assoc_bij [THEN ord_isoI], auto)
   17.85 -done
   17.86 +by (rule sum_assoc_bij [THEN ord_isoI], auto)
   17.87  
   17.88  
   17.89 -(**** Multiplication of relations -- lexicographic product ****)
   17.90 +subsection{*Multiplication of Relations -- Lexicographic Product*}
   17.91  
   17.92  (** Rewrite rule.  Can be used to obtain introduction rules **)
   17.93  
   17.94 @@ -169,23 +164,19 @@
   17.95              (<a',a>: r  & a':A & a:A & b': B & b: B) |   
   17.96              (<b',b>: s  & a'=a & a:A & b': B & b: B)"
   17.97  
   17.98 -apply (unfold rmult_def, blast)
   17.99 -done
  17.100 +by (unfold rmult_def, blast)
  17.101  
  17.102  lemma rmultE: 
  17.103      "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);               
  17.104          [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;         
  17.105          [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q  
  17.106       |] ==> Q"
  17.107 -apply blast 
  17.108 -done
  17.109 +by blast 
  17.110  
  17.111  (** Type checking **)
  17.112  
  17.113  lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)"
  17.114 -apply (unfold rmult_def)
  17.115 -apply (rule Collect_subset)
  17.116 -done
  17.117 +by (unfold rmult_def, rule Collect_subset)
  17.118  
  17.119  lemmas field_rmult = rmult_type [THEN field_rel_subset]
  17.120  
  17.121 @@ -193,8 +184,7 @@
  17.122  
  17.123  lemma linear_rmult:
  17.124      "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
  17.125 -apply (simp add: linear_def, blast) 
  17.126 -done
  17.127 +by (simp add: linear_def, blast) 
  17.128  
  17.129  (** Well-foundedness **)
  17.130  
  17.131 @@ -289,33 +279,28 @@
  17.132  lemma sum_prod_distrib_bij:
  17.133       "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
  17.134        : bij((A+B)*C, (A*C)+(B*C))"
  17.135 -apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " 
  17.136 -       in lam_bijective)
  17.137 -apply auto
  17.138 -done
  17.139 +by (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " 
  17.140 +    in lam_bijective, auto)
  17.141  
  17.142  lemma sum_prod_distrib_ord_iso:
  17.143   "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
  17.144    : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),  
  17.145              (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
  17.146 -apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
  17.147 -done
  17.148 +by (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
  17.149  
  17.150  (** Associativity **)
  17.151  
  17.152  lemma prod_assoc_bij:
  17.153       "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
  17.154 -apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
  17.155 -done
  17.156 +by (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
  17.157  
  17.158  lemma prod_assoc_ord_iso:
  17.159   "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                    
  17.160    : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),   
  17.161              A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
  17.162 -apply (rule prod_assoc_bij [THEN ord_isoI], auto)
  17.163 -done
  17.164 +by (rule prod_assoc_bij [THEN ord_isoI], auto)
  17.165  
  17.166 -(**** Inverse image of a relation ****)
  17.167 +subsection{*Inverse Image of a Relation*}
  17.168  
  17.169  (** Rewrite rule **)
  17.170  
  17.171 @@ -325,8 +310,7 @@
  17.172  (** Type checking **)
  17.173  
  17.174  lemma rvimage_type: "rvimage(A,f,r) <= A*A"
  17.175 -apply (unfold rvimage_def)
  17.176 -apply (rule Collect_subset)
  17.177 +apply (unfold rvimage_def, rule Collect_subset)
  17.178  done
  17.179  
  17.180  lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
  17.181 @@ -410,8 +394,7 @@
  17.182  
  17.183  lemma ord_iso_rvimage_eq: 
  17.184      "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"
  17.185 -apply (unfold ord_iso_def rvimage_def, blast)
  17.186 -done
  17.187 +by (unfold ord_iso_def rvimage_def, blast)
  17.188  
  17.189  
  17.190  (** The "measure" relation is useful with wfrec **)
  17.191 @@ -424,12 +407,10 @@
  17.192  done
  17.193  
  17.194  lemma wf_measure [iff]: "wf(measure(A,f))"
  17.195 -apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
  17.196 -done
  17.197 +by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
  17.198  
  17.199  lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
  17.200 -apply (simp (no_asm) add: measure_def)
  17.201 -done
  17.202 +by (simp (no_asm) add: measure_def)
  17.203  
  17.204  ML {*
  17.205  val measure_def = thm "measure_def";
    18.1 --- a/src/ZF/OrderType.thy	Sun Jul 14 15:11:21 2002 +0200
    18.2 +++ b/src/ZF/OrderType.thy	Sun Jul 14 15:14:43 2002 +0200
    18.3 @@ -3,16 +3,16 @@
    18.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.5      Copyright   1994  University of Cambridge
    18.6  
    18.7 -Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory 
    18.8 -
    18.9 -The order type of a well-ordering is the least ordinal isomorphic to it.
   18.10 -
   18.11 -Ordinal arithmetic is traditionally defined in terms of order types, as here.
   18.12 -But a definition by transfinite recursion would be much simpler!
   18.13  *)
   18.14  
   18.15 +header{*Order Types and Ordinal Arithmetic*}
   18.16 +
   18.17  theory OrderType = OrderArith + OrdQuant + Nat:
   18.18  
   18.19 +text{*The order type of a well-ordering is the least ordinal isomorphic to it.
   18.20 +Ordinal arithmetic is traditionally defined in terms of order types, as it is
   18.21 +here.  But a definition by transfinite recursion would be much simpler!*}
   18.22 +
   18.23  constdefs
   18.24    
   18.25    ordermap  :: "[i,i]=>i"
   18.26 @@ -108,7 +108,7 @@
   18.27  apply (rule lamI [THEN imageI], assumption+)
   18.28  done
   18.29  
   18.30 -(*** Unfolding of ordermap ***)
   18.31 +subsubsection{*Unfolding of ordermap *}
   18.32  
   18.33  (*Useful for cardinality reasoning; see CardinalArith.ML*)
   18.34  lemma ordermap_eq_image: 
   18.35 @@ -145,7 +145,7 @@
   18.36  *)
   18.37  
   18.38  
   18.39 -(*** Showing that ordermap, ordertype yield ordinals ***)
   18.40 +subsubsection{*Showing that ordermap, ordertype yield ordinals *}
   18.41  
   18.42  lemma Ord_ordermap: 
   18.43      "[| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)"
   18.44 @@ -170,7 +170,7 @@
   18.45  done
   18.46  
   18.47  
   18.48 -(*** ordermap preserves the orderings in both directions ***)
   18.49 +subsubsection{*ordermap preserves the orderings in both directions *}
   18.50  
   18.51  lemma ordermap_mono:
   18.52       "[| <w,x>: r;  wf[A](r);  w: A; x: A |]
   18.53 @@ -199,7 +199,7 @@
   18.54               simp add: mem_not_refl)
   18.55  done
   18.56  
   18.57 -(*** Isomorphisms involving ordertype ***)
   18.58 +subsubsection{*Isomorphisms involving ordertype *}
   18.59  
   18.60  lemma ordertype_ord_iso: 
   18.61   "well_ord(A,r)
   18.62 @@ -227,7 +227,7 @@
   18.63  apply (erule ordertype_ord_iso [THEN ord_iso_sym])
   18.64  done
   18.65  
   18.66 -(*** Basic equalities for ordertype ***)
   18.67 +subsubsection{*Basic equalities for ordertype *}
   18.68  
   18.69  (*Ordertype of Memrel*)
   18.70  lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j"
   18.71 @@ -255,7 +255,7 @@
   18.72                           ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
   18.73  lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq]
   18.74  
   18.75 -(*** A fundamental unfolding law for ordertype. ***)
   18.76 +subsubsection{*A fundamental unfolding law for ordertype. *}
   18.77  
   18.78  (*Ordermap returns the same result if applied to an initial segment*)
   18.79  lemma ordermap_pred_eq_ordermap:
   18.80 @@ -332,7 +332,7 @@
   18.81  
   18.82  subsection{*Ordinal Addition*}
   18.83  
   18.84 -(*** Order Type calculations for radd ***)
   18.85 +subsubsection{*Order Type calculations for radd *}
   18.86  
   18.87  (** Addition with 0 **)
   18.88  
   18.89 @@ -398,7 +398,7 @@
   18.90  done
   18.91  
   18.92  
   18.93 -(*** ordify: trivial coercion to an ordinal ***)
   18.94 +subsubsection{*ordify: trivial coercion to an ordinal *}
   18.95  
   18.96  lemma Ord_ordify [iff, TC]: "Ord(ordify(x))"
   18.97  by (simp add: ordify_def)
   18.98 @@ -408,7 +408,7 @@
   18.99  by (simp add: ordify_def)
  18.100  
  18.101  
  18.102 -(*** Basic laws for ordinal addition ***)
  18.103 +subsubsection{*Basic laws for ordinal addition *}
  18.104  
  18.105  lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"
  18.106  by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd
  18.107 @@ -552,7 +552,7 @@
  18.108  done
  18.109  
  18.110  
  18.111 -(*** Ordinal addition with successor -- via associativity! ***)
  18.112 +subsubsection{*Ordinal addition with successor -- via associativity! *}
  18.113  
  18.114  lemma oadd_assoc: "(i++j)++k = i++(j++k)"
  18.115  apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)
  18.116 @@ -599,7 +599,8 @@
  18.117  
  18.118  lemma oadd_Limit: "Limit(j) ==> i++j = (UN k:j. i++k)"
  18.119  apply (frule Limit_has_0 [THEN ltD])
  18.120 -apply (simp (no_asm_simp) add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] Union_eq_UN [symmetric] Limit_Union_eq)
  18.121 +apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] 
  18.122 +                 Union_eq_UN [symmetric] Limit_Union_eq)
  18.123  done
  18.124  
  18.125  lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
  18.126 @@ -634,8 +635,8 @@
  18.127  apply (rule le_trans)
  18.128  apply (rule_tac [2] le_implies_UN_le_UN)
  18.129  apply (erule_tac [2] bspec)
  18.130 -prefer 2 apply assumption
  18.131 -apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
  18.132 + prefer 2 apply assumption
  18.133 +apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
  18.134  done
  18.135  
  18.136  lemma oadd_le_mono1: "k le j ==> k++i le j++i"
  18.137 @@ -752,7 +753,7 @@
  18.138  apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
  18.139  done
  18.140  
  18.141 -(*** A useful unfolding law ***)
  18.142 +subsubsection{*A useful unfolding law *}
  18.143  
  18.144  lemma pred_Pair_eq: 
  18.145   "[| a:A;  b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =      
  18.146 @@ -779,10 +780,12 @@
  18.147                     rmult(i,Memrel(i),j,Memrel(j))) =                    
  18.148           raw_oadd (j**i', j')"
  18.149  apply (unfold raw_oadd_def omult_def)
  18.150 -apply (simp (no_asm_simp) add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 well_ord_Memrel)
  18.151 +apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 
  18.152 +                 well_ord_Memrel)
  18.153  apply (rule trans)
  18.154 -apply (rule_tac [2] ordertype_ord_iso [THEN sum_ord_iso_cong, THEN ordertype_eq])
  18.155 -apply (rule_tac [3] ord_iso_refl)
  18.156 + apply (rule_tac [2] ordertype_ord_iso 
  18.157 +                      [THEN sum_ord_iso_cong, THEN ordertype_eq])
  18.158 +  apply (rule_tac [3] ord_iso_refl)
  18.159  apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])
  18.160  apply (elim SigmaE sumE ltE ssubst)
  18.161  apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
  18.162 @@ -807,7 +810,7 @@
  18.163  apply (rule ltI)
  18.164   prefer 2
  18.165   apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
  18.166 -apply (simp (no_asm_simp) add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
  18.167 +apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
  18.168  apply (rule bexI)
  18.169  prefer 2 apply (blast elim!: ltE)
  18.170  apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
  18.171 @@ -824,7 +827,7 @@
  18.172  apply (blast intro: omult_oadd_lt [THEN ltD] ltI)
  18.173  done
  18.174  
  18.175 -(*** Basic laws for ordinal multiplication ***)
  18.176 +subsubsection{*Basic laws for ordinal multiplication *}
  18.177  
  18.178  (** Ordinal multiplication by zero **)
  18.179  
  18.180 @@ -886,7 +889,8 @@
  18.181  apply (rule prod_ord_iso_cong [OF ord_iso_refl 
  18.182                                    ordertype_ord_iso [THEN ord_iso_sym]])
  18.183  apply (blast intro: well_ord_rmult well_ord_Memrel)+
  18.184 -apply (rule prod_assoc_ord_iso [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
  18.185 +apply (rule prod_assoc_ord_iso 
  18.186 +             [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
  18.187  apply (rule_tac [2] ordertype_eq)
  18.188  apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])
  18.189  apply (blast intro: well_ord_rmult well_ord_Memrel Ord_ordertype)+
  18.190 @@ -905,7 +909,7 @@
  18.191                Union_eq_UN [symmetric] Limit_Union_eq)
  18.192  
  18.193  
  18.194 -(*** Ordering/monotonicity properties of ordinal multiplication ***)
  18.195 +subsubsection{*Ordering/monotonicity properties of ordinal multiplication *}
  18.196  
  18.197  (*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
  18.198  lemma lt_omult1: "[| k<i;  0<j |] ==> k < i**j"
    19.1 --- a/src/ZF/Ordinal.thy	Sun Jul 14 15:11:21 2002 +0200
    19.2 +++ b/src/ZF/Ordinal.thy	Sun Jul 14 15:14:43 2002 +0200
    19.3 @@ -3,9 +3,10 @@
    19.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.5      Copyright   1994  University of Cambridge
    19.6  
    19.7 -Ordinals in Zermelo-Fraenkel Set Theory 
    19.8  *)
    19.9  
   19.10 +header{*Transitive Sets and Ordinals*}
   19.11 +
   19.12  theory Ordinal = WF + Bool + equalities:
   19.13  
   19.14  constdefs
   19.15 @@ -35,9 +36,9 @@
   19.16    "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
   19.17  
   19.18  
   19.19 -(*** Rules for Transset ***)
   19.20 +subsection{*Rules for Transset*}
   19.21  
   19.22 -(** Three neat characterisations of Transset **)
   19.23 +subsubsection{*Three Neat Characterisations of Transset*}
   19.24  
   19.25  lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)"
   19.26  by (unfold Transset_def, blast)
   19.27 @@ -50,7 +51,7 @@
   19.28  lemma Transset_iff_Union_subset: "Transset(A) <-> Union(A) <= A"
   19.29  by (unfold Transset_def, blast)
   19.30  
   19.31 -(** Consequences of downwards closure **)
   19.32 +subsubsection{*Consequences of Downwards Closure*}
   19.33  
   19.34  lemma Transset_doubleton_D: 
   19.35      "[| Transset(C); {a,b}: C |] ==> a:C & b: C"
   19.36 @@ -70,7 +71,7 @@
   19.37      "[| Transset(C); A*B <= C; a: A |] ==> B <= C"
   19.38  by (blast dest: Transset_Pair_D)
   19.39  
   19.40 -(** Closure properties **)
   19.41 +subsubsection{*Closure Properties*}
   19.42  
   19.43  lemma Transset_0: "Transset(0)"
   19.44  by (unfold Transset_def, blast)
   19.45 @@ -109,7 +110,7 @@
   19.46  by (rule Transset_Inter_family, auto) 
   19.47  
   19.48  
   19.49 -(*** Natural Deduction rules for Ord ***)
   19.50 +subsection{*Lemmas for Ordinals*}
   19.51  
   19.52  lemma OrdI:
   19.53      "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i)"
   19.54 @@ -122,7 +123,6 @@
   19.55      "[| Ord(i);  j:i |] ==> Transset(j) "
   19.56  by (unfold Ord_def, blast)
   19.57  
   19.58 -(*** Lemmas for ordinals ***)
   19.59  
   19.60  lemma Ord_in_Ord: "[| Ord(i);  j:i |] ==> Ord(j)"
   19.61  by (unfold Ord_def Transset_def, blast)
   19.62 @@ -147,7 +147,7 @@
   19.63  by (blast dest: OrdmemD)
   19.64  
   19.65  
   19.66 -(*** The construction of ordinals: 0, succ, Union ***)
   19.67 +subsection{*The Construction of Ordinals: 0, succ, Union*}
   19.68  
   19.69  lemma Ord_0 [iff,TC]: "Ord(0)"
   19.70  by (blast intro: OrdI Transset_0)
   19.71 @@ -180,7 +180,7 @@
   19.72  apply (blast intro: Ord_in_Ord)+
   19.73  done
   19.74  
   19.75 -(*** < is 'less than' for ordinals ***)
   19.76 +subsection{*< is 'less Than' for Ordinals*}
   19.77  
   19.78  lemma ltI: "[| i:j;  Ord(j) |] ==> i<j"
   19.79  by (unfold lt_def, blast)
   19.80 @@ -263,7 +263,7 @@
   19.81  
   19.82  lemmas le0D = le0_iff [THEN iffD1, dest!]
   19.83  
   19.84 -(*** Natural Deduction rules for Memrel ***)
   19.85 +subsection{*Natural Deduction Rules for Memrel*}
   19.86  
   19.87  (*The lemmas MemrelI/E give better speed than [iff] here*)
   19.88  lemma Memrel_iff [simp]: "<a,b> : Memrel(A) <-> a:b & a:A & b:A"
   19.89 @@ -311,7 +311,7 @@
   19.90  by (unfold Transset_def, blast)
   19.91  
   19.92  
   19.93 -(*** Transfinite induction ***)
   19.94 +subsection{*Transfinite Induction*}
   19.95  
   19.96  (*Epsilon induction over a transitive set*)
   19.97  lemma Transset_induct: 
   19.98 @@ -339,7 +339,7 @@
   19.99  (*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
  19.100  
  19.101  
  19.102 -(** Proving that < is a linear ordering on the ordinals **)
  19.103 +subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
  19.104  
  19.105  lemma Ord_linear [rule_format]:
  19.106       "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)"
  19.107 @@ -374,7 +374,7 @@
  19.108  lemma not_lt_imp_le: "[| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i"
  19.109  by (rule_tac i = "i" and j = "j" in Ord_linear2, auto)
  19.110  
  19.111 -(** Some rewrite rules for <, le **)
  19.112 +subsubsection{*Some Rewrite Rules for <, le*}
  19.113  
  19.114  lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i<j"
  19.115  by (unfold lt_def, blast)
  19.116 @@ -398,7 +398,7 @@
  19.117  by (blast intro: Ord_0_lt)
  19.118  
  19.119  
  19.120 -(*** Results about less-than or equals ***)
  19.121 +subsection{*Results about Less-Than or Equals*}
  19.122  
  19.123  (** For ordinals, j<=i (subset) implies j le i (less-than or equals) **)
  19.124  
  19.125 @@ -425,7 +425,7 @@
  19.126  lemma all_lt_imp_le: "[| Ord(i);  Ord(j);  !!x. x<j ==> x<i |] ==> j le i"
  19.127  by (blast intro: not_lt_imp_le dest: lt_irrefl)
  19.128  
  19.129 -(** Transitive laws **)
  19.130 +subsubsection{*Transitivity Laws*}
  19.131  
  19.132  lemma lt_trans1: "[| i le j;  j<k |] ==> i<k"
  19.133  by (blast elim!: leE intro: lt_trans)
  19.134 @@ -477,7 +477,7 @@
  19.135  apply (simp add: lt_def) 
  19.136  done
  19.137  
  19.138 -(** Union and Intersection **)
  19.139 +subsubsection{*Union and Intersection*}
  19.140  
  19.141  lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i le i Un j"
  19.142  by (rule Un_upper1 [THEN subset_imp_le], auto)
  19.143 @@ -539,7 +539,7 @@
  19.144  by (blast intro: Ord_trans)
  19.145  
  19.146  
  19.147 -(*** Results about limits ***)
  19.148 +subsection{*Results about Limits*}
  19.149  
  19.150  lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"
  19.151  apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI])
  19.152 @@ -612,7 +612,7 @@
  19.153  by (blast intro: Ord_trans)
  19.154  
  19.155  
  19.156 -(*** Limit ordinals -- general properties ***)
  19.157 +subsection{*Limit Ordinals -- General Properties*}
  19.158  
  19.159  lemma Limit_Union_eq: "Limit(i) ==> Union(i) = i"
  19.160  apply (unfold Limit_def)
  19.161 @@ -666,7 +666,7 @@
  19.162  by (blast elim!: leE)
  19.163  
  19.164  
  19.165 -(** Traditional 3-way case analysis on ordinals **)
  19.166 +subsubsection{*Traditional 3-Way Case Analysis on Ordinals*}
  19.167  
  19.168  lemma Ord_cases_disj: "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)"
  19.169  by (blast intro!: non_succ_LimitI Ord_0_lt)
    20.1 --- a/src/ZF/Perm.thy	Sun Jul 14 15:11:21 2002 +0200
    20.2 +++ b/src/ZF/Perm.thy	Sun Jul 14 15:14:43 2002 +0200
    20.3 @@ -9,6 +9,8 @@
    20.4    -- Lemmas for the Schroeder-Bernstein Theorem
    20.5  *)
    20.6  
    20.7 +header{*Injections, Surjections, Bijections, Composition*}
    20.8 +
    20.9  theory Perm = mono + func:
   20.10  
   20.11  constdefs
   20.12 @@ -35,6 +37,8 @@
   20.13      "bij(A,B) == inj(A,B) Int surj(A,B)"
   20.14  
   20.15  
   20.16 +subsection{*Surjections*}
   20.17 +
   20.18  (** Surjective function space **)
   20.19  
   20.20  lemma surj_is_fun: "f: surj(A,B) ==> f: A->B"
   20.21 @@ -77,6 +81,8 @@
   20.22  done
   20.23  
   20.24  
   20.25 +subsection{*Injections*}
   20.26 +
   20.27  (** Injective function space **)
   20.28  
   20.29  lemma inj_is_fun: "f: inj(A,B) ==> f: A->B"
   20.30 @@ -109,7 +115,7 @@
   20.31  apply (simp_all add: lam_type)
   20.32  done
   20.33  
   20.34 -(** Bijections **)
   20.35 +subsection{*Bijections*}
   20.36  
   20.37  lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)"
   20.38  apply (unfold bij_def)
   20.39 @@ -141,7 +147,7 @@
   20.40  done
   20.41  
   20.42  
   20.43 -(** Identity function **)
   20.44 +subsection{*Identity Function*}
   20.45  
   20.46  lemma idI [intro!]: "a:A ==> <a,a> : id(A)"
   20.47  apply (unfold id_def)
   20.48 @@ -225,7 +231,7 @@
   20.49  lemma right_inverse_bij: "[| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b"
   20.50  by (force simp add: bij_def surj_range)
   20.51  
   20.52 -(** Converses of injections, surjections, bijections **)
   20.53 +subsection{*Converses of Injections, Surjections, Bijections*}
   20.54  
   20.55  lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
   20.56  apply (rule f_imp_injective)
   20.57 @@ -247,7 +253,7 @@
   20.58  
   20.59  
   20.60  
   20.61 -(** Composition of two relations **)
   20.62 +subsection{*Composition of Two Relations*}
   20.63  
   20.64  (*The inductive definition package could derive these theorems for (r O s)*)
   20.65  
   20.66 @@ -270,7 +276,7 @@
   20.67  by blast
   20.68  
   20.69  
   20.70 -(** Domain and Range -- see Suppes, section 3.1 **)
   20.71 +subsection{*Domain and Range -- see Suppes, Section 3.1*}
   20.72  
   20.73  (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
   20.74  lemma range_comp: "range(r O s) <= range(r)"
   20.75 @@ -289,7 +295,7 @@
   20.76  by blast
   20.77  
   20.78  
   20.79 -(** Other results **)
   20.80 +subsection{*Other Results*}
   20.81  
   20.82  lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
   20.83  by blast
   20.84 @@ -315,7 +321,7 @@
   20.85  by blast
   20.86  
   20.87  
   20.88 -(** Composition preserves functions, injections, and surjections **)
   20.89 +subsection{*Composition Preserves Functions, Injections, and Surjections*}
   20.90  
   20.91  lemma comp_function: "[| function(g);  function(f) |] ==> function(f O g)"
   20.92  by (unfold function_def, blast)
   20.93 @@ -367,14 +373,15 @@
   20.94  done
   20.95  
   20.96  
   20.97 -(** Dual properties of inj and surj -- useful for proofs from
   20.98 +subsection{*Dual Properties of @{term inj} and @{term surj}*}
   20.99 +
  20.100 +text{*Useful for proofs from
  20.101      D Pastre.  Automatic theorem proving in set theory. 
  20.102 -    Artificial Intelligence, 10:1--27, 1978. **)
  20.103 +    Artificial Intelligence, 10:1--27, 1978.*}
  20.104  
  20.105  lemma comp_mem_injD1: 
  20.106      "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)"
  20.107 -apply (unfold inj_def, force) 
  20.108 -done
  20.109 +by (unfold inj_def, force) 
  20.110  
  20.111  lemma comp_mem_injD2: 
  20.112      "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
  20.113 @@ -400,7 +407,7 @@
  20.114  apply (blast intro: apply_funtype)
  20.115  done
  20.116  
  20.117 -(** inverses of composition **)
  20.118 +subsubsection{*Inverses of Composition*}
  20.119  
  20.120  (*left inverse of composition; one inclusion is
  20.121          f: A->B ==> id(A) <= converse(f) O f *)
  20.122 @@ -421,7 +428,7 @@
  20.123  done
  20.124  
  20.125  
  20.126 -(** Proving that a function is a bijection **)
  20.127 +subsubsection{*Proving that a Function is a Bijection*}
  20.128  
  20.129  lemma comp_eq_id_iff: 
  20.130      "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"
  20.131 @@ -448,7 +455,9 @@
  20.132  by (simp add: fg_imp_bijective comp_eq_id_iff 
  20.133                left_inverse_lemma right_inverse_lemma)
  20.134  
  20.135 -(** Unions of functions -- cf similar theorems on func.ML **)
  20.136 +subsubsection{*Unions of Functions*}
  20.137 +
  20.138 +text{*See similar theorems in func.thy*}
  20.139  
  20.140  (*Theorem by KG, proof by LCP*)
  20.141  lemma inj_disjoint_Un:
  20.142 @@ -479,7 +488,7 @@
  20.143  done
  20.144  
  20.145  
  20.146 -(** Restrictions as surjections and bijections *)
  20.147 +subsubsection{*Restrictions as Surjections and Bijections*}
  20.148  
  20.149  lemma surj_image:
  20.150      "f: Pi(A,B) ==> f: surj(A, f``A)"
  20.151 @@ -508,7 +517,7 @@
  20.152  done
  20.153  
  20.154  
  20.155 -(*** Lemmas for Ramsey's Theorem ***)
  20.156 +subsubsection{*Lemmas for Ramsey's Theorem*}
  20.157  
  20.158  lemma inj_weaken_type: "[| f: inj(A,B);  B<=D |] ==> f: inj(A,D)"
  20.159  apply (unfold inj_def)
    21.1 --- a/src/ZF/QPair.thy	Sun Jul 14 15:11:21 2002 +0200
    21.2 +++ b/src/ZF/QPair.thy	Sun Jul 14 15:14:43 2002 +0200
    21.3 @@ -3,21 +3,24 @@
    21.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.5      Copyright   1993  University of Cambridge
    21.6  
    21.7 -Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
    21.8 -structures in ZF.  Does not precisely follow Quine's construction.  Thanks
    21.9 -to Thomas Forster for suggesting this approach!
   21.10 -
   21.11 -W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
   21.12 -1966.
   21.13 -
   21.14  Many proofs are borrowed from pair.thy and sum.thy
   21.15  
   21.16  Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
   21.17      is not a limit ordinal? 
   21.18  *)
   21.19  
   21.20 +header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
   21.21 +
   21.22  theory QPair = Sum + mono:
   21.23  
   21.24 +text{*For non-well-founded data
   21.25 +structures in ZF.  Does not precisely follow Quine's construction.  Thanks
   21.26 +to Thomas Forster for suggesting this approach!
   21.27 +
   21.28 +W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
   21.29 +1966.
   21.30 +*}
   21.31 +
   21.32  constdefs
   21.33    QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
   21.34      "<a;b> == a+b"
   21.35 @@ -62,7 +65,7 @@
   21.36  print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
   21.37  
   21.38  
   21.39 -(**** Quine ordered pairing ****)
   21.40 +subsection{*Quine ordered pairing*}
   21.41  
   21.42  (** Lemmas for showing that <a;b> uniquely determines a and b **)
   21.43  
   21.44 @@ -83,8 +86,8 @@
   21.45  by blast
   21.46  
   21.47  
   21.48 -(*** QSigma: Disjoint union of a family of sets
   21.49 -     Generalizes Cartesian product ***)
   21.50 +subsubsection{*QSigma: Disjoint union of a family of sets
   21.51 +     Generalizes Cartesian product*}
   21.52  
   21.53  lemma QSigmaI [intro!]: "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
   21.54  by (simp add: QSigma_def)
   21.55 @@ -95,8 +98,7 @@
   21.56      "[| c: QSigma(A,B);   
   21.57          !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
   21.58       |] ==> P"
   21.59 -apply (simp add: QSigma_def, blast) 
   21.60 -done
   21.61 +by (simp add: QSigma_def, blast) 
   21.62  
   21.63  (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
   21.64  
   21.65 @@ -104,8 +106,7 @@
   21.66      "[| c: QSigma(A,B);   
   21.67          !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
   21.68       |] ==> P"
   21.69 -apply (simp add: QSigma_def, blast) 
   21.70 -done
   21.71 +by (simp add: QSigma_def, blast) 
   21.72  
   21.73  lemma QSigmaE2 [elim!]:
   21.74      "[| <a;b>: QSigma(A,B); [| a:A;  b:B(a) |] ==> P |] ==> P"
   21.75 @@ -129,7 +130,7 @@
   21.76  by blast
   21.77  
   21.78  
   21.79 -(*** Projections: qfst, qsnd ***)
   21.80 +subsubsection{*Projections: qfst, qsnd*}
   21.81  
   21.82  lemma qfst_conv [simp]: "qfst(<a;b>) = a"
   21.83  by (simp add: qfst_def, blast)
   21.84 @@ -147,7 +148,7 @@
   21.85  by auto
   21.86  
   21.87  
   21.88 -(*** Eliminator - qsplit ***)
   21.89 +subsubsection{*Eliminator: qsplit*}
   21.90  
   21.91  (*A META-equality, so that it applies to higher types as well...*)
   21.92  lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
   21.93 @@ -166,7 +167,7 @@
   21.94  done
   21.95  
   21.96  
   21.97 -(*** qsplit for predicates: result type o ***)
   21.98 +subsubsection{*qsplit for predicates: result type o*}
   21.99  
  21.100  lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
  21.101  by (simp add: qsplit_def)
  21.102 @@ -176,14 +177,13 @@
  21.103      "[| qsplit(R,z);  z:QSigma(A,B);                     
  21.104          !!x y. [| z = <x;y>;  R(x,y) |] ==> P            
  21.105      |] ==> P"
  21.106 -apply (simp add: qsplit_def, auto) 
  21.107 -done
  21.108 +by (simp add: qsplit_def, auto) 
  21.109  
  21.110  lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
  21.111  by (simp add: qsplit_def)
  21.112  
  21.113  
  21.114 -(*** qconverse ***)
  21.115 +subsubsection{*qconverse*}
  21.116  
  21.117  lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
  21.118  by (simp add: qconverse_def, blast)
  21.119 @@ -195,8 +195,7 @@
  21.120      "[| yx : qconverse(r);   
  21.121          !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P  
  21.122       |] ==> P"
  21.123 -apply (simp add: qconverse_def, blast) 
  21.124 -done
  21.125 +by (simp add: qconverse_def, blast) 
  21.126  
  21.127  lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
  21.128  by blast
  21.129 @@ -211,7 +210,7 @@
  21.130  by blast
  21.131  
  21.132  
  21.133 -(**** The Quine-inspired notion of disjoint sum ****)
  21.134 +subsection{*The Quine-inspired notion of disjoint sum*}
  21.135  
  21.136  lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
  21.137  
  21.138 @@ -230,8 +229,7 @@
  21.139          !!x. [| x:A;  u=QInl(x) |] ==> P;  
  21.140          !!y. [| y:B;  u=QInr(y) |] ==> P  
  21.141       |] ==> P"
  21.142 -apply (simp add: qsum_defs, blast) 
  21.143 -done
  21.144 +by (simp add: qsum_defs, blast) 
  21.145  
  21.146  
  21.147  (** Injection and freeness equivalences, for rewriting **)
  21.148 @@ -268,8 +266,7 @@
  21.149  
  21.150  lemma qsum_iff:
  21.151       "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"
  21.152 -apply blast
  21.153 -done
  21.154 +by blast
  21.155  
  21.156  lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D"
  21.157  by blast
  21.158 @@ -279,7 +276,7 @@
  21.159  apply blast
  21.160  done
  21.161  
  21.162 -(*** Eliminator -- qcase ***)
  21.163 +subsubsection{*Eliminator -- qcase*}
  21.164  
  21.165  lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
  21.166  by (simp add: qsum_defs )
  21.167 @@ -293,8 +290,7 @@
  21.168          !!x. x: A ==> c(x): C(QInl(x));    
  21.169          !!y. y: B ==> d(y): C(QInr(y))  
  21.170       |] ==> qcase(c,d,u) : C(u)"
  21.171 -apply (simp add: qsum_defs , auto) 
  21.172 -done
  21.173 +by (simp add: qsum_defs , auto) 
  21.174  
  21.175  (** Rules for the Part primitive **)
  21.176  
  21.177 @@ -311,7 +307,7 @@
  21.178  by blast
  21.179  
  21.180  
  21.181 -(*** Monotonicity ***)
  21.182 +subsubsection{*Monotonicity*}
  21.183  
  21.184  lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>"
  21.185  by (simp add: QPair_def sum_mono)
    22.1 --- a/src/ZF/QUniv.thy	Sun Jul 14 15:11:21 2002 +0200
    22.2 +++ b/src/ZF/QUniv.thy	Sun Jul 14 15:14:43 2002 +0200
    22.3 @@ -3,10 +3,9 @@
    22.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.5      Copyright   1993  University of Cambridge
    22.6  
    22.7 -A small universe for lazy recursive types
    22.8  *)
    22.9  
   22.10 -(** Properties involving Transset and Sum **)
   22.11 +header{*A Small Universe for Lazy Recursive Types*}
   22.12  
   22.13  theory QUniv = Univ + QPair + mono + equalities:
   22.14  
   22.15 @@ -27,6 +26,8 @@
   22.16     "quniv(A) == Pow(univ(eclose(A)))"
   22.17  
   22.18  
   22.19 +subsection{*Properties involving Transset and Sum*}
   22.20 +
   22.21  lemma Transset_includes_summands:
   22.22       "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"
   22.23  apply (simp add: sum_def Un_subset_iff) 
   22.24 @@ -39,7 +40,7 @@
   22.25  apply (blast dest: Transset_Pair_D)
   22.26  done
   22.27  
   22.28 -(** Introduction and elimination rules avoid tiresome folding/unfolding **)
   22.29 +subsection{*Introduction and Elimination Rules*}
   22.30  
   22.31  lemma qunivI: "X <= univ(eclose(A)) ==> X : quniv(A)"
   22.32  by (simp add: quniv_def)
   22.33 @@ -52,7 +53,7 @@
   22.34  apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
   22.35  done
   22.36  
   22.37 -(*** Closure properties ***)
   22.38 +subsection{*Closure Properties*}
   22.39  
   22.40  lemma univ_eclose_subset_quniv: "univ(eclose(A)) <= quniv(A)"
   22.41  apply (simp add: quniv_def Transset_iff_Pow [symmetric]) 
   22.42 @@ -90,7 +91,7 @@
   22.43      "[| a <= univ(A);  b <= univ(A) |] ==> <a;b> <= univ(A)"
   22.44  by (simp add: QPair_def sum_subset_univ)
   22.45  
   22.46 -(** Quine disjoint sum **)
   22.47 +subsection{*Quine Disjoint Sum*}
   22.48  
   22.49  lemma QInl_subset_univ: "a <= univ(A) ==> QInl(a) <= univ(A)"
   22.50  apply (unfold QInl_def)
   22.51 @@ -108,7 +109,7 @@
   22.52  apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
   22.53  done
   22.54  
   22.55 -(*** Closure for Quine-inspired products and sums ***)
   22.56 +subsection{*Closure for Quine-Inspired Products and Sums*}
   22.57  
   22.58  (*Quine ordered pairs*)
   22.59  lemma QPair_in_quniv: 
   22.60 @@ -135,7 +136,7 @@
   22.61  by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
   22.62  
   22.63  
   22.64 -(** Quine disjoint sum **)
   22.65 +subsection{*Quine Disjoint Sum*}
   22.66  
   22.67  lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) : quniv(A)"
   22.68  by (simp add: QInl_def zero_in_quniv QPair_in_quniv)
   22.69 @@ -149,7 +150,7 @@
   22.70  lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv]
   22.71  
   22.72  
   22.73 -(*** The natural numbers ***)
   22.74 +subsection{*The Natural Numbers*}
   22.75  
   22.76  lemmas nat_subset_quniv =  subset_trans [OF nat_subset_univ univ_subset_quniv]
   22.77  
   22.78 @@ -161,7 +162,7 @@
   22.79  lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
   22.80  
   22.81  
   22.82 -(*** Intersecting <a;b> with Vfrom... ***)
   22.83 +(*Intersecting <a;b> with Vfrom...*)
   22.84  
   22.85  lemma QPair_Int_Vfrom_succ_subset: 
   22.86   "Transset(X) ==>           
   22.87 @@ -170,7 +171,9 @@
   22.88                product_Int_Vfrom_subset [THEN subset_trans]
   22.89                Sigma_mono [OF Int_lower1 subset_refl])
   22.90  
   22.91 -(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****)
   22.92 +subsection{*"Take-Lemma" Rules*}
   22.93 +
   22.94 +(*for proving a=b by coinduction and c: quniv(A)*)
   22.95  
   22.96  (*Rule for level i -- preserving the level, not decreasing it*)
   22.97  
    23.1 --- a/src/ZF/Sum.thy	Sun Jul 14 15:11:21 2002 +0200
    23.2 +++ b/src/ZF/Sum.thy	Sun Jul 14 15:14:43 2002 +0200
    23.3 @@ -3,12 +3,14 @@
    23.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.5      Copyright   1993  University of Cambridge
    23.6  
    23.7 -Disjoint sums in Zermelo-Fraenkel Set Theory 
    23.8 -"Part" primitive for simultaneous recursive type definitions
    23.9  *)
   23.10  
   23.11 +header{*Disjoint Sums*}
   23.12 +
   23.13  theory Sum = Bool + equalities:
   23.14  
   23.15 +text{*And the "Part" primitive for simultaneous recursive type definitions*}
   23.16 +
   23.17  global
   23.18  
   23.19  constdefs
   23.20 @@ -30,7 +32,7 @@
   23.21  
   23.22  local
   23.23  
   23.24 -(*** Rules for the Part primitive ***)
   23.25 +subsection{*Rules for the @{term Part} Primitive*}
   23.26  
   23.27  lemma Part_iff: 
   23.28      "a : Part(A,h) <-> a:A & (EX y. a=h(y))"
   23.29 @@ -56,7 +58,7 @@
   23.30  done
   23.31  
   23.32  
   23.33 -(*** Rules for Disjoint Sums ***)
   23.34 +subsection{*Rules for Disjoint Sums*}
   23.35  
   23.36  lemmas sum_defs = sum_def Inl_def Inr_def case_def
   23.37  
   23.38 @@ -130,7 +132,7 @@
   23.39  by (simp add: sum_def, blast)
   23.40  
   23.41  
   23.42 -(*** Eliminator -- case ***)
   23.43 +subsection{*The Eliminator: @{term case}*}
   23.44  
   23.45  lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
   23.46  by (simp add: sum_defs)
   23.47 @@ -165,7 +167,7 @@
   23.48  by auto
   23.49  
   23.50  
   23.51 -(*** More rules for Part(A,h) ***)
   23.52 +subsection{*More Rules for @{term "Part(A,h)"}*}
   23.53  
   23.54  lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)"
   23.55  by blast
    24.1 --- a/src/ZF/Trancl.thy	Sun Jul 14 15:11:21 2002 +0200
    24.2 +++ b/src/ZF/Trancl.thy	Sun Jul 14 15:14:43 2002 +0200
    24.3 @@ -1,12 +1,12 @@
    24.4 -(*  Title:      ZF/trancl.thy
    24.5 +(*  Title:      ZF/Trancl.thy
    24.6      ID:         $Id$
    24.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.8      Copyright   1992  University of Cambridge
    24.9  
   24.10 -1. General Properties of relations
   24.11 -2. Transitive closure of a relation
   24.12  *)
   24.13  
   24.14 +header{*Relations: Their General Properties and Transitive Closure*}
   24.15 +
   24.16  theory Trancl = Fixedpt + Perm + mono:
   24.17  
   24.18  constdefs
   24.19 @@ -56,8 +56,7 @@
   24.20  
   24.21  lemma symI:
   24.22       "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
   24.23 -apply (unfold sym_def, blast) 
   24.24 -done
   24.25 +by (unfold sym_def, blast) 
   24.26  
   24.27  lemma antisymI: "[| sym(r); <x,y>: r |]  ==>  <y,x>: r"
   24.28  by (unfold sym_def, blast)
   24.29 @@ -66,8 +65,7 @@
   24.30  
   24.31  lemma antisymI:
   24.32       "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> antisym(r)"
   24.33 -apply (simp add: antisym_def, blast) 
   24.34 -done
   24.35 +by (simp add: antisym_def, blast) 
   24.36  
   24.37  lemma antisymE: "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y"
   24.38  by (simp add: antisym_def, blast)
   24.39 @@ -365,6 +363,12 @@
   24.40  apply (auto simp add: trancl_converse)
   24.41  done
   24.42  
   24.43 +lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl]
   24.44 +  and trancl_induct = trancl_induct [case_names initial step, induct set: trancl]
   24.45 +  and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1]
   24.46 +  and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1]
   24.47 +
   24.48 +
   24.49  ML
   24.50  {*
   24.51  val refl_def = thm "refl_def";
    25.1 --- a/src/ZF/Univ.thy	Sun Jul 14 15:11:21 2002 +0200
    25.2 +++ b/src/ZF/Univ.thy	Sun Jul 14 15:14:43 2002 +0200
    25.3 @@ -3,14 +3,14 @@
    25.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.5      Copyright   1992  University of Cambridge
    25.6  
    25.7 -The cumulative hierarchy and a small universe for recursive types
    25.8 -
    25.9  Standard notation for Vset(i) is V(i), but users might want V for a variable
   25.10  
   25.11  NOTE: univ(A) could be a translation; would simplify many proofs!
   25.12    But Ind_Syntax.univ refers to the constant "Univ.univ"
   25.13  *)
   25.14  
   25.15 +header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
   25.16 +
   25.17  theory Univ = Epsilon + Cardinal:
   25.18  
   25.19  constdefs
   25.20 @@ -35,6 +35,8 @@
   25.21      "univ(A) == Vfrom(A,nat)"
   25.22  
   25.23  
   25.24 +subsection{*Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}*}
   25.25 +
   25.26  text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
   25.27  lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
   25.28  by (subst Vfrom_def [THEN def_transrec], simp)
   25.29 @@ -87,7 +89,7 @@
   25.30  done
   25.31  
   25.32  
   25.33 -subsection{* Basic closure properties *}
   25.34 +subsection{* Basic Closure Properties *}
   25.35  
   25.36  lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
   25.37  by (subst Vfrom, blast)
   25.38 @@ -128,7 +130,7 @@
   25.39  apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
   25.40  done
   25.41  
   25.42 -subsection{* 0, successor and limit equations fof Vfrom *}
   25.43 +subsection{* 0, Successor and Limit Equations for @{term Vfrom} *}
   25.44  
   25.45  lemma Vfrom_0: "Vfrom(A,0) = A"
   25.46  by (subst Vfrom, blast)
   25.47 @@ -169,7 +171,7 @@
   25.48  apply (subst Vfrom, blast)
   25.49  done
   25.50  
   25.51 -subsection{* Vfrom applied to Limit ordinals *}
   25.52 +subsection{* @{term Vfrom} applied to Limit Ordinals *}
   25.53  
   25.54  (*NB. limit ordinals are non-empty:
   25.55        Vfrom(A,0) = A = A Un (\<Union>y\<in>0. Vfrom(A,y)) *)
   25.56 @@ -235,7 +237,7 @@
   25.57  lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n \<in> Vfrom(A,i)"
   25.58  by (blast intro: nat_subset_VLimit [THEN subsetD])
   25.59  
   25.60 -subsubsection{* Closure under disjoint union *}
   25.61 +subsubsection{* Closure under Disjoint Union *}
   25.62  
   25.63  lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   25.64  
   25.65 @@ -261,7 +263,7 @@
   25.66  
   25.67  
   25.68  
   25.69 -subsection{* Properties assuming Transset(A) *}
   25.70 +subsection{* Properties assuming @{term "Transset(A)"} *}
   25.71  
   25.72  lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))"
   25.73  apply (rule_tac a=i in eps_induct)
   25.74 @@ -324,7 +326,7 @@
   25.75  apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
   25.76  done
   25.77  
   25.78 -subsubsection{* products *}
   25.79 +subsubsection{* Products *}
   25.80  
   25.81  lemma prod_in_Vfrom:
   25.82      "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |]
   25.83 @@ -342,7 +344,7 @@
   25.84  apply (blast intro: prod_in_Vfrom Limit_has_succ)
   25.85  done
   25.86  
   25.87 -subsubsection{* Disjoint sums, aka Quine ordered pairs *}
   25.88 +subsubsection{* Disjoint Sums, or Quine Ordered Pairs *}
   25.89  
   25.90  lemma sum_in_Vfrom:
   25.91      "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j |]
   25.92 @@ -361,7 +363,7 @@
   25.93  apply (blast intro: sum_in_Vfrom Limit_has_succ)
   25.94  done
   25.95  
   25.96 -subsubsection{* function space! *}
   25.97 +subsubsection{* Function Space! *}
   25.98  
   25.99  lemma fun_in_Vfrom:
  25.100      "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |] ==>
  25.101 @@ -399,7 +401,7 @@
  25.102  by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
  25.103  
  25.104  
  25.105 -subsection{* The set Vset(i) *}
  25.106 +subsection{* The Set @{term "Vset(i)"} *}
  25.107  
  25.108  lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
  25.109  by (subst Vfrom, blast)
  25.110 @@ -407,7 +409,7 @@
  25.111  lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
  25.112  lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
  25.113  
  25.114 -subsubsection{* Characterisation of the elements of Vset(i) *}
  25.115 +subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *}
  25.116  
  25.117  lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) --> rank(b) < i"
  25.118  apply (erule trans_induct)
  25.119 @@ -454,7 +456,7 @@
  25.120  apply (simp add: Vset_succ) 
  25.121  done
  25.122  
  25.123 -subsubsection{* Reasoning about sets in terms of their elements' ranks *}
  25.124 +subsubsection{* Reasoning about Sets in Terms of Their Elements' Ranks *}
  25.125  
  25.126  lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
  25.127  apply (rule subsetI)
  25.128 @@ -468,7 +470,7 @@
  25.129  apply (blast intro: Ord_rank) 
  25.130  done
  25.131  
  25.132 -subsubsection{* Set up an environment for simplification *}
  25.133 +subsubsection{* Set Up an Environment for Simplification *}
  25.134  
  25.135  lemma rank_Inl: "rank(a) < rank(Inl(a))"
  25.136  apply (unfold Inl_def)
  25.137 @@ -482,7 +484,7 @@
  25.138  
  25.139  lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2
  25.140  
  25.141 -subsubsection{* Recursion over Vset levels! *}
  25.142 +subsubsection{* Recursion over Vset Levels! *}
  25.143  
  25.144  text{*NOT SUITABLE FOR REWRITING: recursive!*}
  25.145  lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
  25.146 @@ -515,7 +517,7 @@
  25.147  done
  25.148  
  25.149  
  25.150 -subsection{* univ(A) *}
  25.151 +subsection{* The Datatype Universe: @{term "univ(A)"} *}
  25.152  
  25.153  lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
  25.154  apply (unfold univ_def)
  25.155 @@ -528,7 +530,7 @@
  25.156  apply (erule Transset_Vfrom)
  25.157  done
  25.158  
  25.159 -subsubsection{* univ(A) as a limit *}
  25.160 +subsubsection{* The Set @{term"univ(A)"} as a Limit *}
  25.161  
  25.162  lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
  25.163  apply (unfold univ_def)
  25.164 @@ -559,7 +561,7 @@
  25.165  apply (blast elim: equalityCE) 
  25.166  done
  25.167  
  25.168 -subsubsection{* Closure properties *}
  25.169 +subsection{* Closure Properties for @{term "univ(A)"}*}
  25.170  
  25.171  lemma zero_in_univ: "0 \<in> univ(A)"
  25.172  apply (unfold univ_def)
  25.173 @@ -576,7 +578,7 @@
  25.174  
  25.175  lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
  25.176  
  25.177 -subsubsection{* Closure under unordered and ordered pairs *}
  25.178 +subsubsection{* Closure under Unordered and Ordered Pairs *}
  25.179  
  25.180  lemma singleton_in_univ: "a: univ(A) ==> {a} \<in> univ(A)"
  25.181  apply (unfold univ_def)
  25.182 @@ -607,7 +609,7 @@
  25.183  done
  25.184  
  25.185  
  25.186 -subsubsection{* The natural numbers *}
  25.187 +subsubsection{* The Natural Numbers *}
  25.188  
  25.189  lemma nat_subset_univ: "nat <= univ(A)"
  25.190  apply (unfold univ_def)
  25.191 @@ -617,7 +619,7 @@
  25.192  text{* n:nat ==> n:univ(A) *}
  25.193  lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
  25.194  
  25.195 -subsubsection{* instances for 1 and 2 *}
  25.196 +subsubsection{* Instances for 1 and 2 *}
  25.197  
  25.198  lemma one_in_univ: "1 \<in> univ(A)"
  25.199  apply (unfold univ_def)
  25.200 @@ -636,7 +638,7 @@
  25.201  lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
  25.202  
  25.203  
  25.204 -subsubsection{* Closure under disjoint union *}
  25.205 +subsubsection{* Closure under Disjoint Union *}
  25.206  
  25.207  lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \<in> univ(A)"
  25.208  apply (unfold univ_def)
  25.209 @@ -669,7 +671,7 @@
  25.210  
  25.211  subsection{* Finite Branching Closure Properties *}
  25.212  
  25.213 -subsubsection{* Closure under finite powerset *}
  25.214 +subsubsection{* Closure under Finite Powerset *}
  25.215  
  25.216  lemma Fin_Vfrom_lemma:
  25.217       "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
  25.218 @@ -693,7 +695,7 @@
  25.219  apply (rule Limit_nat [THEN Fin_VLimit])
  25.220  done
  25.221  
  25.222 -subsubsection{* Closure under finite powers: functions from a natural number *}
  25.223 +subsubsection{* Closure under Finite Powers: Functions from a Natural Number *}
  25.224  
  25.225  lemma nat_fun_VLimit:
  25.226       "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
  25.227 @@ -710,7 +712,7 @@
  25.228  done
  25.229  
  25.230  
  25.231 -subsubsection{* Closure under finite function space *}
  25.232 +subsubsection{* Closure under Finite Function Space *}
  25.233  
  25.234  text{*General but seldom-used version; normally the domain is fixed*}
  25.235  lemma FiniteFun_VLimit1:
  25.236 @@ -749,7 +751,7 @@
  25.237  
  25.238  subsection{** For QUniv.  Properties of Vfrom analogous to the "take-lemma" **}
  25.239  
  25.240 -subsection{* Intersecting a*b with Vfrom... *}
  25.241 +text{* Intersecting a*b with Vfrom... *}
  25.242  
  25.243  text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
  25.244  lemma doubleton_in_Vfrom_D:
    26.1 --- a/src/ZF/WF.thy	Sun Jul 14 15:11:21 2002 +0200
    26.2 +++ b/src/ZF/WF.thy	Sun Jul 14 15:14:43 2002 +0200
    26.3 @@ -3,8 +3,6 @@
    26.4      Author:     Tobias Nipkow and Lawrence C Paulson
    26.5      Copyright   1994  University of Cambridge
    26.6  
    26.7 -Well-founded Recursion
    26.8 -
    26.9  Derived first for transitive relations, and finally for arbitrary WF relations
   26.10  via wf_trancl and trans_trancl.
   26.11  
   26.12 @@ -17,6 +15,8 @@
   26.13  a mess.
   26.14  *)
   26.15  
   26.16 +header{*Well-Founded Recursion*}
   26.17 +
   26.18  theory WF = Trancl + mono + equalities:
   26.19  
   26.20  constdefs
   26.21 @@ -45,7 +45,7 @@
   26.22      "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
   26.23  
   26.24  
   26.25 -(*** Well-founded relations ***)
   26.26 +subsection{*Well-Founded Relations*}
   26.27  
   26.28  (** Equivalences between wf and wf_on **)
   26.29  
   26.30 @@ -153,7 +153,7 @@
   26.31  done
   26.32  
   26.33  
   26.34 -(*** Properties of well-founded relations ***)
   26.35 +subsection{*Basic Properties of Well-Founded Relations*}
   26.36  
   26.37  lemma wf_not_refl: "wf(r) ==> <a,a> ~: r"
   26.38  by (erule_tac a=a in wf_induct, blast)
   26.39 @@ -260,7 +260,7 @@
   26.40  apply (blast dest: transD intro: is_recfun_equal)
   26.41  done
   26.42  
   26.43 -(*** Main Existence Lemma ***)
   26.44 +subsection{*Recursion: Main Existence Lemma*}
   26.45  
   26.46  lemma is_recfun_functional:
   26.47       "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
   26.48 @@ -304,7 +304,7 @@
   26.49  done
   26.50  
   26.51  
   26.52 -(*** Unfolding wftrec ***)
   26.53 +subsection{*Unfolding @{term "wftrec(r,a,H)"}*}
   26.54  
   26.55  lemma the_recfun_cut:
   26.56       "[| wf(r);  trans(r);  <b,a>:r |]
    27.1 --- a/src/ZF/ZF.ML	Sun Jul 14 15:11:21 2002 +0200
    27.2 +++ b/src/ZF/ZF.ML	Sun Jul 14 15:14:43 2002 +0200
    27.3 @@ -504,11 +504,6 @@
    27.4  by (best_tac cantor_cs 1);
    27.5  qed "cantor";
    27.6  
    27.7 -(*Lemma for the inductive definition in theory Zorn*)
    27.8 -Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
    27.9 -by (Blast_tac 1);
   27.10 -qed "Union_in_Pow";
   27.11 -
   27.12  Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
   27.13  by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
   27.14  qed "atomize_ball";
    28.1 --- a/src/ZF/Zorn.thy	Sun Jul 14 15:11:21 2002 +0200
    28.2 +++ b/src/ZF/Zorn.thy	Sun Jul 14 15:14:43 2002 +0200
    28.3 @@ -3,16 +3,15 @@
    28.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    28.5      Copyright   1994  University of Cambridge
    28.6  
    28.7 -Based upon the article
    28.8 -    Abrial & Laffitte, 
    28.9 -    Towards the Mechanization of the Proofs of Some 
   28.10 -    Classical Theorems of Set Theory. 
   28.11 -
   28.12 -Union_in_Pow is proved in ZF.ML
   28.13  *)
   28.14  
   28.15 +header{*Zorn's Lemma*}
   28.16 +
   28.17  theory Zorn = OrderArith + AC + Inductive:
   28.18  
   28.19 +text{*Based upon the unpublished article ``Towards the Mechanization of the
   28.20 +Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*}
   28.21 +
   28.22  constdefs
   28.23    Subset_rel :: "i=>i"
   28.24     "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
   28.25 @@ -31,11 +30,17 @@
   28.26    increasing :: "i=>i"
   28.27      "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
   28.28  
   28.29 -(** We could make the inductive definition conditional on next: increasing(S)
   28.30 +
   28.31 +(*Lemma for the inductive definition below*)
   28.32 +lemma Union_in_Pow: "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
   28.33 +by blast
   28.34 +
   28.35 +
   28.36 +text{*We could make the inductive definition conditional on 
   28.37 +    @{term "next \<in> increasing(S)"}
   28.38      but instead we make this a side-condition of an introduction rule.  Thus
   28.39      the induction rule lets us assume that condition!  Many inductive proofs
   28.40 -    are therefore unconditional.
   28.41 -**)
   28.42 +    are therefore unconditional.*}
   28.43  consts
   28.44    "TFin" :: "[i,i]=>i"
   28.45  
   28.46 @@ -52,16 +57,17 @@
   28.47    type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow
   28.48  
   28.49  
   28.50 -(*** Section 1.  Mathematical Preamble ***)
   28.51 +subsection{*Mathematical Preamble *}
   28.52  
   28.53  lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
   28.54  by blast
   28.55  
   28.56 -lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
   28.57 +lemma Inter_lemma0:
   28.58 +     "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
   28.59  by blast
   28.60  
   28.61  
   28.62 -(*** Section 2.  The Transfinite Construction ***)
   28.63 +subsection{*The Transfinite Construction *}
   28.64  
   28.65  lemma increasingD1: "f: increasing(A) ==> f: Pow(A)->Pow(A)"
   28.66  apply (unfold increasing_def)
   28.67 @@ -83,11 +89,10 @@
   28.68        !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x);  
   28.69        !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y))  
   28.70     |] ==> P(n)"
   28.71 -apply (erule TFin.induct, blast+)
   28.72 -done
   28.73 +by (erule TFin.induct, blast+)
   28.74  
   28.75  
   28.76 -(*** Section 3.  Some Properties of the Transfinite Construction ***)
   28.77 +subsection{*Some Properties of the Transfinite Construction *}
   28.78  
   28.79  lemmas increasing_trans = subset_trans [OF _ increasingD2, 
   28.80                                          OF _ _ TFin_is_subset]
   28.81 @@ -170,8 +175,10 @@
   28.82  done
   28.83  
   28.84  
   28.85 -(*** Section 4.  Hausdorff's Theorem: every set contains a maximal chain ***)
   28.86 -(*** NB: We assume the partial ordering is <=, the subset relation! **)
   28.87 +subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain*}
   28.88 +
   28.89 +text{*NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset
   28.90 +relation!*}
   28.91  
   28.92  (** Defining the "next" operation for Hausdorff's Theorem **)
   28.93  
   28.94 @@ -242,10 +249,11 @@
   28.95              choice_super [THEN super_subset_chain [THEN subsetD]])
   28.96  apply (unfold chain_def)
   28.97  apply (rule CollectI, blast, safe)
   28.98 -apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE], fast+) (*Blast_tac's slow*)
   28.99 +apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+) 
  28.100 +      (*Blast_tac's slow*)
  28.101  done
  28.102  
  28.103 -lemma Hausdorff: "EX c. c : maxchain(S)"
  28.104 +theorem Hausdorff: "EX c. c : maxchain(S)"
  28.105  apply (rule AC_Pi_Pow [THEN exE])
  28.106  apply (rule Hausdorff_next_exists [THEN bexE], assumption)
  28.107  apply (rename_tac ch "next")
  28.108 @@ -266,14 +274,15 @@
  28.109  done
  28.110  
  28.111  
  28.112 -(*** Section 5.  Zorn's Lemma: if all chains in S have upper bounds in S 
  28.113 -                               then S contains a maximal element ***)
  28.114 +subsection{*Zorn's Lemma*}
  28.115 +
  28.116 +text{*If all chains in S have upper bounds in S,
  28.117 +       then S contains a maximal element *}
  28.118  
  28.119  (*Used in the proof of Zorn's Lemma*)
  28.120  lemma chain_extend: 
  28.121      "[| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"
  28.122 -apply (unfold chain_def, blast)
  28.123 -done
  28.124 +by (unfold chain_def, blast)
  28.125  
  28.126  lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"
  28.127  apply (rule Hausdorff [THEN exE])
  28.128 @@ -292,7 +301,7 @@
  28.129  done
  28.130  
  28.131  
  28.132 -(*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
  28.133 +subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*}
  28.134  
  28.135  (*Lemma 5*)
  28.136  lemma TFin_well_lemma5:
  28.137 @@ -393,7 +402,7 @@
  28.138  done
  28.139  
  28.140  (*The wellordering theorem*)
  28.141 -lemma AC_well_ord: "EX r. well_ord(S,r)"
  28.142 +theorem AC_well_ord: "EX r. well_ord(S,r)"
  28.143  apply (rule AC_Pi_Pow [THEN exE])
  28.144  apply (rule Zermelo_next_exists [THEN bexE], assumption)
  28.145  apply (rule exI)
    29.1 --- a/src/ZF/equalities.thy	Sun Jul 14 15:11:21 2002 +0200
    29.2 +++ b/src/ZF/equalities.thy	Sun Jul 14 15:14:43 2002 +0200
    29.3 @@ -3,15 +3,15 @@
    29.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    29.5      Copyright   1992  University of Cambridge
    29.6  
    29.7 -
    29.8 -Basic equations (and inclusions) involving union, intersection, 
    29.9 -converse, domain, range, etc.
   29.10 -
   29.11 -Thanks also to Philippe de Groote.
   29.12  *)
   29.13  
   29.14 +header{*Basic Equalities and Inclusions*}
   29.15 +
   29.16  theory equalities = pair:
   29.17  
   29.18 +text{*These cover union, intersection, converse, domain, range, etc.  Philippe
   29.19 +de Groote proved many of the inclusions.*}
   29.20 +
   29.21  (*FIXME: move to ZF.thy or even to FOL.thy??*)
   29.22  lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
   29.23  by blast
   29.24 @@ -54,10 +54,11 @@
   29.25  lemma the_eq_0 [simp]: "(THE x. False) = 0"
   29.26  by (blast intro: the_0)
   29.27  
   29.28 -text {* \medskip Bounded quantifiers.
   29.29 +subsection{*Bounded Quantifiers*}
   29.30 +text {* \medskip 
   29.31  
   29.32    The following are not added to the default simpset because
   29.33 -  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
   29.34 +  (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
   29.35  
   29.36  lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
   29.37    by blast
   29.38 @@ -71,7 +72,7 @@
   29.39  lemma bex_UN: "(\<exists>z \<in> (UN x:A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
   29.40    by blast
   29.41  
   29.42 -(*** converse ***)
   29.43 +subsection{*Converse of a Relation*}
   29.44  
   29.45  lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>:r"
   29.46  by (unfold converse_def, blast)
   29.47 @@ -105,7 +106,7 @@
   29.48  by blast
   29.49  
   29.50  
   29.51 -(** cons; Finite Sets **)
   29.52 +subsection{*Finite Set Constructions Using @{term cons}*}
   29.53  
   29.54  lemma cons_subsetI: "[| a:C; B<=C |] ==> cons(a,B) <= C"
   29.55  by blast
   29.56 @@ -154,7 +155,7 @@
   29.57  by blast
   29.58  
   29.59  
   29.60 -(*** succ ***)
   29.61 +(** succ **)
   29.62  
   29.63  lemma subset_succI: "i <= succ(i)"
   29.64  by blast
   29.65 @@ -166,14 +167,13 @@
   29.66  
   29.67  lemma succ_subsetE:
   29.68      "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P |] ==> P"
   29.69 -apply (unfold succ_def, blast) 
   29.70 -done
   29.71 +by (unfold succ_def, blast) 
   29.72  
   29.73  lemma succ_subset_iff: "succ(a) <= B <-> (a <= B & a : B)"
   29.74  by (unfold succ_def, blast)
   29.75  
   29.76  
   29.77 -(*** Binary Intersection ***)
   29.78 +subsection{*Binary Intersection*}
   29.79  
   29.80  (** Intersection is the greatest lower bound of two sets **)
   29.81  
   29.82 @@ -225,7 +225,7 @@
   29.83  lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B"
   29.84  by blast
   29.85  
   29.86 -(*** Binary Union ***)
   29.87 +subsection{*Binary Union*}
   29.88  
   29.89  (** Union is the least upper bound of two sets *)
   29.90  
   29.91 @@ -277,7 +277,7 @@
   29.92  lemma Un_eq_Union: "A Un B = Union({A, B})"
   29.93  by blast
   29.94  
   29.95 -(*** Set difference ***)
   29.96 +subsection{*Set Difference*}
   29.97  
   29.98  lemma Diff_subset: "A-B <= A"
   29.99  by blast
  29.100 @@ -354,7 +354,7 @@
  29.101  by (blast elim!: equalityE)
  29.102  
  29.103  
  29.104 -(*** Big Union and Intersection ***)
  29.105 +subsection{*Big Union and Intersection*}
  29.106  
  29.107  (** Big Union is the least upper bound of a set  **)
  29.108  
  29.109 @@ -424,7 +424,7 @@
  29.110       "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"
  29.111  by force
  29.112  
  29.113 -(*** Unions and Intersections of Families ***)
  29.114 +subsection{*Unions and Intersections of Families*}
  29.115  
  29.116  lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"
  29.117  by (blast elim!: equalityE)
  29.118 @@ -739,7 +739,7 @@
  29.119  by blast
  29.120  
  29.121  
  29.122 -(*** Image of a set under a function/relation ***)
  29.123 +subsection{*Image of a Set under a Function or Relation*}
  29.124  
  29.125  lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
  29.126  by (unfold image_def, blast)
  29.127 @@ -784,7 +784,7 @@
  29.128  by blast
  29.129  
  29.130  
  29.131 -(*** Inverse image of a set under a function/relation ***)
  29.132 +subsection{*Inverse Image of a Set under a Function or Relation*}
  29.133  
  29.134  lemma vimage_iff: 
  29.135      "a : r-``B <-> (EX y:B. <a,y>:r)"
  29.136 @@ -868,7 +868,8 @@
  29.137  apply (unfold Inter_def, blast)
  29.138  done
  29.139  
  29.140 -(** Pow **)
  29.141 +
  29.142 +subsection{*Powerset Operator*}
  29.143  
  29.144  lemma Pow_0 [simp]: "Pow(0) = {0}"
  29.145  by blast
  29.146 @@ -897,7 +898,8 @@
  29.147  lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"
  29.148  by blast
  29.149  
  29.150 -(*** RepFun ***)
  29.151 +
  29.152 +subsection{*RepFun*}
  29.153  
  29.154  lemma RepFun_subset: "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B"
  29.155  by blast
  29.156 @@ -910,7 +912,7 @@
  29.157  apply blast
  29.158  done
  29.159  
  29.160 -(*** Collect ***)
  29.161 +subsection{*Collect*}
  29.162  
  29.163  lemma Collect_subset: "Collect(A,P) <= A"
  29.164  by blast
    30.1 --- a/src/ZF/upair.thy	Sun Jul 14 15:11:21 2002 +0200
    30.2 +++ b/src/ZF/upair.thy	Sun Jul 14 15:14:43 2002 +0200
    30.3 @@ -18,6 +18,9 @@
    30.4  setup TypeCheck.setup
    30.5  declare atomize_ball [symmetric, rulify]
    30.6  
    30.7 +(*belongs to theory ZF*)
    30.8 +declare bspec [dest?]
    30.9 +
   30.10  (*** Lemmas about power sets  ***)
   30.11  
   30.12  lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
   30.13 @@ -54,6 +57,9 @@
   30.14  lemma UnI2: "c : B ==> c : A Un B"
   30.15  by simp
   30.16  
   30.17 +(*belongs to theory upair*)
   30.18 +declare UnI1 [elim?]  UnI2 [elim?]
   30.19 +
   30.20  lemma UnE [elim!]: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
   30.21  apply simp 
   30.22  apply blast