merged
authorhaftmann
Mon Sep 21 14:23:12 2009 +0200 (2009-09-21)
changeset 326905fb07ec99828
parent 32689 860e1a2317bd
parent 32629 542f0563d7b4
child 32691 cdf70f1fc9f9
merged
     1.1 --- a/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 14:23:04 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 14:23:12 2009 +0200
     1.3 @@ -83,19 +83,24 @@
     1.4  
     1.5  (*** Progress under weak fairness ***)
     1.6  
     1.7 -declare atMost_Int_atLeast [simp]
     1.8 -
     1.9  lemma leadsTo_common_lemma:
    1.10 -     "[| \<forall>m. F \<in> {m} Co (maxfg m);  
    1.11 -         \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m);  
    1.12 -         n \<in> common |]   
    1.13 -      ==> F \<in> (atMost n) LeadsTo common"
    1.14 -apply (rule LeadsTo_weaken_R)
    1.15 -apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
    1.16 -apply (simp_all (no_asm_simp) del: Int_insert_right_if1)
    1.17 -apply (rule_tac [2] subset_refl)
    1.18 -apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
    1.19 -done
    1.20 +  assumes "\<forall>m. F \<in> {m} Co (maxfg m)"
    1.21 +    and "\<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m)"
    1.22 +    and "n \<in> common"
    1.23 +  shows "F \<in> (atMost n) LeadsTo common"
    1.24 +proof (rule LeadsTo_weaken_R)
    1.25 +  show "F \<in> {..n} LeadsTo {..n} \<inter> id -` {n..} \<union> common"
    1.26 +  proof (induct rule: GreaterThan_bounded_induct [of n _ _ id])
    1.27 +    case 1
    1.28 +    from assms have "\<forall>m\<in>{..<n}. F \<in> {..n} \<inter> {m} LeadsTo {..n} \<inter> {m<..} \<union> common"
    1.29 +      by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
    1.30 +    then show ?case by simp
    1.31 +  qed
    1.32 +next
    1.33 +  from `n \<in> common`
    1.34 +  show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common"
    1.35 +    by (simp add: atMost_Int_atLeast)
    1.36 +qed
    1.37  
    1.38  (*The "\<forall>m \<in> -common" form echoes CMT6.*)
    1.39  lemma leadsTo_common: