16 |
16 |
17 subsubsection\<open>Separation for Order-Isomorphisms\<close> |
17 subsubsection\<open>Separation for Order-Isomorphisms\<close> |
18 |
18 |
19 lemma well_ord_iso_Reflects: |
19 lemma well_ord_iso_Reflects: |
20 "REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> |
20 "REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> |
21 (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r), |
21 (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r), |
22 \<lambda>i x. x\<in>A \<longrightarrow> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i). |
22 \<lambda>i x. x\<in>A \<longrightarrow> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i). |
23 fun_apply(##Lset(i),f,x,y) & pair(##Lset(i),y,x,p) & p \<in> r)]" |
23 fun_apply(##Lset(i),f,x,y) \<and> pair(##Lset(i),y,x,p) \<and> p \<in> r)]" |
24 by (intro FOL_reflections function_reflections) |
24 by (intro FOL_reflections function_reflections) |
25 |
25 |
26 lemma well_ord_iso_separation: |
26 lemma well_ord_iso_separation: |
27 "\<lbrakk>L(A); L(f); L(r)\<rbrakk> |
27 "\<lbrakk>L(A); L(f); L(r)\<rbrakk> |
28 \<Longrightarrow> separation (L, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[L]. (\<exists>p[L]. |
28 \<Longrightarrow> separation (L, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[L]. (\<exists>p[L]. |
29 fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))" |
29 fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))" |
30 apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"], |
30 apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"], |
31 auto) |
31 auto) |
32 apply (rule_tac env="[A,f,r]" in DPow_LsetI) |
32 apply (rule_tac env="[A,f,r]" in DPow_LsetI) |
33 apply (rule sep_rules | simp)+ |
33 apply (rule sep_rules | simp)+ |
34 done |
34 done |
36 |
36 |
37 subsubsection\<open>Separation for \<^term>\<open>obase\<close>\<close> |
37 subsubsection\<open>Separation for \<^term>\<open>obase\<close>\<close> |
38 |
38 |
39 lemma obase_reflects: |
39 lemma obase_reflects: |
40 "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
40 "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
41 ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
41 ordinal(L,x) \<and> membership(L,x,mx) \<and> pred_set(L,A,a,r,par) \<and> |
42 order_isomorphism(L,par,r,x,mx,g), |
42 order_isomorphism(L,par,r,x,mx,g), |
43 \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). |
43 \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). |
44 ordinal(##Lset(i),x) & membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) & |
44 ordinal(##Lset(i),x) \<and> membership(##Lset(i),x,mx) \<and> pred_set(##Lset(i),A,a,r,par) \<and> |
45 order_isomorphism(##Lset(i),par,r,x,mx,g)]" |
45 order_isomorphism(##Lset(i),par,r,x,mx,g)]" |
46 by (intro FOL_reflections function_reflections fun_plus_reflections) |
46 by (intro FOL_reflections function_reflections fun_plus_reflections) |
47 |
47 |
48 lemma obase_separation: |
48 lemma obase_separation: |
49 \<comment> \<open>part of the order type formalization\<close> |
49 \<comment> \<open>part of the order type formalization\<close> |
50 "\<lbrakk>L(A); L(r)\<rbrakk> |
50 "\<lbrakk>L(A); L(r)\<rbrakk> |
51 \<Longrightarrow> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
51 \<Longrightarrow> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
52 ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
52 ordinal(L,x) \<and> membership(L,x,mx) \<and> pred_set(L,A,a,r,par) \<and> |
53 order_isomorphism(L,par,r,x,mx,g))" |
53 order_isomorphism(L,par,r,x,mx,g))" |
54 apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto) |
54 apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto) |
55 apply (rule_tac env="[A,r]" in DPow_LsetI) |
55 apply (rule_tac env="[A,r]" in DPow_LsetI) |
56 apply (rule ordinal_iff_sats sep_rules | simp)+ |
56 apply (rule ordinal_iff_sats sep_rules | simp)+ |
57 done |
57 done |
59 |
59 |
60 subsubsection\<open>Separation for a Theorem about \<^term>\<open>obase\<close>\<close> |
60 subsubsection\<open>Separation for a Theorem about \<^term>\<open>obase\<close>\<close> |
61 |
61 |
62 lemma obase_equals_reflects: |
62 lemma obase_equals_reflects: |
63 "REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> \<not>(\<exists>y[L]. \<exists>g[L]. |
63 "REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> \<not>(\<exists>y[L]. \<exists>g[L]. |
64 ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
64 ordinal(L,y) \<and> (\<exists>my[L]. \<exists>pxr[L]. |
65 membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
65 membership(L,y,my) \<and> pred_set(L,A,x,r,pxr) \<and> |
66 order_isomorphism(L,pxr,r,y,my,g))), |
66 order_isomorphism(L,pxr,r,y,my,g))), |
67 \<lambda>i x. x\<in>A \<longrightarrow> \<not>(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i). |
67 \<lambda>i x. x\<in>A \<longrightarrow> \<not>(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i). |
68 ordinal(##Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). |
68 ordinal(##Lset(i),y) \<and> (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). |
69 membership(##Lset(i),y,my) & pred_set(##Lset(i),A,x,r,pxr) & |
69 membership(##Lset(i),y,my) \<and> pred_set(##Lset(i),A,x,r,pxr) \<and> |
70 order_isomorphism(##Lset(i),pxr,r,y,my,g)))]" |
70 order_isomorphism(##Lset(i),pxr,r,y,my,g)))]" |
71 by (intro FOL_reflections function_reflections fun_plus_reflections) |
71 by (intro FOL_reflections function_reflections fun_plus_reflections) |
72 |
72 |
73 lemma obase_equals_separation: |
73 lemma obase_equals_separation: |
74 "\<lbrakk>L(A); L(r)\<rbrakk> |
74 "\<lbrakk>L(A); L(r)\<rbrakk> |
75 \<Longrightarrow> separation (L, \<lambda>x. x\<in>A \<longrightarrow> \<not>(\<exists>y[L]. \<exists>g[L]. |
75 \<Longrightarrow> separation (L, \<lambda>x. x\<in>A \<longrightarrow> \<not>(\<exists>y[L]. \<exists>g[L]. |
76 ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
76 ordinal(L,y) \<and> (\<exists>my[L]. \<exists>pxr[L]. |
77 membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
77 membership(L,y,my) \<and> pred_set(L,A,x,r,pxr) \<and> |
78 order_isomorphism(L,pxr,r,y,my,g))))" |
78 order_isomorphism(L,pxr,r,y,my,g))))" |
79 apply (rule gen_separation_multi [OF obase_equals_reflects, of "{A,r}"], auto) |
79 apply (rule gen_separation_multi [OF obase_equals_reflects, of "{A,r}"], auto) |
80 apply (rule_tac env="[A,r]" in DPow_LsetI) |
80 apply (rule_tac env="[A,r]" in DPow_LsetI) |
81 apply (rule sep_rules | simp)+ |
81 apply (rule sep_rules | simp)+ |
82 done |
82 done |
83 |
83 |
84 |
84 |
85 subsubsection\<open>Replacement for \<^term>\<open>omap\<close>\<close> |
85 subsubsection\<open>Replacement for \<^term>\<open>omap\<close>\<close> |
86 |
86 |
87 lemma omap_reflects: |
87 lemma omap_reflects: |
88 "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
88 "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B \<and> (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
89 ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
89 ordinal(L,x) \<and> pair(L,a,x,z) \<and> membership(L,x,mx) \<and> |
90 pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)), |
90 pred_set(L,A,a,r,par) \<and> order_isomorphism(L,par,r,x,mx,g)), |
91 \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). |
91 \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B \<and> (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). |
92 \<exists>par \<in> Lset(i). |
92 \<exists>par \<in> Lset(i). |
93 ordinal(##Lset(i),x) & pair(##Lset(i),a,x,z) & |
93 ordinal(##Lset(i),x) \<and> pair(##Lset(i),a,x,z) \<and> |
94 membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) & |
94 membership(##Lset(i),x,mx) \<and> pred_set(##Lset(i),A,a,r,par) \<and> |
95 order_isomorphism(##Lset(i),par,r,x,mx,g))]" |
95 order_isomorphism(##Lset(i),par,r,x,mx,g))]" |
96 by (intro FOL_reflections function_reflections fun_plus_reflections) |
96 by (intro FOL_reflections function_reflections fun_plus_reflections) |
97 |
97 |
98 lemma omap_replacement: |
98 lemma omap_replacement: |
99 "\<lbrakk>L(A); L(r)\<rbrakk> |
99 "\<lbrakk>L(A); L(r)\<rbrakk> |
100 \<Longrightarrow> strong_replacement(L, |
100 \<Longrightarrow> strong_replacement(L, |
101 \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
101 \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
102 ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
102 ordinal(L,x) \<and> pair(L,a,x,z) \<and> membership(L,x,mx) \<and> |
103 pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" |
103 pred_set(L,A,a,r,par) \<and> order_isomorphism(L,par,r,x,mx,g))" |
104 apply (rule strong_replacementI) |
104 apply (rule strong_replacementI) |
105 apply (rule_tac u="{A,r,B}" in gen_separation_multi [OF omap_reflects], auto) |
105 apply (rule_tac u="{A,r,B}" in gen_separation_multi [OF omap_reflects], auto) |
106 apply (rule_tac env="[A,B,r]" in DPow_LsetI) |
106 apply (rule_tac env="[A,B,r]" in DPow_LsetI) |
107 apply (rule sep_rules | simp)+ |
107 apply (rule sep_rules | simp)+ |
108 done |
108 done |
151 |
151 |
152 |
152 |
153 subsubsection\<open>Replacement for \<^term>\<open>wfrank\<close>\<close> |
153 subsubsection\<open>Replacement for \<^term>\<open>wfrank\<close>\<close> |
154 |
154 |
155 lemma wfrank_replacement_Reflects: |
155 lemma wfrank_replacement_Reflects: |
156 "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & |
156 "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A \<and> |
157 (\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
157 (\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
158 (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
158 (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) \<and> |
159 M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
159 M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) \<and> |
160 is_range(L,f,y))), |
160 is_range(L,f,y))), |
161 \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & |
161 \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A \<and> |
162 (\<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow> |
162 (\<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow> |
163 (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(##Lset(i),x,y,z) & |
163 (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(##Lset(i),x,y,z) \<and> |
164 M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y), rplus, x, f) & |
164 M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y), rplus, x, f) \<and> |
165 is_range(##Lset(i),f,y)))]" |
165 is_range(##Lset(i),f,y)))]" |
166 by (intro FOL_reflections function_reflections fun_plus_reflections |
166 by (intro FOL_reflections function_reflections fun_plus_reflections |
167 is_recfun_reflection tran_closure_reflection) |
167 is_recfun_reflection tran_closure_reflection) |
168 |
168 |
169 lemma wfrank_strong_replacement: |
169 lemma wfrank_strong_replacement: |
170 "L(r) \<Longrightarrow> |
170 "L(r) \<Longrightarrow> |
171 strong_replacement(L, \<lambda>x z. |
171 strong_replacement(L, \<lambda>x z. |
172 \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
172 \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
173 (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
173 (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) \<and> |
174 M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
174 M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) \<and> |
175 is_range(L,f,y)))" |
175 is_range(L,f,y)))" |
176 apply (rule strong_replacementI) |
176 apply (rule strong_replacementI) |
177 apply (rule_tac u="{r,B}" |
177 apply (rule_tac u="{r,B}" |
178 in gen_separation_multi [OF wfrank_replacement_Reflects], |
178 in gen_separation_multi [OF wfrank_replacement_Reflects], |
179 auto) |
179 auto) |