--- 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 {*
--- 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)
--- 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
--- 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"
--- 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) []"
--- 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 *}