equal
deleted
inserted
replaced
45 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
45 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
46 and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l" |
46 and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l" |
47 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
47 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
48 begin |
48 begin |
49 |
49 |
50 nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
50 nominal_function (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
51 f |
51 f |
52 where |
52 where |
53 "f (Var x) l = f1 x l" |
53 "f (Var x) l = f1 x l" |
54 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
54 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
55 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
55 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
155 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
155 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
156 finite (supp c)\<rbrakk> |
156 finite (supp c)\<rbrakk> |
157 \<Longrightarrow> P" |
157 \<Longrightarrow> P" |
158 sorry |
158 sorry |
159 |
159 |
160 nominal_primrec |
160 nominal_function |
161 g |
161 g |
162 where |
162 where |
163 "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t" |
163 "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t" |
164 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x" |
164 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x" |
165 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)" |
165 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)" |