src/HOL/UNITY/Transformers.thy
changeset 63146 f1ecba0272f9
parent 62343 24106dc44def
child 67443 3abf6a722518
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Wed May 25 11:49:40 2016 +0200
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Wed May 25 11:50:58 2016 +0200
     1.3 @@ -13,30 +13,30 @@
     1.4      Swiss Federal Institute of Technology Zurich (1997)
     1.5  *)
     1.6  
     1.7 -section{*Predicate Transformers*}
     1.8 +section\<open>Predicate Transformers\<close>
     1.9  
    1.10  theory Transformers imports Comp begin
    1.11  
    1.12 -subsection{*Defining the Predicate Transformers @{term wp},
    1.13 -   @{term awp} and  @{term wens}*}
    1.14 +subsection\<open>Defining the Predicate Transformers @{term wp},
    1.15 +   @{term awp} and  @{term wens}\<close>
    1.16  
    1.17  definition wp :: "[('a*'a) set, 'a set] => 'a set" where  
    1.18 -    --{*Dijkstra's weakest-precondition operator (for an individual command)*}
    1.19 +    \<comment>\<open>Dijkstra's weakest-precondition operator (for an individual command)\<close>
    1.20      "wp act B == - (act^-1 `` (-B))"
    1.21  
    1.22  definition awp :: "['a program, 'a set] => 'a set" where
    1.23 -    --{*Dijkstra's weakest-precondition operator (for a program)*}
    1.24 +    \<comment>\<open>Dijkstra's weakest-precondition operator (for a program)\<close>
    1.25      "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
    1.26  
    1.27  definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where
    1.28 -    --{*The weakest-ensures transformer*}
    1.29 +    \<comment>\<open>The weakest-ensures transformer\<close>
    1.30      "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
    1.31  
    1.32 -text{*The fundamental theorem for wp*}
    1.33 +text\<open>The fundamental theorem for wp\<close>
    1.34  theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
    1.35  by (force simp add: wp_def) 
    1.36  
    1.37 -text{*This lemma is a good deal more intuitive than the definition!*}
    1.38 +text\<open>This lemma is a good deal more intuitive than the definition!\<close>
    1.39  lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
    1.40  by (simp add: wp_def, blast)
    1.41  
    1.42 @@ -46,7 +46,7 @@
    1.43  lemma wp_empty [simp]: "wp act {} = - (Domain act)"
    1.44  by (force simp add: wp_def)
    1.45  
    1.46 -text{*The identity relation is the skip action*}
    1.47 +text\<open>The identity relation is the skip action\<close>
    1.48  lemma wp_Id [simp]: "wp Id B = B"
    1.49  by (simp add: wp_def) 
    1.50  
    1.51 @@ -60,7 +60,7 @@
    1.52  lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
    1.53  by (simp add: awp_def wp_def, blast) 
    1.54  
    1.55 -text{*The fundamental theorem for awp*}
    1.56 +text\<open>The fundamental theorem for awp\<close>
    1.57  theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)"
    1.58  by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
    1.59  
    1.60 @@ -88,8 +88,8 @@
    1.61  lemma wens_Id [simp]: "wens F Id B = B"
    1.62  by (simp add: wens_def gfp_def wp_def awp_def, blast)
    1.63  
    1.64 -text{*These two theorems justify the claim that @{term wens} returns the
    1.65 -weakest assertion satisfying the ensures property*}
    1.66 +text\<open>These two theorems justify the claim that @{term wens} returns the
    1.67 +weakest assertion satisfying the ensures property\<close>
    1.68  lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
    1.69  apply (simp add: wens_def ensures_def transient_def, clarify) 
    1.70  apply (rule rev_bexI, assumption) 
    1.71 @@ -101,7 +101,7 @@
    1.72  by (simp add: wens_def gfp_def constrains_def awp_def wp_def
    1.73                ensures_def transient_def, blast)
    1.74  
    1.75 -text{*These two results constitute assertion (4.13) of the thesis*}
    1.76 +text\<open>These two results constitute assertion (4.13) of the thesis\<close>
    1.77  lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
    1.78  apply (simp add: wens_def wp_def awp_def) 
    1.79  apply (rule gfp_mono, blast) 
    1.80 @@ -110,22 +110,22 @@
    1.81  lemma wens_weakening: "B \<subseteq> wens F act B"
    1.82  by (simp add: wens_def gfp_def, blast)
    1.83  
    1.84 -text{*Assertion (6), or 4.16 in the thesis*}
    1.85 +text\<open>Assertion (6), or 4.16 in the thesis\<close>
    1.86  lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
    1.87  apply (simp add: wens_def wp_def awp_def) 
    1.88  apply (rule gfp_upperbound, blast) 
    1.89  done
    1.90  
    1.91 -text{*Assertion 4.17 in the thesis*}
    1.92 +text\<open>Assertion 4.17 in the thesis\<close>
    1.93  lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
    1.94  by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
    1.95 -  --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
    1.96 +  \<comment>\<open>Proved instantly, yet remarkably fragile. If \<open>Un_subset_iff\<close>
    1.97        is declared as an iff-rule, then it's almost impossible to prove. 
    1.98 -      One proof is via @{text meson} after expanding all definitions, but it's
    1.99 -      slow!*}
   1.100 +      One proof is via \<open>meson\<close> after expanding all definitions, but it's
   1.101 +      slow!\<close>
   1.102  
   1.103 -text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
   1.104 -hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
   1.105 +text\<open>Assertion (7): 4.18 in the thesis.  NOTE that many of these results
   1.106 +hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}\<close>
   1.107  lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
   1.108  apply (simp add: stable_def)
   1.109  apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
   1.110 @@ -134,7 +134,7 @@
   1.111  apply (simp add: wens_weakening)
   1.112  done
   1.113  
   1.114 -text{*Assertion 4.20 in the thesis.*}
   1.115 +text\<open>Assertion 4.20 in the thesis.\<close>
   1.116  lemma wens_Int_eq_lemma:
   1.117        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   1.118         ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
   1.119 @@ -143,8 +143,8 @@
   1.120  apply (simp add: wp_def awp_def, blast)
   1.121  done
   1.122  
   1.123 -text{*Assertion (8): 4.21 in the thesis. Here we indeed require
   1.124 -      @{term "act \<in> Acts F"}*}
   1.125 +text\<open>Assertion (8): 4.21 in the thesis. Here we indeed require
   1.126 +      @{term "act \<in> Acts F"}\<close>
   1.127  lemma wens_Int_eq:
   1.128        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   1.129         ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
   1.130 @@ -155,7 +155,7 @@
   1.131  done
   1.132  
   1.133  
   1.134 -subsection{*Defining the Weakest Ensures Set*}
   1.135 +subsection\<open>Defining the Weakest Ensures Set\<close>
   1.136  
   1.137  inductive_set
   1.138    wens_set :: "['a program, 'a set] => 'a set set"
   1.139 @@ -198,29 +198,29 @@
   1.140  apply (blast intro: wens_set.Union) 
   1.141  done
   1.142  
   1.143 -text{*Assertion (9): 4.27 in the thesis.*}
   1.144 +text\<open>Assertion (9): 4.27 in the thesis.\<close>
   1.145  lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
   1.146  by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
   1.147  
   1.148 -text{*This is the result that requires the definition of @{term wens_set} to
   1.149 +text\<open>This is the result that requires the definition of @{term wens_set} to
   1.150    require @{term W} to be non-empty in the Unio case, for otherwise we should
   1.151 -  always have @{term "{} \<in> wens_set F B"}.*}
   1.152 +  always have @{term "{} \<in> wens_set F B"}.\<close>
   1.153  lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
   1.154  apply (erule wens_set.induct) 
   1.155    apply (blast intro: wens_weakening [THEN subsetD])+
   1.156  done
   1.157  
   1.158  
   1.159 -subsection{*Properties Involving Program Union*}
   1.160 +subsection\<open>Properties Involving Program Union\<close>
   1.161  
   1.162 -text{*Assertion (4.30) of thesis, reoriented*}
   1.163 +text\<open>Assertion (4.30) of thesis, reoriented\<close>
   1.164  lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
   1.165  by (simp add: awp_def wp_def, blast)
   1.166  
   1.167  lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
   1.168  by (subst wens_unfold, fast) 
   1.169  
   1.170 -text{*Assertion (4.31)*}
   1.171 +text\<open>Assertion (4.31)\<close>
   1.172  lemma subset_wens_Join:
   1.173        "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 
   1.174         ==> A \<subseteq> wens (F\<squnion>G) act B"
   1.175 @@ -232,14 +232,14 @@
   1.176  apply (insert wens_subset [of F act B], blast) 
   1.177  done
   1.178  
   1.179 -text{*Assertion (4.32)*}
   1.180 +text\<open>Assertion (4.32)\<close>
   1.181  lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
   1.182  apply (simp add: wens_def) 
   1.183  apply (rule gfp_mono)
   1.184  apply (auto simp add: awp_Join_eq)  
   1.185  done
   1.186  
   1.187 -text{*Lemma, because the inductive step is just too messy.*}
   1.188 +text\<open>Lemma, because the inductive step is just too messy.\<close>
   1.189  lemma wens_Union_inductive_step:
   1.190    assumes awpF: "T-B \<subseteq> awp F T"
   1.191        and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   1.192 @@ -272,14 +272,14 @@
   1.193        and major: "X \<in> wens_set F B"
   1.194    shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
   1.195  apply (rule wens_set.induct [OF major])
   1.196 -  txt{*Basis: trivial*}
   1.197 +  txt\<open>Basis: trivial\<close>
   1.198    apply (blast intro: wens_set.Basis)
   1.199 - txt{*Inductive step*}
   1.200 + txt\<open>Inductive step\<close>
   1.201   apply clarify 
   1.202   apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
   1.203    apply (force intro: wens_set.Wens)
   1.204   apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
   1.205 -txt{*Union: by Axiom of Choice*}
   1.206 +txt\<open>Union: by Axiom of Choice\<close>
   1.207  apply (simp add: ball_conj_distrib Bex_def) 
   1.208  apply (clarify dest!: bchoice) 
   1.209  apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
   1.210 @@ -299,10 +299,10 @@
   1.211  done
   1.212  
   1.213  
   1.214 -subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
   1.215 -text{*Thesis Section 4.3.3*}
   1.216 +subsection \<open>The Set @{term "wens_set F B"} for a Single-Assignment Program\<close>
   1.217 +text\<open>Thesis Section 4.3.3\<close>
   1.218  
   1.219 -text{*We start by proving laws about single-assignment programs*}
   1.220 +text\<open>We start by proving laws about single-assignment programs\<close>
   1.221  lemma awp_single_eq [simp]:
   1.222       "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
   1.223  by (force simp add: awp_def wp_def) 
   1.224 @@ -332,7 +332,7 @@
   1.225  by (simp add: wens_def gfp_def wp_def, blast)
   1.226  
   1.227  
   1.228 -text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
   1.229 +text\<open>Next, we express the @{term "wens_set"} for single-assignment programs\<close>
   1.230  
   1.231  definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where  
   1.232      "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B"
   1.233 @@ -416,7 +416,7 @@
   1.234  apply (simp add: atMost_Suc, blast)
   1.235  done
   1.236  
   1.237 -text{*lemma for Union case*}
   1.238 +text\<open>lemma for Union case\<close>
   1.239  lemma Union_eq_wens_single:
   1.240        "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
   1.241          W \<subseteq> insert (wens_single act B)
   1.242 @@ -439,15 +439,15 @@
   1.243             insert (wens_single act B) (range (wens_single_finite act B))"
   1.244  apply (rule subsetI)  
   1.245  apply (erule wens_set.induct)
   1.246 -  txt{*Basis*} 
   1.247 +  txt\<open>Basis\<close> 
   1.248    apply (fastforce simp add: wens_single_finite_def)
   1.249 - txt{*Wens inductive step*}
   1.250 + txt\<open>Wens inductive step\<close>
   1.251   apply (case_tac "acta = Id", simp)
   1.252   apply (simp add: wens_single_eq)
   1.253   apply (elim disjE)
   1.254   apply (simp add: wens_single_Un_eq)
   1.255   apply (force simp add: wens_single_finite_Un_eq)
   1.256 -txt{*Union inductive step*}
   1.257 +txt\<open>Union inductive step\<close>
   1.258  apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
   1.259   apply (blast dest!: subset_wens_single_finite, simp) 
   1.260  apply (rule disjI1 [OF Union_eq_wens_single], blast+)
   1.261 @@ -471,7 +471,7 @@
   1.262  apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
   1.263  done
   1.264  
   1.265 -text{*Theorem (4.29)*}
   1.266 +text\<open>Theorem (4.29)\<close>
   1.267  theorem wens_set_single_eq:
   1.268       "[|F = mk_program (init, {act}, allowed); single_valued act|]
   1.269        ==> wens_set F B =
   1.270 @@ -481,7 +481,7 @@
   1.271  apply (erule ssubst, erule single_subset_wens_set) 
   1.272  done
   1.273  
   1.274 -text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
   1.275 +text\<open>Generalizing Misra's Fixed Point Union Theorem (4.41)\<close>
   1.276  
   1.277  lemma fp_leadsTo_Join:
   1.278      "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"