Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Project.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/UNITY/Project.thy
    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.
*)

section\<open>Projections of State Sets\<close>

theory Project imports Extend begin

definition projecting :: "['c program => 'c set, 'a*'b => 'c,
                  'a program, 'c program set, 'a program set] => bool" where
    "projecting C h F X' X ==
       \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X"

definition extending :: "['c program => 'c set, 'a*'b => 'c, 'a program,
                 'c program set, 'a program set] => bool" where
    "extending C h F Y' Y ==
       \<forall>G. extend h F  ok G --> F\<squnion>project h (C G) G \<in> Y
              --> extend h F\<squnion>G \<in> Y'"

definition subset_closed :: "'a set set => bool" where
    "subset_closed U == \A \ U. Pow A \ U"

context Extend
begin

lemma 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\<open>Safety\<close>

(*used below to prove Join_project_ensures*)
lemma project_unless:
     "[| G \ stable C; project h C G \ A unless B |]
      ==> G \<in> (C \<inter> 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 Join_project_constrains:
     "(F\project h C G \ A co B) =
        (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &
         F \<in> 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 \<in> (C \<inter> extend_set h A) co C*)
lemma Join_project_stable:
     "extend h F\G \ stable C
      ==> (F\<squnion>project h C G \<in> stable A)  =
          (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &
           F \<in> 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 project_constrains_I:
     "extend h F\G \ extend_set h A co extend_set h B
      ==> F\<squnion>project h C G \<in> A co B"
apply (simp add: project_constrains extend_constrains)
apply (blast intro: constrains_weaken dest: constrains_imp_subset)
done

lemma project_increasing_I:
     "extend h F\G \ increasing (func o f)
      ==> F\<squnion>project h C G \<in> increasing func"
apply (unfold increasing_def stable_def)
apply (simp del: Join_constrains
            add: project_constrains_I extend_set_eq_Collect)
done

lemma Join_project_increasing:
     "(F\project h UNIV G \ increasing func) =
      (extend h F\<squnion>G \<in> 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 project_constrains_D:
     "F\project h UNIV G \ A co B
      ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
by (simp add: project_constrains extend_constrains)

end

subsection\<open>"projecting" and union/intersection (no converses)\<close>

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 \<in> I. X' i) (\<Inter>i \<in> 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 \<in> I. X' i) (\<Union>i \<in> 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 \<in> I. Y' i) (\<Inter>i \<in> 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 \<in> I. Y' i) (\<Union>i \<in> 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)

context Extend
begin

lemma 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 projecting_stable:
     "projecting C h F (stable (extend_set h A)) (stable A)"
apply (unfold stable_def)
apply (rule projecting_constrains)
done

lemma projecting_increasing:
     "projecting C h F (increasing (func o f)) (increasing func)"
apply (unfold projecting_def)
apply (blast intro: project_increasing_I)
done

lemma extending_UNIV: "extending C h F UNIV Y"
apply (simp (no_asm) add: extending_def)
done

lemma 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 extending_stable:
     "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)"
apply (unfold stable_def)
apply (rule extending_constrains)
done

lemma extending_increasing:
     "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)"
by (force simp only: extending_def Join_project_increasing)

subsection\<open>Reachability and project\<close>

(*In practice, C = reachable(...): the inclusion is equality*)
lemma reachable_imp_reachable_project:
     "[| reachable (extend h F\G) \ C;
         z \<in> reachable (extend h F\<squnion>G) |]
      ==> f z \<in> 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 project_Constrains_D:
     "F\project h (reachable (extend h F\G)) G \ A Co B
      ==> extend h F\<squnion>G \<in> (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 project_Stable_D:
     "F\project h (reachable (extend h F\G)) G \ Stable A
      ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
apply (unfold Stable_def)
apply (simp (no_asm_simp) add: project_Constrains_D)
done

lemma project_Always_D:
     "F\project h (reachable (extend h F\G)) G \ Always A
      ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
apply (unfold Always_def)
apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
done

lemma project_Increasing_D:
     "F\project h (reachable (extend h F\G)) G \ Increasing func
      ==> extend h F\<squnion>G \<in> 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\<open>Converse results for weak safety: benefits of the argument C\<close>

(*In practice, C = reachable(...): the inclusion is equality*)
lemma reachable_project_imp_reachable:
     "[| C \ reachable(extend h F\G);
         x \<in> reachable (F\<squnion>project h C G) |]
      ==> \<exists>y. h(x,y) \<in> 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 project_set_reachable_extend_eq:
     "project_set h (reachable (extend h F\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 reachable_extend_Join_subset:
     "reachable (extend h F\G) \ C
      ==> reachable (extend h F\<squnion>G) \<subseteq>
          extend_set h (reachable (F\<squnion>project h C G))"
apply (auto dest: reachable_imp_reachable_project)
done

lemma project_Constrains_I:
     "extend h F\G \ (extend_set h A) Co (extend_set h B)
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> 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 project_Stable_I:
     "extend h F\G \ Stable (extend_set h A)
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
apply (unfold Stable_def)
apply (simp (no_asm_simp) add: project_Constrains_I)
done

lemma project_Always_I:
     "extend h F\G \ Always (extend_set h A)
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
apply (unfold Always_def)
apply (auto simp add: project_Stable_I)
apply (unfold extend_set_def, blast)
done

lemma project_Increasing_I:
    "extend h F\G \ Increasing (func o f)
     ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
apply (unfold Increasing_def, auto)
apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
done

lemma project_Constrains:
     "(F\project h (reachable (extend h F\G)) G \ A Co B) =
      (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
apply (blast intro: project_Constrains_I project_Constrains_D)
done

lemma project_Stable:
     "(F\project h (reachable (extend h F\G)) G \ Stable A) =
      (extend h F\<squnion>G \<in> Stable (extend_set h A))"
apply (unfold Stable_def)
apply (rule project_Constrains)
done

lemma project_Increasing:
   "(F\project h (reachable (extend h F\G)) G \ Increasing func) =
    (extend h F\<squnion>G \<in> Increasing (func o f))"
apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
done

subsection\<open>A lot of redundant theorems: all are proved to facilitate reasoning
    about guarantees.\<close>

lemma projecting_Constrains:
     "projecting (%G. reachable (extend h F\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 projecting_Stable:
     "projecting (%G. reachable (extend h F\G)) h F
                 (Stable (extend_set h A)) (Stable A)"
apply (unfold Stable_def)
apply (rule projecting_Constrains)
done

lemma projecting_Always:
     "projecting (%G. reachable (extend h F\G)) h F
                 (Always (extend_set h A)) (Always A)"
apply (unfold projecting_def)
apply (blast intro: project_Always_I)
done

lemma projecting_Increasing:
     "projecting (%G. reachable (extend h F\G)) h F
                 (Increasing (func o f)) (Increasing func)"
apply (unfold projecting_def)
apply (blast intro: project_Increasing_I)
done

lemma extending_Constrains:
     "extending (%G. reachable (extend h F\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 extending_Stable:
     "extending (%G. reachable (extend h F\G)) h F
                  (Stable (extend_set h A)) (Stable A)"
apply (unfold extending_def)
apply (blast intro: project_Stable_D)
done

lemma extending_Always:
     "extending (%G. reachable (extend h F\G)) h F
                  (Always (extend_set h A)) (Always A)"
apply (unfold extending_def)
apply (blast intro: project_Always_D)
done

lemma extending_Increasing:
     "extending (%G. reachable (extend h F\G)) h F
                  (Increasing (func o f)) (Increasing func)"
apply (unfold extending_def)
apply (blast intro: project_Increasing_D)
done

subsection\<open>leadsETo in the precondition (??)\<close>

subsubsection\<open>transient\<close>

lemma transient_extend_set_imp_project_transient:
     "[| G \ transient (C \ extend_set h A); G \ stable C |]
      ==> project h C G \<in> transient (project_set h C \<inter> 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" for AA BB in thin_rl)
apply (drule bspec, assumption)
apply (simp add: extend_set_def project_act_def, blast)
done

(*converse might hold too?*)
lemma project_extend_transient_D:
     "project h C (extend h F) \ transient (project_set h C \ D)
      ==> F \<in> transient (project_set h C \<inter> D)"
apply (simp add: transient_def Domain_project_act, safe)
apply blast+
done

subsubsection\<open>ensures -- a primitive combining progress with safety\<close>

(*Used to prove project_leadsETo_I*)
lemma ensures_extend_set_imp_project_ensures:
     "[| extend h F \ stable C; G \ stable C;
         extend h F\<squnion>G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]
      ==> F\<squnion>project h C G
            \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
apply (simp add: ensures_def project_constrains 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\<open>Transferring a transient property upwards\<close>
lemma project_transient_extend_set:
     "project h C G \ transient (project_set h C \ A - B)
      ==> G \<in> transient (C \<inter> 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 project_unless2:
     "[| G \ stable C; project h C G \ (project_set h C \ A) unless B |]
      ==> G \<in> (C \<inter> 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 extend_unless:
   "[|extend h F \ stable C; F \ A unless B|]
    ==> extend h F \<in> C \<inter> 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 Join_project_ensures:
     "[| extend h F\G \ stable C;
         F\<squnion>project h C G \<in> A ensures B |]
      ==> extend h F\<squnion>G \<in> (C \<inter> 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\<open>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 PLD_lemma:
     "[| extend h F\G \ stable C;
         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
      ==> extend h F\<squnion>G \<in>
          C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
apply (erule leadsTo_induct)
  apply (blast intro: 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 project_leadsTo_D_lemma:
     "[| extend h F\G \ stable C;
         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
      ==> extend h F\<squnion>G \<in> (C \<inter> 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 Join_project_LeadsTo:
     "[| C = (reachable (extend h F\G));
         F\<squnion>project h C G \<in> A LeadsTo B |]
      ==> extend h F\<squnion>G \<in> (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\<open>Towards the theorem \<open>project_Ensures_D\<close>\<close>

lemma project_ensures_D_lemma:
     "[| G \ stable ((C \ extend_set h A) - (extend_set h B));
         F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;
         extend h F\<squnion>G \<in> stable C |]
      ==> extend h F\<squnion>G \<in> (C \<inter> 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 project_ensures_D:
     "[| F\project h UNIV G \ A ensures B;
         G \<in> stable (extend_set h A - extend_set h B) |]
      ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
apply (rule project_ensures_D_lemma [of _ UNIV, elim_format], auto)
done

lemma project_Ensures_D:
     "[| F\project h (reachable (extend h F\G)) G \ A Ensures B;
         G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -
                     extend_set h B) |]
      ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
apply (unfold Ensures_def)
apply (rule project_ensures_D_lemma [elim_format])
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
done

subsection\<open>Guarantees\<close>

lemma 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 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 \<in> X' *)
lemma project_guarantees_raw:
assumes xguary:  "F \ X guarantees Y"
     and closed:  "subset_closed (AllowedActs F)"
     and project: "!!G. extend h F\G \ X'
                        ==> F\<squnion>project h (C G) G \<in> X"
     and extend:  "!!G. [| F\project h (C G) G \ Y |]
                        ==> extend h F\<squnion>G \<in> 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 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 \<in> 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\<open>guarantees corollaries\<close>

subsubsection\<open>Some could be deleted: the required versions are easy to prove\<close>

lemma extend_guar_increasing:
     "[| F \ UNIV guarantees increasing func;
         subset_closed (AllowedActs F) |]
      ==> extend h F \<in> 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 extend_guar_Increasing:
     "[| F \ UNIV guarantees Increasing func;
         subset_closed (AllowedActs F) |]
      ==> extend h F \<in> 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 extend_guar_Always:
     "[| F \ Always A guarantees Always B;
         subset_closed (AllowedActs F) |]
      ==> extend h F
            \<in> 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\<open>Guarantees with a leadsTo postcondition\<close>

lemma project_leadsTo_D:
     "F\project h UNIV G \ A leadsTo B
      ==> extend h F\<squnion>G \<in> (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 project_LeadsTo_D:
     "F\project h (reachable (extend h F\G)) G \ A LeadsTo B
       ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
apply (rule refl [THEN Join_project_LeadsTo], auto)
done

lemma 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 extending_LeadsTo:
     "extending (%G. reachable (extend h F\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

end

end

¤ Dauer der Verarbeitung: 0.36 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.