# HG changeset patch
# User krauss
# Date 1219938858 -7200
# Node ID 1471f2974eb197c80ef37834ed6119c71fc6ddaa
# Parent  f496e9f343b7aa3caad175388aab136471118a73
more function -> fun

diff -r f496e9f343b7 -r 1471f2974eb1 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -232,6 +232,10 @@
   by (simp add: nat_of_index_aux_def)
 
 
+text {* Measure function (for termination proofs) *}
+
+lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial)
+
 subsection {* ML interface *}
 
 ML {*
diff -r f496e9f343b7 -r 1471f2974eb1 src/HOL/Library/Heap.thy
--- a/src/HOL/Library/Heap.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Library/Heap.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -40,19 +40,8 @@
 instantiation rtype :: countable
 begin
 
-lemma list_size_size_append:
-  "list_size size (xs @ ys) = list_size size xs + list_size size ys"
-  by (induct xs, auto)
-
-lemma rtype_size: "t = RType.RType c ts \<Longrightarrow> t' \<in> set ts \<Longrightarrow> size t' < size t"
-  by (frule split_list) (auto simp add: list_size_size_append)
-
-function to_nat_rtype :: "rtype \<Rightarrow> nat" where
+fun to_nat_rtype :: "rtype \<Rightarrow> nat" where
   "to_nat_rtype (RType.RType c ts) = to_nat (to_nat c, to_nat (map to_nat_rtype ts))"
-by pat_completeness auto
-
-termination by (relation "measure (\<lambda>x. size x)")
-  (simp, simp only: in_measure rtype_size)
 
 instance
 proof (rule countable_classI)
diff -r f496e9f343b7 -r 1471f2974eb1 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -627,11 +627,7 @@
 apply (force)
 apply (rule ty_cases)
 done
-
-termination
-apply(relation "measure (\<lambda>(_,_,_,T). size T)")
-apply(auto)
-done
+termination by lexicographic_order
 
 lemma logical_monotonicity:
  fixes \<Gamma> \<Gamma>' :: Ctxt
diff -r f496e9f343b7 -r 1471f2974eb1 src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -52,11 +52,7 @@
 apply(drule_tac x="a" in meta_spec)
 apply(blast)
 done
-
-termination vsub
-proof
-  show "wf (measure (llam_size \<circ> fst))" by simp
-qed (auto)
+termination by (relation "measure (llam_size \<circ> fst)") auto
 
 lemma vsub_eqvt[eqvt]:
   fixes pi::"name prm" 
diff -r f496e9f343b7 -r 1471f2974eb1 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Word/BinOperations.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -514,24 +514,20 @@
 definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
   "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
 
-function bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   "bin_rsplit_aux n m c bs =
     (if m = 0 | n = 0 then bs else
       let (a, b) = bin_split n c 
       in bin_rsplit_aux n (m - n) a (b # bs))"
-by pat_completeness auto
-termination by (relation "measure (fst o snd)") simp_all
 
 definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
 
-function bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   "bin_rsplitl_aux n m c bs =
     (if m = 0 | n = 0 then bs else
       let (a, b) = bin_split (min m n) c 
       in bin_rsplitl_aux n (m - n) a (b # bs))"
-by pat_completeness auto
-termination by (relation "measure (fst o snd)") simp_all
 
 definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
diff -r f496e9f343b7 -r 1471f2974eb1 src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/ex/Random.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -20,15 +20,10 @@
 where
   "minus_shift r k l = (if k < l then r + k - l else k - l)"
 
-function
+fun
   log :: "index \<Rightarrow> index \<Rightarrow> index"
 where
   "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
-by pat_completeness auto
-termination
-  by (relation "measure (nat_of_index o snd)")
-    (auto simp add: index)
-
 
 subsection {* Random seeds *}