Separate Arity consistency from Cardinality consistency
[darcs-mirror-isa-launchbury.git] / Launchbury / SestoftCorrect.thy
1 theory SestoftCorrect
2 imports BalancedTraces Launchbury Sestoft
3 begin
4
5
6 lemma lemma_2:
7   assumes "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z"
8   and "L = flattn S"
9   shows "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)"
10 using assms
11 proof(induction arbitrary: S  rule:reds.induct)
12   case (Lambda \<Gamma> x e L)
13   show ?case..
14 next
15   case (Application y \<Gamma> e x L \<Delta> \<Theta> z e')
16   note `L = flattn S`[simp]
17   
18   have "(\<Gamma>, App e x, S) \<Rightarrow> (\<Gamma>, e, Arg x # S)"..
19   also have "\<dots> \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', Arg x# S)" by (rule Application) simp
20   also have "\<dots> \<Rightarrow> (\<Delta>, e'[y ::= x], S)"..
21   also have "\<dots> \<Rightarrow>\<^sup>* (\<Theta>, z, S)" by (rule Application) simp
22   finally show ?case.
23 next
24 case (Variable \<Gamma> x e L \<Delta> z S)
25   have "isLam z"
26   proof-
27     from result_evaluated_fresh[OF Variable(2)]
28     obtain y e' where "z = Lam [y]. e'" by blast
29     thus ?thesis by simp
30   qed
31
32   have "x \<notin> domA \<Delta>" by (rule reds_avoids_live[OF Variable(2), where x = x]) simp_all
33
34   note `L = flattn S`[simp]
35
36   from `isLam z` have "isVal z" by (induction z rule:exp_induct) auto
37
38   from `map_of \<Gamma> x = Some e`
39   have "(\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e, Upd x # S)"..
40   also have "\<dots> \<Rightarrow>\<^sup>* (\<Delta>, z, Upd x # S)" by (rule Variable) simp
41   also have "\<dots> \<Rightarrow> ((x,z)#\<Delta>, z, S)" using `x \<notin> domA \<Delta>` `isVal z` by (rule var\<^sub>2)
42   finally show ?case.
43 next
44 case (Let as \<Gamma> L body \<Delta> z S)
45   from Let(1) Let(4)
46   have "atom ` domA as \<sharp>* \<Gamma>" and "atom ` domA as \<sharp>* S" by (auto simp add: fresh_star_Pair)
47   hence "(\<Gamma>, Terms.Let as body, S) \<Rightarrow> (as@\<Gamma>, body, S)"..
48   also have "\<dots> \<Rightarrow>\<^sup>* (\<Delta>, z, S)" by (rule Let) fact
49   finally show ?case.
50 qed
51
52 type_synonym trace = "conf list"
53
54 fun stack :: "conf \<Rightarrow> stack" where "stack (\<Gamma>, e, S) = S"
55                  
56 interpretation traces step.
57
58 abbreviation trace_syn ("_ \<Rightarrow>\<^sup>*\<^bsub>_\<^esub> _" [50,50,50] 50) where "trace_syn \<equiv> trace"
59
60 lemma conf_trace_induct_final[consumes 1, case_names trace_nil trace_cons]:
61   "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> final \<Longrightarrow> (\<And> \<Gamma> e S. final = (\<Gamma>, e, S) \<Longrightarrow> P \<Gamma> e S [] (\<Gamma>, e, S)) \<Longrightarrow> (\<And>\<Gamma> e S T \<Gamma>' e' S'. (\<Gamma>', e', S') \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> final \<Longrightarrow> P \<Gamma>' e' S' T final \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow> (\<Gamma>', e', S') \<Longrightarrow> P \<Gamma> e S ((\<Gamma>', e', S') # T) final) \<Longrightarrow> P \<Gamma> e S T final"
62   by (induction "(\<Gamma>, e, S)" T final arbitrary: \<Gamma> e S rule: trace_induct_final) auto
63
64 interpretation balance_trace step  stack
65   apply default
66   apply (erule step.cases)
67   apply auto
68   done
69
70 abbreviation bal_syn ("_ \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>_\<^esub> _" [50,50,50] 50) where "bal_syn \<equiv> bal"
71
72 lemma lambda_stop:
73   assumes "isVal e"
74   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
75   shows "T=[]"
76   using assms
77   apply -
78   apply (erule balE)
79   apply (erule trace.cases)
80   apply simp
81   apply auto
82   apply (auto elim!: step.cases)
83   done
84
85 nominal_function bool_free :: "exp \<Rightarrow> bool" where
86     "bool_free (Lam [x]. e) \<longleftrightarrow> bool_free e"
87   | "bool_free (Var x) \<longleftrightarrow> True"
88   | "bool_free (App e x) \<longleftrightarrow> bool_free e"
89   | "bool_free (Terms.Let \<Gamma> e) \<longleftrightarrow> (\<forall> (x, e) \<in> set \<Gamma>. bool_free e) \<and> bool_free e"
90   | "bool_free (Bool b) \<longleftrightarrow> False"
91   | "bool_free (scrut ? e\<^sub>1 : e\<^sub>2) \<longleftrightarrow> False"
92 proof-
93 case goal1 thus ?case
94   unfolding bool_free_graph_aux_def eqvt_def 
95   apply rule
96   apply perm_simp
97   apply rule
98   done
99 next
100 case goal3 thus ?case
101   by (metis Terms.Let_def exp_assn.exhaust(1) heapToAssn_asToHeap)
102 next
103 case (goal4 x e x' e')
104   from goal4(5)
105   show ?case
106   proof (rule eqvt_lam_case)
107     fix \<pi> :: perm
108     assume "supp \<pi> \<sharp>* Lam [x]. e"
109       
110     have "bool_free_sumC (\<pi> \<bullet> e) = \<pi> \<bullet> bool_free_sumC e"
111         by (simp add: pemute_minus_self eqvt_at_apply'[OF goal4(1)])
112     also have "\<dots> = bool_free_sumC e" by (simp add: permute_pure)
113     finally show  "bool_free_sumC (\<pi> \<bullet> e) = bool_free_sumC e".
114   qed
115 next
116 case (goal19 as body as' body')
117   from goal19(9)
118   show ?case
119   proof (rule eqvt_let_case)
120     fix \<pi> :: perm
121   
122     from goal19(2,4) have eqvt_at1: "eqvt_at bool_free_sumC body" by auto
123
124     assume assm: "supp \<pi> \<sharp>* Let as body"
125     
126     have "(\<forall> (x,e)\<in>set (\<pi> \<bullet> as). bool_free_sumC e) \<longleftrightarrow> - \<pi> \<bullet> (\<forall> (x,e)\<in>set (\<pi> \<bullet> as). bool_free_sumC e)"
127       by (simp add: permute_pure unpermute_def)
128       thm unpermute_def
129     also have "\<dots> = (\<forall> (x,e)\<in>set as. (- \<pi> \<bullet> bool_free_sumC) e)"
130       by perm_simp (simp add: pemute_minus_self)
131     also have "\<dots> = (\<forall> (x,e)\<in>set as. bool_free_sumC e)"
132       apply (rule ball_cong[OF refl])
133       apply (rule prod.case_cong[OF refl])
134       apply (rule eqvt_at_apply)
135       apply (metis goal19(1))
136       done
137     finally
138     have "(\<forall> (x,e)\<in>set (\<pi> \<bullet> as). bool_free_sumC e) \<longleftrightarrow> (\<forall> (x,e)\<in>set as. bool_free_sumC e)".
139     moreover
140     have "bool_free_sumC (\<pi> \<bullet> body) \<longleftrightarrow>  bool_free_sumC body" 
141       by (metis (full_types) True_eqvt eqvt_at1  eqvt_at_apply' eqvt_bound)
142     ultimately
143     show "((\<forall>a\<in>set (\<pi> \<bullet> as). case a of (x, x0) \<Rightarrow> bool_free_sumC x0) \<and> bool_free_sumC (\<pi> \<bullet> body)) =
144          ((\<forall>a\<in>set as. case a of (x, x0) \<Rightarrow> bool_free_sumC x0) \<and> bool_free_sumC body)" by simp
145   qed
146 qed auto
147 nominal_termination (eqvt) by lexicographic_order
148
149 lemma bool_free_SmartLet[simp]:
150   "bool_free (SmartLet \<Gamma> e) \<longleftrightarrow> (\<forall> (x, e) \<in> set \<Gamma>. bool_free e) \<and> bool_free e"
151 by (auto simp add: SmartLet_def)
152
153  
154 lemma Ball_subst[simp]:
155   "(\<forall>p\<in>set (\<Gamma>[y::h=x]). f p) \<longleftrightarrow> (\<forall>p\<in>set \<Gamma>. case p of (z,e) \<Rightarrow> f (z, e[y::=x]))"
156   by (induction \<Gamma>) auto
157
158 lemma [simp]: "bool_free e[y::=x] \<longleftrightarrow> bool_free e"
159   by (nominal_induct e avoiding: x y rule: exp_strong_induct_set) (auto  simp add: fresh_star_Pair)
160
161 inductive bool_free_stack :: "stack \<Rightarrow> bool" where
162   "bool_free_stack []"
163   | "bool_free_stack S \<Longrightarrow> bool_free_stack (Upd x # S)"
164   | "bool_free_stack S \<Longrightarrow> bool_free_stack (Arg x # S)"
165   | "bool_free_stack S \<Longrightarrow> bool_free_stack (Dummy x # S)"
166
167 inductive_simps bool_free_stack_simps: "bool_free_stack []"  "bool_free_stack (s # S)"
168
169 fun bool_free_conf :: "conf \<Rightarrow> bool" where
170   "bool_free_conf (\<Gamma>, e, S) \<longleftrightarrow> (\<forall> (x, e) \<in> set \<Gamma>. bool_free e) \<and> bool_free e \<and> bool_free_stack S"
171
172 lemma step_bool_free:
173   "c1 \<Rightarrow> c2 \<Longrightarrow> bool_free_conf c1 \<Longrightarrow> bool_free_conf c2"
174   by (cases rule: step.cases) (auto simp add: bool_free_stack_simps dest!: set_mp[OF set_delete_subset] map_of_is_SomeD)
175   
176 lemma step_star_bool_free:
177   assumes  "c \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> c'"
178   assumes "bool_free_conf c"
179   shows "bool_free_conf c'"
180 using assms by (induction) (auto dest: step_bool_free)
181
182 lemma bal_star_bool_free:
183   assumes  "c \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> c'"
184   assumes "bool_free_conf c"
185   shows "bool_free_conf c'"
186 using assms by (metis bal.simps step_star_bool_free)
187
188
189 lemma lemma_3:
190   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
191   assumes "bool_free_conf (\<Gamma>, e, S)"
192   assumes "isLam z"
193   shows "\<Gamma> : e \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z"
194 using assms
195 proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[where f = length])
196   case (less T \<Gamma> e S \<Delta> z)
197   from `(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)`
198   have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)" and "\<forall> c'\<in>set T. S \<lesssim> stack c'" unfolding bal.simps by auto
199
200   from this(1)
201   show ?case
202   proof(cases)
203   case trace_nil
204     from `isLam z` obtain y e' where "z = Lam [y]. e'" by (cases z rule:isLam.cases) auto
205     with trace_nil show ?thesis by (auto intro: reds.intros)
206   next
207   case (trace_cons conf' T')
208     from `T = conf' # T'` and `\<forall> c'\<in>set T. S \<lesssim> stack c'` have "S \<lesssim> stack conf'" by auto
209
210     note step_bool_free[OF `(\<Gamma>, e, S) \<Rightarrow> conf'`  `bool_free_conf (\<Gamma>, _, S)`]
211
212     from `(\<Gamma>, e, S) \<Rightarrow> conf'`
213     show ?thesis
214     proof(cases)
215     case (app\<^sub>1 e x)
216       obtain T\<^sub>1 c\<^sub>3 c\<^sub>4 T\<^sub>2
217       where "T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2" and prem1: "(\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3" and "c\<^sub>3 \<Rightarrow> c\<^sub>4" and prem2: " c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)"
218         by (rule bal_consE[OF  `bal _ T _`[unfolded app\<^sub>1 trace_cons]]) (simp, rule)
219
220       from `T = _` `T' = _` have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T" by auto
221
222       note bal_star_bool_free[OF prem1 `bool_free_conf conf'`[unfolded app\<^sub>1]]
223       note step_bool_free[OF `c\<^sub>3 \<Rightarrow> c\<^sub>4` this]
224
225       from prem1 have "stack c\<^sub>3 =  Arg x # S" by (auto dest:  bal_stackD)
226       moreover
227       from prem2 have "stack c\<^sub>4 = S" by (auto dest: bal_stackD)
228       moreover
229       note `c\<^sub>3 \<Rightarrow> c\<^sub>4`
230       ultimately
231       obtain \<Delta>' y e' where "c\<^sub>3 = (\<Delta>', Lam [y]. e', Arg x # S)" and "c\<^sub>4 = (\<Delta>', e'[y ::= x], S)"
232         by (auto elim!: step.cases simp del: exp_assn.eq_iff)
233
234       
235       from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`] `bool_free_conf conf'`[unfolded app\<^sub>1] isLam_Lam]
236       have "\<Gamma> : e \<Down>\<^bsub>x # (flattn S)\<^esub> \<Delta>' : Lam [y]. e'" by simp
237       moreover
238       from less(1)[OF `length T\<^sub>2 < length T` prem2[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`]  `bool_free_conf c\<^sub>4`[unfolded `c\<^sub>4 = _`] `isLam z`]
239       have "\<Delta>' : e'[y::=x] \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z" by simp
240       ultimately
241       show ?thesis unfolding app\<^sub>1
242         by (rule reds_ApplicationI)
243     next
244     case (app\<^sub>2 y e x S')
245       from `conf' =_` `S = _ # S'` `S \<lesssim> stack conf'`
246       have False by (auto simp add: extends_def)
247       thus ?thesis..
248     next
249     case (var\<^sub>1 x e)
250       obtain T\<^sub>1 c\<^sub>3 c\<^sub>4 T\<^sub>2
251       where "T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2" and prem1: "(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3" and "c\<^sub>3 \<Rightarrow> c\<^sub>4" and prem2: "c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)"
252         by (rule bal_consE[OF  `bal _ T _`[unfolded var\<^sub>1 trace_cons]]) (simp, rule)
253       
254       from `T = _` `T' = _` have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T" by auto
255
256
257       from prem1 have "stack c\<^sub>3 = Upd x # S" by (auto dest:  bal_stackD)
258       moreover
259       from prem2 have "stack c\<^sub>4 = S" by (auto dest: bal_stackD)
260       moreover
261       note `c\<^sub>3 \<Rightarrow> c\<^sub>4`
262       ultimately
263       obtain \<Delta>' z' where "c\<^sub>3 = (\<Delta>', z', Upd x # S)" and "c\<^sub>4 = ((x,z')#\<Delta>', z', S)" and "isVal z'"
264         by (auto elim!: step.cases simp del: exp_assn.eq_iff)
265
266       from `isVal z'` and prem2[unfolded `c\<^sub>4 = _`]
267       have "T\<^sub>2 = []" by (rule lambda_stop)
268       with prem2 `c\<^sub>4 = _`
269       have "z' = z" and "\<Delta> = (x,z)#\<Delta>'" by auto
270           
271       from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`  `z' = _`] `bool_free_conf conf'`[unfolded var\<^sub>1]  `isLam z`]
272       have "delete x \<Gamma> : e \<Down>\<^bsub>x # flattn S\<^esub> \<Delta>' : z" by simp
273       with `map_of _ _ = _`
274       show ?thesis unfolding var\<^sub>1(1) `\<Delta> = _` by rule
275     next
276     case (var\<^sub>2 x S')
277       from `conf' = _` `S = _ # S'` `S \<lesssim> stack conf'`
278       have False by (auto simp add: extends_def)
279       thus ?thesis..
280     next
281     case (let\<^sub>1 as e)
282       from `T = conf' # T'` have "length T' < length T" by auto
283       moreover
284       have "(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)" 
285         using trace_cons `conf' = _`  `\<forall> c'\<in>set T. S \<lesssim> stack c'` by fastforce
286       moreover
287       note `bool_free_conf conf'`[unfolded let\<^sub>1]
288       moreover
289       note `isLam z`
290       ultimately
291       have "as @ \<Gamma> : e \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z" by (rule less)
292       moreover
293       from `atom \` domA as \<sharp>* \<Gamma>`  `atom \` domA as \<sharp>* S`
294       have "atom ` domA as \<sharp>* (\<Gamma>, flattn S)" by (auto simp add: fresh_star_Pair)
295       ultimately
296       show ?thesis unfolding let\<^sub>1  by (rule reds.Let[rotated])
297     next
298     case (if\<^sub>1)
299       with `bool_free_conf (\<Gamma>, e, S)`
300       have False by simp
301       thus ?thesis..
302    next
303     case (if\<^sub>2)
304       with `bool_free_conf (\<Gamma>, e, S)`
305       have False by simp
306       thus ?thesis..
307     qed
308   qed
309 qed
310
311 lemma dummy_stack_extended:
312   "set S \<subseteq>  Dummy ` UNIV \<Longrightarrow> x \<notin> Dummy ` UNIV \<Longrightarrow> (S \<lesssim> x # S') \<longleftrightarrow>  S \<lesssim> S'"
313   apply (auto simp add: extends_def)
314   apply (case_tac S'')
315   apply auto
316   done
317
318 lemma[simp]: "Arg x \<notin> range Dummy"  "Upd x \<notin> range Dummy"   "Alts e\<^sub>1 e\<^sub>2 \<notin> range Dummy" by auto
319
320 lemma dummy_stack_balanced:
321   assumes "set S \<subseteq> Dummy ` UNIV"
322   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)"
323   obtains T where "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
324 proof-
325   from build_trace[OF assms(2)]
326   obtain T where "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"..
327   moreover
328   hence "\<forall> c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'"
329     by (rule conjunct1[OF traces_list_all])
330        (auto elim: step.cases simp add: dummy_stack_extended[OF `set S \<subseteq> Dummy \` UNIV`])
331   ultimately
332   have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
333     by (rule balI) simp
334   thus ?thesis by (rule that)
335 qed
336
337 end