Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Transformers.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/UNITY/Transformers.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   2003  University of Cambridge

Predicate Transformers.  From

    David Meier and Beverly Sanders,
    Composing Leads-to Properties
    Theoretical Computer Science 243:1-2 (2000), 339-361.

    David Meier,
    Progress Properties in Program Refinement and Parallel Composition
    Swiss Federal Institute of Technology Zurich (1997)
*)

section\<open>Predicate Transformers\<close>

theory Transformers imports Comp begin

subsection\<open>Defining the Predicate Transformers \<^term>\<open>wp\<close>,
   \<^term>\<open>awp\<close> and  \<^term>\<open>wens\<close>\<close>

definition wp :: "[('a*'a) set, 'a set] => 'a set" where
    \<comment> \<open>Dijkstra's weakest-precondition operator (for an individual command)\<close>
    "wp act B == - (act\ `` (-B))"

definition awp :: "['a program, 'a set] => 'a set" where
    \<comment> \<open>Dijkstra's weakest-precondition operator (for a program)\<close>
    "awp F B == (\act \ Acts F. wp act B)"

definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where
    \<comment> \<open>The weakest-ensures transformer\<close>
    "wens F act B == gfp(\X. (wp act B \ awp F (B \ X)) \ B)"

text\<open>The fundamental theorem for wp\<close>
theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
by (force simp add: wp_def)

text\<open>This lemma is a good deal more intuitive than the definition!\<close>
lemma in_wp_iff: "(a \ wp act B) = (\x. (a,x) \ act --> x \ B)"
by (simp add: wp_def, blast)

lemma Compl_Domain_subset_wp: "- (Domain act) \ wp act B"
by (force simp add: wp_def)

lemma wp_empty [simp]: "wp act {} = - (Domain act)"
by (force simp add: wp_def)

text\<open>The identity relation is the skip action\<close>
lemma wp_Id [simp]: "wp Id B = B"
by (simp add: wp_def)

lemma wp_totalize_act:
     "wp (totalize_act act) B = (wp act B \ Domain act) \ (B - Domain act)"
by (simp add: wp_def totalize_act_def, blast)

lemma awp_subset: "(awp F A \ A)"
by (force simp add: awp_def wp_def)

lemma awp_Int_eq: "awp F (A\B) = awp F A \ awp F B"
by (simp add: awp_def wp_def, blast)

text\<open>The fundamental theorem for awp\<close>
theorem awp_iff_constrains: "(A <= awp F B) = (F \ A co B)"
by (simp add: awp_def constrains_def wp_iff INT_subset_iff)

lemma awp_iff_stable: "(A \ awp F A) = (F \ stable A)"
by (simp add: awp_iff_constrains stable_def)

lemma stable_imp_awp_ident: "F \ stable A ==> awp F A = A"
apply (rule equalityI [OF awp_subset])
apply (simp add: awp_iff_stable)
done

lemma wp_mono: "(A \ B) ==> wp act A \ wp act B"
by (simp add: wp_def, blast)

lemma awp_mono: "(A \ B) ==> awp F A \ awp F B"
by (simp add: awp_def wp_def, blast)

lemma wens_unfold:
     "wens F act B = (wp act B \ awp F (B \ wens F act B)) \ B"
apply (simp add: wens_def)
apply (rule gfp_unfold)
apply (simp add: mono_def wp_def awp_def, blast)
done

lemma wens_Id [simp]: "wens F Id B = B"
by (simp add: wens_def gfp_def wp_def awp_def, blast)

text\<open>These two theorems justify the claim that \<^term>\<open>wens\<close> returns the
weakest assertion satisfying the ensures property\<close>
lemma ensures_imp_wens: "F \ A ensures B ==> \act \ Acts F. A \ wens F act B"
apply (simp add: wens_def ensures_def transient_def, clarify)
apply (rule rev_bexI, assumption)
apply (rule gfp_upperbound)
apply (simp add: constrains_def awp_def wp_def, blast)
done

lemma wens_ensures: "act \ Acts F ==> F \ (wens F act B) ensures B"
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
              ensures_def transient_def, blast)

text\<open>These two results constitute assertion (4.13) of the thesis\<close>
lemma wens_mono: "(A \ B) ==> wens F act A \ wens F act B"
apply (simp add: wens_def wp_def awp_def)
apply (rule gfp_mono, blast)
done

lemma wens_weakening: "B \ wens F act B"
by (simp add: wens_def gfp_def, blast)

text\<open>Assertion (6), or 4.16 in the thesis\<close>
lemma subset_wens: "A-B \ wp act B \ awp F (B \ A) ==> A \ wens F act B"
apply (simp add: wens_def wp_def awp_def)
apply (rule gfp_upperbound, blast)
done

text\<open>Assertion 4.17 in the thesis\<close>
lemma Diff_wens_constrains: "F \ (wens F act A - A) co wens F act A"
by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
  \<comment> \<open>Proved instantly, yet remarkably fragile. If \<open>Un_subset_iff\<close>
      is declared as an iff-rule, then it's almost impossible to prove.
      One proof is via \<open>meson\<close> after expanding all definitions, but it's
      slow!\<close>

text\<open>Assertion (7): 4.18 in the thesis.  NOTE that many of these results
hold for an arbitrary action.  We often do not require \<^term>\<open>act \<in> Acts F\<close>\<close>
lemma stable_wens: "F \ stable A ==> F \ stable (wens F act A)"
apply (simp add: stable_def)
apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]])
apply (simp add: Un_Int_distrib2 Compl_partition2)
apply (erule constrains_weaken, blast)
apply (simp add: wens_weakening)
done

text\<open>Assertion 4.20 in the thesis.\<close>
lemma wens_Int_eq_lemma:
      "[|T-B \ awp F T; act \ Acts F|]
       ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
apply (rule subset_wens)
apply (rule_tac P="\x. f x \ b" for f b in ssubst [OF wens_unfold])
apply (simp add: wp_def awp_def, blast)
done

text\<open>Assertion (8): 4.21 in the thesis. Here we indeed require
      \<^term>\<open>act \<in> Acts F\<close>\<close>
lemma wens_Int_eq:
      "[|T-B \ awp F T; act \ Acts F|]
       ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
apply (rule equalityI)
apply (simp_all add: Int_lower1)
apply (rule wens_Int_eq_lemma, assumption+)
apply (rule subset_trans [OF _ wens_mono [of "T\B" B]], auto)
done

subsection\<open>Defining the Weakest Ensures Set\<close>

inductive_set
  wens_set :: "['a program, 'a set] => 'a set set"
  for F :: "'a program" and B :: "'a set"
where

  Basis: "B \ wens_set F B"

| Wens:  "[|X \ wens_set F B; act \ Acts F|] ==> wens F act X \ wens_set F B"

| Union: "W \ {} ==> \U \ W. U \ wens_set F B ==> \W \ wens_set F B"

lemma wens_set_imp_co: "A \ wens_set F B ==> F \ (A-B) co A"
apply (erule wens_set.induct)
  apply (simp add: constrains_def)
apply (drule_tac act1=act and A1=X
        in constrains_Un [OF Diff_wens_constrains])
apply (erule constrains_weaken, blast)
apply (simp add: wens_weakening)
apply (rule constrains_weaken)
apply (rule_tac I=W and A="\v. v-B" and A'="\v. v" in constrains_UN, blast+)
done

lemma wens_set_imp_leadsTo: "A \ wens_set F B ==> F \ A leadsTo B"
apply (erule wens_set.induct)
  apply (rule leadsTo_refl)
apply (blast intro: wens_ensures leadsTo_Trans)
apply (blast intro: leadsTo_Union)
done

lemma leadsTo_imp_wens_set: "F \ A leadsTo B ==> \C \ wens_set F B. A \ C"
apply (erule leadsTo_induct_pre)
  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
apply (clarify, drule ensures_weaken_R, assumption)
apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
apply (case_tac "S={}")
apply (simp, blast intro: wens_set.Basis)
apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def)
apply (rule_tac x = "\{Z. \U\S. Z = f U}" in exI)
apply (blast intro: wens_set.Union)
done

text\<open>Assertion (9): 4.27 in the thesis.\<close>
lemma leadsTo_iff_wens_set: "(F \ A leadsTo B) = (\C \ wens_set F B. A \ C)"
by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo)

text\<open>This is the result that requires the definition of \<^term>\<open>wens_set\<close> to
  require \<^term>\<open>W\<close> to be non-empty in the Unio case, for otherwise we should
  always have \<^term>\<open>{} \<in> wens_set F B\<close>.\<close>
lemma wens_set_imp_subset: "A \ wens_set F B ==> B \ A"
apply (erule wens_set.induct)
  apply (blast intro: wens_weakening [THEN subsetD])+
done

subsection\<open>Properties Involving Program Union\<close>

text\<open>Assertion (4.30) of thesis, reoriented\<close>
lemma awp_Join_eq: "awp (F\G) B = awp F B \ awp G B"
by (simp add: awp_def wp_def, blast)

lemma wens_subset: "wens F act B - B \ wp act B \ awp F (B \ wens F act B)"
by (subst wens_unfold, fast)

text\<open>Assertion (4.31)\<close>
lemma subset_wens_Join:
      "[|A = T \ wens F act B; T-B \ awp F T; A-B \ awp G (A \ B)|]
       ==> A \<subseteq> wens (F\<squnion>G) act B"
apply (subgoal_tac "(T \ wens F act B) - B \
                    wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T")
apply (rule subset_wens)
apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
apply (simp add: awp_def wp_def, blast)
apply (insert wens_subset [of F act B], blast)
done

text\<open>Assertion (4.32)\<close>
lemma wens_Join_subset: "wens (F\G) act B \ wens F act B"
apply (simp add: wens_def)
apply (rule gfp_mono)
apply (auto simp add: awp_Join_eq)
done

text\<open>Lemma, because the inductive step is just too messy.\<close>
lemma wens_Union_inductive_step:
  assumes awpF: "T-B \ awp F T"
      and awpG: "!!X. X \ wens_set F B ==> (T\X) - B \ awp G (T\X)"
  shows "[|X \ wens_set F B; act \ Acts F; Y \ X; T\X = T\Y|]
         ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and>
             T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y"
apply (subgoal_tac "wens (F\G) act Y \ wens F act X")
prefer 2
apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
apply (rule equalityI)
prefer 2 apply blast
apply (simp add: Int_lower1)
apply (frule wens_set_imp_subset)
apply (subgoal_tac "T-X \ awp F T")
prefer 2 apply (blast intro: awpF [THEN subsetD])
apply (rule_tac B = "wens (F\G) act (T\X)" in subset_trans)
prefer 2 apply (blast intro!: wens_mono)
apply (subst wens_Int_eq, assumption+)
apply (rule subset_wens_Join [of _ T], simp, blast)
apply (subgoal_tac "T \ wens F act (T\X) \ T\X = T \ wens F act X")
prefer 2
apply (subst wens_Int_eq [symmetric], assumption+)
apply (blast intro: wens_weakening [THEN subsetD], simp)
apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
done

theorem wens_Union:
  assumes awpF: "T-B \ awp F T"
      and awpG: "!!X. X \ wens_set F B ==> (T\X) - B \ awp G (T\X)"
      and major: "X \ wens_set F B"
  shows "\Y \ wens_set (F\G) B. Y \ X & T\X = T\Y"
apply (rule wens_set.induct [OF major])
  txt\<open>Basis: trivial\<close>
  apply (blast intro: wens_set.Basis)
txt\<open>Inductive step\<close>
apply clarify
apply (rule_tac x = "wens (F\G) act Y" in rev_bexI)
  apply (force intro: wens_set.Wens)
apply (simp add: wens_Union_inductive_step [OF awpF awpG])
txt\<open>Union: by Axiom of Choice\<close>
apply (simp add: ball_conj_distrib Bex_def)
apply (clarify dest!: bchoice)
apply (rule_tac x = "\{Z. \U\W. Z = f U}" in exI)
apply (blast intro: wens_set.Union)
done

theorem leadsTo_Join:
  assumes leadsTo: "F \ A leadsTo B"
      and awpF: "T-B \ awp F T"
      and awpG: "!!X. X \ wens_set F B ==> (T\X) - B \ awp G (T\X)"
  shows "F\G \ T\A leadsTo B"
apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE])
apply (rule wens_Union [THEN bexE])
   apply (rule awpF)
  apply (erule awpG, assumption)
apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L])
done

subsection \<open>The Set \<^term>\<open>wens_set F B\<close> for a Single-Assignment Program\<close>
text\<open>Thesis Section 4.3.3\<close>

text\<open>We start by proving laws about single-assignment programs\<close>
lemma awp_single_eq [simp]:
     "awp (mk_program (init, {act}, allowed)) B = B \ wp act B"
by (force simp add: awp_def wp_def)

lemma wp_Un_subset: "wp act A \ wp act B \ wp act (A \ B)"
by (force simp add: wp_def)

lemma wp_Un_eq: "single_valued act ==> wp act (A \ B) = wp act A \ wp act B"
apply (rule equalityI)
apply (force simp add: wp_def single_valued_def)
apply (rule wp_Un_subset)
done

lemma wp_UN_subset: "(\i\I. wp act (A i)) \ wp act (\i\I. A i)"
by (force simp add: wp_def)

lemma wp_UN_eq:
     "[|single_valued act; I\{}|]
      ==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))"
apply (rule equalityI)
prefer 2 apply (rule wp_UN_subset)
apply (simp add: wp_def Image_INT_eq)
done

lemma wens_single_eq:
     "wens (mk_program (init, {act}, allowed)) act B = B \ wp act B"
by (simp add: wens_def gfp_def wp_def, blast)

text\<open>Next, we express the \<^term>\<open>wens_set\<close> for single-assignment programs\<close>

definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where
    "wens_single_finite act B k == \i \ atMost k. (wp act ^^ i) B"

definition wens_single :: "[('a*'a) set, 'a set] => 'a set" where
    "wens_single act B == \i. (wp act ^^ i) B"

lemma wens_single_Un_eq:
      "single_valued act
       ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
apply (rule equalityI)
apply (simp_all add: Un_upper1)
apply (simp add: wens_single_def wp_UN_eq, clarify)
apply (rule_tac a="Suc xa" in UN_I, auto)
done

lemma atMost_nat_nonempty: "atMost (k::nat) \ {}"
by force

lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B"
by (simp add: wens_single_finite_def)

lemma wens_single_finite_Suc:
      "single_valued act
       ==> wens_single_finite act B (Suc k) =
           wens_single_finite act B k \<union> wp act (wens_single_finite act B k)"
apply (simp add: wens_single_finite_def wp_UN_eq [OF _ atMost_nat_nonempty])
apply (force elim!: le_SucE)
done

lemma wens_single_finite_Suc_eq_wens:
     "single_valued act
       ==> wens_single_finite act B (Suc k) =
           wens (mk_program (init, {act}, allowed)) act
                (wens_single_finite act B k)"
by (simp add: wens_single_finite_Suc wens_single_eq)

lemma def_wens_single_finite_Suc_eq_wens:
     "[|F = mk_program (init, {act}, allowed); single_valued act|]
       ==> wens_single_finite act B (Suc k) =
           wens F act (wens_single_finite act B k)"
by (simp add: wens_single_finite_Suc_eq_wens)

lemma wens_single_finite_Un_eq:
      "single_valued act
       ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k)
           \<in> range (wens_single_finite act B)"
by (simp add: wens_single_finite_Suc [symmetric])

lemma wens_single_eq_Union:
      "wens_single act B = \(range (wens_single_finite act B))"
by (simp add: wens_single_finite_def wens_single_def, blast)

lemma wens_single_finite_eq_Union:
     "wens_single_finite act B n = (\k\atMost n. wens_single_finite act B k)"
