# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307484172 -32400
# Node ID 81276d5c74381d05dc126b56609a561b4a4f85ca
# Parent  394664816e24e8b6e4f5dd1341b44ef6c55ad4d9
cbvs can be easily defined without an invariant

diff -r 394664816e24 -r 81276d5c7438 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Jun 07 20:58:00 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 08 07:02:52 2011 +0900
@@ -478,37 +478,22 @@
 termination
   by (relation "measure (size o fst)") (simp_all add: lam.size)
 
-nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+nominal_primrec
   cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
 where
   "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
 | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = (cbvs t (x # xs))"
-apply(simp add: eqvt_def cbvs_graph_def)
-apply (rule, perm_simp, rule)
-  apply (erule cbvs_graph.induct)
-  apply(simp add: fresh_star_def pure_fresh)
-  apply(simp add: fresh_star_def pure_fresh)
-  apply(simp add: fresh_star_def pure_fresh)
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-apply(simp_all add: fresh_star_def)[3]
-apply(blast)
-apply(blast)
-apply(simp_all)
-apply(elim conjE)
-apply clarify
-apply (erule Abs1_eq_fdest)
-apply (simp_all add: ln.fresh)
-apply(simp add: fresh_star_def)
-apply(drule supp_eqvt_at)
-apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2]
-apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
-apply (simp add: eqvt_at_def)
-apply (metis atom_name_def swap_fresh_fresh)
-done
-
+  apply(simp add: eqvt_def cbvs_graph_def)
+  apply(rule, perm_simp, rule)
+  apply(simp_all)
+  apply(case_tac x)
+  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply(auto simp add: fresh_star_def)
+  apply(erule Abs1_eq_fdest)
+  apply(simp_all add: pure_fresh)
+  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  done
 
 termination
   by (relation "measure (size o fst)") (simp_all add: lam.size)