# HG changeset patch
# User krauss
# Date 1248763736 -7200
# Node ID a99723d77ae049aa7f4feccc5d0ccab7e89dd57f
# Parent  64660a887b1597932010e876a5b390bfbbc583d5
moved obsolete same_fst to Recdef.thy

diff -r 64660a887b15 -r a99723d77ae0 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Tue Jul 28 08:48:48 2009 +0200
+++ b/src/HOL/Recdef.thy	Tue Jul 28 08:48:56 2009 +0200
@@ -79,6 +79,32 @@
 use "Tools/recdef.ML"
 setup Recdef.setup
 
+text {*Wellfoundedness of @{text same_fst}*}
+
+definition
+ same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
+where
+    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
+   --{*For @{text rec_def} declarations where the first n parameters
+       stay unchanged in the recursive call. *}
+
+lemma same_fstI [intro!]:
+     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
+by (simp add: same_fst_def)
+
+lemma wf_same_fst:
+  assumes prem: "(!!x. P x ==> wf(R x))"
+  shows "wf(same_fst P R)"
+apply (simp cong del: imp_cong add: wf_def same_fst_def)
+apply (intro strip)
+apply (rename_tac a b)
+apply (case_tac "wf (R a)")
+ apply (erule_tac a = b in wf_induct, blast)
+apply (blast intro: prem)
+done
+
+text {*Rule setup*}
+
 lemmas [recdef_simp] =
   inv_image_def
   measure_def
diff -r 64660a887b15 -r a99723d77ae0 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Jul 28 08:48:48 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Jul 28 08:48:56 2009 +0200
@@ -886,30 +886,6 @@
   qed
 qed
 
-text {*Wellfoundedness of @{text same_fst}*}
-
-definition
- same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
-where
-    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
-   --{*For @{text rec_def} declarations where the first n parameters
-       stay unchanged in the recursive call. *}
-
-lemma same_fstI [intro!]:
-     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
-by (simp add: same_fst_def)
-
-lemma wf_same_fst:
-  assumes prem: "(!!x. P x ==> wf(R x))"
-  shows "wf(same_fst P R)"
-apply (simp cong del: imp_cong add: wf_def same_fst_def)
-apply (intro strip)
-apply (rename_tac a b)
-apply (case_tac "wf (R a)")
- apply (erule_tac a = b in wf_induct, blast)
-apply (blast intro: prem)
-done
-
 
 subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
    stabilize.*}