removed lemmas called lemma1 and lemma2
authorkrauss
Tue Nov 18 21:17:14 2008 +0100 (2008-11-18)
changeset 28845cdfc8ef54a99
parent 28844 ae0611234603
child 28846 9c6025c721d7
removed lemmas called lemma1 and lemma2
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Nov 18 18:25:59 2008 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Nov 18 21:17:14 2008 +0100
     1.3 @@ -908,29 +908,30 @@
     1.4  
     1.5  text{*This material does not appear to be used any longer.*}
     1.6  
     1.7 -lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
     1.8 -apply (induct_tac "k", simp_all)
     1.9 -apply (blast intro: rtrancl_trans)
    1.10 -done
    1.11 +lemma sequence_trans: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
    1.12 +by (induct k) (auto intro: rtrancl_trans)
    1.13  
    1.14 -lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
    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 lemma1)
    1.30 -apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
    1.31 -done
    1.32 +  apply (erule wf_induct, clarify)
    1.33 +  apply (case_tac "EX j. (f (m+j), f m) : r^+")
    1.34 +   apply clarify
    1.35 +   apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
    1.36 +    apply clarify
    1.37 +    apply (rule_tac x = "j+i" in exI)
    1.38 +    apply (simp add: add_ac, blast)
    1.39 +  apply (rule_tac x = 0 in exI, clarsimp)
    1.40 +  apply (drule_tac i = m and k = k in sequence_trans)
    1.41 +  apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
    1.42 +  done
    1.43  
    1.44 -lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
    1.45 -      ==> EX i. ALL k. f (i+k) = f i"
    1.46 -apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
    1.47 -done
    1.48 +  from lem[OF as, THEN spec, of 0, simplified] 
    1.49 +  show ?thesis by auto
    1.50 +qed
    1.51  
    1.52  (* special case of the theorem above: <= *)
    1.53  lemma weak_decr_stable: