--- a/Nominal/Ex/Lambda.thy	Wed Jun 15 12:52:48 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 15 22:36:59 2011 +0100
@@ -10,6 +10,36 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+
+text {* free name function - returns an atom list *}
+
+nominal_primrec 
+  frees_lst :: "lam \<Rightarrow> atom list"
+where
+  "frees_lst (Var x) = [atom x]"
+| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
+| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
+  unfolding eqvt_def frees_lst_graph_def
+  apply (rule, perm_simp, rule)
+apply(rule TrueI)
+apply(rule_tac y="x" in lam.exhaust)
+apply(auto)
+apply (erule Abs_lst1_fcb)
+apply(simp add: supp_removeAll fresh_def)
+apply(drule supp_eqvt_at)
+apply(simp add: finite_supp)
+apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def)
+done
+
+termination
+  by lexicographic_order
+
+text {* a small test lemma *}
+lemma shows "supp t = set (frees_lst t)"
+  by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
+
+text {* free name function - returns an atom set *}
+
 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "lam \<Rightarrow> atom set"
 where
@@ -30,7 +60,7 @@
   done
 
 termination 
-  by (relation "measure size") (auto simp add: lam.size)
+  by lexicographic_order
 
 lemma "frees_set t = supp t"
   by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base)
@@ -42,6 +72,9 @@
   using fresh_fun_eqvt_app[OF a b(1)] a b
   by (metis fresh_fun_app)
 
+
+text {* A test with a locale and an interpretation. *}
+
 locale test =
    fixes f1::"name \<Rightarrow> ('a::pt)"
      and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)"
@@ -78,18 +111,10 @@
   done
 
 termination
-  by (relation "measure size") (auto simp add: lam.size)
-
-thm f.simps
+  by lexicographic_order
 
 end
 
-
-thm test.f.simps
-thm test.f.simps[simplified test_def]
-
-thm test_def
-
 interpretation hei: test
   "%n. (1 :: nat)"
   "%t1 t2 r1 r2. (r1 + r2)"
@@ -100,44 +125,6 @@
   apply (simp_all add: eqvt_def permute_fun_def permute_pure)
   done
 
-thm hei.f.simps
-
-inductive 
-  triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
-where
-  Var: "triv (Var x) n"
-| App: "\<lbrakk>triv t1 n; triv t2 n\<rbrakk> \<Longrightarrow> triv (App t1 t2) n"
-
-lemma 
-  "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)"
-unfolding triv_def
-apply(perm_simp)
-apply(rule refl)
-oops
-(*apply(perm_simp)*)
-
-ML {*
-  Inductive.the_inductive @{context} "Lambda.triv"
-*}
-
-thm triv_def
-
-equivariance triv
-nominal_inductive triv avoids Var: "{}::name set"
-apply(auto simp add: fresh_star_def) 
-done
-
-inductive 
-  triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" 
-where
-  Var1: "triv2 (Var x) 0"
-| Var2: "triv2 (Var x) (n + n)"
-| Var3: "triv2 (Var x) n"
-
-equivariance triv2
-nominal_inductive triv2 .
-
-
 text {* height function *}
 
 nominal_primrec
@@ -156,38 +143,11 @@
 done
 
 termination
-  by (relation "measure size") (simp_all add: lam.size)
+  by lexicographic_order
   
 thm height.simps
 
   
-text {* free name function - returns atom lists *}
-
-nominal_primrec 
-  frees_lst :: "lam \<Rightarrow> atom list"
-where
-  "frees_lst (Var x) = [atom x]"
-| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
-| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
-  unfolding eqvt_def frees_lst_graph_def
-  apply (rule, perm_simp, rule)
-apply(rule TrueI)
-apply(rule_tac y="x" in lam.exhaust)
-apply(auto)
-apply (erule Abs_lst1_fcb)
-apply(simp add: supp_removeAll fresh_def)
-apply(drule supp_eqvt_at)
-apply(simp add: finite_supp)
-apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def)
-done
-
-termination
-  by (relation "measure size") (simp_all add: lam.size)
-
-text {* a small test lemma *}
-lemma shows "supp t = set (frees_lst t)"
-  by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
-
 text {* capture - avoiding substitution *}
 
 nominal_primrec
@@ -213,8 +173,10 @@
 apply(simp_all add: swap_fresh_fresh)
 done
 
+declare lam.size[simp]
+
 termination
-  by (relation "measure (\<lambda>(t,_,_). size t)") (simp_all add: lam.size)
+  by lexicographic_order
 
 lemma subst_eqvt[eqvt]:
   shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
@@ -335,8 +297,6 @@
   finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp
 qed
 
-
-
 section {* Locally Nameless Terms *}
 
 nominal_datatype ln = 
@@ -374,6 +334,8 @@
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
+text {* Function that translates lambda-terms into locally nameless terms *}
+
 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
@@ -397,16 +359,17 @@
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   done
 
+termination
+  by lexicographic_order
 
-termination
-  by (relation "measure (size o fst)") (simp_all add: lam.size)
+text {* count bound-variable occurences *}
 
 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))"
+| "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(simp_all)
@@ -419,8 +382,9 @@
   done
 
 termination
-  by (relation "measure (size o fst)") (simp_all add: lam.size)
+  by lexicographic_order
 
+section {* De Bruijn Terms *}
 
 nominal_datatype db = 
   DBVar nat
@@ -486,7 +450,7 @@
   done
 
 termination
-  by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size)
+  by lexicographic_order
 
 lemma transdb_eqvt[eqvt]:
   "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)"
@@ -502,7 +466,8 @@
 
 lemma db_trans_test:
   assumes a: "y \<noteq> x"
-  shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
+  shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = 
+  Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
   using a by simp
 
 abbreviation
@@ -656,7 +621,7 @@
   done
 
 termination
-  by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size)
+  by lexicographic_order
 
 nominal_primrec
   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"

--- a/Nominal/Nominal2.thy	Wed Jun 15 12:52:48 2011 +0100
+++ b/Nominal/Nominal2.thy	Wed Jun 15 22:36:59 2011 +0100
@@ -464,7 +464,7 @@
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
-     ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
+     ||>> Local_Theory.note ((thms_suffix "size", [simp_attr]), qsize_simps)
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) 
      ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts)