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