author wenzelm Mon, 28 Nov 2005 10:58:40 +0100 changeset 18277 6c2b039b4847 parent 18276 c62ec94e326e child 18278 cbf6f44d73d3
```--- a/src/HOL/Wellfounded_Relations.thy	Mon Nov 28 07:17:07 2005 +0100
+++ b/src/HOL/Wellfounded_Relations.thy	Mon Nov 28 10:58:40 2005 +0100
@@ -78,9 +78,30 @@
apply (rule wf_less_than [THEN wf_inv_image])
done

-lemmas measure_induct =
-    wf_measure [THEN wf_induct, unfolded measure_def inv_image_def,
-                simplified, standard]
+lemma measure_induct_rule [case_names less]:
+  fixes f :: "'a \<Rightarrow> nat"
+  assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  shows "P a"
+proof -
+  have "wf (measure f)" ..
+  then show ?thesis
+  proof induct
+    case (less x)
+    show ?case
+    proof (rule step)
+      fix y
+      assume "f y < f x"
+      then have "(y, x) \<in> measure f"
+        by (simp add: measure_def inv_image_def)
+      then show "P y" by (rule less)
+    qed
+  qed
+qed
+
+lemma measure_induct:
+  fixes f :: "'a \<Rightarrow> nat"
+  shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
+  by (rule measure_induct_rule [of f P a]) iprover

subsection{*Other Ways of Constructing Wellfounded Relations*}```