Fix end-to-end proof to finally obtain the unmodified semantics
[darcs-mirror-isa-launchbury.git] / Launchbury / SestoftConf.thy
1 theory SestoftConf
2 imports Terms Substitution
3 begin
4
5 datatype stack_elem = Alts exp exp | Arg var | Upd var | Dummy var
6
7 instantiation stack_elem :: pt
8 begin
9 definition  "\<pi> \<bullet> x = (case x of (Alts e1 e2) \<Rightarrow> Alts (\<pi> \<bullet> e1) (\<pi> \<bullet> e2) | (Arg v) \<Rightarrow> Arg (\<pi> \<bullet> v) | (Upd v) \<Rightarrow> Upd (\<pi> \<bullet> v) | (Dummy v) \<Rightarrow> Dummy (\<pi> \<bullet> v))"
10 instance
11   by default (auto simp add: permute_stack_elem_def split:stack_elem.split)
12 end
13
14 lemma Alts_eqvt[eqvt]: "\<pi> \<bullet> (Alts e1 e2) = Alts (\<pi> \<bullet> e1) (\<pi> \<bullet> e2)"
15   and Arg_eqvt[eqvt]: "\<pi> \<bullet> (Arg v) = Arg (\<pi> \<bullet> v)"
16   and Upd_eqvt[eqvt]: "\<pi> \<bullet> (Upd v) = Upd (\<pi> \<bullet> v)"
17   and Dummy_eqvt[eqvt]: "\<pi> \<bullet> (Dummy v) = Dummy (\<pi> \<bullet> v)"
18   by (auto simp add: permute_stack_elem_def split:stack_elem.split)
19
20 find_theorems supp name:Pair
21 lemma supp_Alts[simp]: "supp (Alts e1 e2) = supp e1 \<union> supp e2" unfolding supp_def by (auto simp add: Collect_imp_eq Collect_neg_eq)
22 lemma supp_Arg[simp]: "supp (Arg v) = supp v"  unfolding supp_def by auto
23 lemma supp_Upd[simp]: "supp (Upd v) = supp v"  unfolding supp_def by auto
24 lemma supp_Dummy[simp]: "supp (Dummy v) = supp v"  unfolding supp_def by auto
25 lemma fresh_Alts[simp]: "a \<sharp> Alts e1 e2 = (a \<sharp> e1 \<and> a \<sharp> e2)" unfolding fresh_def by auto
26 lemma fresh_star_Alts[simp]: "a \<sharp>* Alts e1 e2 = (a \<sharp>* e1 \<and> a \<sharp>* e2)" unfolding fresh_star_def by auto
27 lemma fresh_Arg[simp]: "a \<sharp> Arg v = a \<sharp> v" unfolding fresh_def by auto
28 lemma fresh_Upd[simp]: "a \<sharp> Upd v = a \<sharp> v" unfolding fresh_def by auto
29 lemma fresh_Dummy[simp]: "a \<sharp> Dummy v = a \<sharp> v" unfolding fresh_def by auto
30 lemma fv_Alts[simp]: "fv (Alts e1 e2) = fv e1 \<union> fv e2"  unfolding fv_def by auto
31 lemma fv_Arg[simp]: "fv (Arg v) = fv v"  unfolding fv_def by auto
32 lemma fv_Upd[simp]: "fv (Upd v) = fv v"  unfolding fv_def by auto
33 lemma fv_Dummy[simp]: "fv (Dummy v) = fv v"  unfolding fv_def by auto
34
35 instance stack_elem :: fs  by (default, case_tac x) (auto simp add: finite_supp)
36
37 type_synonym stack = "stack_elem list"
38
39 fun ap :: "stack \<Rightarrow> var set" where
40   "ap [] = {}"
41 | "ap (Alts e1 e2 # S) = ap S"
42 | "ap (Arg x # S) = insert x (ap S)"
43 | "ap (Upd x # S) = ap S"
44 | "ap (Dummy x # S) = ap S"
45 fun upds :: "stack \<Rightarrow> var set" where
46   "upds [] = {}"
47 | "upds (Alts e1 e2 # S) = upds S"
48 | "upds (Upd x # S) = insert x (upds S)"
49 | "upds (Arg x # S) = upds S"
50 | "upds (Dummy x # S) = upds S"
51 fun dummies :: "stack \<Rightarrow> var set" where
52   "dummies [] = {}"
53 | "dummies (Alts e1 e2 # S) = dummies S"
54 | "dummies (Upd x # S) = dummies S"
55 | "dummies (Arg x # S) = dummies S"
56 | "dummies (Dummy x # S) = insert x (dummies S)"
57 fun flattn :: "stack \<Rightarrow> var list" where
58   "flattn [] = []"
59 | "flattn (Alts e1 e2 # S) = fv_list e1 @ fv_list e2 @ flattn S"
60 | "flattn (Upd x # S) = x # flattn S"
61 | "flattn (Arg x # S) = x # flattn S"
62 | "flattn (Dummy x # S) = x # flattn S"
63 fun upds_list :: "stack \<Rightarrow> var list" where
64   "upds_list [] = []"
65 | "upds_list (Alts e1 e2 # S) = upds_list S"
66 | "upds_list (Upd x # S) = x # upds_list S"
67 | "upds_list (Arg x # S) = upds_list S"
68 | "upds_list (Dummy x # S) = upds_list S"
69
70 lemma set_upds_list[simp]:
71   "set (upds_list S) = upds S"
72   by (induction S rule: upds_list.induct) auto
73
74 lemma ups_fv_subset: "upds S \<subseteq> fv S"
75   by (induction S rule: upds.induct) auto
76 lemma fresh_distinct_ups: "atom ` V \<sharp>* S \<Longrightarrow> V \<inter> upds S = {}"
77    by (auto dest!: fresh_distinct_fv set_mp[OF ups_fv_subset])
78 lemma ap_fv_subset: "ap S \<subseteq> fv S"
79   by (induction S rule: upds.induct) auto
80 lemma dummies_fv_subset: "dummies S \<subseteq> fv S"
81   by (induction S rule: dummies.induct) auto
82
83 lemma fresh_flattn[simp]: "atom (a::var) \<sharp> flattn S \<longleftrightarrow> atom a \<sharp> S"
84   by (induction S rule:flattn.induct) (auto simp add: fresh_Nil fresh_Cons fresh_append fresh_fv[OF finite_fv])
85 lemma fresh_star_flattn[simp]: "atom ` (as:: var set) \<sharp>* flattn S \<longleftrightarrow> atom ` as \<sharp>* S"
86   by (auto simp add: fresh_star_def)
87
88 lemma upds_append[simp]: "upds (S@S') = upds S \<union> upds S'"
89   by (induction S rule: upds.induct) auto
90 lemma upds_map_Dummy[simp]: "upds (map Dummy l) = {}"
91   by (induction l) auto
92
93 lemma upds_list_append[simp]: "upds_list (S@S') = upds_list S @ upds_list S'"
94   by (induction S rule: upds.induct) auto
95 lemma upds_list_map_Dummy[simp]: "upds_list (map Dummy l) = []"
96   by (induction l) auto
97
98 lemma dummies_append[simp]: "dummies (S@S') = dummies S \<union> dummies S'"
99   by (induction S rule: dummies.induct) auto
100 lemma dummies_map_Dummy[simp]: "dummies (map Dummy l) = set l"
101   by (induction l) auto
102
103 lemma map_Dummy_inj[simp]: "map Dummy l = map Dummy l' \<longleftrightarrow> l = l'"
104   apply (induction l arbitrary: l')
105   apply (case_tac [!] l')
106   apply auto
107   done
108
109 type_synonym conf = "(heap \<times> exp \<times> stack)"
110
111 inductive boring_step where
112   "isVal e \<Longrightarrow> boring_step (\<Gamma>, e, Upd x # S)"
113
114
115 fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
116   where "restr_stack V [] = []"
117       | "restr_stack V (Alts e1 e2 # S) = Alts e1 e2 # restr_stack V S"
118       | "restr_stack V (Arg x # S) = Arg x # restr_stack V S"
119       | "restr_stack V (Upd x # S) = (if x \<in> V then Upd x # restr_stack V S else restr_stack V S)"
120       | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"
121
122 lemma restr_stack_cong:
123   "(\<And> x. x \<in> upds S \<Longrightarrow> x \<in> V \<longleftrightarrow> x \<in> V') \<Longrightarrow> restr_stack V S = restr_stack V' S"
124   by (induction V S rule: restr_stack.induct) auto
125
126 lemma upds_restr_stack[simp]: "upds (restr_stack V S) = upds S \<inter> V"
127   by (induction V S rule: restr_stack.induct) auto
128
129 lemma fresh_star_restict_stack[intro]:
130   "a \<sharp>* S \<Longrightarrow> a \<sharp>* restr_stack V S"
131   by (induction V S rule: restr_stack.induct) (auto simp add: fresh_star_Cons)
132
133 lemma restr_stack_restr_stack[simp]:
134   "restr_stack V (restr_stack V' S) = restr_stack (V \<inter> V') S"
135   by (induction V S rule: restr_stack.induct) auto
136
137 lemma Upd_eq_restr_stackD:
138   assumes "Upd x # S = restr_stack V S'"
139   shows "x \<in> V"
140   using arg_cong[where f = upds, OF assms]
141   by auto
142 lemma Upd_eq_restr_stackD2:
143   assumes "restr_stack V S' = Upd x # S"
144   shows "x \<in> V"
145   using arg_cong[where f = upds, OF assms]
146   by auto
147
148
149 lemma restr_stack_noop[simp]:
150   "restr_stack V S = S \<longleftrightarrow> upds S \<subseteq> V"
151   by (induction V S rule: restr_stack.induct)
152      (auto dest: Upd_eq_restr_stackD2)
153   
154
155 subsubsection {* Invariants of the semantics *}
156
157 inductive invariant :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
158   where "(\<And> x y. rel x y \<Longrightarrow> I x \<Longrightarrow> I y) \<Longrightarrow> invariant rel I"
159
160 lemmas invariant.intros[case_names step]
161
162 lemma invariantE:
163   "invariant rel I \<Longrightarrow> rel x y \<Longrightarrow> I x \<Longrightarrow> I y" by (auto elim: invariant.cases)
164
165 lemma invariant_starE:
166   "rtranclp rel x y \<Longrightarrow> invariant rel I \<Longrightarrow>  I x \<Longrightarrow> I y"
167   by (induction rule: rtranclp.induct) (auto elim: invariantE)
168
169 lemma invariant_True:
170   "invariant rel (\<lambda> _. True)"
171 by (auto intro: invariant.intros)
172
173 lemma invariant_conj:
174   "invariant rel I1 \<Longrightarrow> invariant rel I2 \<Longrightarrow> invariant rel (\<lambda> x. I1 x \<and> I2 x)"
175 by (auto simp add: invariant.simps)
176
177
178 thm rtranclp_induct[no_vars]
179
180 lemma rtranclp_invariant_induct[consumes 3, case_names base step]:
181   assumes "r\<^sup>*\<^sup>* a b"
182   assumes "invariant r I"
183   assumes "I a"
184   assumes "P a"
185   assumes "(\<And>y z. r\<^sup>*\<^sup>* a y \<Longrightarrow> r y z \<Longrightarrow> I y \<Longrightarrow> I z \<Longrightarrow> P y \<Longrightarrow> P z)"
186   shows "P b"
187 proof-
188   from assms(1,3)
189   have "P b" and "I b"
190   proof(induction)
191     case base
192     from `P a` show "P a".
193     from `I a` show "I a".
194   next
195     case (step y z)
196     with `I a` have "P y" and "I y" by auto
197
198     from assms(2) `r y z` `I y`
199     show "I z" by (rule invariantE)
200
201     from `r\<^sup>*\<^sup>* a y` `r y z` `I y` `I z` `P y`
202     show "P z" by (rule assms(5))
203   qed
204   thus "P b" by-
205 qed
206
207
208 fun closed :: "conf \<Rightarrow> bool"
209   where "closed (\<Gamma>, e, S) \<longleftrightarrow> fv (\<Gamma>, e, S) \<subseteq> domA \<Gamma> \<union> upds S"
210
211 fun heap_upds_ok where "heap_upds_ok (\<Gamma>,S) \<longleftrightarrow> domA \<Gamma> \<inter> upds S = {} \<and> distinct (upds_list S)"
212
213 abbreviation heap_upds_ok_conf :: "conf \<Rightarrow> bool"
214   where "heap_upds_ok_conf c \<equiv> heap_upds_ok (fst c, snd (snd c))"
215
216 lemma heap_upds_okE: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> upds S"
217   by auto
218
219 lemma heap_upds_ok_Nil[simp]: "heap_upds_ok (\<Gamma>, [])" by auto
220 lemma heap_upds_ok_app1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Arg x # S)" by auto
221 lemma heap_upds_ok_app2: "heap_upds_ok (\<Gamma>, Arg x # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
222 lemma heap_upds_ok_alts1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Alts e1 e2 # S)" by auto
223 lemma heap_upds_ok_alts2: "heap_upds_ok (\<Gamma>, Alts e1 e2 # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
224
225 lemma heap_upds_ok_append:
226   assumes "domA \<Delta> \<inter> upds S = {}"
227   assumes "heap_upds_ok (\<Gamma>,S)"
228   shows "heap_upds_ok (\<Delta>@\<Gamma>, S)"
229   using assms
230   unfolding heap_upds_ok.simps
231   by auto
232
233 lemma heap_upds_ok_let:
234   assumes "atom ` domA \<Delta> \<sharp>* S"
235   assumes "heap_upds_ok (\<Gamma>, S)"
236   shows "heap_upds_ok (\<Delta> @ \<Gamma>, S)"
237 using assms(2) fresh_distinct_fv[OF assms(1)]
238 by (auto intro: heap_upds_ok_append dest: set_mp[OF ups_fv_subset])
239
240 lemma heap_upds_ok_to_stack:
241   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
242   by (auto)
243
244 lemma heap_upds_ok_to_stack':
245   "map_of \<Gamma> x = Some e \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
246   by (metis Domain.DomainI domA_def fst_eq_Domain heap_upds_ok_to_stack map_of_is_SomeD)
247
248 lemma heap_upds_ok_delete:
249   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, S)"
250   by auto
251
252 lemma heap_upds_ok_restrictA:
253   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (restrictA V \<Gamma>, S)"
254   by auto
255
256 lemma heap_upds_ok_restr_stack:
257   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>, restr_stack V S)"
258   apply auto
259   by (induction V S rule: restr_stack.induct) auto
260
261 lemma heap_upds_ok_to_heap:
262   "heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> heap_upds_ok ((x,e) # \<Gamma>, S)"
263   by auto
264
265 lemma heap_upds_ok_reorder:
266   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok ((x,e) # delete x \<Gamma>, S)"
267   by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)
268
269 lemma heap_upds_ok_upd:
270 "heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> x \<notin> domA \<Gamma> \<and> x \<notin> upds S"
271   by auto
272
273
274 lemmas heap_upds_ok_intros[intro] =
275   heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_to_stack' heap_upds_ok_reorder
276   heap_upds_ok_app1 heap_upds_ok_app2 heap_upds_ok_alts1 heap_upds_ok_alts2 heap_upds_ok_delete
277   heap_upds_ok_restrictA heap_upds_ok_restr_stack
278   heap_upds_ok_let
279 lemmas heap_upds_ok.simps[simp del]
280
281
282 end