ea6fb08e096bd9bb708217b1fe72587a1b475759
[darcs-mirror-isa-launchbury.git] / Launchbury / Terms.thy
1 theory Terms
2   imports "Nominal-Utils" Vars  "AList-Utils-Nominal"
3 begin
4
5 subsubsection {* Expressions *}
6
7 text {*
8 This is the main data type of the development; our minimal lambda calculus with recursive let-bindings.
9 It is created using the nominal\_datatype command, which creates alpha-equivalence classes.
10
11 The package does not support nested recursion, so the bindings of the let cannot simply be of type
12 @{text "(var, exp) list"}. Instead, the definition of lists have to be inlined here, as the custom type
13 @{text "assn"}. Later we create conversion functions between these two types, define a properly typed @{text let} 
14 and redo the various lemmas in terms of that, so that afterwards, the type @{text "assn"} is no longer
15 referenced.
16 *}
17
18 nominal_datatype exp =
19   GVar bool var
20 | App exp var
21 | LetA as::assn body::exp binds "bn as" in body as
22 | Lam x::var body::exp binds x in body  ("Lam [_]. _" [100, 100] 100)
23 and assn =
24   ANil | ACons var exp assn
25 binder
26   bn :: "assn \<Rightarrow> atom list"
27 where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"
28
29 abbreviation Var where "Var == GVar False"
30 abbreviation Var1 where "Var1 == GVar True"
31
32 notation (latex output) Terms.Var ("_")
33 notation (latex output) Terms.App ("_ _")
34 notation (latex output) Terms.Lam ("\<lambda>_. _"  [100, 100] 100)
35
36 type_synonym heap = "(var \<times> exp) list"
37
38 lemma exp_assn_size_eqvt[eqvt]: "p \<bullet> (size :: exp \<Rightarrow> nat) = size"
39   by (metis exp_assn.size_eqvt(1) fun_eqvtI permute_pure)
40
41 subsubsection {* Rewriting in terms of heaps *}
42
43 text {*
44 We now work towards using @{type heap} instead of @{type assn}. All this
45 could be skipped if Nominal supported nested recursion.
46 *}
47
48 text {*
49 Conversion from @{typ assn} to @{typ heap}.
50 *}
51
52 nominal_function asToHeap :: "assn \<Rightarrow> heap" 
53  where ANilToHeap: "asToHeap ANil = []"
54  | AConsToHeap: "asToHeap (ACons v e as) = (v, e) # asToHeap as"
55 unfolding eqvt_def asToHeap_graph_aux_def
56 apply rule
57 apply simp
58 apply rule
59 apply(case_tac x rule: exp_assn.exhaust(2))
60 apply auto
61 done
62 nominal_termination(eqvt) by lexicographic_order
63
64 lemma asToHeap_eqvt: "eqvt asToHeap"
65   unfolding eqvt_def
66   by (auto simp add: permute_fun_def asToHeap.eqvt)
67
68 text {* The other direction. *}
69
70 fun heapToAssn :: "heap \<Rightarrow> assn"
71   where "heapToAssn [] = ANil" 
72   | "heapToAssn ((v,e)#\<Gamma>) = ACons v e (heapToAssn \<Gamma>)"
73 declare heapToAssn.simps[simp del]
74
75 lemma heapToAssn_eqvt[simp,eqvt]: "p \<bullet> heapToAssn \<Gamma> =  heapToAssn (p \<bullet> \<Gamma>)"
76   by (induct \<Gamma> rule: heapToAssn.induct)
77      (auto simp add: heapToAssn.simps)
78
79 lemma bn_heapToAssn: "bn (heapToAssn \<Gamma>) = map (\<lambda>x. atom (fst x)) \<Gamma>"
80   by (induct rule: heapToAssn.induct)
81      (auto simp add: heapToAssn.simps exp_assn.bn_defs)
82
83 lemma set_bn_to_atom_domA:
84   "set (bn as) = atom ` domA (asToHeap as)"
85    by (induct as rule: asToHeap.induct)
86       (auto simp add: exp_assn.bn_defs)
87
88 text {*
89 They are inverse to each other.
90 *}
91
92 lemma heapToAssn_asToHeap[simp]:
93   "heapToAssn (asToHeap as) = as"
94   by (induct  rule: exp_assn.inducts(2)[of "\<lambda> _ . True"])
95      (auto simp add: heapToAssn.simps)
96
97 lemma asToHeap_heapToAssn[simp]:
98   "asToHeap (heapToAssn as) = as"
99   by (induct rule: heapToAssn.induct)
100      (auto simp add: heapToAssn.simps)
101
102 lemma heapToAssn_inject[simp]:
103   "heapToAssn x = heapToAssn y \<longleftrightarrow> x = y"
104   by (metis asToHeap_heapToAssn)
105
106 text {*
107 They are transparent to various notions from the Nominal package.
108 *}
109
110 lemma supp_heapToAssn: "supp (heapToAssn \<Gamma>) = supp \<Gamma>"
111   by (induct rule: heapToAssn.induct)
112      (simp_all add: heapToAssn.simps  exp_assn.supp supp_Nil supp_Cons supp_Pair sup_assoc)
113
114 lemma supp_asToHeap: "supp (asToHeap as) = supp as"
115    by (induct as rule: asToHeap.induct)
116       (simp_all add:  exp_assn.supp supp_Nil supp_Cons supp_Pair sup_assoc)
117
118 lemma fv_asToHeap: "fv (asToHeap \<Gamma>) = fv \<Gamma>"
119   unfolding fv_def by (auto simp add: supp_asToHeap)
120
121 lemma fv_heapToAssn: "fv (heapToAssn \<Gamma>) = fv \<Gamma>"
122   unfolding fv_def by (auto simp add: supp_heapToAssn)
123
124 lemma [simp]: "size (heapToAssn \<Gamma>) = size_list (\<lambda> (v,e) . size e) \<Gamma>"
125   by (induct rule: heapToAssn.induct)
126      (simp_all add: heapToAssn.simps)
127
128 lemma Lam_eq_same_var[simp]: "Lam [y]. e = Lam [y]. e' \<longleftrightarrow>  e = e'"
129   by auto (metis fresh_PairD(2) obtain_fresh)
130
131 text {* Now we define the Let constructor in the form that we actually want. *}
132
133 hide_const HOL.Let
134 definition Let :: "heap \<Rightarrow> exp \<Rightarrow> exp"
135   where "Let \<Gamma> e = LetA (heapToAssn \<Gamma>) e"
136
137 notation (latex output) Let ("\<^raw:\textrm{\textsf{let}}> _ \<^raw:\textrm{\textsf{in}}> _")
138
139 abbreviation
140   LetBe :: "var\<Rightarrow>exp\<Rightarrow>exp\<Rightarrow>exp" ("let _ be _ in _ " [100,100,100] 100)
141 where
142   "let x be t1 in t2 \<equiv> Let [(x,t1)] t2"
143
144 text {*
145 We rewrite all (relevant) lemmas about @{term LetA} in terms of @{term Let}.
146 *}
147
148 lemma size_Let[simp]: "size (Let \<Gamma> e) = size_list (\<lambda>p. size (snd p)) \<Gamma> + size e + Suc 0"
149   unfolding Let_def by (auto simp add: split_beta')
150
151 lemma Let_distinct[simp]:
152   "GVar s v \<noteq> Let \<Gamma> e"
153   "Let \<Gamma> e \<noteq> GVar s v"
154   "App e v \<noteq> Let \<Gamma> e'"
155   "Lam [v]. e' \<noteq> Let \<Gamma> e"
156   "Let \<Gamma> e \<noteq> Lam [v]. e'"
157   "Let \<Gamma> e' \<noteq> App e v"
158   unfolding Let_def by simp_all
159
160 lemma Let_perm_simps[simp,eqvt]:
161   "p \<bullet> Let \<Gamma> e = Let (p \<bullet> \<Gamma>) (p \<bullet> e)"
162   unfolding Let_def by simp
163
164 lemma Let_supp:
165   "supp (Let \<Gamma> e) = (supp e \<union> supp \<Gamma>) - atom ` (domA \<Gamma>)"
166   unfolding Let_def by (simp add: exp_assn.supp supp_heapToAssn bn_heapToAssn domA_def image_image)
167
168 lemma Let_fresh[simp]:
169   "a \<sharp> Let \<Gamma> e = (a \<sharp> e \<and> a \<sharp> \<Gamma> \<or> a \<in> atom ` domA \<Gamma>)"
170   unfolding fresh_def by (auto simp add: Let_supp)
171
172 lemma Abs_eq_cong:
173   assumes "\<And> p. (p \<bullet> x = x') \<longleftrightarrow> (p \<bullet> y = y')"
174   assumes "supp y = supp x"
175   assumes "supp y' = supp x'"
176   shows "([a]lst. x = [a']lst. x') \<longleftrightarrow> ([a]lst. y = [a']lst. y')"
177   by (simp add: Abs_eq_iff alpha_lst assms)
178
179 lemma Let_eq_iff[simp]:
180   "(Let \<Gamma> e = Let \<Gamma>' e') = ([map (\<lambda>x. atom (fst x)) \<Gamma> ]lst. (e, \<Gamma>) = [map (\<lambda>x. atom (fst x)) \<Gamma>']lst. (e',\<Gamma>'))"
181   unfolding Let_def 
182   apply (simp add: bn_heapToAssn)
183   apply (rule Abs_eq_cong)
184   apply (simp_all add: supp_Pair supp_heapToAssn)
185   done
186
187 lemma exp_strong_exhaust:
188   fixes c :: "'a :: fs"
189   assumes "(\<And>bool var. y = GVar bool var \<Longrightarrow> P)"
190   assumes "\<And>exp var. y = App exp var \<Longrightarrow> P"
191   assumes "\<And>\<Gamma> exp. atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> y = Let \<Gamma> exp \<Longrightarrow> P"
192   assumes "\<And>var exp. {atom var} \<sharp>* c \<Longrightarrow> y = Lam [var]. exp \<Longrightarrow> P"
193   shows P
194   apply (rule  exp_assn.strong_exhaust(1)[where y = y and c = c])
195   apply (metis assms(1))
196   apply (metis assms(2))
197   apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap)
198   apply (metis assms(4))
199   done
200
201 text {*
202 And finally the induction rules with @{term Let}.
203 *}
204
205 lemma exp_heap_induct[case_names Var App Let Lam Nil Cons]:
206   assumes "\<And>b var. P1 (GVar b var)"
207   assumes "\<And>exp var. P1 exp \<Longrightarrow> P1 (App exp var)"
208   assumes "\<And>\<Gamma> exp. P2 \<Gamma> \<Longrightarrow> P1 exp \<Longrightarrow> P1 (Let \<Gamma> exp)"
209   assumes "\<And>var exp. P1 exp \<Longrightarrow> P1 (Lam [var]. exp)"
210   assumes "P2 []"
211   assumes "\<And>var exp \<Gamma>. P1 exp \<Longrightarrow> P2 \<Gamma> \<Longrightarrow> P2 ((var, exp)#\<Gamma>)"
212   shows "P1 e" and "P2 \<Gamma>"
213 proof-
214   have "P1 e" and "P2 (asToHeap (heapToAssn \<Gamma>))"
215     apply (induct rule: exp_assn.inducts[of P1 "\<lambda> assn. P2 (asToHeap assn)"])
216     apply (metis assms(1))
217     apply (metis assms(2))
218     apply (metis assms(3) Let_def heapToAssn_asToHeap )
219     apply (metis assms(4))
220     apply (metis assms(5) asToHeap.simps(1))
221     apply (metis assms(6) asToHeap.simps(2))
222     done
223   thus "P1 e" and "P2 \<Gamma>" unfolding asToHeap_heapToAssn.
224 qed
225
226 lemma exp_heap_strong_induct[case_names Var App Let Lam Nil Cons]:
227   assumes "\<And>b var c. P1 c (GVar b var)"
228   assumes "\<And>exp var c. (\<And>c. P1 c exp) \<Longrightarrow> P1 c (App exp var)"
229   assumes "\<And>\<Gamma> exp c. atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> (\<And>c. P2 c \<Gamma>) \<Longrightarrow> (\<And>c. P1 c exp) \<Longrightarrow> P1 c (Let \<Gamma> exp)"
230   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P1 c exp) \<Longrightarrow> P1 c (Lam [var]. exp)"
231   assumes "\<And>c. P2 c []"
232   assumes "\<And>var exp \<Gamma> c. (\<And>c. P1 c exp) \<Longrightarrow> (\<And>c. P2 c \<Gamma>) \<Longrightarrow> P2 c ((var,exp)#\<Gamma>)"
233   fixes c :: "'a :: fs"
234   shows "P1 c e" and "P2 c \<Gamma>"
235 proof-
236   have "P1 c e" and "P2 c (asToHeap (heapToAssn \<Gamma>))"
237     apply (induct rule: exp_assn.strong_induct[of P1 "\<lambda> c assn. P2 c (asToHeap assn)"])
238     apply (metis assms(1))
239     apply (metis assms(2))
240     apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap )
241     apply (metis assms(4))
242     apply (metis assms(5) asToHeap.simps(1))
243     apply (metis assms(6) asToHeap.simps(2))
244     done
245   thus "P1 c e" and "P2 c \<Gamma>" unfolding asToHeap_heapToAssn.
246 qed
247
248 subsubsection {* Nice induction rules *}
249
250 text {*
251 These rules can be used instead of the original induction rules, which require a separate
252 goal for @{typ assn}.
253 *}
254
255 lemma exp_induct[case_names Var App Let Lam]:
256   assumes "\<And>b var. P (GVar b var)"
257   assumes "\<And>exp var. P exp \<Longrightarrow> P (App exp var)"
258   assumes "\<And>\<Gamma> exp. (\<And> x. x \<in> domA \<Gamma> \<Longrightarrow>  P (the (map_of \<Gamma> x))) \<Longrightarrow> P exp \<Longrightarrow> P (Let \<Gamma> exp)"
259   assumes "\<And>var exp.  P exp \<Longrightarrow> P (Lam [var]. exp)"
260   shows "P  exp"
261   apply (rule exp_heap_induct[of P "\<lambda> \<Gamma>. (\<forall>x \<in> domA \<Gamma>. P (the (map_of \<Gamma> x)))"])
262   apply (metis assms(1))
263   apply (metis assms(2))
264   apply (metis assms(3))
265   apply (metis assms(4))
266   apply auto
267   done
268
269 lemma  exp_strong_induct_set[case_names Var App Let Lam]:
270   assumes "\<And>b var c. P c (GVar b var)"
271   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
272   assumes "\<And>\<Gamma> exp c.
273     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> (\<And>c x e. (x,e) \<in> set \<Gamma> \<Longrightarrow>  P c e) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
274   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
275   shows "P (c::'a::fs) exp"
276   apply (rule exp_heap_strong_induct(1)[of P "\<lambda> c \<Gamma>. (\<forall>(x,e) \<in> set \<Gamma>. P c e)"])
277   apply (metis assms(1))
278   apply (metis assms(2))
279   apply (metis assms(3) split_conv)
280   apply (metis assms(4))
281   apply auto
282   done
283
284
285 lemma  exp_strong_induct[case_names Var App Let Lam]:
286   assumes "\<And>b var c. P c (GVar b var)"
287   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
288   assumes "\<And>\<Gamma> exp c.
289     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> (\<And>c x. x \<in> domA \<Gamma> \<Longrightarrow>  P c (the (map_of \<Gamma> x))) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
290   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
291   shows "P (c::'a::fs) exp"
292   apply (rule exp_heap_strong_induct(1)[of P "\<lambda> c \<Gamma>. (\<forall>x \<in> domA \<Gamma>. P c (the (map_of \<Gamma> x)))"])
293   apply (metis assms(1))
294   apply (metis assms(2))
295   apply (metis assms(3))
296   apply (metis assms(4))
297   apply auto
298   done
299
300 subsubsection {* Testing alpha equivalence *}
301               
302 lemma alpha_test:
303   shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
304   by (simp add: Abs1_eq_iff fresh_at_base pure_fresh)
305
306 lemma alpha_test2:
307   shows "let x be (Var x) in (Var x) = let y be (Var y) in (Var y)"
308   by (simp add: fresh_Cons fresh_Nil Abs1_eq_iff fresh_Pair add: fresh_at_base pure_fresh)
309
310 lemma alpha_test3:
311   shows "
312     Let [(x, Var y), (y, Var x)] (Var x)
313     =
314     Let [(y, Var x), (x, Var y)] (Var y)" (is "Let ?la ?lb = _")
315   by (simp add: bn_heapToAssn Abs1_eq_iff fresh_Pair fresh_at_base
316                 Abs_swap2[of "atom x" "(?lb, [(x, Var y), (y, Var x)])" "[atom x, atom y]" "atom y"])
317
318 subsubsection {* Free variables *}
319
320 lemma fv_supp_exp: "supp e = atom ` (fv (e::exp) :: var set)" and fv_supp_as: "supp as = atom ` (fv (as::assn) :: var set)"
321   by (induction e and as rule:exp_assn.inducts)
322      (auto simp add: fv_def exp_assn.supp supp_at_base pure_supp)
323
324 lemma fv_supp_heap: "supp (\<Gamma>::heap) = atom ` (fv \<Gamma> :: var set)"
325   by (metis fv_def fv_supp_as supp_heapToAssn)
326
327 lemma fv_Lam[simp]: "fv (Lam [x]. e) = fv e - {x}"
328   unfolding fv_def by (auto simp add: exp_assn.supp)
329 lemma fv_Var[simp]: "fv (GVar b x) = {x}"
330   unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base pure_supp)
331 lemma fv_App[simp]: "fv (App e x) = insert x (fv e)"
332   unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base)
333 lemma fv_Let[simp]: "fv (Let \<Gamma> e) = (fv \<Gamma> \<union> fv e) - domA \<Gamma>"
334   unfolding fv_def by (auto simp add: Let_supp exp_assn.supp supp_at_base set_bn_to_atom_domA)
335
336 lemma finite_fv_exp[simp]: "finite (fv (e::exp) :: var set)"
337   and finite_fv_heap[simp]: "finite (fv (\<Gamma> :: heap) :: var set)"
338   by (induction e rule:exp_heap_induct) auto
339
340
341 lemma fv_delete_heap:
342   assumes "map_of \<Gamma> x = Some e"
343   shows "fv (delete x \<Gamma>, e) \<union> {x} \<subseteq> (fv (\<Gamma>, Var x) :: var set)"
344 proof-
345   have "fv (delete x \<Gamma>) \<subseteq> fv \<Gamma>" by (metis fv_delete_subset)
346   moreover
347   have "(x,e) \<in> set \<Gamma>" by (metis assms map_of_is_SomeD)
348   hence "fv e \<subseteq> fv \<Gamma>" by (metis assms domA_from_set map_of_fv_subset option.sel)
349   moreover
350   have "x \<in> fv (Var x)" by simp
351   ultimately show ?thesis by auto
352 qed
353
354 subsubsection {* Lemmas helping with nominal definitions *}
355
356 lemma eqvt_lam_case:
357   assumes "Lam [x]. e = Lam [x']. e'"
358   assumes "\<And> \<pi> . supp (-\<pi>) \<sharp>* (fv (Lam [x]. e) :: var set) \<Longrightarrow>
359                  supp \<pi> \<sharp>* (Lam [x]. e) \<Longrightarrow>
360         F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (Lam [x]. e) = F e x (Lam [x]. e)"
361   shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
362 proof-
363
364   from assms(1)
365   have "[[atom x]]lst. (e, x) = [[atom x']]lst. (e', x')" by auto
366   then obtain p
367     where "(supp (e, x) - {atom x}) \<sharp>* p"
368     and [simp]: "p \<bullet> x = x'"
369     and [simp]: "p \<bullet> e = e'"
370     unfolding  Abs_eq_iff(3) alpha_lst.simps by auto
371
372   from `_ \<sharp>* p`
373   have *: "supp (-p) \<sharp>* (fv (Lam [x]. e) :: var set)"
374     by (auto simp add: fresh_star_def fresh_def supp_finite_set_at_base supp_Pair fv_supp_exp fv_supp_heap supp_minus_perm)
375
376   from `_ \<sharp>* p`
377   have **: "supp p \<sharp>* Lam [x]. e"
378     by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp)
379
380   have "F e x (Lam [x]. e) =  F (p \<bullet> e) (p \<bullet> x) (Lam [x]. e)" by (rule assms(2)[OF * **, symmetric])
381   also have "\<dots> = F e' x' (Lam [x']. e')" by (simp add: assms(1))
382   finally show ?thesis.
383 qed
384
385 (* Nice idea, but doesn't work well with extra arguments to the function
386
387 lemma eqvt_lam_case_eqvt:
388   assumes "Lam [x]. e = Lam [x']. e'"
389   assumes F_eqvt: "\<And> \<pi> e'. \<pi> \<bullet> F e x e' = F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (\<pi> \<bullet> e')"
390   assumes F_supp: "atom x \<sharp> F e x (Lam [x]. e)"
391   shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
392 using assms(1)
393 proof(rule eqvt_lam_case)
394   have "eqvt F" unfolding eqvt_def by (rule, perm_simp, rule) so rry
395   hence "supp (F e x (Lam [x]. e)) \<subseteq> supp e \<union> supp x \<union> supp (Lam [x]. e)" by (rule supp_fun_app_eqvt3)    
396   with F_supp[unfolded fresh_def]
397   have *: "supp (F e x (Lam [x]. e)) \<subseteq> supp (Lam [x]. e)" by (auto simp add: exp_assn.supp supp_at_base)
398
399   fix \<pi> :: perm
400   assume "supp \<pi> \<sharp>* Lam [x]. e" with *
401   have "supp \<pi> \<sharp>* F e x (Lam [x]. e)" by (auto simp add: fresh_star_def fresh_def)
402   hence "F e x (Lam [x]. e) = \<pi> \<bullet> (F e x (Lam [x]. e))" by (metis perm_supp_eq)
403   also have "\<dots> =  F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (\<pi> \<bullet> (Lam [x]. e))" by (simp add: F_eqvt)
404   also have "\<pi> \<bullet> (Lam [x]. e) = (Lam [x]. e)" using `supp \<pi> \<sharp>* Lam [x]. e` by (metis perm_supp_eq)
405   finally show "F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (Lam [x]. e) = F e x (Lam [x]. e)"..
406 qed
407 *)
408
409 lemma eqvt_let_case:
410   assumes "Let as body = Let as' body'"
411   assumes "\<And> \<pi> .
412     supp (-\<pi>) \<sharp>* (fv (Let as body) :: var set) \<Longrightarrow>
413     supp \<pi> \<sharp>* Let as body \<Longrightarrow>
414     F (\<pi> \<bullet> as) (\<pi> \<bullet> body) (Let as body) = F as body (Let as body)"
415   shows "F as body (Let as body) = F as' body' (Let as' body')"
416 proof-
417   from assms(1)
418   have "[map (\<lambda> p. atom (fst p)) as]lst. (body, as) = [map (\<lambda> p. atom (fst p)) as']lst. (body', as')" by auto
419   then obtain p
420     where "(supp (body, as) - atom ` domA as) \<sharp>* p"
421     and [simp]: "p \<bullet> body = body'"
422     and [simp]: "p \<bullet> as = as'"
423     unfolding  Abs_eq_iff(3) alpha_lst.simps by (auto simp add: domA_def image_image)
424
425   from `_ \<sharp>* p`
426   have *: "supp (-p) \<sharp>* (fv (Terms.Let as body) :: var set)"
427     by (auto simp add: fresh_star_def fresh_def supp_finite_set_at_base supp_Pair fv_supp_exp fv_supp_heap supp_minus_perm)
428
429   from `_ \<sharp>* p`
430   have **: "supp p \<sharp>* Terms.Let as body"
431     by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp fv_supp_heap )
432
433   have "F as body (Let as body) =  F (p \<bullet> as) (p \<bullet> body) (Let as body)" by (rule assms(2)[OF * **, symmetric])
434   also have "\<dots> = F as' body' (Let as' body')" by (simp add: assms(1))
435   finally show ?thesis.
436 qed
437
438 subsubsection {* A smart constructor for lets *}
439
440 text {*
441 Certian program transformations might change the bound variables, possibly making it an empty list.
442 This smart constructor avoids the empty let in the resulting expression. Semantically, it should
443 not make a difference. 
444 *}
445
446 definition SmartLet :: "heap => exp => exp"
447   where "SmartLet \<Gamma> e = (if \<Gamma> = [] then e else Let \<Gamma> e)"
448
449 lemma SmartLet_eqvt[eqvt]: "\<pi> \<bullet> (SmartLet \<Gamma> e) = SmartLet (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
450   unfolding SmartLet_def by perm_simp rule
451
452 lemma SmartLet_supp:
453   "supp (SmartLet \<Gamma> e) = (supp e \<union> supp \<Gamma>) - atom ` (domA \<Gamma>)"
454   unfolding SmartLet_def using Let_supp by (auto simp add: supp_Nil)
455
456 lemma fv_SmartLet[simp]: "fv (SmartLet \<Gamma> e) = (fv \<Gamma> \<union> fv e) - domA \<Gamma>"
457   unfolding SmartLet_def by auto
458
459 subsubsection {* A predicate for value expressions *}
460
461 nominal_function isLam :: "exp \<Rightarrow> bool" where
462   "isLam (GVar b x) = False" |
463   "isLam (Lam [x]. e) = True" |
464   "isLam (App e x) = False" |
465   "isLam (Let as e) = False"
466   unfolding isLam_graph_aux_def eqvt_def
467   apply simp
468   apply simp
469   apply (metis exp_strong_exhaust)
470   apply auto
471   done
472 nominal_termination (eqvt) by lexicographic_order
473
474 lemma isLam_Lam: "isLam (Lam [x]. e)" by simp
475
476 subsubsection {* The notion of thunks *}
477 (*
478 fun thunks :: "heap \<Rightarrow> var set" where
479   "thunks [] = {}"
480   | "thunks ((x,e)#\<Gamma>) = (if isLam e then {} else {x}) \<union> thunks \<Gamma>"
481 *)
482
483 definition thunks :: "heap \<Rightarrow> var set" where
484   "thunks \<Gamma> = {x . case map_of \<Gamma> x of Some e \<Rightarrow> \<not> isLam e | None \<Rightarrow> False}"
485
486 lemma thunks_Nil[simp]: "thunks [] = {}" by (auto simp add: thunks_def)
487
488 lemma thunks_domA: "thunks \<Gamma> \<subseteq> domA \<Gamma>"
489   by (induction \<Gamma> ) (auto simp add: thunks_def)
490
491 lemma thunks_Cons: "thunks ((x,e)#\<Gamma>) = (if isLam e then thunks \<Gamma> - {x} else insert x (thunks \<Gamma>))"
492   by (auto simp add: thunks_def )
493
494 lemma thunks_append[simp]: "thunks (\<Delta>@\<Gamma>) = thunks \<Delta> \<union> (thunks \<Gamma> - domA \<Delta>)"
495   by (induction \<Delta>) (auto simp add: thunks_def )
496
497 lemma thunks_delete[simp]: "thunks (delete x \<Gamma>) = thunks \<Gamma> - {x}"
498   by (induction \<Gamma>) (auto simp add: thunks_def )
499
500 lemma thunksI[intro]: "map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e \<Longrightarrow> x \<in> thunks \<Gamma>"
501   by (induction \<Gamma>) (auto simp add: thunks_def )
502
503 lemma thunksE[intro]: "x \<in> thunks \<Gamma> \<Longrightarrow> map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e"
504   by (induction \<Gamma>) (auto simp add: thunks_def )
505
506 lemma thunks_cong: "map_of \<Gamma> = map_of \<Delta> \<Longrightarrow> thunks \<Gamma> = thunks \<Delta>"
507   by (simp add: thunks_def)
508
509 lemma thunks_eqvt[eqvt]:
510   "\<pi> \<bullet> thunks \<Gamma> = thunks (\<pi> \<bullet> \<Gamma>)"
511     unfolding thunks_def
512     by perm_simp rule
513
514 subsubsection {* Non-recursive Let bindings *}
515
516 definition nonrec :: "heap \<Rightarrow> bool" where
517   "nonrec \<Gamma> = (\<exists> x e. \<Gamma> = [(x,e)] \<and> atom x \<sharp> e)"
518
519
520 lemma nonrecE:
521   assumes "nonrec \<Gamma>"
522   obtains x e where "\<Gamma> = [(x,e)]" and "atom x \<sharp> e"
523   using assms
524   unfolding nonrec_def
525   by blast
526
527 lemma nonrec_eqvt[eqvt]:
528   "nonrec \<Gamma> \<Longrightarrow> nonrec (\<pi> \<bullet> \<Gamma>)"
529   by (erule nonrecE) (auto simp add: nonrec_def)
530
531 lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam]:
532   assumes "\<And>b var. P (GVar b var)"
533   assumes "\<And>exp var. P exp \<Longrightarrow> P (App exp var)"
534   assumes "\<And>\<Gamma> exp. \<not> nonrec \<Gamma> \<Longrightarrow> (\<And> x. x \<in> domA \<Gamma> \<Longrightarrow>  P (the (map_of \<Gamma> x))) \<Longrightarrow> P exp \<Longrightarrow> P (Let \<Gamma> exp)"
535   assumes "\<And>x e exp. atom x \<sharp> e \<Longrightarrow>P e \<Longrightarrow> P exp \<Longrightarrow> P (let x be e in exp)"
536   assumes "\<And>var exp.  P exp \<Longrightarrow> P (Lam [var]. exp)"
537   shows "P exp"
538   apply (rule exp_induct[of P])
539   apply (metis assms(1))
540   apply (metis assms(2))
541   apply (case_tac "nonrec \<Gamma>")
542   apply (erule nonrecE)
543   apply simp
544   apply (metis assms(4))
545   apply (metis assms(3))
546   apply (metis assms(5))
547   done
548
549 lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam]:
550   assumes "\<And>b var c. P c (GVar b var)"
551   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
552   assumes "\<And>\<Gamma> exp c.
553     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> \<not> nonrec \<Gamma> \<Longrightarrow> (\<And>c x. x \<in> domA \<Gamma> \<Longrightarrow>  P c (the (map_of \<Gamma> x))) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
554   assumes "\<And>x e exp c. {atom x} \<sharp>* c \<Longrightarrow> atom x \<sharp> e \<Longrightarrow> (\<And> c. P c e) \<Longrightarrow> (\<And> c. P c exp) \<Longrightarrow> P c (let x be e in exp)"
555   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
556   shows "P (c::'a::fs) exp"
557   apply (rule exp_strong_induct[of P])
558   apply (metis assms(1))
559   apply (metis assms(2))
560   apply (case_tac "nonrec \<Gamma>")
561   apply (erule nonrecE)
562   apply simp
563   apply (metis assms(4))
564   apply (metis assms(3))
565   apply (metis assms(5))
566   done
567
568 lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam]:
569   assumes "\<And>b var c. P c (GVar b var)"
570   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
571   assumes "\<And>\<Gamma> exp c.
572     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> \<not> nonrec \<Gamma> \<Longrightarrow> (\<And>c x e. (x,e) \<in> set \<Gamma> \<Longrightarrow>  P c e) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
573   assumes "\<And>x e exp c. {atom x} \<sharp>* c \<Longrightarrow> atom x \<sharp> e \<Longrightarrow> (\<And> c. P c e) \<Longrightarrow> (\<And> c. P c exp) \<Longrightarrow> P c (let x be e in exp)"
574   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
575   shows "P (c::'a::fs) exp"
576   apply (rule exp_strong_induct_set(1)[of P])
577   apply (metis assms(1))
578   apply (metis assms(2))
579   apply (case_tac "nonrec \<Gamma>")
580   apply (erule nonrecE)
581   apply simp
582   apply (metis assms(4))
583   apply (metis assms(3))
584   apply (metis assms(5))
585   done
586
587
588
589 subsubsection {* Renaming a lambda-bound variable *}
590
591 lemma change_Lam_Variable:
592   assumes "y' \<noteq> y \<Longrightarrow> atom y' \<sharp> (e,  y)"
593   shows   "Lam [y]. e =  Lam [y']. ((y \<leftrightarrow> y') \<bullet> e)"
594 proof(cases "y' = y")
595   case True thus ?thesis by simp
596 next
597   case False
598   from assms[OF this]
599   have "(y \<leftrightarrow> y') \<bullet> (Lam [y]. e) = Lam [y]. e"
600     by -(rule flip_fresh_fresh, (simp add: fresh_Pair)+)
601   moreover
602   have "(y \<leftrightarrow> y') \<bullet> (Lam [y]. e) = Lam [y']. ((y \<leftrightarrow> y') \<bullet> e)"
603     by simp
604   ultimately
605   show "Lam [y]. e =  Lam [y']. ((y \<leftrightarrow> y') \<bullet> e)" by (simp add: fresh_Pair)
606 qed
607
608
609 end