90c9dba091b10cd3e501b872a0ca4546f85cf743
1 theory SestoftCorrect
2 imports Sestoft Launchbury BalancedTraces
3 begin
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]
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
32   have "x \<notin> domA \<Delta>" by (rule reds_avoids_live[OF Variable(2), where x = x]) simp_all
34   note `L = flattn S`[simp]
36   from `isLam z` have "isVal z" by (induction z rule:exp_induct) auto
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
52 type_synonym trace = "conf list"
54 fun stack :: "conf \<Rightarrow> stack" where "stack (\<Gamma>, e, S) = S"
56 interpretation traces step.
58 abbreviation trace_syn ("_ \<Rightarrow>\<^sup>*\<^bsub>_\<^esub> _" [50,50,50] 50) where "trace_syn \<equiv> trace"
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
64 interpretation balance_trace step  stack
65   apply default
66   apply (erule step.cases)
67   apply auto
68   done
70 abbreviation bal_syn ("_ \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>_\<^esub> _" [50,50,50] 50) where "bal_syn \<equiv> bal"
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
85 lemma lemma_3:
86   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
87   assumes "isLam z"
88   shows "\<Gamma> : e \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z"
89 using assms
90 proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[where f = length])
91   case (less T \<Gamma> e S \<Delta> z)
92   from `(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)`
93   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
95   from this(1)
96   show ?case
97   proof(cases)
98   case trace_nil
99     from `isLam z` obtain y e' where "z = Lam [y]. e'" by (cases z rule:isLam.cases) auto
100     with trace_nil show ?thesis by (auto intro: reds.intros)
101   next
102   case (trace_cons conf' T')
103     from `T = conf' # T'` and `\<forall> c'\<in>set T. S \<lesssim> stack c'` have "S \<lesssim> stack conf'" by auto
105     from `(\<Gamma>, e, S) \<Rightarrow> conf'`
106     show ?thesis
107     proof(cases)
108     case (app\<^sub>1 e x)
109       obtain T\<^sub>1 c\<^sub>3 c\<^sub>4 T\<^sub>2
110       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)"
111         by (rule bal_consE[OF  `bal _ T _`[unfolded app\<^sub>1 trace_cons]]) (simp, rule)
113       from `T = _` `T' = _` have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T" by auto
115       from prem1 have "stack c\<^sub>3 =  Arg x # S" by (auto dest:  bal_stackD)
116       moreover
117       from prem2 have "stack c\<^sub>4 = S" by (auto dest: bal_stackD)
118       moreover
119       note `c\<^sub>3 \<Rightarrow> c\<^sub>4`
120       ultimately
121       obtain \<Delta>' y e' where "c\<^sub>3 = (\<Delta>', Lam [y]. e', Arg x # S)" and "c\<^sub>4 = (\<Delta>', e'[y ::= x], S)"
122         by (auto elim!: step.cases simp del: exp_assn.eq_iff)
124       from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`] isLam_Lam]
125       have "\<Gamma> : e \<Down>\<^bsub>x # (flattn S)\<^esub> \<Delta>' : Lam [y]. e'" by simp
126       moreover
127       from less(1)[OF `length T\<^sub>2 < length T` prem2[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`] `isLam z`]
128       have "\<Delta>' : e'[y::=x] \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z" by simp
129       ultimately
130       show ?thesis unfolding app\<^sub>1
131         by (rule reds_ApplicationI)
132     next
133     case (app\<^sub>2 y e x S')
134       from `conf' =_` `S = _ # S'` `S \<lesssim> stack conf'`
135       have False by (auto simp add: extends_def)
136       thus ?thesis..
137     next
138     case (var\<^sub>1 x e)
139       obtain T\<^sub>1 c\<^sub>3 c\<^sub>4 T\<^sub>2
140       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)"
141         by (rule bal_consE[OF  `bal _ T _`[unfolded var\<^sub>1 trace_cons]]) (simp, rule)
143       from `T = _` `T' = _` have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T" by auto
146       from prem1 have "stack c\<^sub>3 = Upd x # S" by (auto dest:  bal_stackD)
147       moreover
148       from prem2 have "stack c\<^sub>4 = S" by (auto dest: bal_stackD)
149       moreover
150       note `c\<^sub>3 \<Rightarrow> c\<^sub>4`
151       ultimately
152       obtain \<Delta>' z' where "c\<^sub>3 = (\<Delta>', z', Upd x # S)" and "c\<^sub>4 = ((x,z')#\<Delta>', z', S)" and "isVal z'"
153         by (auto elim!: step.cases simp del: exp_assn.eq_iff)
155       from `isVal z'` and prem2[unfolded `c\<^sub>4 = _`]
156       have "T\<^sub>2 = []" by (rule lambda_stop)
157       with prem2 `c\<^sub>4 = _`
158       have "z' = z" and "\<Delta> = (x,z)#\<Delta>'" by auto
160       from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`  `z' = _`] `isLam z`]
161       have "delete x \<Gamma> : e \<Down>\<^bsub>x # flattn S\<^esub> \<Delta>' : z" by simp
162       with `map_of _ _ = _`
163       show ?thesis unfolding var\<^sub>1(1) `\<Delta> = _` by rule
164     next
165     case (var\<^sub>2 x S')
166       from `conf' = _` `S = _ # S'` `S \<lesssim> stack conf'`
167       have False by (auto simp add: extends_def)
168       thus ?thesis..
169     next
170     case (let\<^sub>1 as e)
171       from `T = conf' # T'` have "length T' < length T" by auto
172       moreover
173       have "(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)"
174         using trace_cons `conf' = _`  `\<forall> c'\<in>set T. S \<lesssim> stack c'` by fastforce
175       moreover
176       note `isLam z`
177       ultimately
178       have "as @ \<Gamma> : e \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z" by (rule less)
179       moreover
180       from `atom \` domA as \<sharp>* \<Gamma>`  `atom \` domA as \<sharp>* S`
181       have "atom ` domA as \<sharp>* (\<Gamma>, flattn S)" by (auto simp add: fresh_star_Pair)
182       ultimately
183       show ?thesis unfolding let\<^sub>1  by (rule reds.Let[rotated])
184     qed
185   qed
186 qed
188 lemma dummy_stack_extended:
189   "set S \<subseteq>  Dummy ` UNIV \<Longrightarrow> x \<notin> Dummy ` UNIV \<Longrightarrow> (S \<lesssim> x # S') \<longleftrightarrow>  S \<lesssim> S'"
190   apply (auto simp add: extends_def)
191   apply (case_tac S'')
192   apply auto
193   done
195 lemma[simp]: "Arg x \<notin> range Dummy"  "Upd x \<notin> range Dummy" by auto
197 lemma dummy_stack_balanced:
198   assumes "set S \<subseteq> Dummy ` UNIV"
199   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)"
200   obtains T where "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
201 proof-
202   from build_trace[OF assms(2)]
203   obtain T where "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"..
204   moreover
205   hence "\<forall> c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'"
206     by(rule conjunct1[OF traces_list_all]) (auto elim: step.cases simp add: dummy_stack_extended[OF `set S \<subseteq> Dummy \` UNIV`])
207   ultimately
208   have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
209     by (rule balI) simp
210   thus ?thesis by (rule that)
211 qed
213 end