# Theory OG_Tactics

Up to index of Isabelle/HOL/HoareParallel

theory OG_Tactics
imports OG_Hoare
begin

    header {* \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 ⊆ (\<Inter>i∈{i. i<length Ts}. pre(the(com(Ts ! i))));
      \<parallel>- (\<Inter>i∈{i. i<length Ts}. pre(the(com(Ts ! i))))
          (Parallel Ts)
         (\<Inter>i∈{i. i<length Ts}. post(Ts ! i));
      (\<Inter>i∈{i. i<length Ts}. post(Ts ! i)) ⊆ q |]
      ==> \<parallel>- p (Parallel Ts) q"
    apply (rule Conseq)
    prefer 2
     apply fast
    apply assumption+
    done

    lemma SkipRule: "p ⊆ q ==> \<parallel>- 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} ==> \<parallel>- 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: "[| \<parallel>- p c1 r; \<parallel>- r c2 q |] ==> \<parallel>- p (Seq c1 c2) q"
    apply(rule Seq)
    apply fast+
    done

    lemma CondRule:
     "[| p ⊆ {s. (s∈b --> s∈w) ∧ (s∉b --> s∈w')}; \<parallel>- w c1 q; \<parallel>- w' c2 q |]
      ==> \<parallel>- 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; \<parallel>- (i ∩ b) c i ; (i ∩ (-b)) ⊆ q |]
            ==> \<parallel>- 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 @{text
    AnnBasic} and the @{text AnnAwait} commands when the transformation
    performed on the state is the identity, and for an @{text AnnAwait}
    command where the boolean condition is @{text "{s. True}"}: *}

    lemma AnnatomRule:
      "[| atom_com(c); \<parallel>- r c q |]  ==> \<turnstile> (AnnAwait r {s. True} c) q"
    apply(rule AnnAwait)
    apply simp_all
    done

    lemma AnnskipRule:
      "r ⊆ q ==> \<turnstile> (AnnBasic r id) q"
    apply(rule AnnBasic)
    apply simp
    done

    lemma AnnwaitRule:
      "[| (r ∩ b) ⊆ q |] ==> \<turnstile> (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 @{text
    map_ann_hoare}, @{text interfree_aux}, @{text interfree_swap} and
    @{text 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). \<parallel>- (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). \<parallel>- (q ∩ R) r q ∧ (∀p∈(assertions c). \<parallel>- (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:
      "\<parallel>- (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:
      "\<parallel>- (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:
      "\<parallel>- (q ∩ (r ∩ b)) a q ==> interfree_aux (None, q, Some (AnnAwait r b a))"
    by(simp add: interfree_aux_def oghoare_sound)

    constdefs
      interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) => bool"
      "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)

    constdefs map_ann_hoare :: "(('a ann_com_op * 'a assn) list) => bool " ("[\<turnstile>] _" [0] 45)
      "[\<turnstile>] Ts == (∀i<length Ts. ∃c q. Ts!i=(Some c, q) ∧ \<turnstile> c q)"

    lemma MapAnnEmpty: "[\<turnstile>] []"
    by(simp add:map_ann_hoare_def)

    lemma MapAnnList: "[| \<turnstile> c q ; [\<turnstile>] xs |] ==> [\<turnstile>] (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 --> \<turnstile> (c k) (Q k) ==> [\<turnstile>] map (λk. (Some (c k), Q k)) [i..<j]"
    apply(simp add: map_ann_hoare_def less_diff_conv)
    done

    lemma ParallelRule:"[| [\<turnstile>] Ts ; interfree Ts |]
      ==> \<parallel>- (\<Inter>i∈{i. i<length Ts}. pre(the(com(Ts!i))))
              Parallel Ts
            (\<Inter>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. \<turnstile> (c k) (Q k);
       ∀k l. k<n ∧ l<n  ∧ k≠l --> interfree_aux (Some(c k), Q k, Some(c l)) |]
      ==> \<parallel>- (\<Inter>i∈{i. i<n} . pre(c i)) COBEGIN SCHEME [0≤i<n] (c i) (Q i) COEND  (\<Inter>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
    lemma list_lemmas: "length []=0 ∧ length (x#xs) = Suc(length xs)
    ∧ (x#xs) ! 0=x ∧ (x#xs) ! Suc n = xs ! n"
    by simp
    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 Suc_Suc_eq
    Collect_mem_eq ball_simps option.simps primrecdef_list
    lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length

    ML {*
    val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"]))

    val  interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))

    val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list")))
    *}

    text {* The following tactic applies @{text tac} to each conjunct in a
    subgoal of the form @{text "A ==> a1 ∧ a2 ∧ .. ∧ an"}  returning
    @{text n} subgoals, one for each conjunct: *}

    ML {*
    fun conjI_Tac tac i st = st |>
           ( (EVERY [rtac conjI i,
              conjI_Tac 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.  @{text HoareRuleTac} is
     also called at the level of atomic regions, i.e.  @{text "⟨ ⟩"} and
     @{text "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 @{text "\<parallel>- ?p c q"},
     in this case we have precond=False and the generated  verification
     condition would have the form @{text "?p ⊆ …"} which can be solved by
     @{text "rtac subset_refl"}, if True we proceed to simplify it using
     the simplification tactics above.

    \end{description}
    *}

    ML {*

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

    and  AnnWlpTac i = (rtac (thm "AnnSeq") i) THEN (AnnHoareRuleTac (i+1))
    and AnnHoareRuleTac i st = st |>
        ( (AnnWlpTac i THEN AnnHoareRuleTac i )
         ORELSE
          (FIRST[(rtac (thm "AnnskipRule") i),
                 EVERY[rtac (thm "AnnatomRule") i,
                       HoareRuleTac true (i+1)],
                 (rtac (thm "AnnwaitRule") i),
                 rtac (thm "AnnBasic") i,
                 EVERY[rtac (thm "AnnCond1") i,
                       AnnHoareRuleTac (i+3),
                       AnnHoareRuleTac (i+1)],
                 EVERY[rtac (thm "AnnCond2") i,
                       AnnHoareRuleTac (i+1)],
                 EVERY[rtac (thm "AnnWhile") i,
                       AnnHoareRuleTac (i+2)],
                 EVERY[rtac (thm "AnnAwait") i,
                       HoareRuleTac true (i+1)],
                 K all_tac i]))

    and ParallelTac i = EVERY[rtac (thm "ParallelRule") i,
                              interfree_Tac (i+1),
                               MapAnn_Tac i]

    and MapAnn_Tac i st = st |>
        (FIRST[rtac (thm "MapAnnEmpty") i,
               EVERY[rtac (thm "MapAnnList") i,
                     MapAnn_Tac (i+1),
                     AnnHoareRuleTac i],
               EVERY[rtac (thm "MapAnnMap") i,
                     rtac (thm "allI") i,rtac (thm "impI") i,
                     AnnHoareRuleTac i]])

    and interfree_swap_Tac i st = st |>
        (FIRST[rtac (thm "interfree_swap_Empty") i,
               EVERY[rtac (thm "interfree_swap_List") i,
                     interfree_swap_Tac (i+2),
                     interfree_aux_Tac (i+1),
                     interfree_aux_Tac i ],
               EVERY[rtac (thm "interfree_swap_Map") i,
                     rtac (thm "allI") i,rtac (thm "impI") i,
                     conjI_Tac (interfree_aux_Tac) i]])

    and interfree_Tac i st = st |>
       (FIRST[rtac (thm "interfree_Empty") i,
              EVERY[rtac (thm "interfree_List") i,
                    interfree_Tac (i+1),
                    interfree_swap_Tac i],
              EVERY[rtac (thm "interfree_Map") i,
                    rtac (thm "allI") i,rtac (thm "allI") i,rtac (thm "impI") i,
                    interfree_aux_Tac i ]])

    and interfree_aux_Tac i = (before_interfree_simp_tac i ) THEN
            (FIRST[rtac (thm "interfree_aux_rule1") i,
                   dest_assertions_Tac i])

    and dest_assertions_Tac i st = st |>
        (FIRST[EVERY[rtac (thm "AnnBasic_assertions") i,
                     dest_atomics_Tac (i+1),
                     dest_atomics_Tac i],
               EVERY[rtac (thm "AnnSeq_assertions") i,
                     dest_assertions_Tac (i+1),
                     dest_assertions_Tac i],
               EVERY[rtac (thm "AnnCond1_assertions") i,
                     dest_assertions_Tac (i+2),
                     dest_assertions_Tac (i+1),
                     dest_atomics_Tac i],
               EVERY[rtac (thm "AnnCond2_assertions") i,
                     dest_assertions_Tac (i+1),
                     dest_atomics_Tac i],
               EVERY[rtac (thm "AnnWhile_assertions") i,
                     dest_assertions_Tac (i+2),
                     dest_atomics_Tac (i+1),
                     dest_atomics_Tac i],
               EVERY[rtac (thm "AnnAwait_assertions") i,
                     dest_atomics_Tac (i+1),
                     dest_atomics_Tac i],
               dest_atomics_Tac i])

    and dest_atomics_Tac i st = st |>
        (FIRST[EVERY[rtac (thm "AnnBasic_atomics") i,
                     HoareRuleTac true i],
               EVERY[rtac (thm "AnnSeq_atomics") i,
                     dest_atomics_Tac (i+1),
                     dest_atomics_Tac i],
               EVERY[rtac (thm "AnnCond1_atomics") i,
                     dest_atomics_Tac (i+1),
                     dest_atomics_Tac i],
               EVERY[rtac (thm "AnnCond2_atomics") i,
                     dest_atomics_Tac i],
               EVERY[rtac (thm "AnnWhile_atomics") i,
                     dest_atomics_Tac i],
               EVERY[rtac (thm "Annatom_atomics") i,
                     HoareRuleTac true i],
               EVERY[rtac (thm "AnnAwait_atomics") i,
                     HoareRuleTac true i],
                     K all_tac i])
    *}

    text {* The final tactic is given the name @{text oghoare}: *}

    ML {*
    fun oghoare_tac i thm = SUBGOAL (fn (term, _) =>
       (HoareRuleTac true i)) i thm
    *}

    text {* Notice that the tactic for parallel programs @{text
    "oghoare_tac"} is initially invoked with the value @{text true} for
    the parameter @{text 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 i thm = SUBGOAL (fn (term, _) =>
      (AnnHoareRuleTac i)) i thm

    fun interfree_aux_tac i thm = SUBGOAL (fn (term, _) =>
       (interfree_aux_Tac i)) i thm
    *}

    text {* The so defined ML tactics are then ``exported'' to be used in
    Isabelle proofs. *}

    method_setup oghoare = {*
      Method.no_args
        (Method.SIMPLE_METHOD' HEADGOAL (oghoare_tac)) *}
      "verification condition generator for the oghoare logic"

    method_setup annhoare = {*
      Method.no_args
        (Method.SIMPLE_METHOD' HEADGOAL (annhoare_tac)) *}
      "verification condition generator for the ann_hoare logic"

    method_setup interfree_aux = {*
      Method.no_args
        (Method.SIMPLE_METHOD' HEADGOAL (interfree_aux_tac)) *}
      "verification condition generator for interference freedom tests"

    text {* Tactics useful for dealing with the generated verification conditions: *}

    method_setup conjI_tac = {*
      Method.no_args
        (Method.SIMPLE_METHOD' HEADGOAL (conjI_Tac (K all_tac))) *}
      "verification condition generator for interference freedom tests"

    ML {*
    fun disjE_Tac tac i st = st |>
           ( (EVERY [etac disjE i,
              disjE_Tac tac (i+1),
              tac i]) ORELSE (tac i) )
    *}

    method_setup disjE_tac = {*
      Method.no_args
        (Method.SIMPLE_METHOD' HEADGOAL (disjE_Tac (K all_tac))) *}
      "verification condition generator for interference freedom tests"

    end

lemmas ann_hoare_intros:

      r ⊆ {s. f s ∈ q} ==> \<turnstile> AnnBasic r f
                              q

      [| \<turnstile> c0.0
            pre c1.0;
         \<turnstile> c1.0
            q |]
      ==> \<turnstile> AnnSeq c0.0 c1.0
             q

      [| r ∩ b ⊆ pre c1.0; \<turnstile> c1.0
                              q;
         r ∩ - b ⊆ pre c2.0; \<turnstile> c2.0
                                q |]
      ==> \<turnstile> AnnCond1 r b c1.0 c2.0
             q

      [| r ∩ b ⊆ pre c; \<turnstile> c
                           q;
         r ∩ - b ⊆ q |]
      ==> \<turnstile> AnnCond2 r b c
             q

      [| r ⊆ i; i ∩ b ⊆ pre c; \<turnstile> c
                                  i;
         i ∩ - b ⊆ q |]
      ==> \<turnstile> AnnWhile r b i c
             q

      [| atom_com c; \<parallel>- (r ∩ b)
                        c
                        q |]
      ==> \<turnstile> AnnAwait r b c
             q

      [| \<turnstile> c
            q;
         q ⊆ q' |]
      ==> \<turnstile> c
             q'

lemmas ann_hoare_intros:

      r ⊆ {s. f s ∈ q} ==> \<turnstile> AnnBasic r f
                              q

      [| \<turnstile> c0.0
            pre c1.0;
         \<turnstile> c1.0
            q |]
      ==> \<turnstile> AnnSeq c0.0 c1.0
             q

      [| r ∩ b ⊆ pre c1.0; \<turnstile> c1.0
                              q;
         r ∩ - b ⊆ pre c2.0; \<turnstile> c2.0
                                q |]
      ==> \<turnstile> AnnCond1 r b c1.0 c2.0
             q

      [| r ∩ b ⊆ pre c; \<turnstile> c
                           q;
         r ∩ - b ⊆ q |]
      ==> \<turnstile> AnnCond2 r b c
             q

      [| r ⊆ i; i ∩ b ⊆ pre c; \<turnstile> c
                                  i;
         i ∩ - b ⊆ q |]
      ==> \<turnstile> AnnWhile r b i c
             q

      [| atom_com c; \<parallel>- (r ∩ b)
                        c
                        q |]
      ==> \<turnstile> AnnAwait r b c
             q

      [| \<turnstile> c
            q;
         q ⊆ q' |]
      ==> \<turnstile> c
             q'

lemmas oghoare_intros:

      [| ∀i<length Ts. ∃c q. Ts ! i = (Some c, q) ∧ \<turnstile> c
               q;
         interfree Ts |]
      ==> \<parallel>- (INT i:{i. i < length Ts}. pre (the (OG_Hoare.com (Ts ! i))))
             Parallel Ts
             (INT i:{i. i < length Ts}. OG_Hoare.post (Ts ! i))

      \<parallel>- {s. f s ∈ q}
         Basic f
         q

      [| \<parallel>- p
            c1.0
            r;
         \<parallel>- r
            c2.0
            q |]
      ==> \<parallel>- p
             Seq c1.0 c2.0
             q

      [| \<parallel>- (p ∩ b)
            c1.0
            q;
         \<parallel>- (p ∩ - b)
            c2.0
            q |]
      ==> \<parallel>- p
             Cond b c1.0 c2.0
             q

      \<parallel>- (p ∩ b)
         c
         p
      ==> \<parallel>- p
             While b i c
             (p ∩ - b)

      [| p' ⊆ p; \<parallel>- p
                    c
                    q;
         q ⊆ q' |]
      ==> \<parallel>- p'
             c
             q'

lemmas oghoare_intros:

      [| ∀i<length Ts. ∃c q. Ts ! i = (Some c, q) ∧ \<turnstile> c
               q;
         interfree Ts |]
      ==> \<parallel>- (INT i:{i. i < length Ts}. pre (the (OG_Hoare.com (Ts ! i))))
             Parallel Ts
             (INT i:{i. i < length Ts}. OG_Hoare.post (Ts ! i))

      \<parallel>- {s. f s ∈ q}
         Basic f
         q

      [| \<parallel>- p
            c1.0
            r;
         \<parallel>- r
            c2.0
            q |]
      ==> \<parallel>- p
             Seq c1.0 c2.0
             q

      [| \<parallel>- (p ∩ b)
            c1.0
            q;
         \<parallel>- (p ∩ - b)
            c2.0
            q |]
      ==> \<parallel>- p
             Cond b c1.0 c2.0
             q

      \<parallel>- (p ∩ b)
         c
         p
      ==> \<parallel>- p
             While b i c
             (p ∩ - b)

      [| p' ⊆ p; \<parallel>- p
                    c
                    q;
         q ⊆ q' |]
      ==> \<parallel>- p'
             c
             q'

lemma ParallelConseqRule:

      [| p ⊆ (INT i:{i. i < length Ts}. pre (the (OG_Hoare.com (Ts ! i))));
         \<parallel>- (INT i:{i. i < length Ts}. pre (the (OG_Hoare.com (Ts ! i))))
            Parallel Ts
            (INT i:{i. i < length Ts}. OG_Hoare.post (Ts ! i));
         (INT i:{i. i < length Ts}. OG_Hoare.post (Ts ! i)) ⊆ q |]
      ==> \<parallel>- p
             Parallel Ts
             q

lemma SkipRule:

      p ⊆ q ==> \<parallel>- p
                   Basic id
                   q

lemma BasicRule:

      p ⊆ {s. f s ∈ q} ==> \<parallel>- p
                              Basic f
                              q

lemma SeqRule:

      [| \<parallel>- p
            c1.0
            r;
         \<parallel>- r
            c2.0
            q |]
      ==> \<parallel>- p
             Seq c1.0 c2.0
             q

lemma CondRule:

      [| p ⊆ {s. (s ∈ b --> s ∈ w) ∧ (s ∉ b --> s ∈ w')}; \<parallel>- w
                     c1.0
                     q;
         \<parallel>- w'
            c2.0
            q |]
      ==> \<parallel>- p
             Cond b c1.0 c2.0
             q

lemma WhileRule:

      [| p ⊆ i; \<parallel>- (i ∩ b)
                   c
                   i;
         i ∩ - b ⊆ q |]
      ==> \<parallel>- p
             While b i c
             q

lemma AnnatomRule:

      [| atom_com c; \<parallel>- r
                        c
                        q |]
      ==> \<turnstile> AnnAwait r {s. True} c
             q

lemma AnnskipRule:

      r ⊆ q ==> \<turnstile> AnnBasic r id
                   q

lemma AnnwaitRule:

      r ∩ b ⊆ q ==> \<turnstile> AnnAwait r b (Basic id)
                       q

lemma interfree_aux_rule1:

      interfree_aux (co, q, None)

lemma interfree_aux_rule2:

      ∀(R, r)∈atomics a. \<parallel>- (q ∩ R)
                            r
                            q
      ==> interfree_aux (None, q, Some a)

lemma interfree_aux_rule3:

      ∀(R, r)∈atomics a.
         \<parallel>- (q ∩ R)
            r
            q ∧
         (∀p∈assertions c. \<parallel>- (p ∩ R)
                              r
                              p)
      ==> interfree_aux (Some c, q, Some a)

lemma AnnBasic_assertions:

      [| interfree_aux (None, r, Some a); interfree_aux (None, q, Some a) |]
      ==> interfree_aux (Some (AnnBasic r f), q, Some a)

lemma AnnSeq_assertions:

      [| interfree_aux (Some c1.0, q, Some a); interfree_aux (Some c2.0, q, Some a) |]
      ==> interfree_aux (Some (AnnSeq c1.0 c2.0), q, Some a)

lemma AnnCond1_assertions:

      [| interfree_aux (None, r, Some a); interfree_aux (Some c1.0, q, Some a);
         interfree_aux (Some c2.0, q, Some a) |]
      ==> interfree_aux (Some (AnnCond1 r b c1.0 c2.0), q, Some a)

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)

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)

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)

lemma AnnBasic_atomics:

      \<parallel>- (q ∩ r)
         Basic f
         q
      ==> interfree_aux (None, q, Some (AnnBasic r f))

lemma AnnSeq_atomics:

      [| interfree_aux (Any, q, Some a1.0); interfree_aux (Any, q, Some a2.0) |]
      ==> interfree_aux (Any, q, Some (AnnSeq a1.0 a2.0))

lemma AnnCond1_atomics:

      [| interfree_aux (Any, q, Some a1.0); interfree_aux (Any, q, Some a2.0) |]
      ==> interfree_aux (Any, q, Some (AnnCond1 r b a1.0 a2.0))

lemma AnnCond2_atomics:

      interfree_aux (Any, q, Some a) ==> interfree_aux (Any, q, Some (AnnCond2 r b a))

lemma AnnWhile_atomics:

      interfree_aux (Any, q, Some a)
      ==> interfree_aux (Any, q, Some (AnnWhile r b i a))

lemma Annatom_atomics:

      \<parallel>- (q ∩ r)
         a
         q
      ==> interfree_aux (None, q, Some (AnnAwait r {x. True} a))

lemma AnnAwait_atomics:

      \<parallel>- (q ∩ (r ∩ b))
         a
         q
      ==> interfree_aux (None, q, Some (AnnAwait r b a))

lemma interfree_swap_Empty:

      interfree_swap (x, [])

lemma interfree_swap_List:

      [| interfree_aux (OG_Hoare.com x, OG_Hoare.post x, OG_Hoare.com y);
         interfree_aux (OG_Hoare.com y, OG_Hoare.post y, OG_Hoare.com x);
         interfree_swap (x, xs) |]
      ==> interfree_swap (x, y # xs)

lemma interfree_swap_Map:

      ∀k. i ≤ k ∧ k < j -->
          interfree_aux (OG_Hoare.com x, OG_Hoare.post x, c k) ∧
          interfree_aux (c k, Q k, OG_Hoare.com x)
      ==> interfree_swap (x, map (%k. (c k, Q k)) [i..<j])

lemma interfree_Empty:

      interfree []

lemma interfree_List:

      [| interfree_swap (x, xs); interfree xs |] ==> interfree (x # xs)

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])

lemma MapAnnEmpty:

      [\<turnstile>] []

lemma MapAnnList:

      [| \<turnstile> c
            q;
         [\<turnstile>] xs |]
      ==> [\<turnstile>] (Some c, q) # xs

lemma MapAnnMap:

      ∀k. i ≤ k ∧ k < j --> \<turnstile> c k
                               Q k
      ==> [\<turnstile>] map (%k. (Some (c k), Q k)) [i..<j]

lemma ParallelRule:

      [| [\<turnstile>] Ts; interfree Ts |]
      ==> \<parallel>- (INT i:{i. i < length Ts}. pre (the (OG_Hoare.com (Ts ! i))))
             Parallel Ts
             (INT i:{i. i < length Ts}. OG_Hoare.post (Ts ! i))

lemma Compl_Collect:

      - Collect b = {x. ¬ b x}

lemma list_length:

      length [] = 0 ∧ length (x # xs) = Suc (length xs)

lemma list_lemmas:

      length [] = 0 ∧
      length (x # xs) = Suc (length xs) ∧ (x # xs) ! 0 = x ∧ (x # xs) ! Suc n = xs ! n

lemma le_Suc_eq_insert:

      {i. i < Suc n} = insert n {i. i < n}

lemmas primrecdef_list:

      pre (AnnBasic r f) = r

      pre (AnnSeq c1.0 c2.0) = pre c1.0

      pre (AnnCond1 r b c1.0 c2.0) = r

      pre (AnnCond2 r b c) = r

      pre (AnnWhile r b i c) = r

      pre (AnnAwait r b c) = r

      assertions (AnnBasic r f) = {r}

      assertions (AnnSeq c1.0 c2.0) = assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond1 r b c1.0 c2.0) = {r} ∪ assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond2 r b c) = {r} ∪ assertions c

      assertions (AnnWhile r b i c) = {r, i} ∪ assertions c

      assertions (AnnAwait r b c) = {r}

      atomics (AnnBasic r f) = {(r, Basic f)}

      atomics (AnnSeq c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond1 r b c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond2 r b c) = atomics c

      atomics (AnnWhile r b i c) = atomics c

      atomics (AnnAwait r b c) = {(r ∩ b, c)}

      atom_com (Parallel Ts) = False

      atom_com (Basic f) = True

      atom_com (Seq c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (Cond b c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (While b i c) = atom_com c

lemmas primrecdef_list:

      pre (AnnBasic r f) = r

      pre (AnnSeq c1.0 c2.0) = pre c1.0

      pre (AnnCond1 r b c1.0 c2.0) = r

      pre (AnnCond2 r b c) = r

      pre (AnnWhile r b i c) = r

      pre (AnnAwait r b c) = r

      assertions (AnnBasic r f) = {r}

      assertions (AnnSeq c1.0 c2.0) = assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond1 r b c1.0 c2.0) = {r} ∪ assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond2 r b c) = {r} ∪ assertions c

      assertions (AnnWhile r b i c) = {r, i} ∪ assertions c

      assertions (AnnAwait r b c) = {r}

      atomics (AnnBasic r f) = {(r, Basic f)}

      atomics (AnnSeq c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond1 r b c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond2 r b c) = atomics c

      atomics (AnnWhile r b i c) = atomics c

      atomics (AnnAwait r b c) = {(r ∩ b, c)}

      atom_com (Parallel Ts) = False

      atom_com (Basic f) = True

      atom_com (Seq c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (Cond b c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (While b i c) = atom_com c

lemmas my_simp_list:

      length [] = 0 ∧
      length (x # xs) = Suc (length xs) ∧ (x # xs) ! 0 = x ∧ (x # xs) ! Suc n = xs ! n

      fst (a, b) = a

      snd (a, b) = b

      ¬ n < 0

      t = t

      {i. i < Suc n} = insert n {i. i < n}

      Suc m ≠ 0

      0 ≠ Suc m

      (Suc m = Suc n) = (m = n)

      {x. x ∈ A} = A

      (∀x∈A. P x ∨ Q) = ((∀x∈A. P x) ∨ Q)

      (∀x∈A. P ∨ Q x) = (P ∨ (∀x∈A. Q x))

      (∀x∈A. P --> Q x) = (P --> (∀x∈A. Q x))

      (∀x∈A. P x --> Q) = ((∃x∈A. P x) --> Q)

      (∀x∈{}. P x) = True

      (∀x∈UNIV. P x) = (∀x. P x)

      (∀x∈insert a B. P x) = (P a ∧ (∀x∈B. P x))

      (∀x∈Union A. P x) = (∀y∈A. ∀x∈y. P x)

      (∀x∈UNION A B. P x) = (∀a∈A. ∀x∈B a. P x)

      (∀x∈Collect Q. P x) = (∀x. Q x --> P x)

      (∀x∈f ` A. P x) = (∀x∈A. P (f x))

      (¬ (∀x∈A. P x)) = (∃x∈A. ¬ P x)

      None ≠ Some a'

      Some a' ≠ None

      (Some a = Some a') = (a = a')

      option_case f1.0 f2.0 None = f1.0

      option_case f1.0 f2.0 (Some a) = f2.0 a

      size None = 0

      size (Some a) = 0

      option_rec f1.0 f2.0 None = f1.0

      option_rec f1.0 f2.0 (Some a) = f2.0 a

      pre (AnnBasic r f) = r

      pre (AnnSeq c1.0 c2.0) = pre c1.0

      pre (AnnCond1 r b c1.0 c2.0) = r

      pre (AnnCond2 r b c) = r

      pre (AnnWhile r b i c) = r

      pre (AnnAwait r b c) = r

      assertions (AnnBasic r f) = {r}

      assertions (AnnSeq c1.0 c2.0) = assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond1 r b c1.0 c2.0) = {r} ∪ assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond2 r b c) = {r} ∪ assertions c

      assertions (AnnWhile r b i c) = {r, i} ∪ assertions c

      assertions (AnnAwait r b c) = {r}

      atomics (AnnBasic r f) = {(r, Basic f)}

      atomics (AnnSeq c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond1 r b c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond2 r b c) = atomics c

      atomics (AnnWhile r b i c) = atomics c

      atomics (AnnAwait r b c) = {(r ∩ b, c)}

      atom_com (Parallel Ts) = False

      atom_com (Basic f) = True

      atom_com (Seq c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (Cond b c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (While b i c) = atom_com c

lemmas my_simp_list:

      length [] = 0 ∧
      length (x # xs) = Suc (length xs) ∧ (x # xs) ! 0 = x ∧ (x # xs) ! Suc n = xs ! n

      fst (a, b) = a

      snd (a, b) = b

      ¬ n < 0

      t = t

      {i. i < Suc n} = insert n {i. i < n}

      Suc m ≠ 0

      0 ≠ Suc m

      (Suc m = Suc n) = (m = n)

      {x. x ∈ A} = A

      (∀x∈A. P x ∨ Q) = ((∀x∈A. P x) ∨ Q)

      (∀x∈A. P ∨ Q x) = (P ∨ (∀x∈A. Q x))

      (∀x∈A. P --> Q x) = (P --> (∀x∈A. Q x))

      (∀x∈A. P x --> Q) = ((∃x∈A. P x) --> Q)

      (∀x∈{}. P x) = True

      (∀x∈UNIV. P x) = (∀x. P x)

      (∀x∈insert a B. P x) = (P a ∧ (∀x∈B. P x))

      (∀x∈Union A. P x) = (∀y∈A. ∀x∈y. P x)

      (∀x∈UNION A B. P x) = (∀a∈A. ∀x∈B a. P x)

      (∀x∈Collect Q. P x) = (∀x. Q x --> P x)

      (∀x∈f ` A. P x) = (∀x∈A. P (f x))

      (¬ (∀x∈A. P x)) = (∃x∈A. ¬ P x)

      None ≠ Some a'

      Some a' ≠ None

      (Some a = Some a') = (a = a')

      option_case f1.0 f2.0 None = f1.0

      option_case f1.0 f2.0 (Some a) = f2.0 a

      size None = 0

      size (Some a) = 0

      option_rec f1.0 f2.0 None = f1.0

      option_rec f1.0 f2.0 (Some a) = f2.0 a

      pre (AnnBasic r f) = r

      pre (AnnSeq c1.0 c2.0) = pre c1.0

      pre (AnnCond1 r b c1.0 c2.0) = r

      pre (AnnCond2 r b c) = r

      pre (AnnWhile r b i c) = r

      pre (AnnAwait r b c) = r

      assertions (AnnBasic r f) = {r}

      assertions (AnnSeq c1.0 c2.0) = assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond1 r b c1.0 c2.0) = {r} ∪ assertions c1.0 ∪ assertions c2.0

      assertions (AnnCond2 r b c) = {r} ∪ assertions c

      assertions (AnnWhile r b i c) = {r, i} ∪ assertions c

      assertions (AnnAwait r b c) = {r}

      atomics (AnnBasic r f) = {(r, Basic f)}

      atomics (AnnSeq c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond1 r b c1.0 c2.0) = atomics c1.0 ∪ atomics c2.0

      atomics (AnnCond2 r b c) = atomics c

      atomics (AnnWhile r b i c) = atomics c

      atomics (AnnAwait r b c) = {(r ∩ b, c)}

      atom_com (Parallel Ts) = False

      atom_com (Basic f) = True

      atom_com (Seq c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (Cond b c1.0 c2.0) = (atom_com c1.0 ∧ atom_com c2.0)

      atom_com (While b i c) = atom_com c

lemmas ParallelConseq_list:

      INTER A B == {y. ∀x∈A. y ∈ B x}

      {x. P x ∧ Q x} = {x. P x} ∩ {x. Q x}

      length (map f xs) = length xs

      length [i..<j] = j - i

      length (xs @ ys) = length xs + length ys

      length [] = 0 ∧ length (x # xs) = Suc (length xs)

lemmas ParallelConseq_list:

      INTER A B == {y. ∀x∈A. y ∈ B x}

      {x. P x ∧ Q x} = {x. P x} ∩ {x. Q x}

      length (map f xs) = length xs

      length [i..<j] = j - i

      length (xs @ ys) = length xs + length ys

      length [] = 0 ∧ length (x # xs) = Suc (length xs)

#### Tactic for the generation of the verification conditions