# HG changeset patch # User paulson # Date 1058274742 -7200 # Node ID 95d51043d2a31a4fc5a09d39a48bb8c86b34dfa6 # Parent 993471c762b86237c03522710d6c03e7cbdbc94e tidying diff -r 993471c762b8 -r 95d51043d2a3 src/HOL/UNITY/Guar.thy --- a/src/HOL/UNITY/Guar.thy Tue Jul 15 08:25:20 2003 +0200 +++ b/src/HOL/UNITY/Guar.thy Tue Jul 15 15:12:22 2003 +0200 @@ -26,10 +26,10 @@ program_less_le)+) -constdefs +text{*Existential and Universal properties. I formalize the two-program + case, proving equivalence with Chandy and Sanders's n-ary definitions*} - (*Existential and Universal properties. I formalize the two-program - case, proving equivalence with Chandy and Sanders's n-ary definitions*) +constdefs ex_prop :: "'a program set => bool" "ex_prop X == \F G. F ok G -->F \ X | G \ X --> (F\G) \ X" @@ -44,6 +44,11 @@ "strict_uv_prop X == SKIP \ X & (\F G. F ok G --> (F \ X & G \ X) = (F\G \ X))" + +text{*Guarantees properties*} + +constdefs + guar :: "['a program set, 'a program set] => 'a program set" (infixl "guarantees" 55) (*higher than membership, lower than Co*) "X guarantees Y == {F. \G. F ok G --> F\G \ X --> F\G \ Y}" @@ -64,7 +69,7 @@ refines :: "['a program, 'a program, 'a program set] => bool" ("(3_ refines _ wrt _)" [10,10,10] 10) "G refines F wrt X == - \H. (F ok H & G ok H & F\H \ welldef \ X) --> + \H. (F ok H & G ok H & F\H \ welldef \ X) --> (G\H \ welldef \ X)" iso_refines :: "['a program, 'a program, 'a program set] => bool" @@ -79,7 +84,8 @@ by (auto intro: ok_sym simp add: OK_iff_ok) -(*** existential properties ***) +subsection{*Existential Properties*} + lemma ex1 [rule_format]: "[| ex_prop X; finite GG |] ==> GG \ X \ {}--> OK GG (%G. G) --> (\G \ GG. G) \ X" @@ -109,14 +115,14 @@ lemma ex_prop_equiv: "ex_prop X = (\G. G \ X = (\H. (G component_of H) --> H \ X))" apply auto -apply (unfold ex_prop_def component_of_def, safe, blast) -apply blast +apply (unfold ex_prop_def component_of_def, safe, blast, blast) apply (subst Join_commute) apply (drule ok_sym, blast) done -(*** universal properties ***) +subsection{*Universal Properties*} + lemma uv1 [rule_format]: "[| uv_prop X; finite GG |] ==> GG \ X & OK GG (%G. G) --> (\G \ GG. G) \ X" @@ -143,23 +149,20 @@ (\GG. finite GG & GG \ X & OK GG (%G. G) --> (\G \ GG. G): X)" by (blast intro: uv1 uv2) -(*** guarantees ***) +subsection{*Guarantees*} lemma guaranteesI: - "(!!G. [| F ok G; F\G \ X |] ==> F\G \ Y) - ==> F \ X guarantees Y" + "(!!G. [| F ok G; F\G \ X |] ==> F\G \ Y) ==> F \ X guarantees Y" by (simp add: guar_def component_def) lemma guaranteesD: - "[| F \ X guarantees Y; F ok G; F\G \ X |] - ==> F\G \ Y" + "[| F \ X guarantees Y; F ok G; F\G \ X |] ==> F\G \ Y" by (unfold guar_def component_def, blast) (*This version of guaranteesD matches more easily in the conclusion The major premise can no longer be F \ H since we need to reason about G*) lemma component_guaranteesD: - "[| F \ X guarantees Y; F\G = H; H \ X; F ok G |] - ==> H \ Y" + "[| F \ X guarantees Y; F\G = H; H \ X; F ok G |] ==> H \ Y" by (unfold guar_def, blast) lemma guarantees_weaken: @@ -185,10 +188,7 @@ done lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)" -apply (simp (no_asm_use) add: guar_def ex_prop_equiv) -apply safe -apply (auto simp add: component_of_def dest: sym) -done +by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym) lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)" apply (rule iffI) @@ -197,7 +197,7 @@ done -(** Distributive laws. Re-orient to perform miniscoping **) +subsection{*Distributive Laws. Re-Orient to Perform Miniscoping*} lemma guarantees_UN_left: "(\i \ I. X i) guarantees Y = (\i \ I. X i guarantees Y)" @@ -237,7 +237,6 @@ lemma combining1: "[| F \ V guarantees X; F \ (X \ Y) guarantees Z |] ==> F \ (V \ Y) guarantees Z" - by (unfold guar_def, blast) lemma combining2: @@ -259,30 +258,26 @@ by (unfold guar_def, blast) -(*** Additional guarantees laws, by lcp ***) +subsection{*Guarantees: Additional Laws (by lcp)*} lemma guarantees_Join_Int: "[| F \ U guarantees V; G \ X guarantees Y; F ok G |] ==> F\G \ (U \ X) guarantees (V \ Y)" -apply (unfold guar_def) -apply (simp (no_asm)) -apply safe -apply (simp add: Join_assoc) +apply (simp add: guar_def, safe) + apply (simp add: Join_assoc) apply (subgoal_tac "F\G\Ga = G\(F\Ga) ") -apply (simp add: ok_commute) -apply (simp (no_asm_simp) add: Join_ac) + apply (simp add: ok_commute) +apply (simp add: Join_ac) done lemma guarantees_Join_Un: "[| F \ U guarantees V; G \ X guarantees Y; F ok G |] ==> F\G \ (U \ X) guarantees (V \ Y)" -apply (unfold guar_def) -apply (simp (no_asm)) -apply safe -apply (simp add: Join_assoc) +apply (simp add: guar_def, safe) + apply (simp add: Join_assoc) apply (subgoal_tac "F\G\Ga = G\(F\Ga) ") -apply (simp add: ok_commute) -apply (simp (no_asm_simp) add: Join_ac) + apply (simp add: ok_commute) +apply (simp add: Join_ac) done lemma guarantees_JN_INT: @@ -308,17 +303,13 @@ done -(*** guarantees laws for breaking down the program, by lcp ***) +subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*} lemma guarantees_Join_I1: "[| F \ X guarantees Y; F ok G |] ==> F\G \ X guarantees Y" -apply (unfold guar_def) -apply (simp (no_asm)) -apply safe -apply (simp add: Join_assoc) -done +by (simp add: guar_def Join_assoc) -lemma guarantees_Join_I2: +lemma guarantees_Join_I2: "[| G \ X guarantees Y; F ok G |] ==> F\G \ X guarantees Y" apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) apply (blast intro: guarantees_Join_I1) @@ -329,7 +320,8 @@ ==> (\i \ I. (F i)) \ X guarantees Y" apply (unfold guar_def, clarify) apply (drule_tac x = "JOIN (I-{i}) F\G" in spec) -apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric]) +apply (auto intro: OK_imp_ok + simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric]) done @@ -346,12 +338,11 @@ lemma refines_refl: "F refines F wrt X" by (unfold refines_def, blast) - -(* Goalw [refines_def] +(*We'd like transitivity, but how do we get it?*) +lemma refines_trans: "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X" -by Auto_tac -qed "refines_trans"; *) - +apply (simp add: refines_def) +oops lemma strict_ex_refine_lemma: @@ -406,21 +397,14 @@ "(F \ X guarantees Y) = (\H. H \ X \ (F component_of H \ H \ Y))" by (unfold guar_def component_of_def, auto) -lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \ (wg F Y)" +lemma wg_weakest: "!!X. F\ (X guarantees Y) ==> X \ (wg F Y)" by (unfold wg_def, auto) -lemma wg_guarantees: "F:((wg F Y) guarantees Y)" +lemma wg_guarantees: "F\ ((wg F Y) guarantees Y)" by (unfold wg_def guar_def, blast) -lemma wg_equiv: - "(H \ wg F X) = (F component_of H --> H \ X)" -apply (unfold wg_def) -apply (simp (no_asm) add: guarantees_equiv) -apply (rule iffI) -apply (rule_tac [2] x = "{H}" in exI) -apply (blast+) -done - +lemma wg_equiv: "(H \ wg F X) = (F component_of H --> H \ X)" +by (simp add: guarantees_equiv wg_def, blast) lemma component_of_wg: "F component_of H ==> (H \ wg F X) = (H \ X)" by (simp add: wg_equiv) @@ -447,93 +431,62 @@ by (unfold wx_def, auto) lemma wx_ex_prop: "ex_prop (wx X)" -apply (unfold wx_def) -apply (simp (no_asm) add: ex_prop_equiv) -apply safe -apply blast -apply auto +apply (simp add: wx_def ex_prop_equiv, safe, blast) +apply force done lemma wx_weakest: "\Z. Z<= X --> ex_prop Z --> Z \ wx X" -by (unfold wx_def, auto) +by (auto simp add: wx_def) (* Proposition 6 *) lemma wx'_ex_prop: "ex_prop({F. \G. F ok G --> F\G \ X})" apply (unfold ex_prop_def, safe) -apply (drule_tac x = "G\Ga" in spec) -apply (force simp add: ok_Join_iff1 Join_assoc) + apply (drule_tac x = "G\Ga" in spec) + apply (force simp add: ok_Join_iff1 Join_assoc) apply (drule_tac x = "F\Ga" in spec) -apply (simp (no_asm_use) add: ok_Join_iff1) -apply safe -apply (simp (no_asm_simp) add: ok_commute) -apply (subgoal_tac "F\G = G\F") -apply (simp (no_asm_simp) add: Join_assoc) -apply (simp (no_asm) add: Join_commute) +apply (simp add: ok_Join_iff1 ok_commute Join_ac) done -(* Equivalence with the other definition of wx *) - -lemma wx_equiv: - "wx X = {F. \G. F ok G --> (F\G):X}" +text{* Equivalence with the other definition of wx *} +lemma wx_equiv: "wx X = {F. \G. F ok G --> (F\G) \ X}" apply (unfold wx_def, safe) -apply (simp (no_asm_use) add: ex_prop_def) -apply (drule_tac x = x in spec) -apply (drule_tac x = G in spec) -apply (frule_tac c = "x\G" in subsetD, safe) + apply (simp add: ex_prop_def, blast) apply (simp (no_asm)) apply (rule_tac x = "{F. \G. F ok G --> F\G \ X}" in exI, safe) apply (rule_tac [2] wx'_ex_prop) -apply (rotate_tac 1) -apply (drule_tac x = SKIP in spec, auto) +apply (drule_tac x = SKIP in spec)+ +apply auto done -(* Propositions 7 to 11 are about this second definition of wx. And - they are the same as the ones proved for the first definition of wx by equivalence *) +text{* Propositions 7 to 11 are about this second definition of wx. + They are the same as the ones proved for the first definition of wx, + by equivalence *} (* Proposition 12 *) (* Main result of the paper *) -lemma guarantees_wx_eq: - "(X guarantees Y) = wx(-X \ Y)" -apply (unfold guar_def) -apply (simp (no_asm) add: wx_equiv) -done +lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \ Y)" +by (simp add: guar_def wx_equiv) -(* {* Corollary, but this result has already been proved elsewhere *} - "ex_prop(X guarantees Y)" - by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1); - qed "guarantees_ex_prop"; -*) (* Rules given in section 7 of Chandy and Sander's Reasoning About Program composition paper *) - lemma stable_guarantees_Always: - "Init F \ A ==> F:(stable A) guarantees (Always A)" + "Init F \ A ==> F \ (stable A) guarantees (Always A)" apply (rule guaranteesI) -apply (simp (no_asm) add: Join_commute) +apply (simp add: Join_commute) apply (rule stable_Join_Always1) -apply (simp_all add: invariant_def Join_stable) + apply (simp_all add: invariant_def Join_stable) done -(* To be moved to WFair.ML *) -lemma leadsTo_Basis': "[| F \ A co A \ B; F \ transient A |] ==> F \ A leadsTo B" -apply (drule_tac B = "A-B" in constrains_weaken_L) -apply (drule_tac [2] B = "A-B" in transient_strengthen) -apply (rule_tac [3] ensuresI [THEN leadsTo_Basis]) -apply (blast+) -done - - - lemma constrains_guarantees_leadsTo: "F \ transient A ==> F \ (A co A \ B) guarantees (A leadsTo (B-A))" apply (rule guaranteesI) apply (rule leadsTo_Basis') -apply (drule constrains_weaken_R) -prefer 2 apply assumption -apply blast + apply (drule constrains_weaken_R) + prefer 2 apply assumption + apply blast apply (blast intro: Join_transient_I1) done diff -r 993471c762b8 -r 95d51043d2a3 src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Tue Jul 15 08:25:20 2003 +0200 +++ b/src/HOL/UNITY/WFair.thy Tue Jul 15 15:12:22 2003 +0200 @@ -174,6 +174,14 @@ apply (blast intro: leads.Trans) done +lemma leadsTo_Basis': + "[| F \ A co A \ B; F \ transient A |] ==> F \ A leadsTo B" +apply (drule_tac B = "A-B" in constrains_weaken_L) +apply (drule_tac [2] B = "A-B" in transient_strengthen) +apply (rule_tac [3] ensuresI [THEN leadsTo_Basis]) +apply (blast+) +done + lemma transient_imp_leadsTo: "F \ transient A ==> F \ A leadsTo (-A)" by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)