Theory OG_Tactics

section ‹Generation of Verification Conditions›

theory OG_Tactics
imports OG_Hoare
begin

lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq
lemmas oghoare_intros=Parallel Basic Seq Cond While Conseq

lemma ParallelConseqRule:
 "⟦ p ⊆ (⋂i∈{i. i<length Ts}. pre(the(com(Ts ! i))));
  ∥- (⋂i∈{i. i<length Ts}. pre(the(com(Ts ! i))))
      (Parallel Ts)
     (⋂i∈{i. i<length Ts}. post(Ts ! i));
  (⋂i∈{i. i<length Ts}. post(Ts ! i)) ⊆ q ⟧
  ⟹ ∥- p (Parallel Ts) q"
apply (rule Conseq)
prefer 2
 apply fast
apply assumption+
done

lemma SkipRule: "p ⊆ q ⟹ ∥- p (Basic id) q"
apply(rule oghoare_intros)
  prefer 2 apply(rule Basic)
 prefer 2 apply(rule subset_refl)
apply(simp add:Id_def)
done

lemma BasicRule: "p ⊆ {s. (f s)∈q} ⟹ ∥- p (Basic f) q"
apply(rule oghoare_intros)
  prefer 2 apply(rule oghoare_intros)
 prefer 2 apply(rule subset_refl)
apply assumption
done

lemma SeqRule: "⟦ ∥- p c1 r; ∥- r c2 q ⟧ ⟹ ∥- p (Seq c1 c2) q"
apply(rule Seq)
apply fast+
done

lemma CondRule:
 "⟦ p ⊆ {s. (s∈b ⟶ s∈w) ∧ (s∉b ⟶ s∈w')}; ∥- w c1 q; ∥- w' c2 q ⟧
  ⟹ ∥- p (Cond b c1 c2) q"
apply(rule Cond)
 apply(rule Conseq)
 prefer 4 apply(rule Conseq)
apply simp_all
apply force+
done

lemma WhileRule: "⟦ p ⊆ i; ∥- (i ∩ b) c i ; (i ∩ (-b)) ⊆ q ⟧
        ⟹ ∥- p (While b i c) q"
apply(rule Conseq)
 prefer 2 apply(rule While)
apply assumption+
done

text ‹Three new proof rules for special instances of the ‹AnnBasic› and the ‹AnnAwait› commands when the transformation
performed on the state is the identity, and for an ‹AnnAwait›
command where the boolean condition is ‹{s. True}›:›

lemma AnnatomRule:
  "⟦ atom_com(c); ∥- r c q ⟧  ⟹ ⊢ (AnnAwait r {s. True} c) q"
apply(rule AnnAwait)
apply simp_all
done

lemma AnnskipRule:
  "r ⊆ q ⟹ ⊢ (AnnBasic r id) q"
apply(rule AnnBasic)
apply simp
done

lemma AnnwaitRule:
  "⟦ (r ∩ b) ⊆ q ⟧ ⟹ ⊢ (AnnAwait r b (Basic id)) q"
apply(rule AnnAwait)
 apply simp
apply(rule BasicRule)
apply simp
done

text ‹Lemmata to avoid using the definition of ‹map_ann_hoare›, ‹interfree_aux›, ‹interfree_swap› and
‹interfree› by splitting it into different cases:›

lemma interfree_aux_rule1: "interfree_aux(co, q, None)"
by(simp add:interfree_aux_def)

lemma interfree_aux_rule2:
  "∀(R,r)∈(atomics a). ∥- (q ∩ R) r q ⟹ interfree_aux(None, q, Some a)"
apply(simp add:interfree_aux_def)
apply(force elim:oghoare_sound)
done

lemma interfree_aux_rule3:
  "(∀(R, r)∈(atomics a). ∥- (q ∩ R) r q ∧ (∀p∈(assertions c). ∥- (p ∩ R) r p))
  ⟹ interfree_aux(Some c, q, Some a)"
apply(simp add:interfree_aux_def)
apply(force elim:oghoare_sound)
done

lemma AnnBasic_assertions:
  "⟦interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)⟧ ⟹
    interfree_aux(Some (AnnBasic r f), q, Some a)"
apply(simp add: interfree_aux_def)
by force

lemma AnnSeq_assertions:
  "⟦ interfree_aux(Some c1, q, Some a); interfree_aux(Some c2, q, Some a)⟧⟹
   interfree_aux(Some (AnnSeq c1 c2), q, Some a)"
apply(simp add: interfree_aux_def)
by force

lemma AnnCond1_assertions:
  "⟦ interfree_aux(None, r, Some a); interfree_aux(Some c1, q, Some a);
  interfree_aux(Some c2, q, Some a)⟧⟹
  interfree_aux(Some(AnnCond1 r b c1 c2), q, Some a)"
apply(simp add: interfree_aux_def)
by force

lemma AnnCond2_assertions:
  "⟦ interfree_aux(None, r, Some a); interfree_aux(Some c, q, Some a)⟧⟹
  interfree_aux(Some (AnnCond2 r b c), q, Some a)"
apply(simp add: interfree_aux_def)
by force

lemma AnnWhile_assertions:
  "⟦ interfree_aux(None, r, Some a); interfree_aux(None, i, Some a);
  interfree_aux(Some c, q, Some a)⟧⟹
  interfree_aux(Some (AnnWhile r b i c), q, Some a)"
apply(simp add: interfree_aux_def)
by force

lemma AnnAwait_assertions:
  "⟦ interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)⟧⟹
  interfree_aux(Some (AnnAwait r b c), q, Some a)"
apply(simp add: interfree_aux_def)
by force

lemma AnnBasic_atomics:
  "∥- (q ∩ r) (Basic f) q ⟹ interfree_aux(None, q, Some (AnnBasic r f))"
by(simp add: interfree_aux_def oghoare_sound)

lemma AnnSeq_atomics:
  "⟦ interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)⟧⟹
  interfree_aux(Any, q, Some (AnnSeq a1 a2))"
apply(simp add: interfree_aux_def)
by force

lemma AnnCond1_atomics:
  "⟦ interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)⟧⟹
   interfree_aux(Any, q, Some (AnnCond1 r b a1 a2))"
apply(simp add: interfree_aux_def)
by force

lemma AnnCond2_atomics:
  "interfree_aux (Any, q, Some a)⟹ interfree_aux(Any, q, Some (AnnCond2 r b a))"
by(simp add: interfree_aux_def)

lemma AnnWhile_atomics: "interfree_aux (Any, q, Some a)
     ⟹ interfree_aux(Any, q, Some (AnnWhile r b i a))"
by(simp add: interfree_aux_def)

lemma Annatom_atomics:
  "∥- (q ∩ r) a q ⟹ interfree_aux (None, q, Some (AnnAwait r {x. True} a))"
by(simp add: interfree_aux_def oghoare_sound)

lemma AnnAwait_atomics:
  "∥- (q ∩ (r ∩ b)) a q ⟹ interfree_aux (None, q, Some (AnnAwait r b a))"
by(simp add: interfree_aux_def oghoare_sound)

definition interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) ⇒ bool" where
  "interfree_swap == λ(x, xs). ∀y∈set xs. interfree_aux (com x, post x, com y)
  ∧ interfree_aux(com y, post y, com x)"

lemma interfree_swap_Empty: "interfree_swap (x, [])"
by(simp add:interfree_swap_def)

