diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Project.thy --- a/src/HOL/UNITY/Project.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Project.thy Sat Feb 08 16:05:33 2003 +0100 @@ -16,20 +16,20 @@ projecting :: "['c program => 'c set, 'a*'b => 'c, 'a program, 'c program set, 'a program set] => bool" "projecting C h F X' X == - ALL G. extend h F Join G : X' --> F Join project h (C G) G : X" + \G. extend h F Join G \ X' --> F Join project h (C G) G \ X" extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 'c program set, 'a program set] => bool" "extending C h F Y' Y == - ALL G. extend h F ok G --> F Join project h (C G) G : Y - --> extend h F Join G : Y'" + \G. extend h F ok G --> F Join project h (C G) G \ Y + --> extend h F Join G \ Y'" subset_closed :: "'a set set => bool" - "subset_closed U == ALL A: U. Pow A <= U" + "subset_closed U == \A \ U. Pow A \ U" lemma (in Extend) project_extend_constrains_I: - "F : A co B ==> project h C (extend h F) : A co B" + "F \ A co B ==> project h C (extend h F) \ A co B" apply (auto simp add: extend_act_def project_act_def constrains_def) done @@ -38,8 +38,8 @@ (*used below to prove Join_project_ensures*) lemma (in Extend) project_unless [rule_format]: - "[| G : stable C; project h C G : A unless B |] - ==> G : (C Int extend_set h A) unless (extend_set h B)" + "[| G \ stable C; project h C G \ A unless B |] + ==> G \ (C \ extend_set h A) unless (extend_set h B)" apply (simp add: unless_def project_constrains) apply (blast dest: stable_constrains_Int intro: constrains_weaken) done @@ -47,21 +47,21 @@ (*Generalizes project_constrains to the program F Join project h C G useful with guarantees reasoning*) lemma (in Extend) Join_project_constrains: - "(F Join project h C G : A co B) = - (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & - F : A co B)" + "(F Join project h C G \ A co B) = + (extend h F Join G \ (C \ extend_set h A) co (extend_set h B) & + F \ A co B)" apply (simp (no_asm) add: project_constrains) apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] dest: constrains_imp_subset) done (*The condition is required to prove the left-to-right direction - could weaken it to G : (C Int extend_set h A) co C*) + could weaken it to G \ (C \ extend_set h A) co C*) lemma (in Extend) Join_project_stable: - "extend h F Join G : stable C - ==> (F Join project h C G : stable A) = - (extend h F Join G : stable (C Int extend_set h A) & - F : stable A)" + "extend h F Join G \ stable C + ==> (F Join project h C G \ stable A) = + (extend h F Join G \ stable (C \ extend_set h A) & + F \ stable A)" apply (unfold stable_def) apply (simp only: Join_project_constrains) apply (blast intro: constrains_weaken dest: constrains_Int) @@ -69,23 +69,23 @@ (*For using project_guarantees in particular cases*) lemma (in Extend) project_constrains_I: - "extend h F Join G : extend_set h A co extend_set h B - ==> F Join project h C G : A co B" + "extend h F Join G \ extend_set h A co extend_set h B + ==> F Join project h C G \ A co B" apply (simp add: project_constrains extend_constrains) apply (blast intro: constrains_weaken dest: constrains_imp_subset) done lemma (in Extend) project_increasing_I: - "extend h F Join G : increasing (func o f) - ==> F Join project h C G : increasing func" + "extend h F Join G \ increasing (func o f) + ==> F Join project h C G \ increasing func" apply (unfold increasing_def stable_def) apply (simp del: Join_constrains add: project_constrains_I extend_set_eq_Collect) done lemma (in Extend) Join_project_increasing: - "(F Join project h UNIV G : increasing func) = - (extend h F Join G : increasing (func o f))" + "(F Join project h UNIV G \ increasing func) = + (extend h F Join G \ increasing (func o f))" apply (rule iffI) apply (erule_tac [2] project_increasing_I) apply (simp del: Join_stable @@ -95,8 +95,8 @@ (*The UNIV argument is essential*) lemma (in Extend) project_constrains_D: - "F Join project h UNIV G : A co B - ==> extend h F Join G : extend_set h A co extend_set h B" + "F Join project h UNIV G \ A co B + ==> extend h F Join G \ extend_set h A co extend_set h B" by (simp add: project_constrains extend_constrains) @@ -104,26 +104,26 @@ lemma projecting_Int: "[| projecting C h F XA' XA; projecting C h F XB' XB |] - ==> projecting C h F (XA' Int XB') (XA Int XB)" + ==> projecting C h F (XA' \ XB') (XA \ XB)" by (unfold projecting_def, blast) lemma projecting_Un: "[| projecting C h F XA' XA; projecting C h F XB' XB |] - ==> projecting C h F (XA' Un XB') (XA Un XB)" + ==> projecting C h F (XA' \ XB') (XA \ XB)" by (unfold projecting_def, blast) lemma projecting_INT: - "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] - ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)" + "[| !!i. i \ I ==> projecting C h F (X' i) (X i) |] + ==> projecting C h F (\i \ I. X' i) (\i \ I. X i)" by (unfold projecting_def, blast) lemma projecting_UN: - "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] - ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)" + "[| !!i. i \ I ==> projecting C h F (X' i) (X i) |] + ==> projecting C h F (\i \ I. X' i) (\i \ I. X i)" by (unfold projecting_def, blast) lemma projecting_weaken: - "[| projecting C h F X' X; U'<=X'; X<=U |] ==> projecting C h F U' U" + "[| projecting C h F X' X; U'<=X'; X \ U |] ==> projecting C h F U' U" by (unfold projecting_def, auto) lemma projecting_weaken_L: @@ -132,26 +132,26 @@ lemma extending_Int: "[| extending C h F YA' YA; extending C h F YB' YB |] - ==> extending C h F (YA' Int YB') (YA Int YB)" + ==> extending C h F (YA' \ YB') (YA \ YB)" by (unfold extending_def, blast) lemma extending_Un: "[| extending C h F YA' YA; extending C h F YB' YB |] - ==> extending C h F (YA' Un YB') (YA Un YB)" + ==> extending C h F (YA' \ YB') (YA \ YB)" by (unfold extending_def, blast) lemma extending_INT: - "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] - ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)" + "[| !!i. i \ I ==> extending C h F (Y' i) (Y i) |] + ==> extending C h F (\i \ I. Y' i) (\i \ I. Y i)" by (unfold extending_def, blast) lemma extending_UN: - "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] - ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)" + "[| !!i. i \ I ==> extending C h F (Y' i) (Y i) |] + ==> extending C h F (\i \ I. Y' i) (\i \ I. Y i)" by (unfold extending_def, blast) lemma extending_weaken: - "[| extending C h F Y' Y; Y'<=V'; V<=Y |] ==> extending C h F V' V" + "[| extending C h F Y' Y; Y'<=V'; V \ Y |] ==> extending C h F V' V" by (unfold extending_def, auto) lemma extending_weaken_L: @@ -204,9 +204,9 @@ (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_imp_reachable_project: - "[| reachable (extend h F Join G) <= C; - z : reachable (extend h F Join G) |] - ==> f z : reachable (F Join project h C G)" + "[| reachable (extend h F Join G) \ C; + z \ reachable (extend h F Join G) |] + ==> f z \ reachable (F Join project h C G)" apply (erule reachable.induct) apply (force intro!: reachable.Init simp add: split_extended_all, auto) apply (rule_tac act = x in reachable.Acts) @@ -217,8 +217,8 @@ done lemma (in Extend) project_Constrains_D: - "F Join project h (reachable (extend h F Join G)) G : A Co B - ==> extend h F Join G : (extend_set h A) Co (extend_set h B)" + "F Join project h (reachable (extend h F Join G)) G \ A Co B + ==> extend h F Join G \ (extend_set h A) Co (extend_set h B)" apply (unfold Constrains_def) apply (simp del: Join_constrains add: Join_project_constrains, clarify) @@ -227,22 +227,22 @@ done lemma (in Extend) project_Stable_D: - "F Join project h (reachable (extend h F Join G)) G : Stable A - ==> extend h F Join G : Stable (extend_set h A)" + "F Join project h (reachable (extend h F Join G)) G \ Stable A + ==> extend h F Join G \ Stable (extend_set h A)" apply (unfold Stable_def) apply (simp (no_asm_simp) add: project_Constrains_D) done lemma (in Extend) project_Always_D: - "F Join project h (reachable (extend h F Join G)) G : Always A - ==> extend h F Join G : Always (extend_set h A)" + "F Join project h (reachable (extend h F Join G)) G \ Always A + ==> extend h F Join G \ Always (extend_set h A)" apply (unfold Always_def) apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all) done lemma (in Extend) project_Increasing_D: - "F Join project h (reachable (extend h F Join G)) G : Increasing func - ==> extend h F Join G : Increasing (func o f)" + "F Join project h (reachable (extend h F Join G)) G \ Increasing func + ==> extend h F Join G \ Increasing (func o f)" apply (unfold Increasing_def, auto) apply (subst extend_set_eq_Collect [symmetric]) apply (simp (no_asm_simp) add: project_Stable_D) @@ -253,9 +253,9 @@ (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_project_imp_reachable: - "[| C <= reachable(extend h F Join G); - x : reachable (F Join project h C G) |] - ==> EX y. h(x,y) : reachable (extend h F Join G)" + "[| C \ reachable(extend h F Join G); + x \ reachable (F Join project h C G) |] + ==> \y. h(x,y) \ reachable (extend h F Join G)" apply (erule reachable.induct) apply (force intro: reachable.Init) apply (auto simp add: project_act_def) @@ -270,15 +270,15 @@ (*UNUSED*) lemma (in Extend) reachable_extend_Join_subset: - "reachable (extend h F Join G) <= C - ==> reachable (extend h F Join G) <= + "reachable (extend h F Join G) \ C + ==> reachable (extend h F Join G) \ extend_set h (reachable (F Join project h C G))" apply (auto dest: reachable_imp_reachable_project) done lemma (in Extend) project_Constrains_I: - "extend h F Join G : (extend_set h A) Co (extend_set h B) - ==> F Join project h (reachable (extend h F Join G)) G : A Co B" + "extend h F Join G \ (extend_set h A) Co (extend_set h B) + ==> F Join project h (reachable (extend h F Join G)) G \ A Co B" apply (unfold Constrains_def) apply (simp del: Join_constrains add: Join_project_constrains extend_set_Int_distrib) @@ -291,43 +291,43 @@ done lemma (in Extend) project_Stable_I: - "extend h F Join G : Stable (extend_set h A) - ==> F Join project h (reachable (extend h F Join G)) G : Stable A" + "extend h F Join G \ Stable (extend_set h A) + ==> F Join project h (reachable (extend h F Join G)) G \ Stable A" apply (unfold Stable_def) apply (simp (no_asm_simp) add: project_Constrains_I) done lemma (in Extend) project_Always_I: - "extend h F Join G : Always (extend_set h A) - ==> F Join project h (reachable (extend h F Join G)) G : Always A" + "extend h F Join G \ Always (extend_set h A) + ==> F Join project h (reachable (extend h F Join G)) G \ Always A" apply (unfold Always_def) apply (auto simp add: project_Stable_I) apply (unfold extend_set_def, blast) done lemma (in Extend) project_Increasing_I: - "extend h F Join G : Increasing (func o f) - ==> F Join project h (reachable (extend h F Join G)) G : Increasing func" + "extend h F Join G \ Increasing (func o f) + ==> F Join project h (reachable (extend h F Join G)) G \ Increasing func" apply (unfold Increasing_def, auto) apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I) done lemma (in Extend) project_Constrains: - "(F Join project h (reachable (extend h F Join G)) G : A Co B) = - (extend h F Join G : (extend_set h A) Co (extend_set h B))" + "(F Join project h (reachable (extend h F Join G)) G \ A Co B) = + (extend h F Join G \ (extend_set h A) Co (extend_set h B))" apply (blast intro: project_Constrains_I project_Constrains_D) done lemma (in Extend) project_Stable: - "(F Join project h (reachable (extend h F Join G)) G : Stable A) = - (extend h F Join G : Stable (extend_set h A))" + "(F Join project h (reachable (extend h F Join G)) G \ Stable A) = + (extend h F Join G \ Stable (extend_set h A))" apply (unfold Stable_def) apply (rule project_Constrains) done lemma (in Extend) project_Increasing: - "(F Join project h (reachable (extend h F Join G)) G : Increasing func) = - (extend h F Join G : Increasing (func o f))" + "(F Join project h (reachable (extend h F Join G)) G \ Increasing func) = + (extend h F Join G \ Increasing (func o f))" apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect) done @@ -397,30 +397,24 @@ subsubsection{*transient*} lemma (in Extend) transient_extend_set_imp_project_transient: - "[| G : transient (C Int extend_set h A); G : stable C |] - ==> project h C G : transient (project_set h C Int A)" - -apply (unfold transient_def) -apply (auto simp add: Domain_project_act) -apply (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A") -prefer 2 + "[| G \ transient (C \ extend_set h A); G \ stable C |] + ==> project h C G \ transient (project_set h C \ A)" +apply (auto simp add: transient_def Domain_project_act) +apply (subgoal_tac "act `` (C \ extend_set h A) \ - extend_set h A") + prefer 2 apply (simp add: stable_def constrains_def, blast) (*back to main goal*) -apply (erule_tac V = "?AA <= -C Un ?BB" in thin_rl) +apply (erule_tac V = "?AA \ -C \ ?BB" in thin_rl) apply (drule bspec, assumption) apply (simp add: extend_set_def project_act_def, blast) done (*converse might hold too?*) lemma (in Extend) project_extend_transient_D: - "project h C (extend h F) : transient (project_set h C Int D) - ==> F : transient (project_set h C Int D)" -apply (unfold transient_def) -apply (auto simp add: Domain_project_act) -apply (rule bexI) -prefer 2 apply assumption -apply auto -apply (unfold extend_act_def, blast) + "project h C (extend h F) \ transient (project_set h C \ D) + ==> F \ transient (project_set h C \ D)" +apply (simp add: transient_def Domain_project_act, safe) +apply blast+ done @@ -428,11 +422,12 @@ (*Used to prove project_leadsETo_I*) lemma (in Extend) ensures_extend_set_imp_project_ensures: - "[| extend h F : stable C; G : stable C; - extend h F Join G : A ensures B; A-B = C Int extend_set h D |] + "[| extend h F \ stable C; G \ stable C; + extend h F Join G \ A ensures B; A-B = C \ extend_set h D |] ==> F Join project h C G - : (project_set h C Int project_set h A) ensures (project_set h B)" -apply (simp add: ensures_def project_constrains Join_transient extend_transient, clarify) + \ (project_set h C \ project_set h A) ensures (project_set h B)" +apply (simp add: ensures_def project_constrains Join_transient extend_transient, + clarify) apply (intro conjI) (*first subgoal*) apply (blast intro: extend_stable_project_set @@ -457,19 +452,42 @@ [THEN project_extend_transient_D, THEN transient_strengthen]) done +text{*Transferring a transient property upwards*} +lemma (in Extend) project_transient_extend_set: + "project h C G \ transient (project_set h C \ A - B) + ==> G \ transient (C \ extend_set h A - extend_set h B)" +apply (simp add: transient_def project_set_def extend_set_def project_act_def) +apply (elim disjE bexE) + apply (rule_tac x=Id in bexI) + apply (blast intro!: rev_bexI )+ +done + +lemma (in Extend) project_unless2 [rule_format]: + "[| G \ stable C; project h C G \ (project_set h C \ A) unless B |] + ==> G \ (C \ extend_set h A) unless (extend_set h B)" +by (auto dest: stable_constrains_Int intro: constrains_weaken + simp add: unless_def project_constrains Diff_eq Int_assoc + Int_extend_set_lemma) + + +lemma (in Extend) extend_unless: + "[|extend h F \ stable C; F \ A unless B|] + ==> extend h F \ C \ extend_set h A unless extend_set h B" +apply (simp add: unless_def stable_def) +apply (drule constrains_Int) +apply (erule extend_constrains [THEN iffD2]) +apply (erule constrains_weaken, blast) +apply blast +done + (*Used to prove project_leadsETo_D*) lemma (in Extend) Join_project_ensures [rule_format]: - "[| project h C G ~: transient (A-B) | A<=B; - extend h F Join G : stable C; - F Join project h C G : A ensures B |] - ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)" -apply (erule disjE) -prefer 2 apply (blast intro: subset_imp_ensures) -apply (auto dest: extend_transient [THEN iffD2] - intro: transient_strengthen project_set_I - project_unless [THEN unlessD] unlessI - project_extend_constrains_I - simp add: ensures_def Join_transient) + "[| extend h F Join G \ stable C; + F Join project h C G \ A ensures B |] + ==> extend h F Join G \ (C \ extend_set h A) ensures (extend_set h B)" +apply (auto simp add: ensures_eq extend_unless project_unless) +apply (blast intro: extend_transient [THEN iffD2] transient_strengthen) +apply (blast intro: project_transient_extend_set transient_strengthen) done text{*Lemma useful for both STRONG and WEAK progress, but the transient @@ -478,11 +496,10 @@ (*The strange induction formula allows induction over the leadsTo assumption's non-atomic precondition*) lemma (in Extend) PLD_lemma: - "[| ALL D. project h C G : transient D --> D={}; - extend h F Join G : stable C; - F Join project h C G : (project_set h C Int A) leadsTo B |] - ==> extend h F Join G : - C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)" + "[| extend h F Join G \ stable C; + F Join project h C G \ (project_set h C \ A) leadsTo B |] + ==> extend h F Join G \ + C \ extend_set h (project_set h C \ A) leadsTo (extend_set h B)" apply (erule leadsTo_induct) apply (blast intro: leadsTo_Basis Join_project_ensures) apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans) @@ -490,74 +507,28 @@ done lemma (in Extend) project_leadsTo_D_lemma: - "[| ALL D. project h C G : transient D --> D={}; - extend h F Join G : stable C; - F Join project h C G : (project_set h C Int A) leadsTo B |] - ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)" + "[| extend h F Join G \ stable C; + F Join project h C G \ (project_set h C \ A) leadsTo B |] + ==> extend h F Join G \ (C \ extend_set h A) leadsTo (extend_set h B)" apply (rule PLD_lemma [THEN leadsTo_weaken]) apply (auto simp add: split_extended_all) done lemma (in Extend) Join_project_LeadsTo: "[| C = (reachable (extend h F Join G)); - ALL D. project h C G : transient D --> D={}; - F Join project h C G : A LeadsTo B |] - ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)" + F Join project h C G \ A LeadsTo B |] + ==> extend h F Join G \ (extend_set h A) LeadsTo (extend_set h B)" by (simp del: Join_stable add: LeadsTo_def project_leadsTo_D_lemma project_set_reachable_extend_eq) subsection{*Towards the theorem @{text project_Ensures_D}*} - -lemma (in Extend) act_subset_imp_project_act_subset: - "act `` (C Int extend_set h A) <= B - ==> project_act h (Restrict C act) `` (project_set h C Int A) - <= project_set h B" -apply (unfold project_set_def extend_set_def project_act_def, blast) -done - -(*This trivial proof is the complementation part of transferring a transient - property upwards. The hard part would be to - show that G's action has a big enough domain.*) -lemma (in Extend) - "[| act: Acts G; - (project_act h (Restrict C act))`` - (project_set h C Int A - B) <= -(project_set h C Int A - B) |] - ==> act``(C Int extend_set h A - extend_set h B) - <= -(C Int extend_set h A - extend_set h B)" -by (auto simp add: project_set_def extend_set_def project_act_def) - -lemma (in Extend) stable_project_transient: - "[| G : stable ((C Int extend_set h A) - (extend_set h B)); - project h C G : transient (project_set h C Int A - B) |] - ==> (C Int extend_set h A) - extend_set h B = {}" -apply (auto simp add: transient_def subset_Compl_self_eq Domain_project_act split_extended_all, blast) -apply (auto simp add: stable_def constrains_def) -apply (drule bspec, assumption) -apply (auto simp add: Int_Diff extend_set_Diff_distrib [symmetric]) -apply (drule act_subset_imp_project_act_subset) -apply (subgoal_tac "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}") -apply (erule_tac V = "?r``?A <= ?B" in thin_rl)+ -apply (unfold project_set_def extend_set_def project_act_def) -prefer 2 apply blast -apply (rule ccontr) -apply (drule subsetD, blast) -apply (force simp add: split_extended_all) -done - -lemma (in Extend) project_unless2 [rule_format]: - "[| G : stable C; project h C G : (project_set h C Int A) unless B |] - ==> G : (C Int extend_set h A) unless (extend_set h B)" -by (auto dest: stable_constrains_Int intro: constrains_weaken - simp add: unless_def project_constrains Diff_eq Int_assoc - Int_extend_set_lemma) - lemma (in Extend) project_ensures_D_lemma: - "[| G : stable ((C Int extend_set h A) - (extend_set h B)); - F Join project h C G : (project_set h C Int A) ensures B; - extend h F Join G : stable C |] - ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)" + "[| G \ stable ((C \ extend_set h A) - (extend_set h B)); + F Join project h C G \ (project_set h C \ A) ensures B; + extend h F Join G \ stable C |] + ==> extend h F Join G \ (C \ extend_set h A) ensures (extend_set h B)" (*unless*) apply (auto intro!: project_unless2 [unfolded unless_def] intro: project_extend_constrains_I @@ -565,26 +536,24 @@ (*transient*) (*A G-action cannot occur*) prefer 2 - apply (force dest: stable_project_transient - simp del: Diff_eq_empty_iff - simp add: Diff_eq_empty_iff [symmetric]) + apply (blast intro: project_transient_extend_set) (*An F-action*) apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen] simp add: split_extended_all) done lemma (in Extend) project_ensures_D: - "[| F Join project h UNIV G : A ensures B; - G : stable (extend_set h A - extend_set h B) |] - ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)" + "[| F Join project h UNIV G \ A ensures B; + G \ stable (extend_set h A - extend_set h B) |] + ==> extend h F Join G \ (extend_set h A) ensures (extend_set h B)" apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto) done lemma (in Extend) project_Ensures_D: - "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B; - G : stable (reachable (extend h F Join G) Int extend_set h A - + "[| F Join project h (reachable (extend h F Join G)) G \ A Ensures B; + G \ stable (reachable (extend h F Join G) \ extend_set h A - extend_set h B) |] - ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)" + ==> extend h F Join G \ (extend_set h A) Ensures (extend_set h B)" apply (unfold Ensures_def) apply (rule project_ensures_D_lemma [THEN revcut_rl]) apply (auto simp add: project_set_reachable_extend_eq [symmetric]) @@ -594,7 +563,7 @@ subsection{*Guarantees*} lemma (in Extend) project_act_Restrict_subset_project_act: - "project_act h (Restrict C act) <= project_act h act" + "project_act h (Restrict C act) \ project_act h act" apply (auto simp add: project_act_def) done @@ -616,24 +585,24 @@ Not clear that it has a converse [or that we want one!]*) (*The raw version; 3rd premise could be weakened by adding the - precondition extend h F Join G : X' *) + precondition extend h F Join G \ X' *) lemma (in Extend) project_guarantees_raw: - assumes xguary: "F : X guarantees Y" + assumes xguary: "F \ X guarantees Y" and closed: "subset_closed (AllowedActs F)" - and project: "!!G. extend h F Join G : X' - ==> F Join project h (C G) G : X" - and extend: "!!G. [| F Join project h (C G) G : Y |] - ==> extend h F Join G : Y'" - shows "extend h F : X' guarantees Y'" + and project: "!!G. extend h F Join G \ X' + ==> F Join project h (C G) G \ X" + and extend: "!!G. [| F Join project h (C G) G \ Y |] + ==> extend h F Join G \ Y'" + shows "extend h F \ X' guarantees Y'" apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI]) apply (blast intro: closed subset_closed_ok_extend_imp_ok_project) apply (erule project) done lemma (in Extend) project_guarantees: - "[| F : X guarantees Y; subset_closed (AllowedActs F); + "[| F \ X guarantees Y; subset_closed (AllowedActs F); projecting C h F X' X; extending C h F Y' Y |] - ==> extend h F : X' guarantees Y'" + ==> extend h F \ X' guarantees Y'" apply (rule guaranteesI) apply (auto simp add: guaranteesD projecting_def extending_def subset_closed_ok_extend_imp_ok_project) @@ -648,73 +617,58 @@ subsubsection{*Some could be deleted: the required versions are easy to prove*} lemma (in Extend) extend_guar_increasing: - "[| F : UNIV guarantees increasing func; + "[| F \ UNIV guarantees increasing func; subset_closed (AllowedActs F) |] - ==> extend h F : X' guarantees increasing (func o f)" + ==> extend h F \ X' guarantees increasing (func o f)" apply (erule project_guarantees) apply (rule_tac [3] extending_increasing) apply (rule_tac [2] projecting_UNIV, auto) done lemma (in Extend) extend_guar_Increasing: - "[| F : UNIV guarantees Increasing func; + "[| F \ UNIV guarantees Increasing func; subset_closed (AllowedActs F) |] - ==> extend h F : X' guarantees Increasing (func o f)" + ==> extend h F \ X' guarantees Increasing (func o f)" apply (erule project_guarantees) apply (rule_tac [3] extending_Increasing) apply (rule_tac [2] projecting_UNIV, auto) done lemma (in Extend) extend_guar_Always: - "[| F : Always A guarantees Always B; + "[| F \ Always A guarantees Always B; subset_closed (AllowedActs F) |] ==> extend h F - : Always(extend_set h A) guarantees Always(extend_set h B)" + \ Always(extend_set h A) guarantees Always(extend_set h B)" apply (erule project_guarantees) apply (rule_tac [3] extending_Always) apply (rule_tac [2] projecting_Always, auto) done -lemma (in Extend) preserves_project_transient_empty: - "[| G : preserves f; project h C G : transient D |] ==> D={}" -apply (rule stable_transient_empty) - prefer 2 apply assumption -apply (blast intro: project_preserves_id_I - preserves_id_subset_stable [THEN subsetD]) -done - -subsubsection{*Guarantees with a leadsTo postcondition - ALL TOO WEAK because G can't affect F's variables at all**) +subsubsection{*Guarantees with a leadsTo postcondition*} lemma (in Extend) project_leadsTo_D: - "[| F Join project h UNIV G : A leadsTo B; - G : preserves f |] - ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)" -apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken]) -apply (auto dest: preserves_project_transient_empty) + "F Join project h UNIV G \ A leadsTo B + ==> extend h F Join G \ (extend_set h A) leadsTo (extend_set h B)" +apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto) done lemma (in Extend) project_LeadsTo_D: - "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; - G : preserves f |] - ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)" -apply (rule refl [THEN Join_project_LeadsTo]) -apply (auto dest: preserves_project_transient_empty) + "F Join project h (reachable (extend h F Join G)) G \ A LeadsTo B + ==> extend h F Join G \ (extend_set h A) LeadsTo (extend_set h B)" +apply (rule refl [THEN Join_project_LeadsTo], auto) done lemma (in Extend) extending_leadsTo: - "(ALL G. extend h F ok G --> G : preserves f) - ==> extending (%G. UNIV) h F - (extend_set h A leadsTo extend_set h B) (A leadsTo B)" + "extending (%G. UNIV) h F + (extend_set h A leadsTo extend_set h B) (A leadsTo B)" apply (unfold extending_def) apply (blast intro: project_leadsTo_D) done lemma (in Extend) extending_LeadsTo: - "(ALL G. extend h F ok G --> G : preserves f) - ==> extending (%G. reachable (extend h F Join G)) h F - (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)" + "extending (%G. reachable (extend h F Join G)) h F + (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)" apply (unfold extending_def) apply (blast intro: project_LeadsTo_D) done