(* Title: HOL/UNITY/Project.ML ID: $Id: Project.thy,v 1.13 2005/06/17 14:13:10 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge Projections of state sets (also of actions and programs) Inheritance of GUARANTEES properties under extension *) header{*Projections of State Sets*} theory Project imports Extend begin constdefs projecting :: "['c program => 'c set, 'a*'b => 'c, 'a program, 'c program set, 'a program set] => bool" "projecting C h F X' X == ∀G. extend h F\<squnion>G ∈ X' --> F\<squnion>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 == ∀G. extend h F ok G --> F\<squnion>project h (C G) G ∈ Y --> extend h F\<squnion>G ∈ Y'" subset_closed :: "'a set set => bool" "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" apply (auto simp add: extend_act_def project_act_def constrains_def) done subsection{*Safety*} (*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 ∩ 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 (*Generalizes project_constrains to the program F\<squnion>project h C G useful with guarantees reasoning*) lemma (in Extend) Join_project_constrains: "(F\<squnion>project h C G ∈ A co B) = (extend h F\<squnion>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 ∩ extend_set h A) co C*) lemma (in Extend) Join_project_stable: "extend h F\<squnion>G ∈ stable C ==> (F\<squnion>project h C G ∈ stable A) = (extend h F\<squnion>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) done (*For using project_guarantees in particular cases*) lemma (in Extend) project_constrains_I: "extend h F\<squnion>G ∈ extend_set h A co extend_set h B ==> F\<squnion>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\<squnion>G ∈ increasing (func o f) ==> F\<squnion>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\<squnion>project h UNIV G ∈ increasing func) = (extend h F\<squnion>G ∈ increasing (func o f))" apply (rule iffI) apply (erule_tac [2] project_increasing_I) apply (simp del: Join_stable add: increasing_def Join_project_stable) apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1]) done (*The UNIV argument is essential*) lemma (in Extend) project_constrains_D: "F\<squnion>project h UNIV G ∈ A co B ==> extend h F\<squnion>G ∈ extend_set h A co extend_set h B" by (simp add: project_constrains extend_constrains) subsection{*"projecting" and union/intersection (no converses)*} lemma projecting_Int: "[| projecting C h F XA' XA; projecting C h F XB' 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' ∪ 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 (\<Inter>i ∈ I. X' i) (\<Inter>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 (\<Union>i ∈ I. X' i) (\<Union>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" by (unfold projecting_def, auto) lemma projecting_weaken_L: "[| projecting C h F X' X; U'<=X' |] ==> projecting C h F U' X" by (unfold projecting_def, auto) lemma extending_Int: "[| extending C h F YA' YA; extending C h F YB' 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' ∪ 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 (\<Inter>i ∈ I. Y' i) (\<Inter>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 (\<Union>i ∈ I. Y' i) (\<Union>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" by (unfold extending_def, auto) lemma extending_weaken_L: "[| extending C h F Y' Y; Y'<=V' |] ==> extending C h F V' Y" by (unfold extending_def, auto) lemma projecting_UNIV: "projecting C h F X' UNIV" by (simp add: projecting_def) lemma (in Extend) projecting_constrains: "projecting C h F (extend_set h A co extend_set h B) (A co B)" apply (unfold projecting_def) apply (blast intro: project_constrains_I) done lemma (in Extend) projecting_stable: "projecting C h F (stable (extend_set h A)) (stable A)" apply (unfold stable_def) apply (rule projecting_constrains) done lemma (in Extend) projecting_increasing: "projecting C h F (increasing (func o f)) (increasing func)" apply (unfold projecting_def) apply (blast intro: project_increasing_I) done lemma (in Extend) extending_UNIV: "extending C h F UNIV Y" apply (simp (no_asm) add: extending_def) done lemma (in Extend) extending_constrains: "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)" apply (unfold extending_def) apply (blast intro: project_constrains_D) done lemma (in Extend) extending_stable: "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)" apply (unfold stable_def) apply (rule extending_constrains) done lemma (in Extend) extending_increasing: "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)" by (force simp only: extending_def Join_project_increasing) subsection{*Reachability and project*} (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_imp_reachable_project: "[| reachable (extend h F\<squnion>G) ⊆ C; z ∈ reachable (extend h F\<squnion>G) |] ==> f z ∈ reachable (F\<squnion>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) apply auto apply (erule extend_act_D) apply (rule_tac act1 = "Restrict C act" in project_act_I [THEN [3] reachable.Acts], auto) done lemma (in Extend) project_Constrains_D: "F\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ A Co B ==> extend h F\<squnion>G ∈ (extend_set h A) Co (extend_set h B)" apply (unfold Constrains_def) apply (simp del: Join_constrains add: Join_project_constrains, clarify) apply (erule constrains_weaken) apply (auto intro: reachable_imp_reachable_project) done lemma (in Extend) project_Stable_D: "F\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ Stable A ==> extend h F\<squnion>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\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ Always A ==> extend h F\<squnion>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\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ Increasing func ==> extend h F\<squnion>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) done subsection{*Converse results for weak safety: benefits of the argument C *} (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_project_imp_reachable: "[| C ⊆ reachable(extend h F\<squnion>G); x ∈ reachable (F\<squnion>project h C G) |] ==> ∃y. h(x,y) ∈ reachable (extend h F\<squnion>G)" apply (erule reachable.induct) apply (force intro: reachable.Init) apply (auto simp add: project_act_def) apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+ done lemma (in Extend) project_set_reachable_extend_eq: "project_set h (reachable (extend h F\<squnion>G)) = reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)" by (auto dest: subset_refl [THEN reachable_imp_reachable_project] subset_refl [THEN reachable_project_imp_reachable]) (*UNUSED*) lemma (in Extend) reachable_extend_Join_subset: "reachable (extend h F\<squnion>G) ⊆ C ==> reachable (extend h F\<squnion>G) ⊆ extend_set h (reachable (F\<squnion>project h C G))" apply (auto dest: reachable_imp_reachable_project) done lemma (in Extend) project_Constrains_I: "extend h F\<squnion>G ∈ (extend_set h A) Co (extend_set h B) ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ A Co B" apply (unfold Constrains_def) apply (simp del: Join_constrains add: Join_project_constrains extend_set_Int_distrib) apply (rule conjI) prefer 2 apply (force elim: constrains_weaken_L dest!: extend_constrains_project_set subset_refl [THEN reachable_project_imp_reachable]) apply (blast intro: constrains_weaken_L) done lemma (in Extend) project_Stable_I: "extend h F\<squnion>G ∈ Stable (extend_set h A) ==> F\<squnion>project h (reachable (extend h F\<squnion>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\<squnion>G ∈ Always (extend_set h A) ==> F\<squnion>project h (reachable (extend h F\<squnion>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\<squnion>G ∈ Increasing (func o f) ==> F\<squnion>project h (reachable (extend h F\<squnion>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\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ A Co B) = (extend h F\<squnion>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\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ Stable A) = (extend h F\<squnion>G ∈ Stable (extend_set h A))" apply (unfold Stable_def) apply (rule project_Constrains) done lemma (in Extend) project_Increasing: "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ Increasing func) = (extend h F\<squnion>G ∈ Increasing (func o f))" apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect) done subsection{*A lot of redundant theorems: all are proved to facilitate reasoning about guarantees.*} lemma (in Extend) projecting_Constrains: "projecting (%G. reachable (extend h F\<squnion>G)) h F (extend_set h A Co extend_set h B) (A Co B)" apply (unfold projecting_def) apply (blast intro: project_Constrains_I) done lemma (in Extend) projecting_Stable: "projecting (%G. reachable (extend h F\<squnion>G)) h F (Stable (extend_set h A)) (Stable A)" apply (unfold Stable_def) apply (rule projecting_Constrains) done lemma (in Extend) projecting_Always: "projecting (%G. reachable (extend h F\<squnion>G)) h F (Always (extend_set h A)) (Always A)" apply (unfold projecting_def) apply (blast intro: project_Always_I) done lemma (in Extend) projecting_Increasing: "projecting (%G. reachable (extend h F\<squnion>G)) h F (Increasing (func o f)) (Increasing func)" apply (unfold projecting_def) apply (blast intro: project_Increasing_I) done lemma (in Extend) extending_Constrains: "extending (%G. reachable (extend h F\<squnion>G)) h F (extend_set h A Co extend_set h B) (A Co B)" apply (unfold extending_def) apply (blast intro: project_Constrains_D) done lemma (in Extend) extending_Stable: "extending (%G. reachable (extend h F\<squnion>G)) h F (Stable (extend_set h A)) (Stable A)" apply (unfold extending_def) apply (blast intro: project_Stable_D) done lemma (in Extend) extending_Always: "extending (%G. reachable (extend h F\<squnion>G)) h F (Always (extend_set h A)) (Always A)" apply (unfold extending_def) apply (blast intro: project_Always_D) done lemma (in Extend) extending_Increasing: "extending (%G. reachable (extend h F\<squnion>G)) h F (Increasing (func o f)) (Increasing func)" apply (unfold extending_def) apply (blast intro: project_Increasing_D) done subsection{*leadsETo in the precondition (??)*} subsubsection{*transient*} lemma (in Extend) transient_extend_set_imp_project_transient: "[| 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 ∪ ?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 ∩ D) ==> F ∈ transient (project_set h C ∩ D)" apply (simp add: transient_def Domain_project_act, safe) apply blast+ done subsubsection{*ensures -- a primitive combining progress with safety*} (*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\<squnion>G ∈ A ensures B; A-B = C ∩ extend_set h D |] ==> F\<squnion>project h C G ∈ (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 [THEN stableD, THEN constrains_Int, THEN constrains_weaken] dest!: extend_constrains_project_set equalityD1) (*2nd subgoal*) apply (erule stableD [THEN constrains_Int, THEN constrains_weaken]) apply assumption apply (simp (no_asm_use) add: extend_set_def) apply blast apply (simp add: extend_set_Int_distrib extend_set_Un_distrib) apply (blast intro!: extend_set_project_set [THEN subsetD], blast) (*The transient part*) apply auto prefer 2 apply (force dest!: equalityD1 intro: transient_extend_set_imp_project_transient [THEN transient_strengthen]) apply (simp (no_asm_use) add: Int_Diff) apply (force dest!: equalityD1 intro: transient_extend_set_imp_project_transient [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]: "[| extend h F\<squnion>G ∈ stable C; F\<squnion>project h C G ∈ A ensures B |] ==> extend h F\<squnion>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 condition's very strong*} (*The strange induction formula allows induction over the leadsTo assumption's non-atomic precondition*) lemma (in Extend) PLD_lemma: "[| extend h F\<squnion>G ∈ stable C; F\<squnion>project h C G ∈ (project_set h C ∩ A) leadsTo B |] ==> extend h F\<squnion>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) apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union) done lemma (in Extend) project_leadsTo_D_lemma: "[| extend h F\<squnion>G ∈ stable C; F\<squnion>project h C G ∈ (project_set h C ∩ A) leadsTo B |] ==> extend h F\<squnion>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\<squnion>G)); F\<squnion>project h C G ∈ A LeadsTo B |] ==> extend h F\<squnion>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) project_ensures_D_lemma: "[| G ∈ stable ((C ∩ extend_set h A) - (extend_set h B)); F\<squnion>project h C G ∈ (project_set h C ∩ A) ensures B; extend h F\<squnion>G ∈ stable C |] ==> extend h F\<squnion>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 simp add: ensures_def) (*transient*) (*A G-action cannot occur*) prefer 2 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\<squnion>project h UNIV G ∈ A ensures B; G ∈ stable (extend_set h A - extend_set h B) |] ==> extend h F\<squnion>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\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ A Ensures B; G ∈ stable (reachable (extend h F\<squnion>G) ∩ extend_set h A - extend_set h B) |] ==> extend h F\<squnion>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]) done subsection{*Guarantees*} lemma (in Extend) project_act_Restrict_subset_project_act: "project_act h (Restrict C act) ⊆ project_act h act" apply (auto simp add: project_act_def) done lemma (in Extend) subset_closed_ok_extend_imp_ok_project: "[| extend h F ok G; subset_closed (AllowedActs F) |] ==> F ok project h C G" apply (auto simp add: ok_def) apply (rename_tac act) apply (drule subsetD, blast) apply (rule_tac x = "Restrict C (extend_act h act)" in rev_image_eqI) apply simp + apply (cut_tac project_act_Restrict_subset_project_act) apply (auto simp add: subset_closed_def) done (*Weak precondition and postcondition 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\<squnion>G ∈ X' *) lemma (in Extend) project_guarantees_raw: assumes xguary: "F ∈ X guarantees Y" and closed: "subset_closed (AllowedActs F)" and project: "!!G. extend h F\<squnion>G ∈ X' ==> F\<squnion>project h (C G) G ∈ X" and extend: "!!G. [| F\<squnion>project h (C G) G ∈ Y |] ==> extend h F\<squnion>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); projecting C h F X' X; extending C h F Y' 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) done (*It seems that neither "guarantees" law can be proved from the other.*) subsection{*guarantees corollaries*} subsubsection{*Some could be deleted: the required versions are easy to prove*} lemma (in Extend) extend_guar_increasing: "[| F ∈ UNIV guarantees increasing func; subset_closed (AllowedActs 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; subset_closed (AllowedActs 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; subset_closed (AllowedActs F) |] ==> extend h F ∈ 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 subsubsection{*Guarantees with a leadsTo postcondition*} lemma (in Extend) project_leadsTo_D: "F\<squnion>project h UNIV G ∈ A leadsTo B ==> extend h F\<squnion>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\<squnion>project h (reachable (extend h F\<squnion>G)) G ∈ A LeadsTo B ==> extend h F\<squnion>G ∈ (extend_set h A) LeadsTo (extend_set h B)" apply (rule refl [THEN Join_project_LeadsTo], auto) done lemma (in Extend) extending_leadsTo: "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: "extending (%G. reachable (extend h F\<squnion>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 ML {* val projecting_Int = thm "projecting_Int"; val projecting_Un = thm "projecting_Un"; val projecting_INT = thm "projecting_INT"; val projecting_UN = thm "projecting_UN"; val projecting_weaken = thm "projecting_weaken"; val projecting_weaken_L = thm "projecting_weaken_L"; val extending_Int = thm "extending_Int"; val extending_Un = thm "extending_Un"; val extending_INT = thm "extending_INT"; val extending_UN = thm "extending_UN"; val extending_weaken = thm "extending_weaken"; val extending_weaken_L = thm "extending_weaken_L"; val projecting_UNIV = thm "projecting_UNIV"; *} end
lemma project_extend_constrains_I:
[| Extend h; F ∈ A co B |] ==> project h C (extend h F) ∈ A co B
lemma project_unless:
[| Extend h; G ∈ stable C; project h C G ∈ A unless B |] ==> G ∈ C ∩ extend_set h A unless extend_set h B
lemma Join_project_constrains:
Extend h ==> (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)
lemma Join_project_stable:
[| Extend h; 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)
lemma project_constrains_I:
[| Extend h; extend h F Join G ∈ extend_set h A co extend_set h B |] ==> F Join project h C G ∈ A co B
lemma project_increasing_I:
[| Extend h; extend h F Join G ∈ increasing (func o (%z. fst (inv h z))) |] ==> F Join project h C G ∈ increasing func
lemma Join_project_increasing:
Extend h ==> (F Join project h UNIV G ∈ increasing func) = (extend h F Join G ∈ increasing (func o (%z. fst (inv h z))))
lemma project_constrains_D:
[| Extend h; F Join project h UNIV G ∈ A co B |] ==> extend h F Join G ∈ extend_set h A co extend_set h B
lemma projecting_Int:
[| projecting C h F XA' XA; projecting C h F XB' XB |] ==> projecting C h F (XA' ∩ XB') (XA ∩ XB)
lemma projecting_Un:
[| projecting C h F XA' XA; projecting C h F XB' XB |] ==> projecting C h F (XA' ∪ XB') (XA ∪ XB)
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)
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)
lemma projecting_weaken:
[| projecting C h F X' X; U' ⊆ X'; X ⊆ U |] ==> projecting C h F U' U
lemma projecting_weaken_L:
[| projecting C h F X' X; U' ⊆ X' |] ==> projecting C h F U' X
lemma extending_Int:
[| extending C h F YA' YA; extending C h F YB' YB |] ==> extending C h F (YA' ∩ YB') (YA ∩ YB)
lemma extending_Un:
[| extending C h F YA' YA; extending C h F YB' YB |] ==> extending C h F (YA' ∪ YB') (YA ∪ YB)
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)
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)
lemma extending_weaken:
[| extending C h F Y' Y; Y' ⊆ V'; V ⊆ Y |] ==> extending C h F V' V
lemma extending_weaken_L:
[| extending C h F Y' Y; Y' ⊆ V' |] ==> extending C h F V' Y
lemma projecting_UNIV:
projecting C h F X' UNIV
lemma projecting_constrains:
Extend h ==> projecting C h F (extend_set h A co extend_set h B) (A co B)
lemma projecting_stable:
Extend h ==> projecting C h F (stable (extend_set h A)) (stable A)
lemma projecting_increasing:
Extend h ==> projecting C h F (increasing (func o (%z. fst (inv h z)))) (increasing func)
lemma extending_UNIV:
Extend h ==> extending C h F UNIV Y
lemma extending_constrains:
Extend h ==> extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)
lemma extending_stable:
Extend h ==> extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)
lemma extending_increasing:
Extend h ==> extending (%G. UNIV) h F (increasing (func o (%z. fst (inv h z)))) (increasing func)
lemma reachable_imp_reachable_project:
[| Extend h; reachable (extend h F Join G) ⊆ C; z ∈ reachable (extend h F Join G) |] ==> fst (inv h z) ∈ reachable (F Join project h C G)
lemma project_Constrains_D:
[| Extend h; 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
lemma project_Stable_D:
[| Extend h; F Join project h (reachable (extend h F Join G)) G ∈ Stable A |] ==> extend h F Join G ∈ Stable (extend_set h A)
lemma project_Always_D:
[| Extend h; F Join project h (reachable (extend h F Join G)) G ∈ Always A |] ==> extend h F Join G ∈ Always (extend_set h A)
lemma project_Increasing_D:
[| Extend h; F Join project h (reachable (extend h F Join G)) G ∈ Increasing func |] ==> extend h F Join G ∈ Increasing (func o (%z. fst (inv h z)))
lemma reachable_project_imp_reachable:
[| Extend h; 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)
lemma project_set_reachable_extend_eq:
Extend h ==> project_set h (reachable (extend h F Join G)) = reachable (F Join project h (reachable (extend h F Join G)) G)
lemma reachable_extend_Join_subset:
[| Extend h; reachable (extend h F Join G) ⊆ C |] ==> reachable (extend h F Join G) ⊆ extend_set h (reachable (F Join project h C G))
lemma project_Constrains_I:
[| Extend h; 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
lemma project_Stable_I:
[| Extend h; extend h F Join G ∈ Stable (extend_set h A) |] ==> F Join project h (reachable (extend h F Join G)) G ∈ Stable A
lemma project_Always_I:
[| Extend h; extend h F Join G ∈ Always (extend_set h A) |] ==> F Join project h (reachable (extend h F Join G)) G ∈ Always A
lemma project_Increasing_I:
[| Extend h; extend h F Join G ∈ Increasing (func o (%z. fst (inv h z))) |] ==> F Join project h (reachable (extend h F Join G)) G ∈ Increasing func
lemma project_Constrains:
Extend h ==> (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)
lemma project_Stable:
Extend h ==> (F Join project h (reachable (extend h F Join G)) G ∈ Stable A) = (extend h F Join G ∈ Stable (extend_set h A))
lemma project_Increasing:
Extend h ==> (F Join project h (reachable (extend h F Join G)) G ∈ Increasing func) = (extend h F Join G ∈ Increasing (func o (%z. fst (inv h z))))
lemma projecting_Constrains:
Extend h ==> projecting (%G. reachable (extend h F Join G)) h F (extend_set h A Co extend_set h B) (A Co B)
lemma projecting_Stable:
Extend h ==> projecting (%G. reachable (extend h F Join G)) h F (Stable (extend_set h A)) (Stable A)
lemma projecting_Always:
Extend h ==> projecting (%G. reachable (extend h F Join G)) h F (Always (extend_set h A)) (Always A)
lemma projecting_Increasing:
Extend h ==> projecting (%G. reachable (extend h F Join G)) h F (Increasing (func o (%z. fst (inv h z)))) (Increasing func)
lemma extending_Constrains:
Extend h ==> extending (%G. reachable (extend h F Join G)) h F (extend_set h A Co extend_set h B) (A Co B)
lemma extending_Stable:
Extend h ==> extending (%G. reachable (extend h F Join G)) h F (Stable (extend_set h A)) (Stable A)
lemma extending_Always:
Extend h ==> extending (%G. reachable (extend h F Join G)) h F (Always (extend_set h A)) (Always A)
lemma extending_Increasing:
Extend h ==> extending (%G. reachable (extend h F Join G)) h F (Increasing (func o (%z. fst (inv h z)))) (Increasing func)
lemma transient_extend_set_imp_project_transient:
[| Extend h; G ∈ transient (C ∩ extend_set h A); G ∈ stable C |] ==> project h C G ∈ transient (project_set h C ∩ A)
lemma project_extend_transient_D:
[| Extend h; project h C (extend h F) ∈ transient (project_set h C ∩ D) |] ==> F ∈ transient (project_set h C ∩ D)
lemma ensures_extend_set_imp_project_ensures:
[| Extend h; 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 ∩ project_set h A ensures project_set h B
lemma project_transient_extend_set:
[| Extend h; project h C G ∈ transient (project_set h C ∩ A - B) |] ==> G ∈ transient (C ∩ extend_set h A - extend_set h B)
lemma project_unless2:
[| Extend h; 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
lemma extend_unless:
[| Extend h; extend h F ∈ stable C; F ∈ A unless B |] ==> extend h F ∈ C ∩ extend_set h A unless extend_set h B
lemma Join_project_ensures:
[| Extend h; 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
lemma PLD_lemma:
[| Extend h; 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
lemma project_leadsTo_D_lemma:
[| Extend h; 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
lemma Join_project_LeadsTo:
[| Extend h; C = reachable (extend h F Join G); F Join project h C G ∈ A LeadsTo B |] ==> extend h F Join G ∈ extend_set h A LeadsTo extend_set h B
lemma project_ensures_D_lemma:
[| Extend h; 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
lemma project_ensures_D:
[| Extend h; 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
lemma project_Ensures_D:
[| Extend h; 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
lemma project_act_Restrict_subset_project_act:
Extend h ==> project_act h (Restrict C act) ⊆ project_act h act
lemma subset_closed_ok_extend_imp_ok_project:
[| Extend h; extend h F ok G; subset_closed (AllowedActs F) |] ==> F ok project h C G
lemma project_guarantees_raw:
[| Extend h; F ∈ X guarantees Y; subset_closed (AllowedActs F); !!G. extend h F Join G ∈ X' ==> F Join project h (C G) G ∈ X; !!G. F Join project h (C G) G ∈ Y ==> extend h F Join G ∈ Y' |] ==> extend h F ∈ X' guarantees Y'
lemma project_guarantees:
[| Extend h; 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'
lemma extend_guar_increasing:
[| Extend h; F ∈ UNIV guarantees increasing func; subset_closed (AllowedActs F) |] ==> extend h F ∈ X' guarantees increasing (func o (%z. fst (inv h z)))
lemma extend_guar_Increasing:
[| Extend h; F ∈ UNIV guarantees Increasing func; subset_closed (AllowedActs F) |] ==> extend h F ∈ X' guarantees Increasing (func o (%z. fst (inv h z)))
lemma extend_guar_Always:
[| Extend h; F ∈ Always A guarantees Always B; subset_closed (AllowedActs F) |] ==> extend h F ∈ Always (extend_set h A) guarantees Always (extend_set h B)
lemma project_leadsTo_D:
[| Extend h; F Join project h UNIV G ∈ A leadsTo B |] ==> extend h F Join G ∈ extend_set h A leadsTo extend_set h B
lemma project_LeadsTo_D:
[| Extend h; 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
lemma extending_leadsTo:
Extend h ==> extending (%G. UNIV) h F (extend_set h A leadsTo extend_set h B) (A leadsTo B)
lemma extending_LeadsTo:
Extend h ==> extending (%G. reachable (extend h F Join G)) h F (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)