lemma interfree_swap_List:
  "⟦ interfree_aux (com x, post x, com y);
  interfree_aux (com y, post y ,com x); interfree_swap (x, xs) ⟧
  ⟹ interfree_swap (x, y#xs)"
by(simp add:interfree_swap_def)

lemma interfree_swap_Map: "∀k. i≤k ∧ k<j ⟶ interfree_aux (com x, post x, c k)
 ∧ interfree_aux (c k, Q k, com x)
 ⟹ interfree_swap (x, map (λk. (c k, Q k)) [i..<j])"
by(force simp add: interfree_swap_def less_diff_conv)

lemma interfree_Empty: "interfree []"
by(simp add:interfree_def)

lemma interfree_List:
  "⟦ interfree_swap(x, xs); interfree xs ⟧ ⟹ interfree (x#xs)"
apply(simp add:interfree_def interfree_swap_def)
apply clarify
apply(case_tac i)
 apply(case_tac j)
  apply simp_all
apply(case_tac j,simp+)
done

lemma interfree_Map:
  "(∀i j. a≤i ∧ i<b ∧ a≤j ∧ j<b  ∧ i≠j ⟶ interfree_aux (c i, Q i, c j))
  ⟹ interfree (map (λk. (c k, Q k)) [a..<b])"
by(force simp add: interfree_def less_diff_conv)

definition map_ann_hoare :: "(('a ann_com_op * 'a assn) list) ⇒ bool " ("[⊢] _" [0] 45) where
  "[⊢] Ts == (∀i<length Ts. ∃c q. Ts!i=(Some c, q) ∧ ⊢ c q)"

lemma MapAnnEmpty: "[⊢] []"
by(simp add:map_ann_hoare_def)

lemma MapAnnList: "⟦ ⊢ c q ; [⊢] xs ⟧ ⟹ [⊢] (Some c,q)#xs"
apply(simp add:map_ann_hoare_def)
apply clarify
apply(case_tac i,simp+)
done

lemma MapAnnMap:
  "∀k. i≤k ∧ k<j ⟶ ⊢ (c k) (Q k) ⟹ [⊢] map (λk. (Some (c k), Q k)) [i..<j]"
apply(simp add: map_ann_hoare_def less_diff_conv)
done

lemma ParallelRule:"⟦ [⊢] Ts ; interfree Ts ⟧
  ⟹ ∥- (⋂i∈{i. i<length Ts}. pre(the(com(Ts!i))))
          Parallel Ts
        (⋂i∈{i. i<length Ts}. post(Ts!i))"
apply(rule Parallel)
 apply(simp add:map_ann_hoare_def)
apply simp
done
(*
lemma ParamParallelRule:
 "⟦ ∀k<n. ⊢ (c k) (Q k);
   ∀k l. k<n ∧ l<n  ∧ k≠l ⟶ interfree_aux (Some(c k), Q k, Some(c l)) ⟧
  ⟹ ∥- (⋂i∈{i. i<n} . pre(c i)) COBEGIN SCHEME [0≤i<n] (c i) (Q i) COEND  (⋂i∈{i. i<n} . Q i )"
apply(rule ParallelConseqRule)
  apply simp
  apply clarify
  apply force
 apply(rule ParallelRule)
  apply(rule MapAnnMap)
  apply simp
 apply(rule interfree_Map)
 apply simp
apply simp
apply clarify
apply force
done
*)

text ‹The following are some useful lemmas and simplification
tactics to control which theorems are used to simplify at each moment,
so that the original input does not suffer any unexpected
transformation.›

lemma Compl_Collect: "-(Collect b) = {x. ¬(b x)}"
  by fast

lemma list_length: "length []=0" "length (x#xs) = Suc(length xs)"
  by simp_all
lemma list_lemmas: "length []=0" "length (x#xs) = Suc(length xs)"
    "(x#xs) ! 0 = x" "(x#xs) ! Suc n = xs ! n"
  by simp_all
lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
  by auto
lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
lemmas my_simp_list = list_lemmas fst_conv snd_conv
not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
Collect_mem_eq ball_simps option.simps primrecdef_list
lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append

ML ‹
fun before_interfree_simp_tac ctxt =
  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm com.simps}, @{thm post.simps}])

fun interfree_simp_tac ctxt =
  asm_simp_tac (put_simpset HOL_ss ctxt
    addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list})

fun ParallelConseq ctxt =
  simp_tac (put_simpset HOL_basic_ss ctxt
    addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list})
›

text ‹The following tactic applies ‹tac› to each conjunct in a
subgoal of the form ‹A ⟹ a1 ∧ a2 ∧ .. ∧ an›  returning
‹n› subgoals, one for each conjunct:›

ML ‹
fun conjI_Tac ctxt tac i st = st |>
       ( (EVERY [resolve_tac ctxt [conjI] i,
          conjI_Tac ctxt tac (i+1),
          tac i]) ORELSE (tac i) )
›


subsubsection ‹Tactic for the generation of the verification conditions›

text ‹The tactic basically uses two subtactics:

\begin{description}

\item[HoareRuleTac] is called at the level of parallel programs, it
 uses the ParallelTac to solve parallel composition of programs.
 This verification has two parts, namely, (1) all component programs are
 correct and (2) they are interference free.  ‹HoareRuleTac› is
 also called at the level of atomic regions, i.e.  ‹⟨ ⟩› and
 ‹AWAIT b THEN _ END›, and at each interference freedom test.

