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