equal
deleted
inserted
replaced
50 apply(auto simp add: llam.inject) |
50 apply(auto simp add: llam.inject) |
51 apply(rotate_tac 4) |
51 apply(rotate_tac 4) |
52 apply(drule_tac x="a" in meta_spec) |
52 apply(drule_tac x="a" in meta_spec) |
53 apply(blast) |
53 apply(blast) |
54 done |
54 done |
55 |
55 termination by (relation "measure (llam_size \<circ> fst)") auto |
56 termination vsub |
|
57 proof |
|
58 show "wf (measure (llam_size \<circ> fst))" by simp |
|
59 qed (auto) |
|
60 |
56 |
61 lemma vsub_eqvt[eqvt]: |
57 lemma vsub_eqvt[eqvt]: |
62 fixes pi::"name prm" |
58 fixes pi::"name prm" |
63 shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)" |
59 shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)" |
64 by (induct t arbitrary: n rule: llam.induct) |
60 by (induct t arbitrary: n rule: llam.induct) |