# HG changeset patch
# User krauss
# Date 1313046945 -7200
# Node ID 74b3751ea271a0b898072967dadd0ed127012376
# Parent  d282b3c5df7cc6e072d69c3492c97de746e4d052
removed unused material, which does not really belong here

diff -r d282b3c5df7c -r 74b3751ea271 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Aug 10 18:07:32 2011 -0700
+++ b/src/HOL/Wellfounded.thy	Thu Aug 11 09:15:45 2011 +0200
@@ -881,45 +881,6 @@
 done
 
 
-subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
-   stabilize.*}
-
-text{*This material does not appear to be used any longer.*}
-
-lemma sequence_trans: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
-by (induct k) (auto intro: rtrancl_trans)
-
-lemma wf_weak_decr_stable: 
-  assumes as: "ALL i. (f (Suc i), f i) : r^*" "wf (r^+)"
-  shows "EX i. ALL k. f (i+k) = f i"
-proof -
-  have lem: "!!x. [| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
-      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
-  apply (erule wf_induct, clarify)
-  apply (case_tac "EX j. (f (m+j), f m) : r^+")
-   apply clarify
-   apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
-    apply clarify
-    apply (rule_tac x = "j+i" in exI)
-    apply (simp add: add_ac, blast)
-  apply (rule_tac x = 0 in exI, clarsimp)
-  apply (drule_tac i = m and k = k in sequence_trans)
-  apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
-  done
-
-  from lem[OF as, THEN spec, of 0, simplified] 
-  show ?thesis by auto
-qed
-
-(* special case of the theorem above: <= *)
-lemma weak_decr_stable:
-     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
-apply (rule_tac r = pred_nat in wf_weak_decr_stable)
-apply (simp add: pred_nat_trancl_eq_le)
-apply (intro wf_trancl wf_pred_nat)
-done
-
-
 subsection {* size of a datatype value *}
 
 use "Tools/Function/size.ML"