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