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