src/ZF/Constructible/Wellorderings.thy
changeset 13628 87482b5e3f2e
parent 13615 449a70d88b38
child 13634 99a593b49b04
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Fri Oct 04 15:23:58 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Fri Oct 04 15:57:32 2002 +0200
     1.3 @@ -33,13 +33,11 @@
     1.4    wellfounded :: "[i=>o,i]=>o"
     1.5      --{*EVERY non-empty set has an @{text r}-minimal element*}
     1.6      "wellfounded(M,r) == 
     1.7 -	\<forall>x[M]. ~ empty(M,x) 
     1.8 -                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
     1.9 +	\<forall>x[M]. x\<noteq>0 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    1.10    wellfounded_on :: "[i=>o,i,i]=>o"
    1.11      --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
    1.12      "wellfounded_on(M,A,r) == 
    1.13 -	\<forall>x[M]. ~ empty(M,x) --> subset(M,x,A)
    1.14 -                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    1.15 +	\<forall>x[M]. x\<noteq>0 --> x\<subseteq>A --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    1.16  
    1.17    wellordered :: "[i=>o,i,i]=>o"
    1.18      --{*linear and wellfounded on @{text A}*}
    1.19 @@ -124,15 +122,6 @@
    1.20  apply (blast intro: transM)+
    1.21  done
    1.22  
    1.23 -text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
    1.24 -      hypothesis by removing the restriction to @{term A}.*}
    1.25 -lemma (in M_basic) wellfounded_on_induct2: 
    1.26 -     "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  r \<subseteq> A*A;  
    1.27 -       separation(M, \<lambda>x. x\<in>A --> ~P(x));  
    1.28 -       \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
    1.29 -      ==> P(a)";
    1.30 -by (rule wellfounded_on_induct, assumption+, blast)
    1.31 -
    1.32  
    1.33  subsubsection {*Kunen's lemma IV 3.14, page 123*}
    1.34  
    1.35 @@ -297,13 +286,13 @@
    1.36  by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
    1.37  
    1.38  
    1.39 -text{*Surely a shorter proof using lemmas in @{text Order}?
    1.40 -     Like @{text well_ord_iso_preserving}?*}
    1.41 +text{*Can't use @{text well_ord_iso_preserving} because it needs the
    1.42 +strong premise @{term "well_ord(A,r)"}*}
    1.43  lemma (in M_basic) ord_iso_pred_imp_lt:
    1.44       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
    1.45 -       g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
    1.46 -       wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
    1.47 -       Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
    1.48 +         g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
    1.49 +         wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
    1.50 +         Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
    1.51        ==> i < j"
    1.52  apply (frule wellordered_is_trans_on, assumption)
    1.53  apply (frule_tac y=y in transM, assumption) 
    1.54 @@ -351,9 +340,8 @@
    1.55     "obase(M,A,r,z) == 
    1.56  	\<forall>a[M]. 
    1.57           a \<in> z <-> 
    1.58 -          (a\<in>A & (\<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
    1.59 -                   ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    1.60 -                   order_isomorphism(M,par,r,x,mx,g)))"
    1.61 +          (a\<in>A & (\<exists>x[M]. \<exists>g[M]. Ord(x) & 
    1.62 +                   order_isomorphism(M,Order.pred(A,a,r),r,x,Memrel(x),g)))"
    1.63  
    1.64  
    1.65    omap :: "[i=>o,i,i,i] => o"