1 theory Lambda imports "../Nominal2" begin |
|
2 |
|
3 atom_decl name |
|
4 |
|
5 nominal_datatype lam = |
|
6 Var "name" |
|
7 | App "lam" "lam" |
|
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
9 |
|
10 nominal_primrec lam_rec :: |
|
11 "(name \<Rightarrow> 'a :: pt) \<Rightarrow> (lam \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b :: fs \<Rightarrow> lam \<Rightarrow> 'a" |
|
12 where |
|
13 "lam_rec fv fa fl fd P (Var n) = fv n" |
|
14 | "lam_rec fv fa fl fd P (App l r) = fa l r" |
|
15 | "(atom x \<sharp> P \<and> (\<forall>y s. atom y \<sharp> P \<longrightarrow> Lam [x]. t = Lam [y]. s \<longrightarrow> fl x t = fl y s)) \<Longrightarrow> |
|
16 lam_rec fv fa fl fd P (Lam [x]. t) = fl x t" |
|
17 | "(atom x \<sharp> P \<and> \<not>(\<forall>y s. atom y \<sharp> P \<longrightarrow> Lam [x]. t = Lam [y]. s \<longrightarrow> fl x t = fl y s)) \<Longrightarrow> |
|
18 lam_rec fv fa fl fd P (Lam [x]. t) = fd" |
|
19 apply (simp add: eqvt_def lam_rec_graph_def) |
|
20 apply (rule, perm_simp, rule, rule) |
|
21 apply (case_tac x) |
|
22 apply (rule_tac y="f" and c="e" in lam.strong_exhaust) |
|
23 apply metis |
|
24 apply metis |
|
25 unfolding fresh_star_def |
|
26 apply simp |
|
27 apply metis |
|
28 apply simp_all[2] |
|
29 apply (metis (no_types) Pair_inject lam.distinct)+ |
|
30 apply simp |
|
31 apply (metis (no_types) Pair_inject lam.distinct)+ |
|
32 done |
|
33 |
|
34 termination (eqvt) by lexicographic_order |
|
35 |
|
36 lemma lam_rec_cong[fundef_cong]: |
|
37 " (\<And>v. l = Var v \<Longrightarrow> fv v = fv' v) \<Longrightarrow> |
|
38 (\<And>t1 t2. l = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow> |
|
39 (\<And>n t. l = Lam [n]. t \<Longrightarrow> fl n t = fl' n t) \<Longrightarrow> |
|
40 lam_rec fv fa fl fd P l = lam_rec fv' fa' fl' fd P l" |
|
41 apply (rule_tac y="l" and c="P" in lam.strong_exhaust) |
|
42 apply auto |
|
43 apply (case_tac "(\<forall>y s. atom y \<sharp> P \<longrightarrow> Lam [name]. lam = Lam [y]. s \<longrightarrow> fl name lam = fl y s)") |
|
44 apply (subst lam_rec.simps) apply (simp add: fresh_star_def) |
|
45 apply (subst lam_rec.simps) apply (simp add: fresh_star_def) |
|
46 using Abs1_eq_iff lam.eq_iff apply metis |
|
47 apply (subst lam_rec.simps(4)) apply (simp add: fresh_star_def) |
|
48 apply (subst lam_rec.simps(4)) apply (simp add: fresh_star_def) |
|
49 using Abs1_eq_iff lam.eq_iff apply metis |
|
50 done |
|
51 |
|
52 nominal_primrec substr where |
|
53 [simp del]: "substr l y s = lam_rec |
|
54 (%x. if x = y then s else (Var x)) |
|
55 (%t1 t2. App (substr t1 y s) (substr t2 y s)) |
|
56 (%x t. Lam [x]. (substr t y s)) (Lam [y]. Var y) (y, s) l" |
|
57 unfolding eqvt_def substr_graph_def |
|
58 apply (rule, perm_simp, rule, rule) |
|
59 by pat_completeness auto |
|
60 |
|
61 termination (eqvt) by lexicographic_order |
|
62 |
|
63 lemma fresh_fun_eqvt_app3: |
|
64 assumes e: "eqvt f" |
|
65 shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z" |
|
66 using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types)) |
|
67 |
|
68 lemma substr_simps: |
|
69 "substr (Var x) y s = (if x = y then s else (Var x))" |
|
70 "substr (App t1 t2) y s = App (substr t1 y s) (substr t2 y s)" |
|
71 "atom x \<sharp> (y, s) \<Longrightarrow> substr (Lam [x]. t) y s = Lam [x]. (substr t y s)" |
|
72 apply (subst substr.simps) apply (simp only: lam_rec.simps) |
|
73 apply (subst substr.simps) apply (simp only: lam_rec.simps) |
|
74 apply (subst substr.simps) apply (subst lam_rec.simps) |
|
75 apply (auto simp add: Abs1_eq_iff substr.eqvt swap_fresh_fresh) |
|
76 apply (rule fresh_fun_eqvt_app3[of substr]) |
|
77 apply (simp add: eqvt_def eqvts_raw) |
|
78 apply (simp_all add: fresh_Pair) |
|
79 done |
|
80 |
|
81 end |
|
82 |
|
83 |
|
84 |
|