5 nominal_datatype lam = |
5 nominal_datatype lam = |
6 Var "name" |
6 Var "name" |
7 | App "lam" "lam" |
7 | App "lam" "lam" |
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
9 |
9 |
|
10 nominal_primrec lookup where |
|
11 "lookup (n :: name) m [] \<longleftrightarrow> (n = m)" |
|
12 | "lookup n m ((hn, hm) # t) \<longleftrightarrow> |
|
13 (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)" |
|
14 apply (simp add: eqvt_def lookup_graph_def) |
|
15 apply (rule, perm_simp, rule, rule) |
|
16 by pat_completeness auto |
|
17 |
|
18 termination (eqvt) by lexicographic_order |
|
19 |
10 nominal_primrec lam2_rec where |
20 nominal_primrec lam2_rec where |
11 "lam2_rec faa fll xs (Var n) (Var m) = (n = m \<or> (n, m) \<in> set xs)" |
21 "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs" |
12 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
22 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
13 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
23 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
14 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
24 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
15 | "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2" |
25 | "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2" |
16 | "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False" |
26 | "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False" |
210 apply (simp add: fresh_star_def) |
220 apply (simp add: fresh_star_def) |
211 apply metis |
221 apply metis |
212 apply lexicographic_order |
222 apply lexicographic_order |
213 done |
223 done |
214 |
224 |
|
225 lemma foldr_eqvt[eqvt]: |
|
226 "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)" |
|
227 apply (induct b) |
|
228 apply simp_all |
|
229 apply (perm_simp) |
|
230 apply simp |
|
231 done |
|
232 |
|
233 nominal_primrec |
|
234 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
|
235 where |
|
236 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
237 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
238 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
239 unfolding eqvt_def subst_graph_def |
|
240 apply (rule, perm_simp, rule) |
|
241 apply(rule TrueI) |
|
242 apply(auto) |
|
243 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
244 apply(blast)+ |
|
245 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
|
246 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
|
247 apply(simp_all add: Abs_fresh_iff) |
|
248 apply(simp add: fresh_star_def fresh_Pair) |
|
249 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
250 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
251 done |
|
252 |
|
253 termination (eqvt) by lexicographic_order |
|
254 |
|
255 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
|
256 "swapequal l r [] \<longleftrightarrow> l = r" |
|
257 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
|
258 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
|
259 unfolding eqvt_def swapequal_graph_def |
|
260 apply (rule, perm_simp, rule) |
|
261 apply(rule TrueI) |
|
262 apply (case_tac x) |
|
263 apply (case_tac c) |
|
264 apply metis |
|
265 apply (case_tac aa) |
|
266 apply (rename_tac l r lst h t hl hr) |
|
267 apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh) |
|
268 apply simp |
|
269 apply simp |
|
270 apply simp |
|
271 sorry |
|
272 |
|
273 termination (eqvt) by lexicographic_order |
|
274 |
|
275 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs" |
|
276 apply (induct xs arbitrary: m n) |
|
277 apply simp |
|
278 apply (case_tac a) |
|
279 apply simp |
|
280 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
281 apply (subst swapequal.simps) |
|
282 apply (simp add: fresh_Pair lam.fresh fresh_Nil) |
|
283 apply (case_tac "n = aa \<and> m = b") |
|
284 apply simp |
|
285 defer |
|
286 apply (case_tac "n = aa") |
|
287 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
288 defer |
|
289 apply (simp add: fresh_Pair_elim fresh_at_base flip_def) |
|
290 apply (case_tac "m = b") |
|
291 apply simp |
|
292 defer |
|
293 apply simp |
|
294 sorry |
|
295 |
|
296 (* |
|
297 lemma lookup_property: |
|
298 assumes "distinct (map fst xs @ map snd xs)" |
|
299 shows "aux (Var n) (Var m) xs = swapequal (Var n) (Var m) xs" |
|
300 using assms |
|
301 apply (induct xs arbitrary: n m) |
|
302 apply simp |
|
303 apply simp |
|
304 apply (case_tac a) |
|
305 apply simp |
|
306 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
307 apply (subst swapequal.simps) |
|
308 apply (simp add: fresh_Pair lam.fresh fresh_Cons) |
|
309 apply auto[1] |
|
310 |
|
311 apply (case_tac "n = aa \<and> m = b") |
|
312 apply simp |
|
313 proof - |
|
314 have "lookup n m xs = (fold (\<lambda>(x, y) t. if n = t then y else t) xs n = m)" |
|
315 using assms |
|
316 proof (induct xs, simp) |
|
317 fix a b xs |
|
318 assume d: "distinct (map fst xs @ map snd xs) \<Longrightarrow> |
|
319 lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" |
|
320 assume "distinct (map fst (a # xs) @ map snd (a # xs))" |
|
321 then have "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" |
|
322 using d by simp |
|
323 then show "lookup n m (a # xs) = |
|
324 (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)" |
|
325 proof (cases a) |
|
326 case (Pair b c) |
|
327 assume "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" "a = (b, c)" |
|
328 then show "lookup n m (a # xs) = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)" |
|
329 apply simp |
|
330 apply auto |
|
331 sledgehammer |
|
332 |
|
333 apply - |
|
334 apply (case_tac a) |
|
335 apply auto |
|
336 |
|
337 |
|
338 apply simp |
|
339 apply (case_tac a) |
|
340 apply simp |
|
341 apply metis |
|
342 also have "... = (Var (foldr (\<lambda>(x, y) t. if n = t then y else t) xs n) = Var m)" by simp |
|
343 also have "... = (foldr (\<lambda>(x, y) t. subst t x (Var y)) xs (Var n) = Var m)" |
|
344 apply (rule arg_cong) back |
|
345 apply (induct xs) |
|
346 apply simp |
|
347 apply (case_tac a) |
|
348 apply simp |
|
349 apply auto |
|
350 find_theorems "fold _ _ _ = fold _ _ _" |
|
351 apply (induct xs) apply simp |
|
352 apply simp |
|
353 apply (case_tac a) |
|
354 apply simp |
|
355 apply (simp only: lookup.simps) |
|
356 apply simp |
|
357 apply clarify |
|
358 apply (case_tac "n = aa") |
|
359 apply (case_tac "m = ba") |
|
360 apply simp |
|
361 apply (induct_tac xs) |
|
362 apply simp |
|
363 apply simp |
|
364 sorry*) |
|
365 |
|
366 lemma reord: " |
|
367 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
|
368 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
|
369 sorry |
|
370 |
|
371 lemma need: |
|
372 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
|
373 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |
|
374 using assms |
|
375 apply (induct xs arbitrary: t s x y) |
|
376 apply (rule_tac x="(x, y, t, s)" and ?'a="name" in obtain_fresh) |
|
377 apply (simp add: fresh_Pair_elim fresh_Nil) |
|
378 apply (subst swapequal.simps) |
|
379 apply (simp add: fresh_Pair fresh_Nil) |
|
380 apply auto[1] |
|
381 apply simp |
|
382 apply (subgoal_tac "[[atom x]]lst. t = [[atom a]]lst. ((x \<leftrightarrow> a) \<bullet> t)") |
|
383 apply (subgoal_tac "[[atom y]]lst. s = [[atom a]]lst. ((y \<leftrightarrow> a) \<bullet> s)") |
|
384 apply simp |
|
385 apply (simp add: Abs1_eq_iff) |
|
386 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1] |
|
387 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
|
388 apply (simp add: Abs1_eq_iff) |
|
389 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1] |
|
390 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
|
391 apply clarify |
|
392 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
|
393 apply clarify |
|
394 apply (subst reord) |
|
395 apply auto[4] |
|
396 apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh) |
|
397 apply (rename_tac f) |
|
398 apply (subst (2) swapequal.simps) |
|
399 apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons) |
|
400 apply auto[1] |
|
401 apply (subst swapequal.simps) |
|
402 apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons) |
|
403 apply auto[1] |
|
404 apply simp |
|
405 apply (simp add: flip_def) |
|
406 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
407 done |
|
408 |
|
409 lemma aux_alphaish: |
|
410 assumes "distinct (map fst xs @ map snd xs)" |
|
411 shows "aux x y xs \<longleftrightarrow> swapequal x y xs" |
|
412 using assms |
|
413 apply (induct xs x y rule: aux_induct) |
|
414 apply (simp add: lookup_swapequal) |
|
415 prefer 8 |
|
416 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
|
417 apply (elim conjE) |
|
418 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
|
419 apply (subgoal_tac "x \<notin> fst ` set xs \<and> |
|
420 x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs") |
|
421 apply (simp) |
|
422 apply (subst need) |
|
423 apply auto[1] |
|
424 sorry |
|
425 |
|
426 lemma |
|
427 "aux x y [] \<longleftrightarrow> (x = y)" |
|
428 by (simp_all add: supp_Nil aux_alphaish) |
|
429 |
215 end |
430 end |
216 |
431 |
217 |
432 |
218 |
433 |