equal
deleted
inserted
replaced
109 apply(perm_simp) |
109 apply(perm_simp) |
110 apply(rule) |
110 apply(rule) |
111 done |
111 done |
112 |
112 |
113 |
113 |
114 nominal_primrec |
114 nominal_function |
115 height_trm :: "trm \<Rightarrow> nat" |
115 height_trm :: "trm \<Rightarrow> nat" |
116 where |
116 where |
117 "height_trm (Var x) = 1" |
117 "height_trm (Var x) = 1" |
118 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
118 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
119 | "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)" |
119 | "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)" |
141 |
141 |
142 (* assn-function prevents automatic discharge |
142 (* assn-function prevents automatic discharge |
143 termination by lexicographic_order |
143 termination by lexicographic_order |
144 *) |
144 *) |
145 |
145 |
146 nominal_primrec |
146 nominal_function |
147 subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
147 subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
148 where |
148 where |
149 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
149 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
150 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
150 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
151 | "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> |
151 | "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> |
195 |
195 |
196 oops |
196 oops |
197 |
197 |
198 |
198 |
199 |
199 |
200 nominal_primrec |
200 nominal_function |
201 <<<<<<< variant A |
201 <<<<<<< variant A |
202 (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2") |
202 (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2") |
203 >>>>>>> variant B |
203 >>>>>>> variant B |
204 ####### Ancestor |
204 ####### Ancestor |
205 (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y") |
205 (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y") |
332 apply(simp_all add: trm_assn.fv_defs supp_at_base) |
332 apply(simp_all add: trm_assn.fv_defs supp_at_base) |
333 done |
333 done |
334 |
334 |
335 text {* works, but only because no recursion in as *} |
335 text {* works, but only because no recursion in as *} |
336 |
336 |
337 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
337 nominal_function (invariant "\<lambda>x (y::atom set). finite y") |
338 frees_set :: "trm \<Rightarrow> atom set" |
338 frees_set :: "trm \<Rightarrow> atom set" |
339 where |
339 where |
340 "frees_set (Var x) = {atom x}" |
340 "frees_set (Var x) = {atom x}" |
341 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
341 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
342 | "frees_set (Let as t) = (frees_set t) - (set (bn as)) \<union> (fv_bn as)" |
342 | "frees_set (Let as t) = (frees_set t) - (set (bn as)) \<union> (fv_bn as)" |
379 back |
379 back |
380 apply(simp) |
380 apply(simp) |
381 done |
381 done |
382 |
382 |
383 |
383 |
384 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
384 nominal_function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
385 subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and |
385 subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and |
386 subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90) |
386 subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90) |
387 where |
387 where |
388 "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))" |
388 "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))" |
389 | "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])" |
389 | "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])" |