equal
deleted
inserted
replaced
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 lam_rec :: |
10 nominal_function 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" |
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 |
12 where |
13 "lam_rec fv fa fl fd P (Var n) = fv n" |
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" |
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> |
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> |
47 apply (subst lam_rec.simps(4)) apply (simp add: fresh_star_def) |
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) |
48 apply (subst lam_rec.simps(4)) apply (simp add: fresh_star_def) |
49 using Abs1_eq_iff lam.eq_iff apply metis |
49 using Abs1_eq_iff lam.eq_iff apply metis |
50 done |
50 done |
51 |
51 |
52 nominal_primrec substr where |
52 nominal_function substr where |
53 [simp del]: "substr l y s = lam_rec |
53 [simp del]: "substr l y s = lam_rec |
54 (%x. if x = y then s else (Var x)) |
54 (%x. if x = y then s else (Var x)) |
55 (%t1 t2. App (substr t1 y s) (substr t2 y s)) |
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" |
56 (%x t. Lam [x]. (substr t y s)) (Lam [y]. Var y) (y, s) l" |
57 unfolding eqvt_def substr_graph_def |
57 unfolding eqvt_def substr_graph_def |