author haftmann Mon Sep 21 14:22:32 2009 +0200 (2009-09-21) changeset 32629 542f0563d7b4 parent 32625 f270520df7de child 32630 133e4a6474e3 child 32690 5fb07ec99828
isarified proof
```     1.1 --- a/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 12:23:05 2009 +0200
1.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 14:22:32 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.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.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.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.*)