\item[AnnHoareRuleTac] is for component programs which
 are annotated programs and so, there are not unknown assertions
 (no need to use the parameter precond, see NOTE).

 NOTE: precond(::bool) informs if the subgoal has the form ‹∥- ?p c q›,
 in this case we have precond=False and the generated  verification
 condition would have the form ‹?p ⊆ …› which can be solved by
 ‹rtac subset_refl›, if True we proceed to simplify it using
 the simplification tactics above.

\end{description}
›

ML ‹

fun WlpTac ctxt i = resolve_tac ctxt @{thms SeqRule} i THEN HoareRuleTac ctxt false (i + 1)
and HoareRuleTac ctxt precond i st = st |>
    ( (WlpTac ctxt i THEN HoareRuleTac ctxt precond i)
      ORELSE
      (FIRST[resolve_tac ctxt @{thms SkipRule} i,
             resolve_tac ctxt @{thms BasicRule} i,
             EVERY[resolve_tac ctxt @{thms ParallelConseqRule} i,
                   ParallelConseq ctxt (i+2),
                   ParallelTac ctxt (i+1),
                   ParallelConseq ctxt i],
             EVERY[resolve_tac ctxt @{thms CondRule} i,
                   HoareRuleTac ctxt false (i+2),
                   HoareRuleTac ctxt false (i+1)],
             EVERY[resolve_tac ctxt @{thms WhileRule} i,
                   HoareRuleTac ctxt true (i+1)],
             K all_tac i ]
       THEN (if precond then (K all_tac i) else resolve_tac ctxt @{thms subset_refl} i)))

and AnnWlpTac ctxt i = resolve_tac ctxt @{thms AnnSeq} i THEN AnnHoareRuleTac ctxt (i + 1)
and AnnHoareRuleTac ctxt i st = st |>
    ( (AnnWlpTac ctxt i THEN AnnHoareRuleTac ctxt i )
     ORELSE
      (FIRST[(resolve_tac ctxt @{thms AnnskipRule} i),
             EVERY[resolve_tac ctxt @{thms AnnatomRule} i,
                   HoareRuleTac ctxt true (i+1)],
             (resolve_tac ctxt @{thms AnnwaitRule} i),
             resolve_tac ctxt @{thms AnnBasic} i,
             EVERY[resolve_tac ctxt @{thms AnnCond1} i,
                   AnnHoareRuleTac ctxt (i+3),
                   AnnHoareRuleTac ctxt (i+1)],
             EVERY[resolve_tac ctxt @{thms AnnCond2} i,
                   AnnHoareRuleTac ctxt (i+1)],
             EVERY[resolve_tac ctxt @{thms AnnWhile} i,
                   AnnHoareRuleTac ctxt (i+2)],
             EVERY[resolve_tac ctxt @{thms AnnAwait} i,
                   HoareRuleTac ctxt true (i+1)],
             K all_tac i]))

and ParallelTac ctxt i = EVERY[resolve_tac ctxt @{thms ParallelRule} i,
                          interfree_Tac ctxt (i+1),
                           MapAnn_Tac ctxt i]

and MapAnn_Tac ctxt i st = st |>
    (FIRST[resolve_tac ctxt @{thms MapAnnEmpty} i,
           EVERY[resolve_tac ctxt @{thms MapAnnList} i,
                 MapAnn_Tac ctxt (i+1),
                 AnnHoareRuleTac ctxt i],
           EVERY[resolve_tac ctxt @{thms MapAnnMap} i,
                 resolve_tac ctxt @{thms allI} i,
                 resolve_tac ctxt @{thms impI} i,
                 AnnHoareRuleTac ctxt i]])

and interfree_swap_Tac ctxt i st = st |>
    (FIRST[resolve_tac ctxt @{thms interfree_swap_Empty} i,
           EVERY[resolve_tac ctxt @{thms interfree_swap_List} i,
                 interfree_swap_Tac ctxt (i+2),
                 interfree_aux_Tac ctxt (i+1),
                 interfree_aux_Tac ctxt i ],
           EVERY[resolve_tac ctxt @{thms interfree_swap_Map} i,
                 resolve_tac ctxt @{thms allI} i,
                 resolve_tac ctxt @{thms impI} i,
                 conjI_Tac ctxt (interfree_aux_Tac ctxt) i]])

