# HG changeset patch
# User wenzelm
# Date 1133171920 -3600
# Node ID 6c2b039b4847f976c4064407acea84ed24a289e0
# Parent  c62ec94e326e7bf14ccb5921c88d5ccb75746355
added proof of measure_induct_rule;

diff -r c62ec94e326e -r 6c2b039b4847 src/HOL/Wellfounded_Relations.thy
--- 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*}