# HG changeset patch # User haftmann # Date 1253535792 -7200 # Node ID 5fb07ec998286870194947b6197f4d626505ea88 # Parent 860e1a2317bd09ae55e3f428d1bd3ad7a3a9cbee# Parent 542f0563d7b4ae76e3340e3e6fc9a624ad770f14 merged diff -r 860e1a2317bd -r 5fb07ec99828 src/HOL/UNITY/Simple/Common.thy --- a/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 14:23:04 2009 +0200 +++ b/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 14:23:12 2009 +0200 @@ -83,19 +83,24 @@ (*** Progress under weak fairness ***) -declare atMost_Int_atLeast [simp] - lemma leadsTo_common_lemma: - "[| \m. F \ {m} Co (maxfg m); - \m \ lessThan n. F \ {m} LeadsTo (greaterThan m); - n \ common |] - ==> F \ (atMost n) LeadsTo common" -apply (rule LeadsTo_weaken_R) -apply (rule_tac f = id and l = n in GreaterThan_bounded_induct) -apply (simp_all (no_asm_simp) del: Int_insert_right_if1) -apply (rule_tac [2] subset_refl) -apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) -done + assumes "\m. F \ {m} Co (maxfg m)" + and "\m \ lessThan n. F \ {m} LeadsTo (greaterThan m)" + and "n \ common" + shows "F \ (atMost n) LeadsTo common" +proof (rule LeadsTo_weaken_R) + show "F \ {..n} LeadsTo {..n} \ id -` {n..} \ common" + proof (induct rule: GreaterThan_bounded_induct [of n _ _ id]) + case 1 + from assms have "\m\{.. {..n} \ {m} LeadsTo {..n} \ {m<..} \ common" + by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) + then show ?case by simp + qed +next + from `n \ common` + show "{..n} \ id -` {n..} \ common \ common" + by (simp add: atMost_Int_atLeast) +qed (*The "\m \ -common" form echoes CMT6.*) lemma leadsTo_common: