wenzelm@24147: (*  Title:      HOL/UNITY/Project.thy
paulson@7630:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7630:     Copyright   1999  University of Cambridge
paulson@7630: 
wenzelm@32960: Projections of state sets (also of actions and programs).
paulson@7630: 
wenzelm@32960: Inheritance of GUARANTEES properties under extension.
paulson@7630: *)
paulson@7630: 
paulson@13798: header{*Projections of State Sets*}
paulson@13798: 
haftmann@16417: theory Project imports Extend begin
paulson@7826: 
haftmann@35416: definition projecting :: "['c program => 'c set, 'a*'b => 'c, 
haftmann@35416:                   'a program, 'c program set, 'a program set] => bool" where
paulson@10064:     "projecting C h F X' X ==
paulson@13819:        \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X"
paulson@7826: 
haftmann@35416: definition extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
haftmann@35416:                  'c program set, 'a program set] => bool" where
paulson@10064:     "extending C h F Y' Y ==
paulson@13819:        \<forall>G. extend h F  ok G --> F\<squnion>project h (C G) G \<in> Y
wenzelm@32960:               --> extend h F\<squnion>G \<in> Y'"
paulson@10064: 
haftmann@35416: definition subset_closed :: "'a set set => bool" where
paulson@13812:     "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"  
paulson@7826: 
paulson@13790: 
paulson@13790: lemma (in Extend) project_extend_constrains_I:
paulson@13812:      "F \<in> A co B ==> project h C (extend h F) \<in> A co B"
paulson@13790: apply (auto simp add: extend_act_def project_act_def constrains_def)
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*Safety*}
paulson@13790: 
paulson@13790: (*used below to prove Join_project_ensures*)
paulson@13798: lemma (in Extend) project_unless [rule_format]:
paulson@13812:      "[| G \<in> stable C;  project h C G \<in> A unless B |]  
paulson@13812:       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
paulson@13790: apply (simp add: unless_def project_constrains)
paulson@13790: apply (blast dest: stable_constrains_Int intro: constrains_weaken)
paulson@13790: done
paulson@13790: 
paulson@13819: (*Generalizes project_constrains to the program F\<squnion>project h C G
paulson@13790:   useful with guarantees reasoning*)
paulson@13790: lemma (in Extend) Join_project_constrains:
paulson@13819:      "(F\<squnion>project h C G \<in> A co B)  =   
paulson@13819:         (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
paulson@13812:          F \<in> A co B)"
paulson@13790: apply (simp (no_asm) add: project_constrains)
paulson@13790: apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 
paulson@13790:              dest: constrains_imp_subset)
paulson@13790: done
paulson@13790: 
paulson@13790: (*The condition is required to prove the left-to-right direction
paulson@13812:   could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
paulson@13790: lemma (in Extend) Join_project_stable: 
paulson@13819:      "extend h F\<squnion>G \<in> stable C  
paulson@13819:       ==> (F\<squnion>project h C G \<in> stable A)  =   
paulson@13819:           (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &   
paulson@13812:            F \<in> stable A)"
paulson@13790: apply (unfold stable_def)
paulson@13790: apply (simp only: Join_project_constrains)
paulson@13790: apply (blast intro: constrains_weaken dest: constrains_Int)
paulson@13790: done
paulson@13790: 
paulson@13790: (*For using project_guarantees in particular cases*)
paulson@13790: lemma (in Extend) project_constrains_I:
paulson@13819:      "extend h F\<squnion>G \<in> extend_set h A co extend_set h B  
paulson@13819:       ==> F\<squnion>project h C G \<in> A co B"
paulson@13790: apply (simp add: project_constrains extend_constrains)
paulson@13790: apply (blast intro: constrains_weaken dest: constrains_imp_subset)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_increasing_I: 
paulson@13819:      "extend h F\<squnion>G \<in> increasing (func o f)  
paulson@13819:       ==> F\<squnion>project h C G \<in> increasing func"
paulson@13790: apply (unfold increasing_def stable_def)
paulson@13790: apply (simp del: Join_constrains
paulson@13790:             add: project_constrains_I extend_set_eq_Collect)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) Join_project_increasing:
paulson@13819:      "(F\<squnion>project h UNIV G \<in> increasing func)  =   
paulson@13819:       (extend h F\<squnion>G \<in> increasing (func o f))"
paulson@13790: apply (rule iffI)
paulson@13790: apply (erule_tac [2] project_increasing_I)
paulson@13790: apply (simp del: Join_stable
paulson@13790:             add: increasing_def Join_project_stable)
paulson@13790: apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1])
paulson@13790: done
paulson@13790: 
paulson@13790: (*The UNIV argument is essential*)
paulson@13790: lemma (in Extend) project_constrains_D:
paulson@13819:      "F\<squnion>project h UNIV G \<in> A co B  
paulson@13819:       ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
paulson@13790: by (simp add: project_constrains extend_constrains)
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*"projecting" and union/intersection (no converses)*}
paulson@13790: 
paulson@13790: lemma projecting_Int: 
paulson@13790:      "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
paulson@13812:       ==> projecting C h F (XA' \<inter> XB') (XA \<inter> XB)"
paulson@13790: by (unfold projecting_def, blast)
paulson@13790: 
paulson@13790: lemma projecting_Un: 
paulson@13790:      "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
paulson@13812:       ==> projecting C h F (XA' \<union> XB') (XA \<union> XB)"
paulson@13790: by (unfold projecting_def, blast)
paulson@13790: 
paulson@13790: lemma projecting_INT: 
paulson@13812:      "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
paulson@13812:       ==> projecting C h F (\<Inter>i \<in> I. X' i) (\<Inter>i \<in> I. X i)"
paulson@13790: by (unfold projecting_def, blast)
paulson@13790: 
paulson@13790: lemma projecting_UN: 
paulson@13812:      "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
paulson@13812:       ==> projecting C h F (\<Union>i \<in> I. X' i) (\<Union>i \<in> I. X i)"
paulson@13790: by (unfold projecting_def, blast)
paulson@13790: 
paulson@13790: lemma projecting_weaken: 
paulson@13812:      "[| projecting C h F X' X;  U'<=X';  X \<subseteq> U |] ==> projecting C h F U' U"
paulson@13790: by (unfold projecting_def, auto)
paulson@13790: 
paulson@13790: lemma projecting_weaken_L: 
paulson@13790:      "[| projecting C h F X' X;  U'<=X' |] ==> projecting C h F U' X"
paulson@13790: by (unfold projecting_def, auto)
paulson@13790: 
paulson@13790: lemma extending_Int: 
paulson@13790:      "[| extending C h F YA' YA;  extending C h F YB' YB |]  
paulson@13812:       ==> extending C h F (YA' \<inter> YB') (YA \<inter> YB)"
paulson@13790: by (unfold extending_def, blast)
paulson@13790: 
paulson@13790: lemma extending_Un: 
paulson@13790:      "[| extending C h F YA' YA;  extending C h F YB' YB |]  
paulson@13812:       ==> extending C h F (YA' \<union> YB') (YA \<union> YB)"
paulson@13790: by (unfold extending_def, blast)
paulson@13790: 
paulson@13790: lemma extending_INT: 
paulson@13812:      "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
paulson@13812:       ==> extending C h F (\<Inter>i \<in> I. Y' i) (\<Inter>i \<in> I. Y i)"
paulson@13790: by (unfold extending_def, blast)
paulson@13790: 
paulson@13790: lemma extending_UN: 
paulson@13812:      "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
paulson@13812:       ==> extending C h F (\<Union>i \<in> I. Y' i) (\<Union>i \<in> I. Y i)"
paulson@13790: by (unfold extending_def, blast)
paulson@13790: 
paulson@13790: lemma extending_weaken: 
paulson@13812:      "[| extending C h F Y' Y;  Y'<=V';  V \<subseteq> Y |] ==> extending C h F V' V"
paulson@13790: by (unfold extending_def, auto)
paulson@13790: 
paulson@13790: lemma extending_weaken_L: 
paulson@13790:      "[| extending C h F Y' Y;  Y'<=V' |] ==> extending C h F V' Y"
paulson@13790: by (unfold extending_def, auto)
paulson@13790: 
paulson@13790: lemma projecting_UNIV: "projecting C h F X' UNIV"
paulson@13790: by (simp add: projecting_def)
paulson@13790: 
paulson@13790: lemma (in Extend) projecting_constrains: 
paulson@13790:      "projecting C h F (extend_set h A co extend_set h B) (A co B)"
paulson@13790: apply (unfold projecting_def)
paulson@13790: apply (blast intro: project_constrains_I)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) projecting_stable: 
paulson@13790:      "projecting C h F (stable (extend_set h A)) (stable A)"
paulson@13790: apply (unfold stable_def)
paulson@13790: apply (rule projecting_constrains)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) projecting_increasing: 
paulson@13790:      "projecting C h F (increasing (func o f)) (increasing func)"
paulson@13790: apply (unfold projecting_def)
paulson@13790: apply (blast intro: project_increasing_I)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_UNIV: "extending C h F UNIV Y"
paulson@13790: apply (simp (no_asm) add: extending_def)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_constrains: 
paulson@13790:      "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)"
paulson@13790: apply (unfold extending_def)
paulson@13790: apply (blast intro: project_constrains_D)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_stable: 
paulson@13790:      "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)"
paulson@13790: apply (unfold stable_def)
paulson@13790: apply (rule extending_constrains)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_increasing: 
paulson@13790:      "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)"
paulson@13790: by (force simp only: extending_def Join_project_increasing)
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*Reachability and project*}
paulson@13790: 
paulson@13790: (*In practice, C = reachable(...): the inclusion is equality*)
paulson@13790: lemma (in Extend) reachable_imp_reachable_project:
paulson@13819:      "[| reachable (extend h F\<squnion>G) \<subseteq> C;   
paulson@13819:          z \<in> reachable (extend h F\<squnion>G) |]  
paulson@13819:       ==> f z \<in> reachable (F\<squnion>project h C G)"
paulson@13790: apply (erule reachable.induct)
paulson@13790: apply (force intro!: reachable.Init simp add: split_extended_all, auto)
paulson@13790:  apply (rule_tac act = x in reachable.Acts)
paulson@13790:  apply auto
paulson@13790:  apply (erule extend_act_D)
paulson@13790: apply (rule_tac act1 = "Restrict C act"
paulson@13790:        in project_act_I [THEN [3] reachable.Acts], auto) 
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Constrains_D: 
paulson@13819:      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B   
paulson@13819:       ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)"
paulson@13790: apply (unfold Constrains_def)
paulson@13790: apply (simp del: Join_constrains
paulson@13790:             add: Join_project_constrains, clarify)
paulson@13790: apply (erule constrains_weaken)
paulson@13790: apply (auto intro: reachable_imp_reachable_project)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Stable_D: 
paulson@13819:      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A   
paulson@13819:       ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
paulson@13790: apply (unfold Stable_def)
paulson@13790: apply (simp (no_asm_simp) add: project_Constrains_D)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Always_D: 
paulson@13819:      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A   
paulson@13819:       ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
paulson@13790: apply (unfold Always_def)
paulson@13790: apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Increasing_D: 
paulson@13819:      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func   
paulson@13819:       ==> extend h F\<squnion>G \<in> Increasing (func o f)"
paulson@13790: apply (unfold Increasing_def, auto)
paulson@13790: apply (subst extend_set_eq_Collect [symmetric])
paulson@13790: apply (simp (no_asm_simp) add: project_Stable_D)
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*Converse results for weak safety: benefits of the argument C *}
paulson@13790: 
paulson@13790: (*In practice, C = reachable(...): the inclusion is equality*)
paulson@13790: lemma (in Extend) reachable_project_imp_reachable:
paulson@13819:      "[| C \<subseteq> reachable(extend h F\<squnion>G);    
paulson@13819:          x \<in> reachable (F\<squnion>project h C G) |]  
paulson@13819:       ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)"
paulson@13790: apply (erule reachable.induct)
paulson@13790: apply  (force intro: reachable.Init)
paulson@13790: apply (auto simp add: project_act_def)
paulson@13790: apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_set_reachable_extend_eq:
paulson@13819:      "project_set h (reachable (extend h F\<squnion>G)) =  
paulson@13819:       reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)"
paulson@13790: by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 
paulson@13790:                subset_refl [THEN reachable_project_imp_reachable])
paulson@13790: 
paulson@13790: (*UNUSED*)
paulson@13790: lemma (in Extend) reachable_extend_Join_subset:
paulson@13819:      "reachable (extend h F\<squnion>G) \<subseteq> C   
paulson@13819:       ==> reachable (extend h F\<squnion>G) \<subseteq>  
paulson@13819:           extend_set h (reachable (F\<squnion>project h C G))"
paulson@13790: apply (auto dest: reachable_imp_reachable_project)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Constrains_I: 
paulson@13819:      "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)   
paulson@13819:       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B"
paulson@13790: apply (unfold Constrains_def)
paulson@13790: apply (simp del: Join_constrains
paulson@13790:             add: Join_project_constrains extend_set_Int_distrib)
paulson@13790: apply (rule conjI)
paulson@13790:  prefer 2 
paulson@13790:  apply (force elim: constrains_weaken_L
paulson@13790:               dest!: extend_constrains_project_set
paulson@13790:                      subset_refl [THEN reachable_project_imp_reachable])
paulson@13790: apply (blast intro: constrains_weaken_L)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Stable_I: 
paulson@13819:      "extend h F\<squnion>G \<in> Stable (extend_set h A)   
paulson@13819:       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
paulson@13790: apply (unfold Stable_def)
paulson@13790: apply (simp (no_asm_simp) add: project_Constrains_I)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Always_I: 
paulson@13819:      "extend h F\<squnion>G \<in> Always (extend_set h A)   
paulson@13819:       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
paulson@13790: apply (unfold Always_def)
paulson@13790: apply (auto simp add: project_Stable_I)
paulson@13790: apply (unfold extend_set_def, blast)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Increasing_I: 
paulson@13819:     "extend h F\<squnion>G \<in> Increasing (func o f)   
paulson@13819:      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
paulson@13790: apply (unfold Increasing_def, auto)
paulson@13790: apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Constrains:
paulson@13819:      "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B)  =   
paulson@13819:       (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
paulson@13790: apply (blast intro: project_Constrains_I project_Constrains_D)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Stable: 
paulson@13819:      "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A)  =   
paulson@13819:       (extend h F\<squnion>G \<in> Stable (extend_set h A))"
paulson@13790: apply (unfold Stable_def)
paulson@13790: apply (rule project_Constrains)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Increasing: 
paulson@13819:    "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func)  =  
paulson@13819:     (extend h F\<squnion>G \<in> Increasing (func o f))"
paulson@13790: apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
paulson@13790: done
paulson@13790: 
paulson@13798: subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
paulson@13798:     about guarantees.*}
paulson@13790: 
paulson@13790: lemma (in Extend) projecting_Constrains: 
paulson@13819:      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                  (extend_set h A Co extend_set h B) (A Co B)"
paulson@13790: 
paulson@13790: apply (unfold projecting_def)
paulson@13790: apply (blast intro: project_Constrains_I)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) projecting_Stable: 
paulson@13819:      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                  (Stable (extend_set h A)) (Stable A)"
paulson@13790: apply (unfold Stable_def)
paulson@13790: apply (rule projecting_Constrains)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) projecting_Always: 
paulson@13819:      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                  (Always (extend_set h A)) (Always A)"
paulson@13790: apply (unfold projecting_def)
paulson@13790: apply (blast intro: project_Always_I)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) projecting_Increasing: 
paulson@13819:      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                  (Increasing (func o f)) (Increasing func)"
paulson@13790: apply (unfold projecting_def)
paulson@13790: apply (blast intro: project_Increasing_I)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_Constrains: 
paulson@13819:      "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                   (extend_set h A Co extend_set h B) (A Co B)"
paulson@13790: apply (unfold extending_def)
paulson@13790: apply (blast intro: project_Constrains_D)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_Stable: 
paulson@13819:      "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                   (Stable (extend_set h A)) (Stable A)"
paulson@13790: apply (unfold extending_def)
paulson@13790: apply (blast intro: project_Stable_D)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_Always: 
paulson@13819:      "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                   (Always (extend_set h A)) (Always A)"
paulson@13790: apply (unfold extending_def)
paulson@13790: apply (blast intro: project_Always_D)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_Increasing: 
paulson@13819:      "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790:                   (Increasing (func o f)) (Increasing func)"
paulson@13790: apply (unfold extending_def)
paulson@13790: apply (blast intro: project_Increasing_D)
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*leadsETo in the precondition (??)*}
paulson@13790: 
paulson@13798: subsubsection{*transient*}
paulson@13790: 
paulson@13790: lemma (in Extend) transient_extend_set_imp_project_transient: 
paulson@13812:      "[| G \<in> transient (C \<inter> extend_set h A);  G \<in> stable C |]   
paulson@13812:       ==> project h C G \<in> transient (project_set h C \<inter> A)"
paulson@13812: apply (auto simp add: transient_def Domain_project_act)
paulson@13812: apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A")
paulson@13812:  prefer 2
paulson@13790:  apply (simp add: stable_def constrains_def, blast) 
paulson@13790: (*back to main goal*)
paulson@13812: apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl)
paulson@13790: apply (drule bspec, assumption) 
paulson@13790: apply (simp add: extend_set_def project_act_def, blast)
paulson@13790: done
paulson@13790: 
paulson@13790: (*converse might hold too?*)
paulson@13790: lemma (in Extend) project_extend_transient_D: 
paulson@13812:      "project h C (extend h F) \<in> transient (project_set h C \<inter> D)  
paulson@13812:       ==> F \<in> transient (project_set h C \<inter> D)"
paulson@13812: apply (simp add: transient_def Domain_project_act, safe)
paulson@13812: apply blast+
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13798: subsubsection{*ensures -- a primitive combining progress with safety*}
paulson@13790: 
paulson@13790: (*Used to prove project_leadsETo_I*)
paulson@13790: lemma (in Extend) ensures_extend_set_imp_project_ensures:
paulson@13812:      "[| extend h F \<in> stable C;  G \<in> stable C;   
paulson@13819:          extend h F\<squnion>G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
paulson@13819:       ==> F\<squnion>project h C G   
paulson@13812:             \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
paulson@13812: apply (simp add: ensures_def project_constrains Join_transient extend_transient,
paulson@13812:        clarify)
paulson@13790: apply (intro conjI) 
paulson@13790: (*first subgoal*)
paulson@13790: apply (blast intro: extend_stable_project_set 
paulson@13790:                   [THEN stableD, THEN constrains_Int, THEN constrains_weaken] 
paulson@13790:              dest!: extend_constrains_project_set equalityD1)
paulson@13790: (*2nd subgoal*)
paulson@13790: apply (erule stableD [THEN constrains_Int, THEN constrains_weaken])
paulson@13790:     apply assumption
paulson@13790:    apply (simp (no_asm_use) add: extend_set_def)
paulson@13790:    apply blast
paulson@13790:  apply (simp add: extend_set_Int_distrib extend_set_Un_distrib)
paulson@13790:  apply (blast intro!: extend_set_project_set [THEN subsetD], blast)
paulson@13790: (*The transient part*)
paulson@13790: apply auto
paulson@13790:  prefer 2
paulson@13790:  apply (force dest!: equalityD1
paulson@13790:               intro: transient_extend_set_imp_project_transient
paulson@13790:                          [THEN transient_strengthen])
paulson@13790: apply (simp (no_asm_use) add: Int_Diff)
paulson@13790: apply (force dest!: equalityD1 
paulson@13790:              intro: transient_extend_set_imp_project_transient 
paulson@13790:                [THEN project_extend_transient_D, THEN transient_strengthen])
paulson@13790: done
paulson@13790: 
paulson@13812: text{*Transferring a transient property upwards*}
paulson@13812: lemma (in Extend) project_transient_extend_set:
paulson@13812:      "project h C G \<in> transient (project_set h C \<inter> A - B)
paulson@13812:       ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
paulson@13812: apply (simp add: transient_def project_set_def extend_set_def project_act_def)
paulson@13812: apply (elim disjE bexE)
paulson@13812:  apply (rule_tac x=Id in bexI)  
paulson@13812:   apply (blast intro!: rev_bexI )+
paulson@13812: done
paulson@13812: 
paulson@13812: lemma (in Extend) project_unless2 [rule_format]:
paulson@13812:      "[| G \<in> stable C;  project h C G \<in> (project_set h C \<inter> A) unless B |]  
paulson@13812:       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
paulson@13812: by (auto dest: stable_constrains_Int intro: constrains_weaken
paulson@13812:          simp add: unless_def project_constrains Diff_eq Int_assoc 
paulson@13812:                    Int_extend_set_lemma)
paulson@13812: 
paulson@13812: 
paulson@13812: lemma (in Extend) extend_unless:
paulson@13812:    "[|extend h F \<in> stable C; F \<in> A unless B|]
paulson@13812:     ==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B"
paulson@13812: apply (simp add: unless_def stable_def)
paulson@13812: apply (drule constrains_Int) 
paulson@13812: apply (erule extend_constrains [THEN iffD2]) 
paulson@13812: apply (erule constrains_weaken, blast) 
paulson@13812: apply blast 
paulson@13812: done
paulson@13812: 
paulson@13790: (*Used to prove project_leadsETo_D*)
paulson@13798: lemma (in Extend) Join_project_ensures [rule_format]:
paulson@13819:      "[| extend h F\<squnion>G \<in> stable C;   
paulson@13819:          F\<squnion>project h C G \<in> A ensures B |]  
paulson@13819:       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
paulson@13812: apply (auto simp add: ensures_eq extend_unless project_unless)
paulson@13812: apply (blast intro:  extend_transient [THEN iffD2] transient_strengthen)  
paulson@13812: apply (blast intro: project_transient_extend_set transient_strengthen)  
paulson@13790: done
paulson@13790: 
paulson@13798: text{*Lemma useful for both STRONG and WEAK progress, but the transient
paulson@13798:     condition's very strong*}
paulson@13790: 
paulson@13790: (*The strange induction formula allows induction over the leadsTo
paulson@13790:   assumption's non-atomic precondition*)
paulson@13790: lemma (in Extend) PLD_lemma:
paulson@13819:      "[| extend h F\<squnion>G \<in> stable C;   
paulson@13819:          F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
paulson@13819:       ==> extend h F\<squnion>G \<in>  
paulson@13812:           C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
paulson@13790: apply (erule leadsTo_induct)
paulson@13790:   apply (blast intro: leadsTo_Basis Join_project_ensures)
paulson@13790:  apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
paulson@13790: apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_leadsTo_D_lemma:
paulson@13819:      "[| extend h F\<squnion>G \<in> stable C;   
paulson@13819:          F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
paulson@13819:       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
paulson@13790: apply (rule PLD_lemma [THEN leadsTo_weaken])
paulson@13790: apply (auto simp add: split_extended_all)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) Join_project_LeadsTo:
paulson@13819:      "[| C = (reachable (extend h F\<squnion>G));  
paulson@13819:          F\<squnion>project h C G \<in> A LeadsTo B |]  
paulson@13819:       ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
paulson@13790: by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
paulson@13790:                                   project_set_reachable_extend_eq)
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*Towards the theorem @{text project_Ensures_D}*}
paulson@13790: 
paulson@13790: lemma (in Extend) project_ensures_D_lemma:
paulson@13812:      "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
paulson@13819:          F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;   
paulson@13819:          extend h F\<squnion>G \<in> stable C |]  
paulson@13819:       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
paulson@13790: (*unless*)
paulson@13790: apply (auto intro!: project_unless2 [unfolded unless_def] 
paulson@13790:             intro: project_extend_constrains_I 
paulson@13790:             simp add: ensures_def)
paulson@13790: (*transient*)
paulson@13790: (*A G-action cannot occur*)
paulson@13790:  prefer 2
paulson@13812:  apply (blast intro: project_transient_extend_set) 
paulson@13790: (*An F-action*)
paulson@13790: apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
paulson@13790:              simp add: split_extended_all)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_ensures_D:
paulson@13819:      "[| F\<squnion>project h UNIV G \<in> A ensures B;   
paulson@13812:          G \<in> stable (extend_set h A - extend_set h B) |]  
paulson@13819:       ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
paulson@13790: apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_Ensures_D: 
paulson@13819:      "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B;   
paulson@13819:          G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -  
paulson@13790:                      extend_set h B) |]  
paulson@13819:       ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
paulson@13790: apply (unfold Ensures_def)
paulson@13790: apply (rule project_ensures_D_lemma [THEN revcut_rl])
paulson@13790: apply (auto simp add: project_set_reachable_extend_eq [symmetric])
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*Guarantees*}
paulson@13790: 
paulson@13790: lemma (in Extend) project_act_Restrict_subset_project_act:
paulson@13812:      "project_act h (Restrict C act) \<subseteq> project_act h act"
paulson@13790: apply (auto simp add: project_act_def)
paulson@13790: done
wenzelm@32960:                                            
wenzelm@32960:                                                            
paulson@13790: lemma (in Extend) subset_closed_ok_extend_imp_ok_project:
paulson@13790:      "[| extend h F ok G; subset_closed (AllowedActs F) |]  
paulson@13790:       ==> F ok project h C G"
paulson@13790: apply (auto simp add: ok_def)
paulson@13790: apply (rename_tac act) 
paulson@13790: apply (drule subsetD, blast)
paulson@13790: apply (rule_tac x = "Restrict C  (extend_act h act)" in rev_image_eqI)
paulson@13790: apply simp +
paulson@13790: apply (cut_tac project_act_Restrict_subset_project_act)
paulson@13790: apply (auto simp add: subset_closed_def)
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13790: (*Weak precondition and postcondition
paulson@13790:   Not clear that it has a converse [or that we want one!]*)
paulson@13790: 
paulson@13790: (*The raw version; 3rd premise could be weakened by adding the
paulson@13819:   precondition extend h F\<squnion>G \<in> X' *)
paulson@13790: lemma (in Extend) project_guarantees_raw:
paulson@13812:  assumes xguary:  "F \<in> X guarantees Y"
paulson@13790:      and closed:  "subset_closed (AllowedActs F)"
paulson@13819:      and project: "!!G. extend h F\<squnion>G \<in> X' 
paulson@13819:                         ==> F\<squnion>project h (C G) G \<in> X"
paulson@13819:      and extend:  "!!G. [| F\<squnion>project h (C G) G \<in> Y |]  
paulson@13819:                         ==> extend h F\<squnion>G \<in> Y'"
paulson@13812:  shows "extend h F \<in> X' guarantees Y'"
paulson@13790: apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
paulson@13790: apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
paulson@13790: apply (erule project)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_guarantees:
paulson@13812:      "[| F \<in> X guarantees Y;  subset_closed (AllowedActs F);  
paulson@13790:          projecting C h F X' X;  extending C h F Y' Y |]  
paulson@13812:       ==> extend h F \<in> X' guarantees Y'"
paulson@13790: apply (rule guaranteesI)
paulson@13790: apply (auto simp add: guaranteesD projecting_def extending_def
paulson@13790:                       subset_closed_ok_extend_imp_ok_project)
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13790: (*It seems that neither "guarantees" law can be proved from the other.*)
paulson@13790: 
paulson@13790: 
paulson@13798: subsection{*guarantees corollaries*}
paulson@13790: 
paulson@13798: subsubsection{*Some could be deleted: the required versions are easy to prove*}
paulson@13790: 
paulson@13790: lemma (in Extend) extend_guar_increasing:
paulson@13812:      "[| F \<in> UNIV guarantees increasing func;   
paulson@13790:          subset_closed (AllowedActs F) |]  
paulson@13812:       ==> extend h F \<in> X' guarantees increasing (func o f)"
paulson@13790: apply (erule project_guarantees)
paulson@13790: apply (rule_tac [3] extending_increasing)
paulson@13790: apply (rule_tac [2] projecting_UNIV, auto)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extend_guar_Increasing:
paulson@13812:      "[| F \<in> UNIV guarantees Increasing func;   
paulson@13790:          subset_closed (AllowedActs F) |]  
paulson@13812:       ==> extend h F \<in> X' guarantees Increasing (func o f)"
paulson@13790: apply (erule project_guarantees)
paulson@13790: apply (rule_tac [3] extending_Increasing)
paulson@13790: apply (rule_tac [2] projecting_UNIV, auto)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extend_guar_Always:
paulson@13812:      "[| F \<in> Always A guarantees Always B;   
paulson@13790:          subset_closed (AllowedActs F) |]  
paulson@13790:       ==> extend h F                    
paulson@13812:             \<in> Always(extend_set h A) guarantees Always(extend_set h B)"
paulson@13790: apply (erule project_guarantees)
paulson@13790: apply (rule_tac [3] extending_Always)
paulson@13790: apply (rule_tac [2] projecting_Always, auto)
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13812: subsubsection{*Guarantees with a leadsTo postcondition*}
paulson@13790: 
paulson@13790: lemma (in Extend) project_leadsTo_D:
paulson@13819:      "F\<squnion>project h UNIV G \<in> A leadsTo B
paulson@13819:       ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)"
paulson@13812: apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) project_LeadsTo_D:
paulson@13819:      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B   
paulson@13819:        ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
paulson@13812: apply (rule refl [THEN Join_project_LeadsTo], auto)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_leadsTo: 
paulson@13812:      "extending (%G. UNIV) h F  
paulson@13812:                 (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
paulson@13790: apply (unfold extending_def)
paulson@13790: apply (blast intro: project_leadsTo_D)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma (in Extend) extending_LeadsTo: 
paulson@13819:      "extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13812:                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
paulson@13790: apply (unfold extending_def)
paulson@13790: apply (blast intro: project_LeadsTo_D)
paulson@13790: done
paulson@13790: 
paulson@7826: end