src/HOL/Hoare_Parallel/OG_Tactics.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62042 6c6ccf573479
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 section \<open>Generation of Verification Conditions\<close>
     2 
     3 theory OG_Tactics
     4 imports OG_Hoare
     5 begin
     6 
     7 lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq
     8 lemmas oghoare_intros=Parallel Basic Seq Cond While Conseq
     9 
    10 lemma ParallelConseqRule:
    11  "\<lbrakk> p \<subseteq> (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i))));
    12   \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i))))
    13       (Parallel Ts)
    14      (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i));
    15   (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i)) \<subseteq> q \<rbrakk>
    16   \<Longrightarrow> \<parallel>- p (Parallel Ts) q"
    17 apply (rule Conseq)
    18 prefer 2
    19  apply fast
    20 apply assumption+
    21 done
    22 
    23 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> \<parallel>- p (Basic id) q"
    24 apply(rule oghoare_intros)
    25   prefer 2 apply(rule Basic)
    26  prefer 2 apply(rule subset_refl)
    27 apply(simp add:Id_def)
    28 done
    29 
    30 lemma BasicRule: "p \<subseteq> {s. (f s)\<in>q} \<Longrightarrow> \<parallel>- p (Basic f) q"
    31 apply(rule oghoare_intros)
    32   prefer 2 apply(rule oghoare_intros)
    33  prefer 2 apply(rule subset_refl)
    34 apply assumption
    35 done
    36 
    37 lemma SeqRule: "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q"
    38 apply(rule Seq)
    39 apply fast+
    40 done
    41 
    42 lemma CondRule:
    43  "\<lbrakk> p \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>w) \<and> (s\<notin>b \<longrightarrow> s\<in>w')}; \<parallel>- w c1 q; \<parallel>- w' c2 q \<rbrakk>
    44   \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q"
    45 apply(rule Cond)
    46  apply(rule Conseq)
    47  prefer 4 apply(rule Conseq)
    48 apply simp_all
    49 apply force+
    50 done
    51 
    52 lemma WhileRule: "\<lbrakk> p \<subseteq> i; \<parallel>- (i \<inter> b) c i ; (i \<inter> (-b)) \<subseteq> q \<rbrakk>
    53         \<Longrightarrow> \<parallel>- p (While b i c) q"
    54 apply(rule Conseq)
    55  prefer 2 apply(rule While)
    56 apply assumption+
    57 done
    58 
    59 text \<open>Three new proof rules for special instances of the \<open>AnnBasic\<close> and the \<open>AnnAwait\<close> commands when the transformation
    60 performed on the state is the identity, and for an \<open>AnnAwait\<close>
    61 command where the boolean condition is \<open>{s. True}\<close>:\<close>
    62 
    63 lemma AnnatomRule:
    64   "\<lbrakk> atom_com(c); \<parallel>- r c q \<rbrakk>  \<Longrightarrow> \<turnstile> (AnnAwait r {s. True} c) q"
    65 apply(rule AnnAwait)
    66 apply simp_all
    67 done
    68 
    69 lemma AnnskipRule:
    70   "r \<subseteq> q \<Longrightarrow> \<turnstile> (AnnBasic r id) q"
    71 apply(rule AnnBasic)
    72 apply simp
    73 done
    74 
    75 lemma AnnwaitRule:
    76   "\<lbrakk> (r \<inter> b) \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b (Basic id)) q"
    77 apply(rule AnnAwait)
    78  apply simp
    79 apply(rule BasicRule)
    80 apply simp
    81 done
    82 
    83 text \<open>Lemmata to avoid using the definition of \<open>map_ann_hoare\<close>, \<open>interfree_aux\<close>, \<open>interfree_swap\<close> and
    84 \<open>interfree\<close> by splitting it into different cases:\<close>
    85 
    86 lemma interfree_aux_rule1: "interfree_aux(co, q, None)"
    87 by(simp add:interfree_aux_def)
    88 
    89 lemma interfree_aux_rule2:
    90   "\<forall>(R,r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<Longrightarrow> interfree_aux(None, q, Some a)"
    91 apply(simp add:interfree_aux_def)
    92 apply(force elim:oghoare_sound)
    93 done
    94 
    95 lemma interfree_aux_rule3:
    96   "(\<forall>(R, r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<and> (\<forall>p\<in>(assertions c). \<parallel>- (p \<inter> R) r p))
    97   \<Longrightarrow> interfree_aux(Some c, q, Some a)"
    98 apply(simp add:interfree_aux_def)
    99 apply(force elim:oghoare_sound)
   100 done
   101 
   102 lemma AnnBasic_assertions:
   103   "\<lbrakk>interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk> \<Longrightarrow>
   104     interfree_aux(Some (AnnBasic r f), q, Some a)"
   105 apply(simp add: interfree_aux_def)
   106 by force
   107 
   108 lemma AnnSeq_assertions:
   109   "\<lbrakk> interfree_aux(Some c1, q, Some a); interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow>
   110    interfree_aux(Some (AnnSeq c1 c2), q, Some a)"
   111 apply(simp add: interfree_aux_def)
   112 by force
   113 
   114 lemma AnnCond1_assertions:
   115   "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c1, q, Some a);
   116   interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow>
   117   interfree_aux(Some(AnnCond1 r b c1 c2), q, Some a)"
   118 apply(simp add: interfree_aux_def)
   119 by force
   120 
   121 lemma AnnCond2_assertions:
   122   "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow>
   123   interfree_aux(Some (AnnCond2 r b c), q, Some a)"
   124 apply(simp add: interfree_aux_def)
   125 by force
   126 
   127 lemma AnnWhile_assertions:
   128   "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, i, Some a);
   129   interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow>
   130   interfree_aux(Some (AnnWhile r b i c), q, Some a)"
   131 apply(simp add: interfree_aux_def)
   132 by force
   133 
   134 lemma AnnAwait_assertions:
   135   "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk>\<Longrightarrow>
   136   interfree_aux(Some (AnnAwait r b c), q, Some a)"
   137 apply(simp add: interfree_aux_def)
   138 by force
   139 
   140 lemma AnnBasic_atomics:
   141   "\<parallel>- (q \<inter> r) (Basic f) q \<Longrightarrow> interfree_aux(None, q, Some (AnnBasic r f))"
   142 by(simp add: interfree_aux_def oghoare_sound)
   143 
   144 lemma AnnSeq_atomics:
   145   "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow>
   146   interfree_aux(Any, q, Some (AnnSeq a1 a2))"
   147 apply(simp add: interfree_aux_def)
   148 by force
   149 
   150 lemma AnnCond1_atomics:
   151   "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow>
   152    interfree_aux(Any, q, Some (AnnCond1 r b a1 a2))"
   153 apply(simp add: interfree_aux_def)
   154 by force
   155 
   156 lemma AnnCond2_atomics:
   157   "interfree_aux (Any, q, Some a)\<Longrightarrow> interfree_aux(Any, q, Some (AnnCond2 r b a))"
   158 by(simp add: interfree_aux_def)
   159 
   160 lemma AnnWhile_atomics: "interfree_aux (Any, q, Some a)
   161      \<Longrightarrow> interfree_aux(Any, q, Some (AnnWhile r b i a))"
   162 by(simp add: interfree_aux_def)
   163 
   164 lemma Annatom_atomics:
   165   "\<parallel>- (q \<inter> r) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r {x. True} a))"
   166 by(simp add: interfree_aux_def oghoare_sound)
   167 
   168 lemma AnnAwait_atomics:
   169   "\<parallel>- (q \<inter> (r \<inter> b)) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r b a))"
   170 by(simp add: interfree_aux_def oghoare_sound)
   171 
   172 definition interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) \<Rightarrow> bool" where
   173   "interfree_swap == \<lambda>(x, xs). \<forall>y\<in>set xs. interfree_aux (com x, post x, com y)
   174   \<and> interfree_aux(com y, post y, com x)"
   175 
   176 lemma interfree_swap_Empty: "interfree_swap (x, [])"
   177 by(simp add:interfree_swap_def)
   178 
   179 lemma interfree_swap_List:
   180   "\<lbrakk> interfree_aux (com x, post x, com y);
   181   interfree_aux (com y, post y ,com x); interfree_swap (x, xs) \<rbrakk>
   182   \<Longrightarrow> interfree_swap (x, y#xs)"
   183 by(simp add:interfree_swap_def)
   184 
   185 lemma interfree_swap_Map: "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> interfree_aux (com x, post x, c k)
   186  \<and> interfree_aux (c k, Q k, com x)
   187  \<Longrightarrow> interfree_swap (x, map (\<lambda>k. (c k, Q k)) [i..<j])"
   188 by(force simp add: interfree_swap_def less_diff_conv)
   189 
   190 lemma interfree_Empty: "interfree []"
   191 by(simp add:interfree_def)
   192 
   193 lemma interfree_List:
   194   "\<lbrakk> interfree_swap(x, xs); interfree xs \<rbrakk> \<Longrightarrow> interfree (x#xs)"
   195 apply(simp add:interfree_def interfree_swap_def)
   196 apply clarify
   197 apply(case_tac i)
   198  apply(case_tac j)
   199   apply simp_all
   200 apply(case_tac j,simp+)
   201 done
   202 
   203 lemma interfree_Map:
   204   "(\<forall>i j. a\<le>i \<and> i<b \<and> a\<le>j \<and> j<b  \<and> i\<noteq>j \<longrightarrow> interfree_aux (c i, Q i, c j))
   205   \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..<b])"
   206 by(force simp add: interfree_def less_diff_conv)
   207 
   208 definition map_ann_hoare :: "(('a ann_com_op * 'a assn) list) \<Rightarrow> bool " ("[\<turnstile>] _" [0] 45) where
   209   "[\<turnstile>] Ts == (\<forall>i<length Ts. \<exists>c q. Ts!i=(Some c, q) \<and> \<turnstile> c q)"
   210 
   211 lemma MapAnnEmpty: "[\<turnstile>] []"
   212 by(simp add:map_ann_hoare_def)
   213 
   214 lemma MapAnnList: "\<lbrakk> \<turnstile> c q ; [\<turnstile>] xs \<rbrakk> \<Longrightarrow> [\<turnstile>] (Some c,q)#xs"
   215 apply(simp add:map_ann_hoare_def)
   216 apply clarify
   217 apply(case_tac i,simp+)
   218 done
   219 
   220 lemma MapAnnMap:
   221   "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> \<turnstile> (c k) (Q k) \<Longrightarrow> [\<turnstile>] map (\<lambda>k. (Some (c k), Q k)) [i..<j]"
   222 apply(simp add: map_ann_hoare_def less_diff_conv)
   223 done
   224 
   225 lemma ParallelRule:"\<lbrakk> [\<turnstile>] Ts ; interfree Ts \<rbrakk>
   226   \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i))))
   227           Parallel Ts
   228         (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"
   229 apply(rule Parallel)
   230  apply(simp add:map_ann_hoare_def)
   231 apply simp
   232 done
   233 (*
   234 lemma ParamParallelRule:
   235  "\<lbrakk> \<forall>k<n. \<turnstile> (c k) (Q k);
   236    \<forall>k l. k<n \<and> l<n  \<and> k\<noteq>l \<longrightarrow> interfree_aux (Some(c k), Q k, Some(c l)) \<rbrakk>
   237   \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<n} . pre(c i)) COBEGIN SCHEME [0\<le>i<n] (c i) (Q i) COEND  (\<Inter>i\<in>{i. i<n} . Q i )"
   238 apply(rule ParallelConseqRule)
   239   apply simp
   240   apply clarify
   241   apply force
   242  apply(rule ParallelRule)
   243   apply(rule MapAnnMap)
   244   apply simp
   245  apply(rule interfree_Map)
   246  apply simp
   247 apply simp
   248 apply clarify
   249 apply force
   250 done
   251 *)
   252 
   253 text \<open>The following are some useful lemmas and simplification
   254 tactics to control which theorems are used to simplify at each moment,
   255 so that the original input does not suffer any unexpected
   256 transformation.\<close>
   257 
   258 lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
   259   by fast
   260 
   261 lemma list_length: "length []=0" "length (x#xs) = Suc(length xs)"
   262   by simp_all
   263 lemma list_lemmas: "length []=0" "length (x#xs) = Suc(length xs)"
   264     "(x#xs) ! 0 = x" "(x#xs) ! Suc n = xs ! n"
   265   by simp_all
   266 lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
   267   by auto
   268 lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
   269 lemmas my_simp_list = list_lemmas fst_conv snd_conv
   270 not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
   271 Collect_mem_eq ball_simps option.simps primrecdef_list
   272 lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append
   273 
   274 ML \<open>
   275 fun before_interfree_simp_tac ctxt =
   276   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm com.simps}, @{thm post.simps}])
   277 
   278 fun interfree_simp_tac ctxt =
   279   asm_simp_tac (put_simpset HOL_ss ctxt
   280     addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list})
   281 
   282 fun ParallelConseq ctxt =
   283   simp_tac (put_simpset HOL_basic_ss ctxt
   284     addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list})
   285 \<close>
   286 
   287 text \<open>The following tactic applies \<open>tac\<close> to each conjunct in a
   288 subgoal of the form \<open>A \<Longrightarrow> a1 \<and> a2 \<and> .. \<and> an\<close>  returning
   289 \<open>n\<close> subgoals, one for each conjunct:\<close>
   290 
   291 ML \<open>
   292 fun conjI_Tac ctxt tac i st = st |>
   293        ( (EVERY [resolve_tac ctxt [conjI] i,
   294           conjI_Tac ctxt tac (i+1),
   295           tac i]) ORELSE (tac i) )
   296 \<close>
   297 
   298 
   299 subsubsection \<open>Tactic for the generation of the verification conditions\<close>
   300 
   301 text \<open>The tactic basically uses two subtactics:
   302 
   303 \begin{description}
   304 
   305 \item[HoareRuleTac] is called at the level of parallel programs, it
   306  uses the ParallelTac to solve parallel composition of programs.
   307  This verification has two parts, namely, (1) all component programs are
   308  correct and (2) they are interference free.  \<open>HoareRuleTac\<close> is
   309  also called at the level of atomic regions, i.e.  \<open>\<langle> \<rangle>\<close> and
   310  \<open>AWAIT b THEN _ END\<close>, and at each interference freedom test.
   311 
   312 \item[AnnHoareRuleTac] is for component programs which
   313  are annotated programs and so, there are not unknown assertions
   314  (no need to use the parameter precond, see NOTE).
   315 
   316  NOTE: precond(::bool) informs if the subgoal has the form \<open>\<parallel>- ?p c q\<close>,
   317  in this case we have precond=False and the generated  verification
   318  condition would have the form \<open>?p \<subseteq> \<dots>\<close> which can be solved by
   319  \<open>rtac subset_refl\<close>, if True we proceed to simplify it using
   320  the simplification tactics above.
   321 
   322 \end{description}
   323 \<close>
   324 
   325 ML \<open>
   326 
   327 fun WlpTac ctxt i = resolve_tac ctxt @{thms SeqRule} i THEN HoareRuleTac ctxt false (i + 1)
   328 and HoareRuleTac ctxt precond i st = st |>
   329     ( (WlpTac ctxt i THEN HoareRuleTac ctxt precond i)
   330       ORELSE
   331       (FIRST[resolve_tac ctxt @{thms SkipRule} i,
   332              resolve_tac ctxt @{thms BasicRule} i,
   333              EVERY[resolve_tac ctxt @{thms ParallelConseqRule} i,
   334                    ParallelConseq ctxt (i+2),
   335                    ParallelTac ctxt (i+1),
   336                    ParallelConseq ctxt i],
   337              EVERY[resolve_tac ctxt @{thms CondRule} i,
   338                    HoareRuleTac ctxt false (i+2),
   339                    HoareRuleTac ctxt false (i+1)],
   340              EVERY[resolve_tac ctxt @{thms WhileRule} i,
   341                    HoareRuleTac ctxt true (i+1)],
   342              K all_tac i ]
   343        THEN (if precond then (K all_tac i) else resolve_tac ctxt @{thms subset_refl} i)))
   344 
   345 and AnnWlpTac ctxt i = resolve_tac ctxt @{thms AnnSeq} i THEN AnnHoareRuleTac ctxt (i + 1)
   346 and AnnHoareRuleTac ctxt i st = st |>
   347     ( (AnnWlpTac ctxt i THEN AnnHoareRuleTac ctxt i )
   348      ORELSE
   349       (FIRST[(resolve_tac ctxt @{thms AnnskipRule} i),
   350              EVERY[resolve_tac ctxt @{thms AnnatomRule} i,
   351                    HoareRuleTac ctxt true (i+1)],
   352              (resolve_tac ctxt @{thms AnnwaitRule} i),
   353              resolve_tac ctxt @{thms AnnBasic} i,
   354              EVERY[resolve_tac ctxt @{thms AnnCond1} i,
   355                    AnnHoareRuleTac ctxt (i+3),
   356                    AnnHoareRuleTac ctxt (i+1)],
   357              EVERY[resolve_tac ctxt @{thms AnnCond2} i,
   358                    AnnHoareRuleTac ctxt (i+1)],
   359              EVERY[resolve_tac ctxt @{thms AnnWhile} i,
   360                    AnnHoareRuleTac ctxt (i+2)],
   361              EVERY[resolve_tac ctxt @{thms AnnAwait} i,
   362                    HoareRuleTac ctxt true (i+1)],
   363              K all_tac i]))
   364 
   365 and ParallelTac ctxt i = EVERY[resolve_tac ctxt @{thms ParallelRule} i,
   366                           interfree_Tac ctxt (i+1),
   367                            MapAnn_Tac ctxt i]
   368 
   369 and MapAnn_Tac ctxt i st = st |>
   370     (FIRST[resolve_tac ctxt @{thms MapAnnEmpty} i,
   371            EVERY[resolve_tac ctxt @{thms MapAnnList} i,
   372                  MapAnn_Tac ctxt (i+1),
   373                  AnnHoareRuleTac ctxt i],
   374            EVERY[resolve_tac ctxt @{thms MapAnnMap} i,
   375                  resolve_tac ctxt @{thms allI} i,
   376                  resolve_tac ctxt @{thms impI} i,
   377                  AnnHoareRuleTac ctxt i]])
   378 
   379 and interfree_swap_Tac ctxt i st = st |>
   380     (FIRST[resolve_tac ctxt @{thms interfree_swap_Empty} i,
   381            EVERY[resolve_tac ctxt @{thms interfree_swap_List} i,
   382                  interfree_swap_Tac ctxt (i+2),
   383                  interfree_aux_Tac ctxt (i+1),
   384                  interfree_aux_Tac ctxt i ],
   385            EVERY[resolve_tac ctxt @{thms interfree_swap_Map} i,
   386                  resolve_tac ctxt @{thms allI} i,
   387                  resolve_tac ctxt @{thms impI} i,
   388                  conjI_Tac ctxt (interfree_aux_Tac ctxt) i]])
   389 
   390 and interfree_Tac ctxt i st = st |>
   391    (FIRST[resolve_tac ctxt @{thms interfree_Empty} i,
   392           EVERY[resolve_tac ctxt @{thms interfree_List} i,
   393                 interfree_Tac ctxt (i+1),
   394                 interfree_swap_Tac ctxt i],
   395           EVERY[resolve_tac ctxt @{thms interfree_Map} i,
   396                 resolve_tac ctxt @{thms allI} i,
   397                 resolve_tac ctxt @{thms allI} i,
   398                 resolve_tac ctxt @{thms impI} i,
   399                 interfree_aux_Tac ctxt i ]])
   400 
   401 and interfree_aux_Tac ctxt i = (before_interfree_simp_tac ctxt i ) THEN
   402         (FIRST[resolve_tac ctxt @{thms interfree_aux_rule1} i,
   403                dest_assertions_Tac ctxt i])
   404 
   405 and dest_assertions_Tac ctxt i st = st |>
   406     (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_assertions} i,
   407                  dest_atomics_Tac ctxt (i+1),
   408                  dest_atomics_Tac ctxt i],
   409            EVERY[resolve_tac ctxt @{thms AnnSeq_assertions} i,
   410                  dest_assertions_Tac ctxt (i+1),
   411                  dest_assertions_Tac ctxt i],
   412            EVERY[resolve_tac ctxt @{thms AnnCond1_assertions} i,
   413                  dest_assertions_Tac ctxt (i+2),
   414                  dest_assertions_Tac ctxt (i+1),
   415                  dest_atomics_Tac ctxt i],
   416            EVERY[resolve_tac ctxt @{thms AnnCond2_assertions} i,
   417                  dest_assertions_Tac ctxt (i+1),
   418                  dest_atomics_Tac ctxt i],
   419            EVERY[resolve_tac ctxt @{thms AnnWhile_assertions} i,
   420                  dest_assertions_Tac ctxt (i+2),
   421                  dest_atomics_Tac ctxt (i+1),
   422                  dest_atomics_Tac ctxt i],
   423            EVERY[resolve_tac ctxt @{thms AnnAwait_assertions} i,
   424                  dest_atomics_Tac ctxt (i+1),
   425                  dest_atomics_Tac ctxt i],
   426            dest_atomics_Tac ctxt i])
   427 
   428 and dest_atomics_Tac ctxt i st = st |>
   429     (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_atomics} i,
   430                  HoareRuleTac ctxt true i],
   431            EVERY[resolve_tac ctxt @{thms AnnSeq_atomics} i,
   432                  dest_atomics_Tac ctxt (i+1),
   433                  dest_atomics_Tac ctxt i],
   434            EVERY[resolve_tac ctxt @{thms AnnCond1_atomics} i,
   435                  dest_atomics_Tac ctxt (i+1),
   436                  dest_atomics_Tac ctxt i],
   437            EVERY[resolve_tac ctxt @{thms AnnCond2_atomics} i,
   438                  dest_atomics_Tac ctxt i],
   439            EVERY[resolve_tac ctxt @{thms AnnWhile_atomics} i,
   440                  dest_atomics_Tac ctxt i],
   441            EVERY[resolve_tac ctxt @{thms Annatom_atomics} i,
   442                  HoareRuleTac ctxt true i],
   443            EVERY[resolve_tac ctxt @{thms AnnAwait_atomics} i,
   444                  HoareRuleTac ctxt true i],
   445                  K all_tac i])
   446 \<close>
   447 
   448 
   449 text \<open>The final tactic is given the name \<open>oghoare\<close>:\<close>
   450 
   451 ML \<open>
   452 fun oghoare_tac ctxt = SUBGOAL (fn (_, i) => HoareRuleTac ctxt true i)
   453 \<close>
   454 
   455 text \<open>Notice that the tactic for parallel programs \<open>oghoare_tac\<close> is initially invoked with the value \<open>true\<close> for
   456 the parameter \<open>precond\<close>.
   457 
   458 Parts of the tactic can be also individually used to generate the
   459 verification conditions for annotated sequential programs and to
   460 generate verification conditions out of interference freedom tests:\<close>
   461 
   462 ML \<open>
   463 fun annhoare_tac ctxt = SUBGOAL (fn (_, i) => AnnHoareRuleTac ctxt i)
   464 
   465 fun interfree_aux_tac ctxt = SUBGOAL (fn (_, i) => interfree_aux_Tac ctxt i)
   466 \<close>
   467 
   468 text \<open>The so defined ML tactics are then ``exported'' to be used in
   469 Isabelle proofs.\<close>
   470 
   471 method_setup oghoare = \<open>
   472   Scan.succeed (SIMPLE_METHOD' o oghoare_tac)\<close>
   473   "verification condition generator for the oghoare logic"
   474 
   475 method_setup annhoare = \<open>
   476   Scan.succeed (SIMPLE_METHOD' o annhoare_tac)\<close>
   477   "verification condition generator for the ann_hoare logic"
   478 
   479 method_setup interfree_aux = \<open>
   480   Scan.succeed (SIMPLE_METHOD' o interfree_aux_tac)\<close>
   481   "verification condition generator for interference freedom tests"
   482 
   483 text \<open>Tactics useful for dealing with the generated verification conditions:\<close>
   484 
   485 method_setup conjI_tac = \<open>
   486   Scan.succeed (fn ctxt => SIMPLE_METHOD' (conjI_Tac ctxt (K all_tac)))\<close>
   487   "verification condition generator for interference freedom tests"
   488 
   489 ML \<open>
   490 fun disjE_Tac ctxt tac i st = st |>
   491        ( (EVERY [eresolve_tac ctxt [disjE] i,
   492           disjE_Tac ctxt tac (i+1),
   493           tac i]) ORELSE (tac i) )
   494 \<close>
   495 
   496 method_setup disjE_tac = \<open>
   497   Scan.succeed (fn ctxt => SIMPLE_METHOD' (disjE_Tac ctxt (K all_tac)))\<close>
   498   "verification condition generator for interference freedom tests"
   499 
   500 end