153 apply clarify |
153 apply clarify |
154 apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'") |
154 apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'") |
155 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff) |
155 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff) |
156 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+ |
156 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+ |
157 |
157 |
158 termination |
158 termination (eqvt) by (relation "measure size") (simp_all) |
159 by (relation "measure size") (simp_all add: lt.size) |
|
160 |
159 |
161 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim] |
160 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim] |
162 |
161 |
163 lemma [simp]: "supp (M*) = supp M" |
162 lemma [simp]: "supp (M*) = supp M" |
164 by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair) |
163 by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair) |
165 (simp_all only: atom_eq_iff[symmetric], blast+) |
164 (simp_all only: atom_eq_iff[symmetric], blast+) |
166 |
165 |
167 lemma [simp]: "x \<sharp> M* = x \<sharp> M" |
166 lemma [simp]: "x \<sharp> M* = x \<sharp> M" |
168 unfolding fresh_def by simp |
167 unfolding fresh_def by simp |
169 |
|
170 (* Will be provided automatically by nominal_primrec *) |
|
171 lemma CPS_eqvt[eqvt]: |
|
172 shows "p \<bullet> M* = (p \<bullet> M)*" |
|
173 apply (induct M rule: lt.induct) |
|
174 apply (rule_tac x="(name, p \<bullet> name, p)" and ?'a="name" in obtain_fresh) |
|
175 apply simp |
|
176 apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric]) |
|
177 apply (metis atom_eqvt flip_fresh_fresh fresh_perm atom_eq_iff fresh_at_base) |
|
178 apply (rule_tac x="(name, lt, p \<bullet> name, p \<bullet> lt, p)" and ?'a="name" in obtain_fresh) |
|
179 apply simp |
|
180 apply (metis atom_eqvt fresh_perm atom_eq_iff) |
|
181 apply (rule_tac x="(lt1, p \<bullet> lt1, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh) |
|
182 apply (rule_tac x="(a, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh) |
|
183 apply (rule_tac x="(a, aa, p)" and ?'a="name" in obtain_fresh) |
|
184 apply (simp) |
|
185 apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric]) |
|
186 apply (metis atom_eqvt fresh_perm atom_eq_iff) |
|
187 done |
|
188 |
168 |
189 nominal_primrec |
169 nominal_primrec |
190 convert:: "lt => lt" ("_+" [250] 250) |
170 convert:: "lt => lt" ("_+" [250] 250) |
191 where |
171 where |
192 "(Var x)+ = Var x" |
172 "(Var x)+ = Var x" |
195 unfolding convert_graph_def eqvt_def |
175 unfolding convert_graph_def eqvt_def |
196 apply (rule, perm_simp, rule, rule) |
176 apply (rule, perm_simp, rule, rule) |
197 apply (erule lt.exhaust) |
177 apply (erule lt.exhaust) |
198 apply (simp_all) |
178 apply (simp_all) |
199 apply blast |
179 apply blast |
200 apply (simp add: Abs1_eq_iff CPS_eqvt) |
180 apply (simp add: Abs1_eq_iff CPS.eqvt) |
201 by blast |
181 by blast |
202 |
182 |
203 termination |
183 termination (eqvt) |
204 by (relation "measure size") (simp_all add: lt.size) |
184 by (relation "measure size") (simp_all) |
205 |
185 |
206 lemma convert_supp[simp]: |
186 lemma convert_supp[simp]: |
207 shows "supp (M+) = supp M" |
187 shows "supp (M+) = supp M" |
208 by (induct M rule: lt.induct, simp_all add: lt.supp) |
188 by (induct M rule: lt.induct, simp_all add: lt.supp) |
209 |
189 |
210 lemma convert_fresh[simp]: |
190 lemma convert_fresh[simp]: |
211 shows "x \<sharp> (M+) = x \<sharp> M" |
191 shows "x \<sharp> (M+) = x \<sharp> M" |
212 unfolding fresh_def by simp |
192 unfolding fresh_def by simp |
213 |
|
214 lemma convert_eqvt[eqvt]: |
|
215 shows "p \<bullet> (M+) = (p \<bullet> M)+" |
|
216 by (nominal_induct M rule: lt.strong_induct, auto simp add: CPS_eqvt) |
|
217 |
193 |
218 lemma [simp]: |
194 lemma [simp]: |
219 shows "isValue (p \<bullet> (M::lt)) = isValue M" |
195 shows "isValue (p \<bullet> (M::lt)) = isValue M" |
220 by (nominal_induct M rule: lt.strong_induct) auto |
196 by (nominal_induct M rule: lt.strong_induct) auto |
221 |
197 |
263 apply rule |
239 apply rule |
264 apply (auto simp add: flip_fresh_fresh[symmetric]) |
240 apply (auto simp add: flip_fresh_fresh[symmetric]) |
265 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+ |
241 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+ |
266 done |
242 done |
267 |
243 |
268 termination |
244 termination (eqvt) |
269 by (relation "measure (\<lambda>(t, _). size t)") (simp_all add: lt.size) |
245 by (relation "measure (\<lambda>(t, _). size t)") (simp_all) |
270 |
246 |
271 section{* lemma related to Kapply *} |
247 section{* lemma related to Kapply *} |
272 |
248 |
273 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)" |
249 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)" |
274 by (nominal_induct V rule: lt.strong_induct) auto |
250 by (nominal_induct V rule: lt.strong_induct) auto |