apply (auto simp add: wens_single_finite_def)
apply (blast intro: le_trans)
done

lemma wens_single_finite_mono:
     "m \ n ==> wens_single_finite act B m \ wens_single_finite act B n"
by (force simp add:  wens_single_finite_eq_Union [of act B n])

lemma wens_single_finite_subset_wens_single:
      "wens_single_finite act B k \ wens_single act B"
by (simp add: wens_single_eq_Union, blast)

lemma subset_wens_single_finite:
      "[|W \ wens_single_finite act B ` (atMost k); single_valued act; W\{}|]
       ==> \<exists>m. \<Union>W = wens_single_finite act B m"
apply (induct k)
apply (rule_tac x=0 in exI, simp, blast)
apply (auto simp add: atMost_Suc)
apply (case_tac "wens_single_finite act B (Suc k) \ W")
prefer 2 apply blast
apply (drule_tac x="Suc k" in spec)
apply (erule notE, rule equalityI)
prefer 2 apply blast
apply (subst wens_single_finite_eq_Union)
apply (simp add: atMost_Suc, blast)
done

text\<open>lemma for Union case\<close>
lemma Union_eq_wens_single:
      "\\k. \ W \ wens_single_finite act B ` {..k};
        W \<subseteq> insert (wens_single act B)
            (range (wens_single_finite act B))\<rbrakk>
       \<Longrightarrow> \<Union>W = wens_single act B"
apply (cases "wens_single act B \ W")
apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD])
apply (simp add: wens_single_eq_Union)
apply (rule equalityI, blast)
apply (simp add: UN_subset_iff, clarify)
apply (subgoal_tac "\y\W. \n. y = wens_single_finite act B n & i\n")
apply (blast intro: wens_single_finite_mono [THEN subsetD])
apply (drule_tac x=i in spec)
apply (force simp add: atMost_def)
done

lemma wens_set_subset_single:
      "single_valued act
       ==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq>
           insert (wens_single act B) (range (wens_single_finite act B))"
apply (rule subsetI)
apply (erule wens_set.induct)
  txt\<open>Basis\<close>
  apply (fastforce simp add: wens_single_finite_def)
txt\<open>Wens inductive step\<close>
apply (case_tac "acta = Id", simp)
apply (simp add: wens_single_eq)
apply (elim disjE)
apply (simp add: wens_single_Un_eq)
apply (force simp add: wens_single_finite_Un_eq)
txt\<open>Union inductive step\<close>
apply (case_tac "\k. W \ wens_single_finite act B ` (atMost k)")
apply (blast dest!: subset_wens_single_finite, simp)
apply (rule disjI1 [OF Union_eq_wens_single], blast+)
done

lemma wens_single_finite_in_wens_set:
      "single_valued act \
         wens_single_finite act B k
         \<in> wens_set (mk_program (init, {act}, allowed)) B"
apply (induct_tac k)
apply (simp add: wens_single_finite_def wens_set.Basis)
apply (simp add: wens_set.Wens
                 wens_single_finite_Suc_eq_wens [of act B _ init allowed])
done

lemma single_subset_wens_set:
      "single_valued act
       ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq>
           wens_set (mk_program (init, {act}, allowed)) B"
apply (simp add: image_def wens_single_eq_Union)
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
done

text\<open>Theorem (4.29)\<close>
theorem wens_set_single_eq:
     "[|F = mk_program (init, {act}, allowed); single_valued act|]
      ==> wens_set F B =
          insert (wens_single act B) (range (wens_single_finite act B))"
apply (rule equalityI)
apply (simp add: wens_set_subset_single)
apply (erule ssubst, erule single_subset_wens_set)
done

text\<open>Generalizing Misra's Fixed Point Union Theorem (4.41)\<close>

lemma fp_leadsTo_Join:
    "[|T-B \ awp F T; T-B \ FP G; F \ A leadsTo B|] ==> F\G \ T\A leadsTo B"
apply (rule leadsTo_Join, assumption, blast)
apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast)
done

end

¤ Dauer der Verarbeitung: 0.26 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.