1.1 --- a/src/HOL/Library/Code_Index.thy	Thu Aug 28 15:33:33 2008 +0200
     1.2 +++ b/src/HOL/Library/Code_Index.thy	Thu Aug 28 17:54:18 2008 +0200
     1.3 @@ -232,6 +232,10 @@
     1.4    by (simp add: nat_of_index_aux_def)
     1.5  
     1.6  
     1.7 +text {* Measure function (for termination proofs) *}
     1.8 +
     1.9 +lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial)
    1.10 +
    1.11  subsection {* ML interface *}
    1.12  
    1.13  ML {*

     2.1 --- a/src/HOL/Library/Heap.thy	Thu Aug 28 15:33:33 2008 +0200
     2.2 +++ b/src/HOL/Library/Heap.thy	Thu Aug 28 17:54:18 2008 +0200
     2.3 @@ -40,19 +40,8 @@
     2.4  instantiation rtype :: countable
     2.5  begin
     2.6  
     2.7 -lemma list_size_size_append:
     2.8 -  "list_size size (xs @ ys) = list_size size xs + list_size size ys"
     2.9 -  by (induct xs, auto)
    2.10 -
    2.11 -lemma rtype_size: "t = RType.RType c ts \<Longrightarrow> t' \<in> set ts \<Longrightarrow> size t' < size t"
    2.12 -  by (frule split_list) (auto simp add: list_size_size_append)
    2.13 -
    2.14 -function to_nat_rtype :: "rtype \<Rightarrow> nat" where
    2.15 +fun to_nat_rtype :: "rtype \<Rightarrow> nat" where
    2.16    "to_nat_rtype (RType.RType c ts) = to_nat (to_nat c, to_nat (map to_nat_rtype ts))"
    2.17 -by pat_completeness auto
    2.18 -
    2.19 -termination by (relation "measure (\<lambda>x. size x)")
    2.20 -  (simp, simp only: in_measure rtype_size)
    2.21  
    2.22  instance
    2.23  proof (rule countable_classI)

     3.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Thu Aug 28 15:33:33 2008 +0200
     3.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Aug 28 17:54:18 2008 +0200
     3.3 @@ -627,11 +627,7 @@
     3.4  apply (force)
     3.5  apply (rule ty_cases)
     3.6  done
     3.7 -
     3.8 -termination
     3.9 -apply(relation "measure (\<lambda>(_,_,_,T). size T)")
    3.10 -apply(auto)
    3.11 -done
    3.12 +termination by lexicographic_order
    3.13  
    3.14  lemma logical_monotonicity:
    3.15   fixes \<Gamma> \<Gamma>' :: Ctxt

     4.1 --- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Aug 28 15:33:33 2008 +0200
     4.2 +++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Aug 28 17:54:18 2008 +0200
     4.3 @@ -52,11 +52,7 @@
     4.4  apply(drule_tac x="a" in meta_spec)
     4.5  apply(blast)
     4.6  done
     4.7 -
     4.8 -termination vsub
     4.9 -proof
    4.10 -  show "wf (measure (llam_size \<circ> fst))" by simp
    4.11 -qed (auto)
    4.12 +termination by (relation "measure (llam_size \<circ> fst)") auto
    4.13  
    4.14  lemma vsub_eqvt[eqvt]:
    4.15    fixes pi::"name prm" 

     5.1 --- a/src/HOL/Word/BinOperations.thy	Thu Aug 28 15:33:33 2008 +0200
     5.2 +++ b/src/HOL/Word/BinOperations.thy	Thu Aug 28 17:54:18 2008 +0200
     5.3 @@ -514,24 +514,20 @@
     5.4  definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
     5.5    "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
     5.6  
     5.7 -function bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
     5.8 +fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
     5.9    "bin_rsplit_aux n m c bs =
    5.10      (if m = 0 | n = 0 then bs else
    5.11        let (a, b) = bin_split n c 
    5.12        in bin_rsplit_aux n (m - n) a (b # bs))"
    5.13 -by pat_completeness auto
    5.14 -termination by (relation "measure (fst o snd)") simp_all
    5.15  
    5.16  definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
    5.17    "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
    5.18  
    5.19 -function bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    5.20 +fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    5.21    "bin_rsplitl_aux n m c bs =
    5.22      (if m = 0 | n = 0 then bs else
    5.23        let (a, b) = bin_split (min m n) c 
    5.24        in bin_rsplitl_aux n (m - n) a (b # bs))"
    5.25 -by pat_completeness auto
    5.26 -termination by (relation "measure (fst o snd)") simp_all
    5.27  
    5.28  definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
    5.29    "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"

     6.1 --- a/src/HOL/ex/Random.thy	Thu Aug 28 15:33:33 2008 +0200
     6.2 +++ b/src/HOL/ex/Random.thy	Thu Aug 28 17:54:18 2008 +0200
     6.3 @@ -20,15 +20,10 @@
     6.4  where
     6.5    "minus_shift r k l = (if k < l then r + k - l else k - l)"
     6.6  
     6.7 -function
     6.8 +fun
     6.9    log :: "index \<Rightarrow> index \<Rightarrow> index"
    6.10  where
    6.11    "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    6.12 -by pat_completeness auto
    6.13 -termination
    6.14 -  by (relation "measure (nat_of_index o snd)")
    6.15 -    (auto simp add: index)
    6.16 -
    6.17  
    6.18  subsection {* Random seeds *}
    6.19