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 |
10 nominal_function lookup where |
11 "lookup (n :: name) m [] \<longleftrightarrow> (n = m)" |
11 "lookup (n :: name) m [] \<longleftrightarrow> (n = m)" |
12 | "lookup n m ((hn, hm) # t) \<longleftrightarrow> |
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)" |
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) |
14 apply (simp add: eqvt_def lookup_graph_def) |
15 apply (rule, perm_simp, rule, rule) |
15 apply (rule, perm_simp, rule, rule) |
16 by pat_completeness auto |
16 by pat_completeness auto |
17 |
17 |
18 termination (eqvt) by lexicographic_order |
18 termination (eqvt) by lexicographic_order |
19 |
19 |
20 nominal_primrec lam2_rec where |
20 nominal_function lam2_rec where |
21 "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs" |
21 "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs" |
22 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
22 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
23 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
23 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
24 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
24 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
25 | "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" |
95 apply metis |
95 apply metis |
96 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
96 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
97 apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def) |
97 apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def) |
98 done |
98 done |
99 |
99 |
100 nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" |
100 nominal_function aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" |
101 where |
101 where |
102 [simp del]: "aux l r xs = lam2_rec |
102 [simp del]: "aux l r xs = lam2_rec |
103 (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs)) |
103 (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs)) |
104 (%x t y s. aux t s ((x, y) # xs)) xs l r" |
104 (%x t y s. aux t s ((x, y) # xs)) xs l r" |
105 unfolding eqvt_def aux_graph_def |
105 unfolding eqvt_def aux_graph_def |
202 apply (simp add: fresh_star_def) |
202 apply (simp add: fresh_star_def) |
203 apply metis |
203 apply metis |
204 apply lexicographic_order |
204 apply lexicographic_order |
205 done |
205 done |
206 |
206 |
207 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
207 nominal_function swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
208 "swapequal l r [] \<longleftrightarrow> l = r" |
208 "swapequal l r [] \<longleftrightarrow> l = r" |
209 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
209 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
210 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
210 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
211 unfolding eqvt_def swapequal_graph_def |
211 unfolding eqvt_def swapequal_graph_def |
212 apply (rule, perm_simp, rule, rule TrueI) |
212 apply (rule, perm_simp, rule, rule TrueI) |