Add Null and (e ? e : e)
[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 lemma finite_fv_exp[simp]: "finite (fv (e::exp) :: var set)"
370   and finite_fv_heap[simp]: "finite (fv (\<Gamma> :: heap) :: var set)"
371   by (induction e rule:exp_heap_induct) auto
372
373
374 lemma fv_delete_heap:
375   assumes "map_of \<Gamma> x = Some e"
376   shows "fv (delete x \<Gamma>, e) \<union> {x} \<subseteq> (fv (\<Gamma>, Var x) :: var set)"
377 proof-
378   have "fv (delete x \<Gamma>) \<subseteq> fv \<Gamma>" by (metis fv_delete_subset)
379   moreover
380   have "(x,e) \<in> set \<Gamma>" by (metis assms map_of_is_SomeD)
381   hence "fv e \<subseteq> fv \<Gamma>" by (metis assms domA_from_set map_of_fv_subset option.sel)
382   moreover
383   have "x \<in> fv (Var x)" by simp
384   ultimately show ?thesis by auto
385 qed
386
387 subsubsection {* Lemmas helping with nominal definitions *}
388
389 lemma eqvt_lam_case:
390   assumes "Lam [x]. e = Lam [x']. e'"
391   assumes "\<And> \<pi> . supp (-\<pi>) \<sharp>* (fv (Lam [x]. e) :: var set) \<Longrightarrow>
392                  supp \<pi> \<sharp>* (Lam [x]. e) \<Longrightarrow>
393         F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (Lam [x]. e) = F e x (Lam [x]. e)"
394   shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
395 proof-
396
397   from assms(1)
398   have "[[atom x]]lst. (e, x) = [[atom x']]lst. (e', x')" by auto
399   then obtain p
400     where "(supp (e, x) - {atom x}) \<sharp>* p"
401     and [simp]: "p \<bullet> x = x'"
402     and [simp]: "p \<bullet> e = e'"
403     unfolding  Abs_eq_iff(3) alpha_lst.simps by auto
404
405   from `_ \<sharp>* p`
406   have *: "supp (-p) \<sharp>* (fv (Lam [x]. e) :: var set)"
407     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)
408
409   from `_ \<sharp>* p`
410   have **: "supp p \<sharp>* Lam [x]. e"
411     by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp)
412
413   have "F e x (Lam [x]. e) =  F (p \<bullet> e) (p \<bullet> x) (Lam [x]. e)" by (rule assms(2)[OF * **, symmetric])
414   also have "\<dots> = F e' x' (Lam [x']. e')" by (simp add: assms(1))
415   finally show ?thesis.
416 qed
417
418 (* Nice idea, but doesn't work well with extra arguments to the function
419
420 lemma eqvt_lam_case_eqvt:
421   assumes "Lam [x]. e = Lam [x']. e'"
422   assumes F_eqvt: "\<And> \<pi> e'. \<pi> \<bullet> F e x e' = F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (\<pi> \<bullet> e')"
423   assumes F_supp: "atom x \<sharp> F e x (Lam [x]. e)"
424   shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
425 using assms(1)
426 proof(rule eqvt_lam_case)
427   have "eqvt F" unfolding eqvt_def by (rule, perm_simp, rule) so rry
428   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)    
429   with F_supp[unfolded fresh_def]
430   have *: "supp (F e x (Lam [x]. e)) \<subseteq> supp (Lam [x]. e)" by (auto simp add: exp_assn.supp supp_at_base)
431
432   fix \<pi> :: perm
433   assume "supp \<pi> \<sharp>* Lam [x]. e" with *
434   have "supp \<pi> \<sharp>* F e x (Lam [x]. e)" by (auto simp add: fresh_star_def fresh_def)
435   hence "F e x (Lam [x]. e) = \<pi> \<bullet> (F e x (Lam [x]. e))" by (metis perm_supp_eq)
436   also have "\<dots> =  F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (\<pi> \<bullet> (Lam [x]. e))" by (simp add: F_eqvt)
437   also have "\<pi> \<bullet> (Lam [x]. e) = (Lam [x]. e)" using `supp \<pi> \<sharp>* Lam [x]. e` by (metis perm_supp_eq)
438   finally show "F (\<pi> \<bullet> e) (\<pi> \<bullet> x) (Lam [x]. e) = F e x (Lam [x]. e)"..
439 qed
440 *)
441
442 lemma eqvt_let_case:
443   assumes "Let as body = Let as' body'"
444   assumes "\<And> \<pi> .
445     supp (-\<pi>) \<sharp>* (fv (Let as body) :: var set) \<Longrightarrow>
446     supp \<pi> \<sharp>* Let as body \<Longrightarrow>
447     F (\<pi> \<bullet> as) (\<pi> \<bullet> body) (Let as body) = F as body (Let as body)"
448   shows "F as body (Let as body) = F as' body' (Let as' body')"
449 proof-
450   from assms(1)
451   have "[map (\<lambda> p. atom (fst p)) as]lst. (body, as) = [map (\<lambda> p. atom (fst p)) as']lst. (body', as')" by auto
452   then obtain p
453     where "(supp (body, as) - atom ` domA as) \<sharp>* p"
454     and [simp]: "p \<bullet> body = body'"
455     and [simp]: "p \<bullet> as = as'"
456     unfolding  Abs_eq_iff(3) alpha_lst.simps by (auto simp add: domA_def image_image)
457
458   from `_ \<sharp>* p`
459   have *: "supp (-p) \<sharp>* (fv (Terms.Let as body) :: var set)"
460     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)
461
462   from `_ \<sharp>* p`
463   have **: "supp p \<sharp>* Terms.Let as body"
464     by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp fv_supp_heap )
465
466   have "F as body (Let as body) =  F (p \<bullet> as) (p \<bullet> body) (Let as body)" by (rule assms(2)[OF * **, symmetric])
467   also have "\<dots> = F as' body' (Let as' body')" by (simp add: assms(1))
468   finally show ?thesis.
469 qed
470
471 subsubsection {* A smart constructor for lets *}
472
473 text {*
474 Certian program transformations might change the bound variables, possibly making it an empty list.
475 This smart constructor avoids the empty let in the resulting expression. Semantically, it should
476 not make a difference. 
477 *}
478
479 definition SmartLet :: "heap => exp => exp"
480   where "SmartLet \<Gamma> e = (if \<Gamma> = [] then e else Let \<Gamma> e)"
481
482 lemma SmartLet_eqvt[eqvt]: "\<pi> \<bullet> (SmartLet \<Gamma> e) = SmartLet (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
483   unfolding SmartLet_def by perm_simp rule
484
485 lemma SmartLet_supp:
486   "supp (SmartLet \<Gamma> e) = (supp e \<union> supp \<Gamma>) - atom ` (domA \<Gamma>)"
487   unfolding SmartLet_def using Let_supp by (auto simp add: supp_Nil)
488
489 lemma fv_SmartLet[simp]: "fv (SmartLet \<Gamma> e) = (fv \<Gamma> \<union> fv e) - domA \<Gamma>"
490   unfolding SmartLet_def by auto
491
492 subsubsection {* A predicate for value expressions *}
493
494 nominal_function isLam :: "exp \<Rightarrow> bool" where
495   "isLam (Var x) = False" |
496   "isLam (Lam [x]. e) = True" |
497   "isLam (App e x) = False" |
498   "isLam (Let as e) = False" |
499   "isLam Null = False" |
500   "isLam (scrut ? e1 : e2) = False"
501   unfolding isLam_graph_aux_def eqvt_def
502   apply simp
503   apply simp
504   apply (metis exp_strong_exhaust)
505   apply auto
506   done
507 nominal_termination (eqvt) by lexicographic_order
508
509 lemma isLam_Lam: "isLam (Lam [x]. e)" by simp
510
511 subsubsection {* The notion of thunks *}
512 (*
513 fun thunks :: "heap \<Rightarrow> var set" where
514   "thunks [] = {}"
515   | "thunks ((x,e)#\<Gamma>) = (if isLam e then {} else {x}) \<union> thunks \<Gamma>"
516 *)
517
518 definition thunks :: "heap \<Rightarrow> var set" where
519   "thunks \<Gamma> = {x . case map_of \<Gamma> x of Some e \<Rightarrow> \<not> isLam e | None \<Rightarrow> False}"
520
521 lemma thunks_Nil[simp]: "thunks [] = {}" by (auto simp add: thunks_def)
522
523 lemma thunks_domA: "thunks \<Gamma> \<subseteq> domA \<Gamma>"
524   by (induction \<Gamma> ) (auto simp add: thunks_def)
525
526 lemma thunks_Cons: "thunks ((x,e)#\<Gamma>) = (if isLam e then thunks \<Gamma> - {x} else insert x (thunks \<Gamma>))"
527   by (auto simp add: thunks_def )
528
529 lemma thunks_append[simp]: "thunks (\<Delta>@\<Gamma>) = thunks \<Delta> \<union> (thunks \<Gamma> - domA \<Delta>)"
530   by (induction \<Delta>) (auto simp add: thunks_def )
531
532 lemma thunks_delete[simp]: "thunks (delete x \<Gamma>) = thunks \<Gamma> - {x}"
533   by (induction \<Gamma>) (auto simp add: thunks_def )
534
535 lemma thunksI[intro]: "map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e \<Longrightarrow> x \<in> thunks \<Gamma>"
536   by (induction \<Gamma>) (auto simp add: thunks_def )
537
538 lemma thunksE[intro]: "x \<in> thunks \<Gamma> \<Longrightarrow> map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e"
539   by (induction \<Gamma>) (auto simp add: thunks_def )
540
541 lemma thunks_cong: "map_of \<Gamma> = map_of \<Delta> \<Longrightarrow> thunks \<Gamma> = thunks \<Delta>"
542   by (simp add: thunks_def)
543
544 lemma thunks_eqvt[eqvt]:
545   "\<pi> \<bullet> thunks \<Gamma> = thunks (\<pi> \<bullet> \<Gamma>)"
546     unfolding thunks_def
547     by perm_simp rule
548
549 subsubsection {* Non-recursive Let bindings *}
550
551 definition nonrec :: "heap \<Rightarrow> bool" where
552   "nonrec \<Gamma> = (\<exists> x e. \<Gamma> = [(x,e)] \<and> atom x \<sharp> e)"
553
554
555 lemma nonrecE:
556   assumes "nonrec \<Gamma>"
557   obtains x e where "\<Gamma> = [(x,e)]" and "atom x \<sharp> e"
558   using assms
559   unfolding nonrec_def
560   by blast
561
562 lemma nonrec_eqvt[eqvt]:
563   "nonrec \<Gamma> \<Longrightarrow> nonrec (\<pi> \<bullet> \<Gamma>)"
564   by (erule nonrecE) (auto simp add: nonrec_def)
565
566 lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam Null IfThenElse]:
567   assumes "\<And>var. P (Var var)"
568   assumes "\<And>exp var. P exp \<Longrightarrow> P (App exp var)"
569   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)"
570   assumes "\<And>x e exp. atom x \<sharp> e \<Longrightarrow> P e \<Longrightarrow> P exp \<Longrightarrow> P (let x be e in exp)"
571   assumes "\<And>var exp.  P exp \<Longrightarrow> P (Lam [var]. exp)"
572   assumes "P Null"
573   assumes "\<And> scrut e1 e2. P scrut \<Longrightarrow> P e1 \<Longrightarrow> P e2 \<Longrightarrow> P (scrut ? e1 : e2)"
574   shows "P exp"
575   apply (rule exp_induct[of P])
576   apply (metis assms(1))
577   apply (metis assms(2))
578   apply (case_tac "nonrec \<Gamma>")
579   apply (erule nonrecE)
580   apply simp
581   apply (metis assms(4))
582   apply (metis assms(3))
583   apply (metis assms(5))
584   apply (metis assms(6))
585   apply (metis assms(7))
586   done
587
588 lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam Null IfThenElse]:
589   assumes "\<And>var c. P c (Var var)"
590   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
591   assumes "\<And>\<Gamma> exp c.
592     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)"
593   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)"
594   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
595   assumes "\<And> c. P c Null"
596   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)"
597   shows "P (c::'a::fs) exp"
598   apply (rule exp_strong_induct[of P])
599   apply (metis assms(1))
600   apply (metis assms(2))
601   apply (case_tac "nonrec \<Gamma>")
602   apply (erule nonrecE)
603   apply simp
604   apply (metis assms(4))
605   apply (metis assms(3))
606   apply (metis assms(5))
607   apply (metis assms(6))
608   apply (metis assms(7))
609   done
610
611 lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam Null IfThenElse]:
612   assumes "\<And>var c. P c (Var var)"
613   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
614   assumes "\<And>\<Gamma> exp c.
615     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)"
616   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)"
617   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
618   assumes "\<And> c. P c Null"
619   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)"
620   shows "P (c::'a::fs) exp"
621   apply (rule exp_strong_induct_set(1)[of P])
622   apply (metis assms(1))
623   apply (metis assms(2))
624   apply (case_tac "nonrec \<Gamma>")
625   apply (erule nonrecE)
626   apply simp
627   apply (metis assms(4))
628   apply (metis assms(3))
629   apply (metis assms(5))
630   apply (metis assms(6))
631   apply (metis assms(7))
632   done
633
634
635
636 subsubsection {* Renaming a lambda-bound variable *}
637
638 lemma change_Lam_Variable:
639   assumes "y' \<noteq> y \<Longrightarrow> atom y' \<sharp> (e,  y)"
640   shows   "Lam [y]. e =  Lam [y']. ((y \<leftrightarrow> y') \<bullet> e)"
641 proof(cases "y' = y")
642   case True thus ?thesis by simp
643 next
644   case False
645   from assms[OF this]
646   have "(y \<leftrightarrow> y') \<bullet> (Lam [y]. e) = Lam [y]. e"
647     by -(rule flip_fresh_fresh, (simp add: fresh_Pair)+)
648   moreover
649   have "(y \<leftrightarrow> y') \<bullet> (Lam [y]. e) = Lam [y']. ((y \<leftrightarrow> y') \<bullet> e)"
650     by simp
651   ultimately
652   show "Lam [y]. e =  Lam [y']. ((y \<leftrightarrow> y') \<bullet> e)" by (simp add: fresh_Pair)
653 qed
654
655
656 end