925031305ed557a583764b23df0bf9ded4f4a945
[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
34 instance stack_elem :: fs  by (default, case_tac x) (auto simp add: finite_supp)
35
36 type_synonym stack = "stack_elem list"
37
38 fun ap :: "stack \<Rightarrow> var set" where
39   "ap [] = {}"
40 | "ap (Alts e1 e2 # S) = ap S"
41 | "ap (Arg x # S) = insert x (ap S)"
42 | "ap (Upd x # S) = ap S"
43 | "ap (Dummy x # S) = ap S"
44 fun upds :: "stack \<Rightarrow> var set" where
45   "upds [] = {}"
46 | "upds (Alts e1 e2 # S) = upds S"
47 | "upds (Upd x # S) = insert x (upds S)"
48 | "upds (Arg x # S) = upds S"
49 | "upds (Dummy x # S) = upds S"
50 fun flattn :: "stack \<Rightarrow> var list" where
51   "flattn [] = []"
52 | "flattn (Alts e1 e2 # S) = fv_list e1 @ fv_list e2 @ flattn S"
53 | "flattn (Upd x # S) = x # flattn S"
54 | "flattn (Arg x # S) = x # flattn S"
55 | "flattn (Dummy x # S) = x # flattn S"
56 fun upds_list :: "stack \<Rightarrow> var list" where
57   "upds_list [] = []"
58 | "upds_list (Alts e1 e2 # S) = upds_list S"
59 | "upds_list (Upd x # S) = x # upds_list S"
60 | "upds_list (Arg x # S) = upds_list S"
61 | "upds_list (Dummy x # S) = upds_list S"
62
63 lemma set_upds_list[simp]:
64   "set (upds_list S) = upds S"
65   by (induction S rule: upds_list.induct) auto
66
67 lemma ups_fv_subset: "upds S \<subseteq> fv S"
68   by (induction S rule: upds.induct) auto
69 lemma ap_fv_subset: "ap S \<subseteq> fv S"
70   by (induction S rule: upds.induct) auto
71
72 lemma fresh_flattn[simp]: "atom (a::var) \<sharp> flattn S \<longleftrightarrow> atom a \<sharp> S"
73   by (induction S rule:flattn.induct) (auto simp add: fresh_Nil fresh_Cons fresh_append fresh_fv[OF finite_fv])
74 lemma fresh_star_flattn[simp]: "atom ` (as:: var set) \<sharp>* flattn S \<longleftrightarrow> atom ` as \<sharp>* S"
75   by (auto simp add: fresh_star_def)
76
77 type_synonym conf = "(heap \<times> exp \<times> stack)"
78
79 inductive boring_step where
80   "isVal e \<Longrightarrow> boring_step (\<Gamma>, e, Upd x # S)"
81
82
83 fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
84   where "restr_stack V [] = []"
85       | "restr_stack V (Alts e1 e2 # S) = Alts e1 e2 # restr_stack V S"
86       | "restr_stack V (Arg x # S) = Arg x # restr_stack V S"
87       | "restr_stack V (Upd x # S) = (if x \<in> V then Upd x # restr_stack V S else restr_stack V S)"
88       | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"
89
90 lemma restr_stack_cong:
91   "(\<And> x. x \<in> upds S \<Longrightarrow> x \<in> V \<longleftrightarrow> x \<in> V') \<Longrightarrow> restr_stack V S = restr_stack V' S"
92   by (induction V S rule: restr_stack.induct) auto
93
94 lemma upds_restr_stack[simp]: "upds (restr_stack V S) = upds S \<inter> V"
95   by (induction V S rule: restr_stack.induct) auto
96
97 lemma fresh_star_restict_stack[intro]:
98   "a \<sharp>* S \<Longrightarrow> a \<sharp>* restr_stack V S"
99   by (induction V S rule: restr_stack.induct) (auto simp add: fresh_star_Cons)
100
101 lemma restr_stack_restr_stack[simp]:
102   "restr_stack V (restr_stack V' S) = restr_stack (V \<inter> V') S"
103   by (induction V S rule: restr_stack.induct) auto
104
105 lemma Upd_eq_restr_stackD:
106   assumes "Upd x # S = restr_stack V S'"
107   shows "x \<in> V"
108   using arg_cong[where f = upds, OF assms]
109   by auto
110 lemma Upd_eq_restr_stackD2:
111   assumes "restr_stack V S' = Upd x # S"
112   shows "x \<in> V"
113   using arg_cong[where f = upds, OF assms]
114   by auto
115
116
117 lemma restr_stack_noop[simp]:
118   "restr_stack V S = S \<longleftrightarrow> upds S \<subseteq> V"
119   by (induction V S rule: restr_stack.induct)
120      (auto dest: Upd_eq_restr_stackD2)
121   
122
123   
124
125
126 fun heap_upds_ok where "heap_upds_ok (\<Gamma>,S) \<longleftrightarrow> domA \<Gamma> \<inter> upds S = {} \<and> distinct (upds_list S)"
127
128 abbreviation heap_upds_ok_conf :: "conf \<Rightarrow> bool"
129   where "heap_upds_ok_conf c \<equiv> heap_upds_ok (fst c, snd (snd c))"
130
131 lemma heap_upds_okE: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> upds S"
132   by auto
133
134 lemma heap_upds_ok_Nil[simp]: "heap_upds_ok (\<Gamma>, [])" by auto
135 lemma heap_upds_ok_app1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Arg x # S)" by auto
136 lemma heap_upds_ok_app2: "heap_upds_ok (\<Gamma>, Arg x # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
137 lemma heap_upds_ok_alts1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Alts e1 e2 # S)" by auto
138 lemma heap_upds_ok_alts2: "heap_upds_ok (\<Gamma>, Alts e1 e2 # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
139
140 lemma heap_upds_ok_append:
141   assumes "domA \<Delta> \<inter> domA \<Gamma> = {}"
142   assumes "domA \<Delta> \<inter> upds S = {}"
143   assumes "heap_upds_ok (\<Gamma>,S)"
144   shows "heap_upds_ok (\<Delta>@\<Gamma>, S)"
145   using assms
146   unfolding heap_upds_ok.simps
147   by auto
148
149 lemma heap_upds_ok_to_stack:
150   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
151   by (auto)
152
153 lemma heap_upds_ok_to_stack':
154   "map_of \<Gamma> x = Some e \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
155   by (metis Domain.DomainI domA_def fst_eq_Domain heap_upds_ok_to_stack map_of_is_SomeD)
156
157 lemma heap_upds_ok_delete:
158   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, S)"
159   by auto
160
161 lemma heap_upds_ok_restrictA:
162   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (restrictA V \<Gamma>, S)"
163   by auto
164
165 lemma heap_upds_ok_restr_stack:
166   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>, restr_stack V S)"
167   apply auto
168   by (induction V S rule: restr_stack.induct) auto
169
170 lemma heap_upds_ok_to_heap:
171   "heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> heap_upds_ok ((x,e) # \<Gamma>, S)"
172   by auto
173
174 lemma heap_upds_ok_reorder:
175   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok ((x,e) # delete x \<Gamma>, S)"
176   by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)
177
178 lemma heap_upds_ok_upd:
179 "heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> x \<notin> domA \<Gamma> \<and> x \<notin> upds S"
180   by auto
181
182
183 lemmas heap_upds_ok_intros[intro] =
184   heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_to_stack' heap_upds_ok_reorder
185   heap_upds_ok_app1 heap_upds_ok_app2 heap_upds_ok_alts1 heap_upds_ok_alts2 heap_upds_ok_delete
186   heap_upds_ok_restrictA heap_upds_ok_restr_stack
187 lemmas heap_upds_ok.simps[simp del]
188
189
190 end