src/HOL/Wellfounded.thy
changeset 44144 74b3751ea271
parent 43140 504d72a39638
child 44921 58eef4843641
     1.1 --- a/src/HOL/Wellfounded.thy	Wed Aug 10 18:07:32 2011 -0700
     1.2 +++ b/src/HOL/Wellfounded.thy	Thu Aug 11 09:15:45 2011 +0200
     1.3 @@ -881,45 +881,6 @@
     1.4  done
     1.5  
     1.6  
     1.7 -subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
     1.8 -   stabilize.*}
     1.9 -
    1.10 -text{*This material does not appear to be used any longer.*}
    1.11 -
    1.12 -lemma sequence_trans: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
    1.13 -by (induct k) (auto intro: rtrancl_trans)
    1.14 -
    1.15 -lemma wf_weak_decr_stable: 
    1.16 -  assumes as: "ALL i. (f (Suc i), f i) : r^*" "wf (r^+)"
    1.17 -  shows "EX i. ALL k. f (i+k) = f i"
    1.18 -proof -
    1.19 -  have lem: "!!x. [| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
    1.20 -      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
    1.21 -  apply (erule wf_induct, clarify)
    1.22 -  apply (case_tac "EX j. (f (m+j), f m) : r^+")
    1.23 -   apply clarify
    1.24 -   apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
    1.25 -    apply clarify
    1.26 -    apply (rule_tac x = "j+i" in exI)
    1.27 -    apply (simp add: add_ac, blast)
    1.28 -  apply (rule_tac x = 0 in exI, clarsimp)
    1.29 -  apply (drule_tac i = m and k = k in sequence_trans)
    1.30 -  apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
    1.31 -  done
    1.32 -
    1.33 -  from lem[OF as, THEN spec, of 0, simplified] 
    1.34 -  show ?thesis by auto
    1.35 -qed
    1.36 -
    1.37 -(* special case of the theorem above: <= *)
    1.38 -lemma weak_decr_stable:
    1.39 -     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
    1.40 -apply (rule_tac r = pred_nat in wf_weak_decr_stable)
    1.41 -apply (simp add: pred_nat_trancl_eq_le)
    1.42 -apply (intro wf_trancl wf_pred_nat)
    1.43 -done
    1.44 -
    1.45 -
    1.46  subsection {* size of a datatype value *}
    1.47  
    1.48  use "Tools/Function/size.ML"