and interfree_Tac ctxt i st = st |>
   (FIRST[resolve_tac ctxt @{thms interfree_Empty} i,
          EVERY[resolve_tac ctxt @{thms interfree_List} i,
                interfree_Tac ctxt (i+1),
                interfree_swap_Tac ctxt i],
          EVERY[resolve_tac ctxt @{thms interfree_Map} i,
                resolve_tac ctxt @{thms allI} i,
                resolve_tac ctxt @{thms allI} i,
                resolve_tac ctxt @{thms impI} i,
                interfree_aux_Tac ctxt i ]])

and interfree_aux_Tac ctxt i = (before_interfree_simp_tac ctxt i ) THEN
        (FIRST[resolve_tac ctxt @{thms interfree_aux_rule1} i,
               dest_assertions_Tac ctxt i])

and dest_assertions_Tac ctxt i st = st |>
    (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_assertions} i,
                 dest_atomics_Tac ctxt (i+1),
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnSeq_assertions} i,
                 dest_assertions_Tac ctxt (i+1),
                 dest_assertions_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnCond1_assertions} i,
                 dest_assertions_Tac ctxt (i+2),
                 dest_assertions_Tac ctxt (i+1),
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnCond2_assertions} i,
                 dest_assertions_Tac ctxt (i+1),
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnWhile_assertions} i,
                 dest_assertions_Tac ctxt (i+2),
                 dest_atomics_Tac ctxt (i+1),
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnAwait_assertions} i,
                 dest_atomics_Tac ctxt (i+1),
                 dest_atomics_Tac ctxt i],
           dest_atomics_Tac ctxt i])

and dest_atomics_Tac ctxt i st = st |>
    (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_atomics} i,
                 HoareRuleTac ctxt true i],
           EVERY[resolve_tac ctxt @{thms AnnSeq_atomics} i,
                 dest_atomics_Tac ctxt (i+1),
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnCond1_atomics} i,
                 dest_atomics_Tac ctxt (i+1),
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnCond2_atomics} i,
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms AnnWhile_atomics} i,
                 dest_atomics_Tac ctxt i],
           EVERY[resolve_tac ctxt @{thms Annatom_atomics} i,
                 HoareRuleTac ctxt true i],
           EVERY[resolve_tac ctxt @{thms AnnAwait_atomics} i,
                 HoareRuleTac ctxt true i],
                 K all_tac i])
›


text ‹The final tactic is given the name ‹oghoare›:›

ML ‹
fun oghoare_tac ctxt = SUBGOAL (fn (_, i) => HoareRuleTac ctxt true i)
›

text ‹Notice that the tactic for parallel programs ‹oghoare_tac› is initially invoked with the value ‹true› for
the parameter ‹precond›.

Parts of the tactic can be also individually used to generate the
verification conditions for annotated sequential programs and to
generate verification conditions out of interference freedom tests:›

ML ‹
fun annhoare_tac ctxt = SUBGOAL (fn (_, i) => AnnHoareRuleTac ctxt i)

fun interfree_aux_tac ctxt = SUBGOAL (fn (_, i) => interfree_aux_Tac ctxt i)
›

text ‹The so defined ML tactics are then ``exported'' to be used in
Isabelle proofs.›

method_setup oghoare = ‹
  Scan.succeed (SIMPLE_METHOD' o oghoare_tac)›
  "verification condition generator for the oghoare logic"

method_setup annhoare = ‹
  Scan.succeed (SIMPLE_METHOD' o annhoare_tac)›
  "verification condition generator for the ann_hoare logic"

method_setup interfree_aux = ‹
  Scan.succeed (SIMPLE_METHOD' o interfree_aux_tac)›
  "verification condition generator for interference freedom tests"

text ‹Tactics useful for dealing with the generated verification conditions:›

method_setup conjI_tac = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (conjI_Tac ctxt (K all_tac)))›
  "verification condition generator for interference freedom tests"

ML ‹
fun disjE_Tac ctxt tac i st = st |>
       ( (EVERY [eresolve_tac ctxt [disjE] i,
          disjE_Tac ctxt tac (i+1),
          tac i]) ORELSE (tac i) )
›

method_setup disjE_tac = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (disjE_Tac ctxt (K all_tac)))›
  "verification condition generator for interference freedom tests"

end