src/ZF/Constructible/Wellorderings.thy
changeset 13299 3a932abf97e8
parent 13298 b4f370679c65
child 13306 6eebcddee32b
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 16:59:54 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 18:29:50 2002 +0200
     1.3 @@ -13,27 +13,27 @@
     1.4  
     1.5  constdefs
     1.6    irreflexive :: "[i=>o,i,i]=>o"
     1.7 -    "irreflexive(M,A,r) == \<forall>x\<in>A. M(x) --> <x,x> \<notin> r"
     1.8 +    "irreflexive(M,A,r) == \<forall>x[M]. x\<in>A --> <x,x> \<notin> r"
     1.9    
    1.10    transitive_rel :: "[i=>o,i,i]=>o"
    1.11      "transitive_rel(M,A,r) == 
    1.12 -	\<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> (\<forall>z\<in>A. M(z) --> 
    1.13 +	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A --> (\<forall>z[M]. z\<in>A --> 
    1.14                            <x,y>\<in>r --> <y,z>\<in>r --> <x,z>\<in>r))"
    1.15  
    1.16    linear_rel :: "[i=>o,i,i]=>o"
    1.17      "linear_rel(M,A,r) == 
    1.18 -	\<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> <x,y>\<in>r | x=y | <y,x>\<in>r)"
    1.19 +	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A --> <x,y>\<in>r | x=y | <y,x>\<in>r)"
    1.20  
    1.21    wellfounded :: "[i=>o,i]=>o"
    1.22      --{*EVERY non-empty set has an @{text r}-minimal element*}
    1.23      "wellfounded(M,r) == 
    1.24 -	\<forall>x. M(x) --> ~ empty(M,x) 
    1.25 -                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
    1.26 +	\<forall>x[M]. ~ empty(M,x) 
    1.27 +                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    1.28    wellfounded_on :: "[i=>o,i,i]=>o"
    1.29      --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
    1.30      "wellfounded_on(M,A,r) == 
    1.31 -	\<forall>x. M(x) --> ~ empty(M,x) --> subset(M,x,A)
    1.32 -                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
    1.33 +	\<forall>x[M]. ~ empty(M,x) --> subset(M,x,A)
    1.34 +                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    1.35  
    1.36    wellordered :: "[i=>o,i,i]=>o"
    1.37      --{*every non-empty subset of @{text A} has an @{text r}-minimal element*}
    1.38 @@ -82,7 +82,7 @@
    1.39       "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
    1.40  apply (simp add: wellfounded_on_def wellfounded_def, safe)
    1.41   apply blast 
    1.42 -apply (drule_tac x=x in spec, blast) 
    1.43 +apply (drule_tac x=x in rspec, assumption, blast) 
    1.44  done
    1.45  
    1.46  lemma (in M_axioms) wellfounded_on_imp_wellfounded:
    1.47 @@ -104,8 +104,8 @@
    1.48           \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
    1.49        ==> P(a)";
    1.50  apply (simp (no_asm_use) add: wellfounded_def)
    1.51 -apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in spec)
    1.52 -apply (blast dest: transM)
    1.53 +apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in rspec)
    1.54 +apply (blast dest: transM)+
    1.55  done
    1.56  
    1.57  lemma (in M_axioms) wellfounded_on_induct: 
    1.58 @@ -114,8 +114,8 @@
    1.59         \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |]
    1.60        ==> P(a)";
    1.61  apply (simp (no_asm_use) add: wellfounded_on_def)
    1.62 -apply (drule_tac x="{z\<in>A. z\<in>A --> ~P(z)}" in spec)
    1.63 -apply (blast intro: transM) 
    1.64 +apply (drule_tac x="{z\<in>A. z\<in>A --> ~P(z)}" in rspec)
    1.65 +apply (blast intro: transM)+
    1.66  done
    1.67  
    1.68  text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
    1.69 @@ -284,9 +284,8 @@
    1.70  lemma (in M_axioms) wellfounded_on_asym:
    1.71       "[| wellfounded_on(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
    1.72  apply (simp add: wellfounded_on_def) 
    1.73 -apply (drule_tac x="{x,a}" in spec) 
    1.74 -apply (simp add: cons_closed) 
    1.75 -apply (blast dest: transM) 
    1.76 +apply (drule_tac x="{x,a}" in rspec) 
    1.77 +apply (blast dest: transM)+
    1.78  done
    1.79  
    1.80  lemma (in M_axioms) wellordered_asym:
    1.81 @@ -319,12 +318,12 @@
    1.82    --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
    1.83  apply (simp add: pred_iff) 
    1.84  apply (subgoal_tac
    1.85 -       "\<exists>h. M(h) & h \<in> ord_iso(Order.pred(A,y,r), r, 
    1.86 +       "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r, 
    1.87                                 Order.pred(A, converse(f)`j, r), r)")
    1.88   apply (clarify, frule wellordered_iso_pred_eq, assumption+)
    1.89   apply (blast dest: wellordered_asym)  
    1.90 -apply (intro exI conjI) 
    1.91 - prefer 2 apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
    1.92 +apply (intro rexI)
    1.93 + apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
    1.94  done
    1.95  
    1.96  
    1.97 @@ -358,7 +357,7 @@
    1.98     "omap(M,A,r,f) == 
    1.99  	\<forall>z[M].
   1.100           z \<in> f <-> 
   1.101 -          (\<exists>a\<in>A. M(a) & 
   1.102 +          (\<exists>a[M]. a\<in>A & 
   1.103             (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
   1.104                           pair(M,a,x,z) & membership(M,x,mx) & 
   1.105                           pred_set(M,A,a,r,par) &  
   1.106 @@ -366,7 +365,7 @@
   1.107  
   1.108  
   1.109    otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
   1.110 -   "otype(M,A,r,i) == \<exists>f. M(f) & omap(M,A,r,f) & is_range(M,f,i)"
   1.111 +   "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
   1.112  
   1.113  
   1.114  
   1.115 @@ -560,7 +559,8 @@
   1.116  apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) 
   1.117  apply (frule wellordered_is_wellfounded_on, assumption)
   1.118  apply (erule wellfounded_on_induct, assumption+)
   1.119 - apply (insert obase_equals_separation, simp add: Memrel_closed pred_closed, clarify) 
   1.120 + apply (insert obase_equals_separation)
   1.121 + apply (simp add: rex_def, clarify) 
   1.122  apply (rename_tac b) 
   1.123  apply (subgoal_tac "Order.pred(A,b,r) <= B") 
   1.124   prefer 2 apply (force simp add: pred_iff obase_iff)  
   1.125 @@ -593,7 +593,7 @@
   1.126  apply (simp add: omap_def) 
   1.127  apply (insert omap_replacement [of A r])
   1.128  apply (simp add: strong_replacement_def, clarify) 
   1.129 -apply (drule_tac x=x in spec, clarify) 
   1.130 +apply (drule_tac x=x in rspec, clarify) 
   1.131  apply (simp add: Memrel_closed pred_closed obase_iff)
   1.132  apply (erule impE) 
   1.133   apply (clarsimp simp add: univalent_def)
   1.134 @@ -605,17 +605,18 @@
   1.135  declare rall_simps [simp] rex_simps [simp]
   1.136  
   1.137  lemma (in M_axioms) otype_exists:
   1.138 -     "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"
   1.139 +     "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)"
   1.140  apply (insert omap_exists [of A r])  
   1.141  apply (simp add: otype_def, safe)
   1.142 -apply (rule_tac x="range(x)" in exI) 
   1.143 -apply blast 
   1.144 +apply (rule_tac x="range(x)" in rexI) 
   1.145 +apply blast+
   1.146  done
   1.147  
   1.148  theorem (in M_axioms) omap_ord_iso_otype:
   1.149       "[| wellordered(M,A,r); M(A); M(r) |]
   1.150 -      ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   1.151 +      ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   1.152  apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   1.153 +apply (rename_tac i) 
   1.154  apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
   1.155  apply (rule Ord_otype) 
   1.156      apply (force simp add: otype_def range_closed) 
   1.157 @@ -624,8 +625,9 @@
   1.158  
   1.159  lemma (in M_axioms) ordertype_exists:
   1.160       "[| wellordered(M,A,r); M(A); M(r) |]
   1.161 -      ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   1.162 +      ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   1.163  apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   1.164 +apply (rename_tac i) 
   1.165  apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
   1.166  apply (rule Ord_otype) 
   1.167      apply (force simp add: otype_def range_closed)