equal
deleted
inserted
replaced
131 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
131 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
132 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" |
132 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" |
133 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
133 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
134 begin |
134 begin |
135 |
135 |
136 nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
136 nominal_function (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
137 f |
137 f |
138 where |
138 where |
139 "f (Var x) l = f1 x l" |
139 "f (Var x) l = f1 x l" |
140 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
140 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
141 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
141 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
242 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
242 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
243 finite (supp c)\<rbrakk> |
243 finite (supp c)\<rbrakk> |
244 \<Longrightarrow> P" |
244 \<Longrightarrow> P" |
245 sorry |
245 sorry |
246 |
246 |
247 nominal_primrec |
247 nominal_function |
248 g |
248 g |
249 where |
249 where |
250 "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t" |
250 "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t" |
251 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x" |
251 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x" |
252 | "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)" |
252 | "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)" |