author krauss Tue Nov 18 21:17:14 2008 +0100 (2008-11-18) changeset 28845 cdfc8ef54a99 parent 28844 ae0611234603 child 28846 9c6025c721d7
removed lemmas called lemma1 and lemma2
 src/HOL/Wellfounded.thy file | annotate | diff | revisions
```     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.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.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:
```