1 (* $Id$ *) |
1 (* $Id$ *) |
2 |
2 |
3 theory lam_substs |
3 theory lam_substs |
4 imports "../nominal" |
4 imports "Iteration" |
5 begin |
5 begin |
6 |
6 |
7 text {* Contains all the reasoning infrastructure for the |
|
8 lambda-calculus that the nominal datatype package |
|
9 does not yet provide. *} |
|
10 |
|
11 atom_decl name |
|
12 |
|
13 nominal_datatype lam = Var "name" |
|
14 | App "lam" "lam" |
|
15 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
|
16 |
|
17 types 'a f1_ty = "name\<Rightarrow>('a::pt_name)" |
|
18 'a f2_ty = "'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
|
19 'a f3_ty = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
|
20 |
|
21 lemma f3_freshness_conditions: |
|
22 fixes f3::"('a::pt_name) f3_ty" |
|
23 and y ::"name prm \<Rightarrow> 'a::pt_name" |
|
24 and a ::"name" |
|
25 and pi1::"name prm" |
|
26 and pi2::"name prm" |
|
27 assumes a: "finite ((supp f3)::name set)" |
|
28 and b: "finite ((supp y)::name set)" |
|
29 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
30 shows "\<exists>(a''::name). a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')]))) \<and> |
|
31 a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')]))) a''" |
|
32 proof - |
|
33 from c obtain a' where d0: "a'\<sharp>f3" and d1: "\<forall>(y::'a::pt_name). a'\<sharp>f3 a' y" by force |
|
34 have "\<exists>(a''::name). a''\<sharp>(f3,a,a',pi1,pi2,y)" |
|
35 by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 a b) |
|
36 then obtain a'' where d2: "a''\<sharp>f3" and d3: "a''\<noteq>a'" and d3b: "a''\<sharp>(f3,a,pi1,pi2,y)" |
|
37 by (auto simp add: fresh_prod at_fresh[OF at_name_inst]) |
|
38 have d3c: "a''\<notin>((supp (f3,a,pi1,pi2,y))::name set)" using d3b by (simp add: fresh_def) |
|
39 have d4: "a''\<sharp>f3 a'' (y (pi1@[(a,pi2\<bullet>a'')]))" |
|
40 proof - |
|
41 have d5: "[(a'',a')]\<bullet>f3 = f3" |
|
42 by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF d2, OF d0]) |
|
43 from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))" |
|
44 by (simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
|
45 hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 |
|
46 by (simp add: at_calc[OF at_name_inst] pt_fun_app_eq[OF pt_name_inst, OF at_name_inst]) |
|
47 hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi1@[(a,pi2\<bullet>a'')])))))" by force |
|
48 thus ?thesis by (simp only: pt_pi_rev[OF pt_name_inst, OF at_name_inst]) |
|
49 qed |
|
50 have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')])))" |
|
51 proof - |
|
52 from a b have d7: "finite ((supp (f3,a,pi1,pi2,y))::name set)" by (simp add: supp_prod fs_name1) |
|
53 have e: "((supp (f3,a,pi1,pi2,y))::name set) supports (\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')])))" |
|
54 by (supports_simp add: perm_append) |
|
55 from e d7 d3c show ?thesis by (rule supports_fresh) |
|
56 qed |
|
57 from d6 d4 show ?thesis by force |
|
58 qed |
|
59 |
|
60 lemma f3_freshness_conditions_simple: |
|
61 fixes f3::"('a::pt_name) f3_ty" |
|
62 and y ::"name prm \<Rightarrow> 'a::pt_name" |
|
63 and a ::"name" |
|
64 and pi::"name prm" |
|
65 assumes a: "finite ((supp f3)::name set)" |
|
66 and b: "finite ((supp y)::name set)" |
|
67 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
68 shows "\<exists>(a''::name). a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) \<and> a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) a''" |
|
69 proof - |
|
70 from c obtain a' where d0: "a'\<sharp>f3" and d1: "\<forall>(y::'a::pt_name). a'\<sharp>f3 a' y" by force |
|
71 have "\<exists>(a''::name). a''\<sharp>(f3,a,a',pi,y)" |
|
72 by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 a b) |
|
73 then obtain a'' where d2: "a''\<sharp>f3" and d3: "a''\<noteq>a'" and d3b: "a''\<sharp>(f3,a,pi,y)" |
|
74 by (auto simp add: fresh_prod at_fresh[OF at_name_inst]) |
|
75 have d3c: "a''\<notin>((supp (f3,a,pi,y))::name set)" using d3b by (simp add: fresh_def) |
|
76 have d4: "a''\<sharp>f3 a'' (y (pi@[(a,a'')]))" |
|
77 proof - |
|
78 have d5: "[(a'',a')]\<bullet>f3 = f3" |
|
79 by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF d2, OF d0]) |
|
80 from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))" |
|
81 by (simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
|
82 hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 |
|
83 by (simp add: at_calc[OF at_name_inst] pt_fun_app_eq[OF pt_name_inst, OF at_name_inst]) |
|
84 hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi@[(a,a'')])))))" by force |
|
85 thus ?thesis by (simp only: pt_pi_rev[OF pt_name_inst, OF at_name_inst]) |
|
86 qed |
|
87 have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')])))" |
|
88 proof - |
|
89 from a b have d7: "finite ((supp (f3,a,pi,y))::name set)" by (simp add: supp_prod fs_name1) |
|
90 have "((supp (f3,a,pi,y))::name set) supports (\<lambda>a'. f3 a' (y (pi@[(a,a')])))" |
|
91 by (supports_simp add: perm_append) |
|
92 with d7 d3c show ?thesis by (simp add: supports_fresh) |
|
93 qed |
|
94 from d6 d4 show ?thesis by force |
|
95 qed |
|
96 |
|
97 lemma f3_fresh_fun_supports: |
|
98 fixes f3::"('a::pt_name) f3_ty" |
|
99 and a ::"name" |
|
100 and pi1::"name prm" |
|
101 and y ::"name prm \<Rightarrow> 'a::pt_name" |
|
102 assumes a: "finite ((supp f3)::name set)" |
|
103 and b: "finite ((supp y)::name set)" |
|
104 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
105 shows "((supp (f3,a,y))::name set) supports (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))" |
|
106 proof (auto simp add: "op supports_def" perm_fun_def expand_fun_eq fresh_def[symmetric]) |
|
107 fix b::"name" and c::"name" and pi::"name prm" |
|
108 assume b1: "b\<sharp>(f3,a,y)" |
|
109 and b2: "c\<sharp>(f3,a,y)" |
|
110 from b1 b2 have b3: "[(b,c)]\<bullet>f3=f3" and t4: "[(b,c)]\<bullet>a=a" and t5: "[(b,c)]\<bullet>y=y" |
|
111 by (simp_all add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst] fresh_prod) |
|
112 let ?g = "\<lambda>a'. f3 a' (y (([(b,c)]\<bullet>pi)@[(a,a')]))" |
|
113 and ?h = "\<lambda>a'. f3 a' (y (pi@[(a,a')]))" |
|
114 have a0: "finite ((supp (f3,a,[(b,c)]\<bullet>pi,y))::name set)" using a b |
|
115 by (simp add: supp_prod fs_name1) |
|
116 have a1: "((supp (f3,a,[(b,c)]\<bullet>pi,y))::name set) supports ?g" by (supports_simp add: perm_append) |
|
117 hence a2: "finite ((supp ?g)::name set)" using a0 by (rule supports_finite) |
|
118 have a3: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" |
|
119 by (rule f3_freshness_conditions_simple[OF a, OF b, OF c]) |
|
120 have "((supp (f3,a,y))::name set) \<subseteq> (supp (f3,a,[(b,c)]\<bullet>pi,y))" by (force simp add: supp_prod) |
|
121 have a4: "[(b,c)]\<bullet>?g = ?h" using b1 b2 |
|
122 by (simp add: fresh_prod, perm_simp add: perm_append) |
|
123 have "[(b,c)]\<bullet>(fresh_fun ?g) = fresh_fun ([(b,c)]\<bullet>?g)" |
|
124 by (simp add: fresh_fun_equiv[OF pt_name_inst, OF at_name_inst, OF a2, OF a3]) |
|
125 also have "\<dots> = fresh_fun ?h" using a4 by simp |
|
126 finally show "[(b,c)]\<bullet>(fresh_fun ?g) = fresh_fun ?h" . |
|
127 qed |
|
128 |
|
129 lemma f3_fresh_fun_supp_finite: |
|
130 fixes f3::"('a::pt_name) f3_ty" |
|
131 and a ::"name" |
|
132 and pi1::"name prm" |
|
133 and y ::"name prm \<Rightarrow> 'a::pt_name" |
|
134 assumes a: "finite ((supp f3)::name set)" |
|
135 and b: "finite ((supp y)::name set)" |
|
136 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
137 shows "finite ((supp (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')])))))::name set)" |
|
138 proof - |
|
139 have "((supp (f3,a,y))::name set) supports (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))" |
|
140 using a b c by (rule f3_fresh_fun_supports) |
|
141 moreover |
|
142 have "finite ((supp (f3,a,y))::name set)" using a b by (simp add: supp_prod fs_name1) |
|
143 ultimately show ?thesis by (rule supports_finite) |
|
144 qed |
|
145 |
|
146 types 'a recT = "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam\<times>(name prm \<Rightarrow> ('a::pt_name))) set" |
|
147 |
|
148 consts |
|
149 rec :: "('a::pt_name) recT" |
|
150 |
|
151 inductive "rec f1 f2 f3" |
|
152 intros |
|
153 r1: "(Var a,\<lambda>pi. f1 (pi\<bullet>a))\<in>rec f1 f2 f3" |
|
154 r2: "\<lbrakk>finite ((supp y1)::name set);(t1,y1)\<in>rec f1 f2 f3; |
|
155 finite ((supp y2)::name set);(t2,y2)\<in>rec f1 f2 f3\<rbrakk> |
|
156 \<Longrightarrow> (App t1 t2,\<lambda>pi. f2 (y1 pi) (y2 pi))\<in>rec f1 f2 f3" |
|
157 r3: "\<lbrakk>finite ((supp y)::name set);(t,y)\<in>rec f1 f2 f3\<rbrakk> |
|
158 \<Longrightarrow> (Lam [a].t,\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))\<in>rec f1 f2 f3" |
|
159 |
|
160 constdefs |
|
161 rfun' :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> name prm \<Rightarrow> ('a::pt_name)" |
|
162 "rfun' f1 f2 f3 t \<equiv> (THE y. (t,y)\<in>rec f1 f2 f3)" |
|
163 |
|
164 rfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)" |
|
165 "rfun f1 f2 f3 t \<equiv> rfun' f1 f2 f3 t ([]::name prm)" |
|
166 |
|
167 lemma rec_prm_eq[rule_format]: |
|
168 fixes f1 ::"('a::pt_name) f1_ty" |
|
169 and f2 ::"('a::pt_name) f2_ty" |
|
170 and f3 ::"('a::pt_name) f3_ty" |
|
171 and t ::"lam" |
|
172 and y ::"name prm \<Rightarrow> ('a::pt_name)" |
|
173 shows "(t,y)\<in>rec f1 f2 f3 \<Longrightarrow> (\<forall>(pi1::name prm) (pi2::name prm). pi1 \<triangleq> pi2 \<longrightarrow> (y pi1 = y pi2))" |
|
174 apply(erule rec.induct) |
|
175 apply(auto simp add: pt3[OF pt_name_inst]) |
|
176 apply(rule_tac f="fresh_fun" in arg_cong) |
|
177 apply(auto simp add: expand_fun_eq) |
|
178 apply(drule_tac x="pi1@[(a,x)]" in spec) |
|
179 apply(drule_tac x="pi2@[(a,x)]" in spec) |
|
180 apply(force simp add: prm_eq_def pt2[OF pt_name_inst]) |
|
181 done |
|
182 |
|
183 (* silly helper lemma *) |
|
184 lemma rec_trans: |
|
185 fixes f1 ::"('a::pt_name) f1_ty" |
|
186 and f2 ::"('a::pt_name) f2_ty" |
|
187 and f3 ::"('a::pt_name) f3_ty" |
|
188 and t ::"lam" |
|
189 and y ::"name prm \<Rightarrow> ('a::pt_name)" |
|
190 assumes a: "(t,y)\<in>rec f1 f2 f3" |
|
191 and b: "y=y'" |
|
192 shows "(t,y')\<in>rec f1 f2 f3" |
|
193 using a b by simp |
|
194 |
|
195 lemma rec_prm_equiv: |
|
196 fixes f1 ::"('a::pt_name) f1_ty" |
|
197 and f2 ::"('a::pt_name) f2_ty" |
|
198 and f3 ::"('a::pt_name) f3_ty" |
|
199 and t ::"lam" |
|
200 and y ::"name prm \<Rightarrow> ('a::pt_name)" |
|
201 and pi ::"name prm" |
|
202 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
203 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
204 and a: "(t,y)\<in>rec f1 f2 f3" |
|
205 shows "(pi\<bullet>t,pi\<bullet>y)\<in>rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" |
|
206 using a |
|
207 proof (induct) |
|
208 case (r1 c) |
|
209 let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). f1 (pi'\<bullet>c))" |
|
210 and ?g'="\<lambda>(pi'::name prm). (pi\<bullet>f1) (pi'\<bullet>(pi\<bullet>c))" |
|
211 have "?g'=?g" |
|
212 proof (auto simp only: expand_fun_eq perm_fun_def) |
|
213 fix pi'::"name prm" |
|
214 let ?h = "((rev pi)\<bullet>(pi'\<bullet>(pi\<bullet>c)))" |
|
215 and ?h'= "(((rev pi)\<bullet>pi')\<bullet>c)" |
|
216 have "?h' = ((rev pi)\<bullet>pi')\<bullet>((rev pi)\<bullet>(pi\<bullet>c))" |
|
217 by (simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst]) |
|
218 also have "\<dots> = ?h" |
|
219 by (simp add: pt_perm_compose[OF pt_name_inst, OF at_name_inst,symmetric]) |
|
220 finally show "pi\<bullet>(f1 ?h) = pi\<bullet>(f1 ?h')" by simp |
|
221 qed |
|
222 thus ?case by (force intro: rec_trans rec.r1) |
|
223 next |
|
224 case (r2 t1 t2 y1 y2) |
|
225 assume a1: "finite ((supp y1)::name set)" |
|
226 and a2: "finite ((supp y2)::name set)" |
|
227 and a3: "(pi\<bullet>t1,pi\<bullet>y1) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" |
|
228 and a4: "(pi\<bullet>t2,pi\<bullet>y2) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" |
|
229 from a1 a2 have a1': "finite ((supp (pi\<bullet>y1))::name set)" and a2': "finite ((supp (pi\<bullet>y2))::name set)" |
|
230 by (simp_all add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst]) |
|
231 let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). f2 (y1 pi') (y2 pi'))" |
|
232 and ?g'="\<lambda>(pi'::name prm). (pi\<bullet>f2) ((pi\<bullet>y1) pi') ((pi\<bullet>y2) pi')" |
|
233 have "?g'=?g" by (simp add: expand_fun_eq perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst]) |
|
234 thus ?case using a1' a2' a3 a4 by (force intro: rec.r2 rec_trans) |
|
235 next |
|
236 case (r3 a t y) |
|
237 assume a1: "finite ((supp y)::name set)" |
|
238 and a2: "(pi\<bullet>t,pi\<bullet>y) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" |
|
239 from a1 have a1': "finite ((supp (pi\<bullet>y))::name set)" |
|
240 by (simp add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst]) |
|
241 let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi'@[(a,a')]))))" |
|
242 and ?g'="(\<lambda>(pi'::name prm). fresh_fun (\<lambda>a'. (pi\<bullet>f3) a' ((pi\<bullet>y) (pi'@[((pi\<bullet>a),a')]))))" |
|
243 have "?g'=?g" |
|
244 proof (auto simp add: expand_fun_eq perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst] |
|
245 perm_append) |
|
246 fix pi'::"name prm" |
|
247 let ?h = "\<lambda>a'. pi\<bullet>(f3 ((rev pi)\<bullet>a') (y (((rev pi)\<bullet>pi')@[(a,(rev pi)\<bullet>a')])))" |
|
248 and ?h' = "\<lambda>a'. f3 a' (y (((rev pi)\<bullet>pi')@[(a,a')]))" |
|
249 have fs_f3: "finite ((supp f3)::name set)" using f by (simp add: supp_prod) |
|
250 have fs_h': "finite ((supp ?h')::name set)" |
|
251 proof - |
|
252 have "((supp (f3,a,(rev pi)\<bullet>pi',y))::name set) supports ?h'" |
|
253 by (supports_simp add: perm_append) |
|
254 moreover |
|
255 have "finite ((supp (f3,a,(rev pi)\<bullet>pi',y))::name set)" using a1 fs_f3 |
|
256 by (simp add: supp_prod fs_name1) |
|
257 ultimately show ?thesis by (rule supports_finite) |
|
258 qed |
|
259 have fcond: "\<exists>(a''::name). a''\<sharp>?h' \<and> a''\<sharp>(?h' a'')" |
|
260 by (rule f3_freshness_conditions_simple[OF fs_f3, OF a1, OF c]) |
|
261 have "fresh_fun ?h = fresh_fun (pi\<bullet>?h')" |
|
262 by (simp add: perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst]) |
|
263 also have "\<dots> = pi\<bullet>(fresh_fun ?h')" |
|
264 by (simp add: fresh_fun_equiv[OF pt_name_inst, OF at_name_inst, OF fs_h', OF fcond]) |
|
265 finally show "fresh_fun ?h = pi\<bullet>(fresh_fun ?h')" . |
|
266 qed |
|
267 thus ?case using a1' a2 by (force intro: rec.r3 rec_trans) |
|
268 qed |
|
269 |
|
270 |
|
271 lemma rec_perm: |
|
272 fixes f1 ::"('a::pt_name) f1_ty" |
|
273 and f2 ::"('a::pt_name) f2_ty" |
|
274 and f3 ::"('a::pt_name) f3_ty" |
|
275 and pi1::"name prm" |
|
276 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
277 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
278 and a: "(t,y)\<in>rec f1 f2 f3" |
|
279 shows "(pi1\<bullet>t, \<lambda>pi2. y (pi2@pi1))\<in>rec f1 f2 f3" |
|
280 proof - |
|
281 have lem: "\<forall>(y::name prm\<Rightarrow>('a::pt_name))(pi::name prm). |
|
282 finite ((supp y)::name set) \<longrightarrow> finite ((supp (\<lambda>pi'. y (pi'@pi)))::name set)" |
|
283 proof (intro strip) |
|
284 fix y::"name prm\<Rightarrow>('a::pt_name)" and pi::"name prm" |
|
285 assume "finite ((supp y)::name set)" |
|
286 hence "finite ((supp (y,pi))::name set)" by (simp add: supp_prod fs_name1) |
|
287 moreover |
|
288 have "((supp (y,pi))::name set) supports (\<lambda>pi'. y (pi'@pi))" |
|
289 by (supports_simp add: perm_append) |
|
290 ultimately show "finite ((supp (\<lambda>pi'. y (pi'@pi)))::name set)" by (simp add: supports_finite) |
|
291 qed |
|
292 from a |
|
293 show ?thesis |
|
294 proof (induct) |
|
295 case (r1 c) |
|
296 show ?case |
|
297 by (auto simp add: pt2[OF pt_name_inst], rule rec.r1) |
|
298 next |
|
299 case (r2 t1 t2 y1 y2) |
|
300 thus ?case using lem by (auto intro!: rec.r2) |
|
301 next |
|
302 case (r3 c t y) |
|
303 assume a0: "(t,y)\<in>rec f1 f2 f3" |
|
304 and a1: "finite ((supp y)::name set)" |
|
305 and a2: "(pi1\<bullet>t,\<lambda>pi2. y (pi2@pi1))\<in>rec f1 f2 f3" |
|
306 from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod) |
|
307 show ?case |
|
308 proof(simp) |
|
309 have a3: "finite ((supp (\<lambda>pi2. y (pi2@pi1)))::name set)" using lem a1 by force |
|
310 let ?g' = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' ((\<lambda>pi2. y (pi2@pi1)) (pi@[(pi1\<bullet>c,a')])))" |
|
311 and ?g = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@[(pi1\<bullet>c,a')]@pi1)))" |
|
312 and ?h = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@pi1@[(c,a')])))" |
|
313 have eq1: "?g = ?g'" by simp |
|
314 have eq2: "?g'= ?h" |
|
315 proof (auto simp only: expand_fun_eq) |
|
316 fix pi::"name prm" |
|
317 let ?q = "\<lambda>a'. f3 a' (y ((pi@[(pi1\<bullet>c,a')])@pi1))" |
|
318 and ?q' = "\<lambda>a'. f3 a' (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" |
|
319 and ?r = "\<lambda>a'. f3 a' (y ((pi@pi1)@[(c,a')]))" |
|
320 and ?r' = "\<lambda>a'. f3 a' (y (pi@(pi1@[(c,a')])))" |
|
321 have eq3a: "?r = ?r'" by simp |
|
322 have eq3: "?q = ?q'" |
|
323 proof (auto simp only: expand_fun_eq) |
|
324 fix a'::"name" |
|
325 have "(y ((pi@[(pi1\<bullet>c,a')])@pi1)) = (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" |
|
326 proof - |
|
327 have "((pi@[(pi1\<bullet>c,a')])@pi1) \<triangleq> ((pi@pi1)@[(c,(rev pi1)\<bullet>a')])" |
|
328 by (force simp add: prm_eq_def at_append[OF at_name_inst] |
|
329 at_calc[OF at_name_inst] at_bij[OF at_name_inst] |
|
330 at_pi_rev[OF at_name_inst] at_rev_pi[OF at_name_inst]) |
|
331 with a0 show ?thesis by (rule rec_prm_eq) |
|
332 qed |
|
333 thus "f3 a' (y ((pi@[(pi1\<bullet>c,a')])@pi1)) = f3 a' (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" by simp |
|
334 qed |
|
335 have fs_a: "finite ((supp ?q')::name set)" |
|
336 proof - |
|
337 have "((supp (f3,c,(pi@pi1),(rev pi1),y))::name set) supports ?q'" |
|
338 by (supports_simp add: perm_append fresh_list_append fresh_list_rev) |
|
339 moreover |
|
340 have "finite ((supp (f3,c,(pi@pi1),(rev pi1),y))::name set)" using f' a1 |
|
341 by (simp add: supp_prod fs_name1) |
|
342 ultimately show ?thesis by (rule supports_finite) |
|
343 qed |
|
344 have fs_b: "finite ((supp ?r)::name set)" |
|
345 proof - |
|
346 have "((supp (f3,c,(pi@pi1),y))::name set) supports ?r" |
|
347 by (supports_simp add: perm_append fresh_list_append) |
|
348 moreover |
|
349 have "finite ((supp (f3,c,(pi@pi1),y))::name set)" using f' a1 |
|
350 by (simp add: supp_prod fs_name1) |
|
351 ultimately show ?thesis by (rule supports_finite) |
|
352 qed |
|
353 have c1: "\<exists>(a''::name). a''\<sharp>?q' \<and> a''\<sharp>(?q' a'')" |
|
354 by (rule f3_freshness_conditions[OF f', OF a1, OF c]) |
|
355 have c2: "\<exists>(a''::name). a''\<sharp>?r \<and> a''\<sharp>(?r a'')" |
|
356 by (rule f3_freshness_conditions_simple[OF f', OF a1, OF c]) |
|
357 have c3: "\<exists>(d::name). d\<sharp>(?q',?r,(rev pi1))" |
|
358 by (rule at_exists_fresh[OF at_name_inst], |
|
359 simp only: finite_Un supp_prod fs_a fs_b fs_name1, simp) |
|
360 then obtain d::"name" where d1: "d\<sharp>?q'" and d2: "d\<sharp>?r" and d3: "d\<sharp>(rev pi1)" |
|
361 by (auto simp only: fresh_prod) |
|
362 have eq4: "(rev pi1)\<bullet>d = d" using d3 by (simp add: at_prm_fresh[OF at_name_inst]) |
|
363 have "fresh_fun ?q = fresh_fun ?q'" using eq3 by simp |
|
364 also have "\<dots> = ?q' d" using fs_a c1 d1 |
|
365 by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst]) |
|
366 also have "\<dots> = ?r d" using fs_b c2 d2 eq4 |
|
367 by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst]) |
|
368 also have "\<dots> = fresh_fun ?r" using fs_b c2 d2 |
|
369 by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst]) |
|
370 finally show "fresh_fun ?q = fresh_fun ?r'" by simp |
|
371 qed |
|
372 from a3 a2 have "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t), ?g')\<in>rec f1 f2 f3" by (rule rec.r3) |
|
373 thus "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t), ?h)\<in>rec f1 f2 f3" using eq2 by simp |
|
374 qed |
|
375 qed |
|
376 qed |
|
377 |
|
378 lemma rec_perm_rev: |
|
379 fixes f1::"('a::pt_name) f1_ty" |
|
380 and f2::"('a::pt_name) f2_ty" |
|
381 and f3::"('a::pt_name) f3_ty" |
|
382 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
383 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
384 and a: "(pi\<bullet>t,y)\<in>rec f1 f2 f3" |
|
385 shows "(t, \<lambda>pi2. y (pi2@(rev pi)))\<in>rec f1 f2 f3" |
|
386 proof - |
|
387 from a have "((rev pi)\<bullet>(pi\<bullet>t),\<lambda>pi2. y (pi2@(rev pi)))\<in>rec f1 f2 f3" |
|
388 by (rule rec_perm[OF f, OF c]) |
|
389 thus ?thesis by (simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst]) |
|
390 qed |
|
391 |
|
392 |
|
393 lemma rec_unique: |
|
394 fixes f1::"('a::pt_name) f1_ty" |
|
395 and f2::"('a::pt_name) f2_ty" |
|
396 and f3::"('a::pt_name) f3_ty" |
|
397 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
398 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
399 and a: "(t,y)\<in>rec f1 f2 f3" |
|
400 shows "\<forall>(y'::name prm\<Rightarrow>('a::pt_name))(pi::name prm). |
|
401 (t,y')\<in>rec f1 f2 f3 \<longrightarrow> y pi = y' pi" |
|
402 using a |
|
403 proof (induct) |
|
404 case (r1 c) |
|
405 show ?case |
|
406 apply(auto) |
|
407 apply(ind_cases "(Var c, y') \<in> rec f1 f2 f3") |
|
408 apply(simp_all add: lam.distinct lam.inject) |
|
409 done |
|
410 next |
|
411 case (r2 t1 t2 y1 y2) |
|
412 thus ?case |
|
413 apply(clarify) |
|
414 apply(ind_cases "(App t1 t2, y') \<in> rec f1 f2 f3") |
|
415 apply(simp_all (no_asm_use) only: lam.distinct lam.inject) |
|
416 apply(clarify) |
|
417 apply(drule_tac x="y1" in spec) |
|
418 apply(drule_tac x="y2" in spec) |
|
419 apply(auto) |
|
420 done |
|
421 next |
|
422 case (r3 c t y) |
|
423 assume i1: "finite ((supp y)::name set)" |
|
424 and i2: "(t,y)\<in>rec f1 f2 f3" |
|
425 and i3: "\<forall>(y'::name prm\<Rightarrow>('a::pt_name))(pi::name prm). |
|
426 (t,y')\<in>rec f1 f2 f3 \<longrightarrow> y pi = y' pi" |
|
427 from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod) |
|
428 show ?case |
|
429 proof (auto) |
|
430 fix y'::"name prm\<Rightarrow>('a::pt_name)" and pi::"name prm" |
|
431 assume i4: "(Lam [c].t, y') \<in> rec f1 f2 f3" |
|
432 from i4 show "fresh_fun (\<lambda>a'. f3 a' (y (pi@[(c,a')]))) = y' pi" |
|
433 proof (cases, simp_all add: lam.distinct lam.inject, auto) |
|
434 fix a::"name" and t'::"lam" and y''::"name prm\<Rightarrow>('a::pt_name)" |
|
435 assume i5: "[c].t = [a].t'" |
|
436 and i6: "(t',y'')\<in>rec f1 f2 f3" |
|
437 and i6':"finite ((supp y'')::name set)" |
|
438 let ?g = "\<lambda>a'. f3 a' (y (pi@[(c,a')]))" |
|
439 and ?h = "\<lambda>a'. f3 a' (y'' (pi@[(a,a')]))" |
|
440 show "fresh_fun ?g = fresh_fun ?h" using i5 |
|
441 proof (cases "a=c") |
|
442 case True |
|
443 assume i7: "a=c" |
|
444 with i5 have i8: "t=t'" by (simp add: alpha) |
|
445 show "fresh_fun ?g = fresh_fun ?h" using i3 i6 i7 i8 by simp |
|
446 next |
|
447 case False |
|
448 assume i9: "a\<noteq>c" |
|
449 with i5[symmetric] have i10: "t'=[(a,c)]\<bullet>t" and i11: "a\<sharp>t" by (simp_all add: alpha) |
|
450 have r1: "finite ((supp ?g)::name set)" |
|
451 proof - |
|
452 have "((supp (f3,c,pi,y))::name set) supports ?g" |
|
453 by (supports_simp add: perm_append) |
|
454 moreover |
|
455 have "finite ((supp (f3,c,pi,y))::name set)" using f' i1 |
|
456 by (simp add: supp_prod fs_name1) |
|
457 ultimately show ?thesis by (rule supports_finite) |
|
458 qed |
|
459 have r2: "finite ((supp ?h)::name set)" |
|
460 proof - |
|
461 have "((supp (f3,a,pi,y''))::name set) supports ?h" |
|
462 by (supports_simp add: perm_append) |
|
463 moreover |
|
464 have "finite ((supp (f3,a,pi,y''))::name set)" using f' i6' |
|
465 by (simp add: supp_prod fs_name1) |
|
466 ultimately show ?thesis by (rule supports_finite) |
|
467 qed |
|
468 have c1: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" |
|
469 by (rule f3_freshness_conditions_simple[OF f', OF i1, OF c]) |
|
470 have c2: "\<exists>(a''::name). a''\<sharp>?h \<and> a''\<sharp>(?h a'')" |
|
471 by (rule f3_freshness_conditions_simple[OF f', OF i6', OF c]) |
|
472 have "\<exists>(d::name). d\<sharp>(?g,?h,t,a,c)" |
|
473 by (rule at_exists_fresh[OF at_name_inst], |
|
474 simp only: finite_Un supp_prod r1 r2 fs_name1, simp) |
|
475 then obtain d::"name" |
|
476 where f1: "d\<sharp>?g" and f2: "d\<sharp>?h" and f3: "d\<sharp>t" and f4: "d\<noteq>a" and f5: "d\<noteq>c" |
|
477 by (force simp add: fresh_prod at_fresh[OF at_name_inst] at_fresh[OF at_name_inst]) |
|
478 have g1: "[(a,d)]\<bullet>t = t" |
|
479 by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF i11, OF f3]) |
|
480 from i6 have "(([(a,c)]@[(a,d)])\<bullet>t,y'')\<in>rec f1 f2 f3" using g1 i10 by (simp only: pt_name2) |
|
481 hence "(t, \<lambda>pi2. y'' (pi2@(rev ([(a,c)]@[(a,d)]))))\<in>rec f1 f2 f3" |
|
482 by (simp only: rec_perm_rev[OF f, OF c]) |
|
483 hence g2: "(t, \<lambda>pi2. y'' (pi2@([(a,d)]@[(a,c)])))\<in>rec f1 f2 f3" by simp |
|
484 have "distinct [a,c,d]" using i9 f4 f5 by force |
|
485 hence g3: "(pi@[(c,d)]@[(a,d)]@[(a,c)]) \<triangleq> (pi@[(a,d)])" |
|
486 by (force simp add: prm_eq_def at_calc[OF at_name_inst] at_append[OF at_name_inst]) |
|
487 have "fresh_fun ?g = ?g d" using r1 c1 f1 |
|
488 by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst]) |
|
489 also have "\<dots> = f3 d ((\<lambda>pi2. y'' (pi2@([(a,d)]@[(a,c)]))) (pi@[(c,d)]))" using i3 g2 by simp |
|
490 also have "\<dots> = f3 d (y'' (pi@[(c,d)]@[(a,d)]@[(a,c)]))" by simp |
|
491 also have "\<dots> = f3 d (y'' (pi@[(a,d)]))" using i6 g3 by (simp add: rec_prm_eq) |
|
492 also have "\<dots> = fresh_fun ?h" using r2 c2 f2 |
|
493 by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst]) |
|
494 finally show "fresh_fun ?g = fresh_fun ?h" . |
|
495 qed |
|
496 qed |
|
497 qed |
|
498 qed |
|
499 |
|
500 lemma rec_total_aux: |
|
501 fixes f1::"('a::pt_name) f1_ty" |
|
502 and f2::"('a::pt_name) f2_ty" |
|
503 and f3::"('a::pt_name) f3_ty" |
|
504 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
505 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
506 shows "\<exists>(y::name prm\<Rightarrow>('a::pt_name)). ((t,y)\<in>rec f1 f2 f3) \<and> (finite ((supp y)::name set))" |
|
507 proof (induct t rule: lam.induct_weak) |
|
508 case (Var c) |
|
509 have a1: "(Var c,\<lambda>(pi::name prm). f1 (pi\<bullet>c))\<in>rec f1 f2 f3" by (rule rec.r1) |
|
510 have a2: "finite ((supp (\<lambda>(pi::name prm). f1 (pi\<bullet>c)))::name set)" |
|
511 proof - |
|
512 have "((supp (f1,c))::name set) supports (\<lambda>(pi::name prm). f1 (pi\<bullet>c))" by (supports_simp) |
|
513 moreover have "finite ((supp (f1,c))::name set)" using f by (simp add: supp_prod fs_name1) |
|
514 ultimately show ?thesis by (rule supports_finite) |
|
515 qed |
|
516 from a1 a2 show ?case by force |
|
517 next |
|
518 case (App t1 t2) |
|
519 assume "\<exists>y1. (t1,y1)\<in>rec f1 f2 f3 \<and> finite ((supp y1)::name set)" |
|
520 then obtain y1::"name prm \<Rightarrow> ('a::pt_name)" |
|
521 where a11: "(t1,y1)\<in>rec f1 f2 f3" and a12: "finite ((supp y1)::name set)" by force |
|
522 assume "\<exists>y2. (t2,y2)\<in>rec f1 f2 f3 \<and> finite ((supp y2)::name set)" |
|
523 then obtain y2::"name prm \<Rightarrow> ('a::pt_name)" |
|
524 where a21: "(t2,y2)\<in>rec f1 f2 f3" and a22: "finite ((supp y2)::name set)" by force |
|
525 |
|
526 have a1: "(App t1 t2,\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi))\<in>rec f1 f2 f3" |
|
527 using a12 a11 a22 a21 by (rule rec.r2) |
|
528 have a2: "finite ((supp (\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi)))::name set)" |
|
529 proof - |
|
530 have "((supp (f2,y1,y2))::name set) supports (\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi))" |
|
531 by (supports_simp) |
|
532 moreover have "finite ((supp (f2,y1,y2))::name set)" using f a21 a22 |
|
533 by (simp add: supp_prod fs_name1) |
|
534 ultimately show ?thesis by (rule supports_finite) |
|
535 qed |
|
536 from a1 a2 show ?case by force |
|
537 next |
|
538 case (Lam a t) |
|
539 assume "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)" |
|
540 then obtain y::"name prm \<Rightarrow> ('a::pt_name)" |
|
541 where a11: "(t,y)\<in>rec f1 f2 f3" and a12: "finite ((supp y)::name set)" by force |
|
542 from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod) |
|
543 have a1: "(Lam [a].t,\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))\<in>rec f1 f2 f3" |
|
544 using a12 a11 by (rule rec.r3) |
|
545 have a2: "finite ((supp (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')])))))::name set)" |
|
546 using f' a12 c by (rule f3_fresh_fun_supp_finite) |
|
547 from a1 a2 show ?case by force |
|
548 qed |
|
549 |
|
550 lemma rec_total: |
|
551 fixes f1::"('a::pt_name) f1_ty" |
|
552 and f2::"('a::pt_name) f2_ty" |
|
553 and f3::"('a::pt_name) f3_ty" |
|
554 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
555 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
556 shows "\<exists>(y::name prm\<Rightarrow>('a::pt_name)). ((t,y)\<in>rec f1 f2 f3)" |
|
557 proof - |
|
558 have "\<exists>y. ((t,y)\<in>rec f1 f2 f3) \<and> (finite ((supp y)::name set))" |
|
559 by (rule rec_total_aux[OF f, OF c]) |
|
560 thus ?thesis by force |
|
561 qed |
|
562 |
|
563 lemma rec_function: |
|
564 fixes f1::"('a::pt_name) f1_ty" |
|
565 and f2::"('a::pt_name) f2_ty" |
|
566 and f3::"('a::pt_name) f3_ty" |
|
567 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
568 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
569 shows "\<exists>!y. (t,y)\<in>rec f1 f2 f3" |
|
570 proof (rule ex_ex1I) |
|
571 case goal1 |
|
572 show ?case by (rule rec_total[OF f, OF c]) |
|
573 next |
|
574 case (goal2 y1 y2) |
|
575 assume a1: "(t,y1)\<in>rec f1 f2 f3" and a2: "(t,y2)\<in>rec f1 f2 f3" |
|
576 hence "\<forall>pi. y1 pi = y2 pi" using rec_unique[OF f, OF c] by force |
|
577 thus ?case by (force simp add: expand_fun_eq) |
|
578 qed |
|
579 |
|
580 lemma theI2': |
|
581 assumes a1: "P a" |
|
582 and a2: "\<exists>!x. P x" |
|
583 and a3: "P a \<Longrightarrow> Q a" |
|
584 shows "Q (THE x. P x)" |
|
585 apply(rule theI2) |
|
586 apply(rule a1) |
|
587 apply(subgoal_tac "\<exists>!x. P x") |
|
588 apply(auto intro: a1 simp add: Ex1_def) |
|
589 apply(fold Ex1_def) |
|
590 apply(rule a2) |
|
591 apply(subgoal_tac "x=a") |
|
592 apply(simp) |
|
593 apply(rule a3) |
|
594 apply(assumption) |
|
595 apply(subgoal_tac "\<exists>!x. P x") |
|
596 apply(auto intro: a1 simp add: Ex1_def) |
|
597 apply(fold Ex1_def) |
|
598 apply(rule a2) |
|
599 done |
|
600 |
|
601 lemma rfun'_equiv: |
|
602 fixes f1::"('a::pt_name) f1_ty" |
|
603 and f2::"('a::pt_name) f2_ty" |
|
604 and f3::"('a::pt_name) f3_ty" |
|
605 and pi::"name prm" |
|
606 and t ::"lam" |
|
607 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
608 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
609 shows "pi\<bullet>(rfun' f1 f2 f3 t) = rfun' (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)" |
|
610 apply(auto simp add: rfun'_def) |
|
611 apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)") |
|
612 apply(auto) |
|
613 apply(rule sym) |
|
614 apply(rule_tac a="y" in theI2') |
|
615 apply(assumption) |
|
616 apply(rule rec_function[OF f, OF c]) |
|
617 apply(rule the1_equality) |
|
618 apply(rule rec_function) |
|
619 apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)") |
|
620 apply(simp add: supp_prod) |
|
621 apply(simp add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst]) |
|
622 apply(rule f) |
|
623 apply(subgoal_tac "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)") |
|
624 apply(auto) |
|
625 apply(rule_tac x="pi\<bullet>a" in exI) |
|
626 apply(auto) |
|
627 apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
|
628 apply(drule_tac x="(rev pi)\<bullet>x" in spec) |
|
629 apply(subgoal_tac "(pi\<bullet>f3) (pi\<bullet>a) x = pi\<bullet>(f3 a ((rev pi)\<bullet>x))") |
|
630 apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
|
631 apply(subgoal_tac "pi\<bullet>(f3 a ((rev pi)\<bullet>x)) = (pi\<bullet>f3) (pi\<bullet>a) (pi\<bullet>((rev pi)\<bullet>x))") |
|
632 apply(simp) |
|
633 apply(simp add: pt_pi_rev[OF pt_name_inst, OF at_name_inst]) |
|
634 apply(simp add: pt_fun_app_eq[OF pt_name_inst, OF at_name_inst]) |
|
635 apply(rule c) |
|
636 apply(rule rec_prm_equiv) |
|
637 apply(rule f, rule c, assumption) |
|
638 apply(rule rec_total_aux) |
|
639 apply(rule f) |
|
640 apply(rule c) |
|
641 done |
|
642 |
|
643 lemma rfun'_equiv_aux: |
|
644 fixes pi::"name prm" |
|
645 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
646 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
647 shows "pi\<bullet>(rfun' f1 f2 f3 t pi') = (pi\<bullet>rfun' f1 f2 f3 t) (pi\<bullet>pi')" |
|
648 by (simp add: perm_app) |
|
649 |
|
650 lemma rfun'_supports: |
|
651 fixes f1::"('a::pt_name) f1_ty" |
|
652 and f2::"('a::pt_name) f2_ty" |
|
653 and f3::"('a::pt_name) f3_ty" |
|
654 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
655 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
656 shows "((supp (f1,f2,f3,t))::name set) supports (rfun' f1 f2 f3 t)" |
|
657 proof (auto simp add: "op supports_def" fresh_def[symmetric]) |
|
658 fix a::"name" and b::"name" |
|
659 assume a1: "a\<sharp>(f1,f2,f3,t)" |
|
660 and a2: "b\<sharp>(f1,f2,f3,t)" |
|
661 from a1 a2 have "[(a,b)]\<bullet>f1=f1" and "[(a,b)]\<bullet>f2=f2" and "[(a,b)]\<bullet>f3=f3" and "[(a,b)]\<bullet>t=t" |
|
662 by (simp_all add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst] fresh_prod) |
|
663 thus "[(a,b)]\<bullet>(rfun' f1 f2 f3 t) = rfun' f1 f2 f3 t" |
|
664 by (simp add: rfun'_equiv[OF f, OF c]) |
|
665 qed |
|
666 |
|
667 lemma rfun'_finite_supp: |
|
668 fixes f1::"('a::pt_name) f1_ty" |
|
669 and f2::"('a::pt_name) f2_ty" |
|
670 and f3::"('a::pt_name) f3_ty" |
|
671 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
672 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
673 shows "finite ((supp (rfun' f1 f2 f3 t))::name set)" |
|
674 apply(rule supports_finite) |
|
675 apply(rule rfun'_supports[OF f, OF c]) |
|
676 apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)") |
|
677 apply(simp add: supp_prod fs_name1) |
|
678 apply(rule f) |
|
679 done |
|
680 |
|
681 lemma rfun'_prm: |
|
682 fixes f1::"('a::pt_name) f1_ty" |
|
683 and f2::"('a::pt_name) f2_ty" |
|
684 and f3::"('a::pt_name) f3_ty" |
|
685 and pi1::"name prm" |
|
686 and pi2::"name prm" |
|
687 and t ::"lam" |
|
688 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
689 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
690 shows "rfun' f1 f2 f3 (pi1\<bullet>t) pi2 = rfun' f1 f2 f3 t (pi2@pi1)" |
|
691 apply(auto simp add: rfun'_def) |
|
692 apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)") |
|
693 apply(auto) |
|
694 apply(rule_tac a="y" in theI2') |
|
695 apply(assumption) |
|
696 apply(rule rec_function[OF f, OF c]) |
|
697 apply(rule_tac a="\<lambda>pi2. y (pi2@pi1)" in theI2') |
|
698 apply(rule rec_perm) |
|
699 apply(rule f, rule c) |
|
700 apply(assumption) |
|
701 apply(rule rec_function) |
|
702 apply(rule f) |
|
703 apply(rule c) |
|
704 apply(simp) |
|
705 apply(rule rec_total_aux) |
|
706 apply(rule f) |
|
707 apply(rule c) |
|
708 done |
|
709 |
|
710 lemma rfun_Var: |
|
711 fixes f1::"('a::pt_name) f1_ty" |
|
712 and f2::"('a::pt_name) f2_ty" |
|
713 and f3::"('a::pt_name) f3_ty" |
|
714 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
715 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
716 shows "rfun f1 f2 f3 (Var c) = (f1 c)" |
|
717 apply(auto simp add: rfun_def rfun'_def) |
|
718 apply(subgoal_tac "(THE y. (Var c, y) \<in> rec f1 f2 f3) = (\<lambda>(pi::name prm). f1 (pi\<bullet>c))")(*A*) |
|
719 apply(simp) |
|
720 apply(rule the1_equality) |
|
721 apply(rule rec_function) |
|
722 apply(rule f) |
|
723 apply(rule c) |
|
724 apply(rule rec.r1) |
|
725 done |
|
726 |
|
727 lemma rfun_App: |
|
728 fixes f1::"('a::pt_name) f1_ty" |
|
729 and f2::"('a::pt_name) f2_ty" |
|
730 and f3::"('a::pt_name) f3_ty" |
|
731 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
732 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
733 shows "rfun f1 f2 f3 (App t1 t2) = (f2 (rfun f1 f2 f3 t1) (rfun f1 f2 f3 t2))" |
|
734 apply(auto simp add: rfun_def rfun'_def) |
|
735 apply(subgoal_tac "(THE y. (App t1 t2, y)\<in>rec f1 f2 f3) = |
|
736 (\<lambda>(pi::name prm). f2 ((rfun' f1 f2 f3 t1) pi) ((rfun' f1 f2 f3 t2) pi))")(*A*) |
|
737 apply(simp add: rfun'_def) |
|
738 apply(rule the1_equality) |
|
739 apply(rule rec_function[OF f, OF c]) |
|
740 apply(rule rec.r2) |
|
741 apply(rule rfun'_finite_supp[OF f, OF c]) |
|
742 apply(subgoal_tac "\<exists>y. (t1,y)\<in>rec f1 f2 f3") |
|
743 apply(erule exE, simp add: rfun'_def) |
|
744 apply(rule_tac a="y" in theI2') |
|
745 apply(assumption) |
|
746 apply(rule rec_function[OF f, OF c]) |
|
747 apply(assumption) |
|
748 apply(rule rec_total[OF f, OF c]) |
|
749 apply(rule rfun'_finite_supp[OF f, OF c]) |
|
750 apply(subgoal_tac "\<exists>y. (t2,y)\<in>rec f1 f2 f3") |
|
751 apply(auto simp add: rfun'_def) |
|
752 apply(rule_tac a="y" in theI2') |
|
753 apply(assumption) |
|
754 apply(rule rec_function[OF f, OF c]) |
|
755 apply(assumption) |
|
756 apply(rule rec_total[OF f, OF c]) |
|
757 done |
|
758 |
|
759 lemma rfun_Lam_aux1: |
|
760 fixes f1::"('a::pt_name) f1_ty" |
|
761 and f2::"('a::pt_name) f2_ty" |
|
762 and f3::"('a::pt_name) f3_ty" |
|
763 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
764 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
765 shows "rfun f1 f2 f3 (Lam [a].t) = fresh_fun (\<lambda>a'. f3 a' (rfun' f1 f2 f3 t ([]@[(a,a')])))" |
|
766 apply(simp add: rfun_def rfun'_def) |
|
767 apply(subgoal_tac "(THE y. (Lam [a].t, y)\<in>rec f1 f2 f3) = |
|
768 (\<lambda>(pi::name prm). fresh_fun(\<lambda>a'. f3 a' ((rfun' f1 f2 f3 t) (pi@[(a,a')]))))")(*A*) |
|
769 apply(simp add: rfun'_def[symmetric]) |
|
770 apply(rule the1_equality) |
|
771 apply(rule rec_function[OF f, OF c]) |
|
772 apply(rule rec.r3) |
|
773 apply(rule rfun'_finite_supp[OF f, OF c]) |
|
774 apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3") |
|
775 apply(erule exE, simp add: rfun'_def) |
|
776 apply(rule_tac a="y" in theI2') |
|
777 apply(assumption) |
|
778 apply(rule rec_function[OF f, OF c]) |
|
779 apply(assumption) |
|
780 apply(rule rec_total[OF f, OF c]) |
|
781 done |
|
782 |
|
783 lemma rfun_Lam_aux2: |
|
784 fixes f1::"('a::pt_name) f1_ty" |
|
785 and f2::"('a::pt_name) f2_ty" |
|
786 and f3::"('a::pt_name) f3_ty" |
|
787 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
788 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
789 and a: "b\<sharp>(a,t,f1,f2,f3)" |
|
790 shows "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))" |
|
791 proof - |
|
792 from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod) |
|
793 have eq1: "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = rfun f1 f2 f3 (Lam [a].t)" |
|
794 proof - |
|
795 have "Lam [a].t = Lam [b].([(a,b)]\<bullet>t)" using a |
|
796 by (force simp add: lam.inject alpha fresh_prod at_fresh[OF at_name_inst] |
|
797 pt_swap_bij[OF pt_name_inst, OF at_name_inst] |
|
798 pt_fresh_left[OF pt_name_inst, OF at_name_inst] at_calc[OF at_name_inst]) |
|
799 thus ?thesis by simp |
|
800 qed |
|
801 let ?g = "(\<lambda>a'. f3 a' (rfun' f1 f2 f3 t ([]@[(a,a')])))" |
|
802 have a0: "((supp (f3,a,([]::name prm),rfun' f1 f2 f3 t))::name set) supports ?g" |
|
803 by (supports_simp add: perm_append rfun'_equiv_aux[OF f, OF c]) |
|
804 have a1: "finite ((supp (f3,a,([]::name prm),rfun' f1 f2 f3 t))::name set)" |
|
805 using f' by (simp add: supp_prod fs_name1 rfun'_finite_supp[OF f, OF c]) |
|
806 from a0 a1 have a2: "finite ((supp ?g)::name set)" |
|
807 by (rule supports_finite) |
|
808 have c0: "finite ((supp (rfun' f1 f2 f3 t))::name set)" |
|
809 by (rule rfun'_finite_supp[OF f, OF c]) |
|
810 have c1: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" |
|
811 by (rule f3_freshness_conditions_simple[OF f', OF c0, OF c]) |
|
812 have c2: "b\<sharp>?g" |
|
813 proof - |
|
814 have fs_g: "finite ((supp (f1,f2,f3,t))::name set)" using f |
|
815 by (simp add: supp_prod fs_name1) |
|
816 have "((supp (f1,f2,f3,t))::name set) supports (rfun' f1 f2 f3 t)" |
|
817 by (simp add: rfun'_supports[OF f, OF c]) |
|
818 hence c3: "b\<sharp>(rfun' f1 f2 f3 t)" using fs_g |
|
819 proof(rule supports_fresh, simp add: fresh_def[symmetric]) |
|
820 show "b\<sharp>(f1,f2,f3,t)" using a by (simp add: fresh_prod) |
|
821 qed |
|
822 show ?thesis |
|
823 proof(rule supports_fresh[OF a0, OF a1], simp add: fresh_def[symmetric]) |
|
824 show "b\<sharp>(f3,a,([]::name prm),rfun' f1 f2 f3 t)" using a c3 |
|
825 by (simp add: fresh_prod fresh_list_nil) |
|
826 qed |
|
827 qed |
|
828 (* main proof *) |
|
829 have "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = rfun f1 f2 f3 (Lam [a].t)" by (simp add: eq1) |
|
830 also have "\<dots> = fresh_fun ?g" by (rule rfun_Lam_aux1[OF f, OF c]) |
|
831 also have "\<dots> = ?g b" using c2 |
|
832 by (rule fresh_fun_app[OF pt_name_inst, OF at_name_inst, OF a2, OF c1]) |
|
833 also have "\<dots> = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))" |
|
834 by (simp add: rfun_def rfun'_prm[OF f, OF c]) |
|
835 finally show "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))" . |
|
836 qed |
|
837 |
|
838 |
|
839 lemma rfun_Lam: |
|
840 fixes f1::"('a::pt_name) f1_ty" |
|
841 and f2::"('a::pt_name) f2_ty" |
|
842 and f3::"('a::pt_name) f3_ty" |
|
843 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
844 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
845 and a: "b\<sharp>(f1,f2,f3)" |
|
846 shows "rfun f1 f2 f3 (Lam [b].t) = f3 b (rfun f1 f2 f3 t)" |
|
847 proof - |
|
848 have "\<exists>(a::name). a\<sharp>(b,t)" |
|
849 by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1) |
|
850 then obtain a::"name" where a1: "a\<sharp>b" and a2: "a\<sharp>t" by (force simp add: fresh_prod) |
|
851 have "rfun f1 f2 f3 (Lam [b].t) = rfun f1 f2 f3 (Lam [b].(([(a,b)])\<bullet>([(a,b)]\<bullet>t)))" |
|
852 by (simp add: pt_swap_bij[OF pt_name_inst, OF at_name_inst]) |
|
853 also have "\<dots> = f3 b (rfun f1 f2 f3 (([(a,b)])\<bullet>([(a,b)]\<bullet>t)))" |
|
854 proof(rule rfun_Lam_aux2[OF f, OF c]) |
|
855 have "b\<sharp>([(a,b)]\<bullet>t)" using a1 a2 |
|
856 by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] at_calc[OF at_name_inst] |
|
857 at_fresh[OF at_name_inst]) |
|
858 thus "b\<sharp>(a,[(a,b)]\<bullet>t,f1,f2,f3)" using a a1 by (force simp add: fresh_prod at_fresh[OF at_name_inst]) |
|
859 qed |
|
860 also have "\<dots> = f3 b (rfun f1 f2 f3 t)" by (simp add: pt_swap_bij[OF pt_name_inst, OF at_name_inst]) |
|
861 finally show ?thesis . |
|
862 qed |
|
863 |
|
864 lemma rec_unique: |
|
865 fixes fun::"lam \<Rightarrow> ('a::pt_name)" |
|
866 and f1::"('a::pt_name) f1_ty" |
|
867 and f2::"('a::pt_name) f2_ty" |
|
868 and f3::"('a::pt_name) f3_ty" |
|
869 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
870 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
871 and a1: "\<forall>c. fun (Var c) = f1 c" |
|
872 and a2: "\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)" |
|
873 and a3: "\<forall>a t. a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)" |
|
874 shows "fun t = rfun f1 f2 f3 t" |
|
875 apply (rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fun t = rfun f1 f2 f3 t"]) |
|
876 apply(fold fresh_def) |
|
877 (* finite support *) |
|
878 apply(rule f) |
|
879 (* VAR *) |
|
880 apply(simp add: a1 rfun_Var[OF f, OF c, symmetric]) |
|
881 (* APP *) |
|
882 apply(simp add: a2 rfun_App[OF f, OF c, symmetric]) |
|
883 (* LAM *) |
|
884 apply(simp add: a3 rfun_Lam[OF f, OF c, symmetric]) |
|
885 done |
|
886 |
|
887 lemma rec_function: |
|
888 fixes f1::"('a::pt_name) f1_ty" |
|
889 and f2::"('a::pt_name) f2_ty" |
|
890 and f3::"('a::pt_name) f3_ty" |
|
891 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
892 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
|
893 shows "(\<exists>!(fun::lam \<Rightarrow> ('a::pt_name)). |
|
894 (\<forall>c. fun (Var c) = f1 c) \<and> |
|
895 (\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)) \<and> |
|
896 (\<forall>a t. a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)))" |
|
897 apply(rule_tac a="\<lambda>t. rfun f1 f2 f3 t" in ex1I) |
|
898 (* existence *) |
|
899 apply(simp add: rfun_Var[OF f, OF c]) |
|
900 apply(simp add: rfun_App[OF f, OF c]) |
|
901 apply(simp add: rfun_Lam[OF f, OF c]) |
|
902 (* uniqueness *) |
|
903 apply(auto simp add: expand_fun_eq) |
|
904 apply(rule rec_unique[OF f, OF c]) |
|
905 apply(force)+ |
|
906 done |
|
907 |
|
908 (* "real" recursion *) |
|
909 |
|
910 types 'a f1_ty' = "name\<Rightarrow>('a::pt_name)" |
|
911 'a f2_ty' = "lam\<Rightarrow>lam\<Rightarrow>'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
|
912 'a f3_ty' = "lam\<Rightarrow>name\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
|
913 |
|
914 constdefs |
|
915 rfun_gen' :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> (lam\<times>'a::pt_name)" |
|
916 "rfun_gen' f1 f2 f3 t \<equiv> (rfun |
|
917 (\<lambda>(a::name). (Var a,f1 a)) |
|
918 (\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2))) |
|
919 (\<lambda>(a::name) r. (Lam [a].(fst r),f3 (fst r) a (snd r))) |
|
920 t)" |
|
921 |
|
922 rfun_gen :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> 'a::pt_name" |
|
923 "rfun_gen f1 f2 f3 t \<equiv> snd(rfun_gen' f1 f2 f3 t)" |
|
924 |
|
925 |
|
926 |
|
927 lemma f1'_supports: |
|
928 fixes f1::"('a::pt_name) f1_ty'" |
|
929 shows "((supp f1)::name set) supports (\<lambda>(a::name). (Var a,f1 a))" |
|
930 by (supports_simp) |
|
931 |
|
932 lemma f2'_supports: |
|
933 fixes f2::"('a::pt_name) f2_ty'" |
|
934 shows "((supp f2)::name set) supports |
|
935 (\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2)))" |
|
936 by (supports_simp add: perm_fst perm_snd) |
|
937 |
|
938 lemma f3'_supports: |
|
939 fixes f3::"('a::pt_name) f3_ty'" |
|
940 shows "((supp f3)::name set) supports (\<lambda>(a::name) r. (Lam [a].(fst r),f3 (fst r) a (snd r)))" |
|
941 by (supports_simp add: perm_fst perm_snd) |
|
942 |
|
943 lemma fcb': |
|
944 fixes f3::"('a::pt_name) f3_ty'" |
|
945 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
946 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)" |
|
947 shows "\<exists>a. a \<sharp> (\<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))) \<and> |
|
948 (\<forall>y. a \<sharp> (Lam [a].fst y, f3 (fst y) a (snd y)))" |
|
949 using c f |
|
950 apply(auto) |
|
951 apply(rule_tac x="a" in exI) |
|
952 apply(auto simp add: abs_fresh fresh_prod) |
|
953 apply(rule supports_fresh) |
|
954 apply(rule f3'_supports) |
|
955 apply(simp add: supp_prod) |
|
956 apply(simp add: fresh_def) |
|
957 done |
|
958 |
|
959 lemma fsupp': |
|
960 fixes f1::"('a::pt_name) f1_ty'" |
|
961 and f2::"('a::pt_name) f2_ty'" |
|
962 and f3::"('a::pt_name) f3_ty'" |
|
963 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
964 shows "finite((supp |
|
965 (\<lambda>a. (Var a, f1 a), |
|
966 \<lambda>r1 r2. |
|
967 (App (fst r1) (fst r2), |
|
968 f2 (fst r1) (fst r2) (snd r1) (snd r2)), |
|
969 \<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))))::name set)" |
|
970 using f |
|
971 apply(auto simp add: supp_prod) |
|
972 apply(rule supports_finite) |
|
973 apply(rule f1'_supports) |
|
974 apply(assumption) |
|
975 apply(rule supports_finite) |
|
976 apply(rule f2'_supports) |
|
977 apply(assumption) |
|
978 apply(rule supports_finite) |
|
979 apply(rule f3'_supports) |
|
980 apply(assumption) |
|
981 done |
|
982 |
|
983 lemma rfun_gen'_fst: |
|
984 fixes f1::"('a::pt_name) f1_ty'" |
|
985 and f2::"('a::pt_name) f2_ty'" |
|
986 and f3::"('a::pt_name) f3_ty'" |
|
987 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
988 and c: "(\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y))" |
|
989 shows "fst (rfun_gen' f1 f2 f3 t) = t" |
|
990 apply(rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fst (rfun_gen' f1 f2 f3 t) = t"]) |
|
991 apply(fold fresh_def) |
|
992 apply(simp add: f) |
|
993 apply(unfold rfun_gen'_def) |
|
994 apply(simp only: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
|
995 apply(simp) |
|
996 apply(simp only: rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
|
997 apply(simp) |
|
998 apply(auto) |
|
999 apply(rule trans) |
|
1000 apply(rule_tac f="fst" in arg_cong) |
|
1001 apply(rule rfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
|
1002 apply(auto simp add: fresh_prod) |
|
1003 apply(rule supports_fresh) |
|
1004 apply(rule f1'_supports) |
|
1005 apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)") |
|
1006 apply(simp add: supp_prod) |
|
1007 apply(rule f) |
|
1008 apply(simp add: fresh_def) |
|
1009 apply(rule supports_fresh) |
|
1010 apply(rule f2'_supports) |
|
1011 apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)") |
|
1012 apply(simp add: supp_prod) |
|
1013 apply(rule f) |
|
1014 apply(simp add: fresh_def) |
|
1015 apply(rule supports_fresh) |
|
1016 apply(rule f3'_supports) |
|
1017 apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)") |
|
1018 apply(simp add: supp_prod) |
|
1019 apply(rule f) |
|
1020 apply(simp add: fresh_def) |
|
1021 done |
|
1022 |
|
1023 lemma rfun_gen'_Var: |
|
1024 fixes f1::"('a::pt_name) f1_ty'" |
|
1025 and f2::"('a::pt_name) f2_ty'" |
|
1026 and f3::"('a::pt_name) f3_ty'" |
|
1027 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
1028 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)" |
|
1029 shows "rfun_gen' f1 f2 f3 (Var c) = (Var c, f1 c)" |
|
1030 apply(simp add: rfun_gen'_def) |
|
1031 apply(simp add: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
|
1032 done |
|
1033 |
|
1034 lemma rfun_gen'_App: |
|
1035 fixes f1::"('a::pt_name) f1_ty'" |
|
1036 and f2::"('a::pt_name) f2_ty'" |
|
1037 and f3::"('a::pt_name) f3_ty'" |
|
1038 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
1039 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)" |
|
1040 shows "rfun_gen' f1 f2 f3 (App t1 t2) = |
|
1041 (App t1 t2, f2 t1 t2 (rfun_gen f1 f2 f3 t1) (rfun_gen f1 f2 f3 t2))" |
|
1042 apply(simp add: rfun_gen'_def) |
|
1043 apply(rule trans) |
|
1044 apply(rule rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
|
1045 apply(fold rfun_gen'_def) |
|
1046 apply(simp_all add: rfun_gen'_fst[OF f, OF c]) |
|
1047 apply(simp_all add: rfun_gen_def) |
|
1048 done |
|
1049 |
|
1050 lemma rfun_gen'_Lam: |
|
1051 fixes f1::"('a::pt_name) f1_ty'" |
|
1052 and f2::"('a::pt_name) f2_ty'" |
|
1053 and f3::"('a::pt_name) f3_ty'" |
|
1054 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
1055 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)" |
|
1056 and a: "b\<sharp>(f1,f2,f3)" |
|
1057 shows "rfun_gen' f1 f2 f3 (Lam [b].t) = (Lam [b].t, f3 t b (rfun_gen f1 f2 f3 t))" |
|
1058 using a f |
|
1059 apply(simp add: rfun_gen'_def) |
|
1060 apply(rule trans) |
|
1061 apply(rule rfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
|
1062 apply(auto simp add: fresh_prod) |
|
1063 apply(rule supports_fresh) |
|
1064 apply(rule f1'_supports) |
|
1065 apply(simp add: supp_prod) |
|
1066 apply(simp add: fresh_def) |
|
1067 apply(rule supports_fresh) |
|
1068 apply(rule f2'_supports) |
|
1069 apply(simp add: supp_prod) |
|
1070 apply(simp add: fresh_def) |
|
1071 apply(rule supports_fresh) |
|
1072 apply(rule f3'_supports) |
|
1073 apply(simp add: supp_prod) |
|
1074 apply(simp add: fresh_def) |
|
1075 apply(fold rfun_gen'_def) |
|
1076 apply(simp_all add: rfun_gen'_fst[OF f, OF c]) |
|
1077 apply(simp_all add: rfun_gen_def) |
|
1078 done |
|
1079 |
|
1080 lemma rfun_gen_Var: |
|
1081 fixes f1::"('a::pt_name) f1_ty'" |
|
1082 and f2::"('a::pt_name) f2_ty'" |
|
1083 and f3::"('a::pt_name) f3_ty'" |
|
1084 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
1085 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)" |
|
1086 shows "rfun_gen f1 f2 f3 (Var c) = f1 c" |
|
1087 apply(unfold rfun_gen_def) |
|
1088 apply(simp add: rfun_gen'_Var[OF f, OF c]) |
|
1089 done |
|
1090 |
|
1091 lemma rfun_gen_App: |
|
1092 fixes f1::"('a::pt_name) f1_ty'" |
|
1093 and f2::"('a::pt_name) f2_ty'" |
|
1094 and f3::"('a::pt_name) f3_ty'" |
|
1095 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
1096 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)" |
|
1097 shows "rfun_gen f1 f2 f3 (App t1 t2) = f2 t1 t2 (rfun_gen f1 f2 f3 t1) (rfun_gen f1 f2 f3 t2)" |
|
1098 apply(unfold rfun_gen_def) |
|
1099 apply(simp add: rfun_gen'_App[OF f, OF c]) |
|
1100 apply(simp add: rfun_gen_def) |
|
1101 done |
|
1102 |
|
1103 lemma rfun_gen_Lam: |
|
1104 fixes f1::"('a::pt_name) f1_ty'" |
|
1105 and f2::"('a::pt_name) f2_ty'" |
|
1106 and f3::"('a::pt_name) f3_ty'" |
|
1107 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
|
1108 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)" |
|
1109 and a: "b\<sharp>(f1,f2,f3)" |
|
1110 shows "rfun_gen f1 f2 f3 (Lam [b].t) = f3 t b (rfun_gen f1 f2 f3 t)" |
|
1111 using a |
|
1112 apply(unfold rfun_gen_def) |
|
1113 apply(simp add: rfun_gen'_Lam[OF f, OF c]) |
|
1114 apply(simp add: rfun_gen_def) |
|
1115 done |
|
1116 |
7 |
1117 constdefs |
8 constdefs |
1118 depth_Var :: "name \<Rightarrow> nat" |
9 depth_Var :: "name \<Rightarrow> nat" |
1119 "depth_Var \<equiv> \<lambda>(a::name). 1" |
10 "depth_Var \<equiv> \<lambda>(a::name). 1" |
1120 |
11 |