Theory RG_Hoare

section ‹The Proof System›

theory RG_Hoare imports RG_Tran begin

subsection ‹Proof System for Component Programs›

declare Un_subset_iff [simp del] sup.bounded_iff [simp del]

definition stable :: "'a set ⇒ ('a × 'a) set ⇒ bool" where
  "stable ≡ λf g. (∀x y. x ∈ f ⟶ (x, y) ∈ g ⟶ y ∈ f)"

inductive
  rghoare :: "['a com, 'a set, ('a × 'a) set, ('a × 'a) set, 'a set] ⇒ bool"
    ("⊢ _ sat [_, _, _, _]" [60,0,0,0,0] 45)
where
  Basic: "⟦ pre ⊆ {s. f s ∈ post}; {(s,t). s ∈ pre ∧ (t=f s ∨ t=s)} ⊆ guar;
            stable pre rely; stable post rely ⟧
           ⟹ ⊢ Basic f sat [pre, rely, guar, post]"

| Seq: "⟦ ⊢ P sat [pre, rely, guar, mid]; ⊢ Q sat [mid, rely, guar, post] ⟧
           ⟹ ⊢ Seq P Q sat [pre, rely, guar, post]"

| Cond: "⟦ stable pre rely; ⊢ P1 sat [pre ∩ b, rely, guar, post];
           ⊢ P2 sat [pre ∩ -b, rely, guar, post]; ∀s. (s,s)∈guar ⟧
          ⟹ ⊢ Cond b P1 P2 sat [pre, rely, guar, post]"

| While: "⟦ stable pre rely; (pre ∩ -b) ⊆ post; stable post rely;
            ⊢ P sat [pre ∩ b, rely, guar, pre]; ∀s. (s,s)∈guar ⟧
          ⟹ ⊢ While b P sat [pre, rely, guar, post]"

| Await: "⟦ stable pre rely; stable post rely;
            ∀V. ⊢ P sat [pre ∩ b ∩ {V}, {(s, t). s = t},
                UNIV, {s. (V, s) ∈ guar} ∩ post] ⟧
           ⟹ ⊢ Await b P sat [pre, rely, guar, post]"

| Conseq: "⟦ pre ⊆ pre'; rely ⊆ rely'; guar' ⊆ guar; post' ⊆ post;
             ⊢ P sat [pre', rely', guar', post'] ⟧
            ⟹ ⊢ P sat [pre, rely, guar, post]"

definition Pre :: "'a rgformula ⇒ 'a set" where
  "Pre x ≡ fst(snd x)"

definition Post :: "'a rgformula ⇒ 'a set" where
  "Post x ≡ snd(snd(snd(snd x)))"

definition Rely :: "'a rgformula ⇒ ('a × 'a) set" where
  "Rely x ≡ fst(snd(snd x))"

definition Guar :: "'a rgformula ⇒ ('a × 'a) set" where
  "Guar x ≡ fst(snd(snd(snd x)))"

definition Com :: "'a rgformula ⇒ 'a com" where
  "Com x ≡ fst x"

subsection ‹Proof System for Parallel Programs›

type_synonym 'a par_rgformula =
  "('a rgformula) list × 'a set × ('a × 'a) set × ('a × 'a) set × 'a set"

inductive
  par_rghoare :: "('a rgformula) list ⇒ 'a set ⇒ ('a × 'a) set ⇒ ('a × 'a) set ⇒ 'a set ⇒ bool"
    ("⊢ _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
where
  Parallel:
  "⟦ ∀i<length xs. rely ∪ (⋃j∈{j. j<length xs ∧ j≠i}. Guar(xs!j)) ⊆ Rely(xs!i);
    (⋃j∈{j. j<length xs}. Guar(xs!j)) ⊆ guar;
     pre ⊆ (⋂i∈{i. i<length xs}. Pre(xs!i));
    (⋂i∈{i. i<length xs}. Post(xs!i)) ⊆ post;
    ∀i<length xs. ⊢ Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] ⟧
   ⟹  ⊢ xs SAT [pre, rely, guar, post]"

section ‹Soundness›

subsubsection ‹Some previous lemmas›

lemma tl_of_assum_in_assum:
  "(P, s) # (P, t) # xs ∈ assum (pre, rely) ⟹ stable pre rely
  ⟹ (P, t) # xs ∈ assum (pre, rely)"
apply(simp add:assum_def)
apply clarify
apply(rule conjI)
 apply(erule_tac x=0 in allE)
 apply(simp (no_asm_use)only:stable_def)
 apply(erule allE,erule allE,erule impE,assumption,erule mp)
 apply(simp add:Env)
apply clarify
apply(erule_tac x="Suc i" in allE)
apply simp
done

lemma etran_in_comm:
  "(P, t) # xs ∈ comm(guar, post) ⟹ (P, s) # (P, t) # xs ∈ comm(guar, post)"
apply(simp add:comm_def)
apply clarify
apply(case_tac i,simp+)
done

lemma ctran_in_comm:
  "⟦(s, s) ∈ guar; (Q, s) # xs ∈ comm(guar, post)⟧
  ⟹ (P, s) # (Q, s) # xs ∈ comm(guar, post)"
apply(simp add:comm_def)
apply clarify
apply(case_tac i,simp+)
done

lemma takecptn_is_cptn [rule_format, elim!]:
  "∀j. c ∈ cptn ⟶ take (Suc j) c ∈ cptn"
apply(induct "c")
 apply(force elim: cptn.cases)
apply clarify
apply(case_tac j)
 apply simp
 apply(rule CptnOne)
apply simp
apply(force intro:cptn.intros elim:cptn.cases)
done

lemma dropcptn_is_cptn [rule_format,elim!]:
  "∀j<length c. c ∈ cptn ⟶ drop j c ∈ cptn"
apply(induct "c")
 apply(force elim: cptn.cases)
apply clarify
apply(case_tac j,simp+)
apply(erule cptn.cases)
  apply simp
 apply force
apply force
done

lemma takepar_cptn_is_par_cptn [rule_format,elim]:
  "∀j. c ∈ par_cptn ⟶ take (Suc j) c ∈ par_cptn"
apply(induct "c")
 apply(force elim: cptn.cases)
apply clarify
apply(case_tac j,simp)
 apply(rule ParCptnOne)
apply(force intro:par_cptn.intros elim:par_cptn.cases)
done

lemma droppar_cptn_is_par_cptn [rule_format]:
  "∀j<length c. c ∈ par_cptn ⟶ drop j c ∈ par_cptn"
apply(induct "c")
 apply(force elim: par_cptn.cases)
apply clarify
apply(case_tac j,simp+)
apply(erule par_cptn.cases)
  apply simp
 apply force
apply force
done

lemma tl_of_cptn_is_cptn: "⟦x # xs ∈ cptn; xs ≠ []⟧ ⟹ xs  ∈ cptn"
apply(subgoal_tac "1 < length (x # xs)")
 apply(drule dropcptn_is_cptn,simp+)
done

lemma not_ctran_None [rule_format]:
  "∀s. (None, s)#xs ∈ cptn ⟶ (∀i<length xs. ((None, s)#xs)!i -e→ xs!i)"
apply(induct xs,simp+)
apply clarify
apply(erule cptn.cases,simp)
 apply simp
 apply(case_tac i,simp)
  apply(rule Env)
 apply simp
apply(force elim:ctran.cases)
done

lemma cptn_not_empty [simp]:"[] ∉ cptn"
apply(force elim:cptn.cases)
done

lemma etran_or_ctran [rule_format]:
  "∀m i. x∈cptn ⟶ m ≤ length x
   ⟶ (∀i. Suc i < m ⟶ ¬ x!i -c→ x!Suc i) ⟶ Suc i < m
   ⟶ x!i -e→ x!Suc i"
  supply [[simproc del: defined_all]]
apply(induct x,simp)
apply clarify
apply(erule cptn.cases,simp)
 apply(case_tac i,simp)
  apply(rule Env)
 apply simp
 apply(erule_tac x="m - 1" in allE)
 apply(case_tac m,simp,simp)
 apply(subgoal_tac "(∀i. Suc i < nata ⟶ (((P, t) # xs) ! i, xs ! i) ∉ ctran)")
  apply force
 apply clarify
   apply(erule_tac x="Suc ia" in allE,simp)
apply(erule_tac x="0" and P="λj. H j ⟶ (J j) ∉ ctran" for H J in allE,simp)
done

lemma etran_or_ctran2 [rule_format]:
  "∀i. Suc i<length x ⟶ x∈cptn ⟶ (x!i -c→ x!Suc i ⟶ ¬ x!i -e→ x!Suc i)
  ∨ (x!i -e→ x!Suc i ⟶ ¬ x!i -c→ x!Suc i)"
apply(induct x)
 apply simp
apply clarify
apply(erule cptn.cases,simp)
 apply(case_tac i,simp+)
apply(case_tac i,simp)
 apply(force elim:etran.cases)
apply simp
done

lemma etran_or_ctran2_disjI1:
  "⟦ x∈cptn; Suc i<length x; x!i -c→ x!Suc i⟧ ⟹ ¬ x!i -e→ x!Suc i"
by(drule etran_or_ctran2,simp_all)

lemma etran_or_ctran2_disjI2:
  "⟦ x∈cptn; Suc i<length x; x!i -e→ x!Suc i⟧ ⟹ ¬ x!i -c→ x!Suc i"
by(drule etran_or_ctran2,simp_all)

lemma not_ctran_None2 [rule_format]:
  "⟦ (None, s) # xs ∈cptn; i<length xs⟧ ⟹ ¬ ((None, s) # xs) ! i -c→ xs ! i"
apply(frule not_ctran_None,simp)
apply(case_tac i,simp)
 apply(force elim:etranE)
apply simp
apply(rule etran_or_ctran2_disjI2,simp_all)
apply(force intro:tl_of_cptn_is_cptn)
done

lemma Ex_first_occurrence [rule_format]: "P (n::nat) ⟶ (∃m. P m ∧ (∀i<m. ¬ P i))"
apply(rule nat_less_induct)
apply clarify
apply(case_tac "∀m. m<n ⟶ ¬ P m")
apply auto
done

lemma stability [rule_format]:
  "∀j k. x ∈ cptn ⟶ stable p rely ⟶ j≤k ⟶ k<length x ⟶ snd(x!j)∈p  ⟶
  (∀i. (Suc i)<length x ⟶
          (x!i -e→ x!(Suc i)) ⟶ (snd(x!i), snd(x!(Suc i))) ∈ rely) ⟶
  (∀i. j≤i ∧ i<k ⟶ x!i -e→ x!Suc i) ⟶ snd(x!k)∈p ∧ fst(x!j)=fst(x!k)"
  supply [[simproc del: defined_all]]
apply(induct x)
 apply clarify
 apply(force elim:cptn.cases)
apply clarify
apply(erule cptn.cases,simp)
 apply simp
 apply(case_tac k,simp,simp)
 apply(case_tac j,simp)
  apply(erule_tac x=0 in allE)
  apply(erule_tac x="nat" and P="λj. (0≤j) ⟶ (J j)" for J in allE,simp)
  apply(subgoal_tac "t∈p")
   apply(subgoal_tac "(∀i. i < length xs ⟶ ((P, t) # xs) ! i -e→ xs ! i ⟶ (snd (((P, t) # xs) ! i), snd (xs ! i)) ∈ rely)")
    apply clarify
    apply(erule_tac x="Suc i" and P="λj. (H j) ⟶ (J j)∈etran" for H J in allE,simp)
   apply clarify
   apply(erule_tac x="Suc i" and P="λj. (H j) ⟶ (J j) ⟶ (T j)∈rely" for H J T in allE,simp)
  apply(erule_tac x=0 and P="λj. (H j) ⟶ (J j)∈etran ⟶ T j" for H J T in allE,simp)
  apply(simp(no_asm_use) only:stable_def)
  apply(erule_tac x=s in allE)
  apply(erule_tac x=t in allE)
  apply simp
  apply(erule mp)
  apply(erule mp)
  apply(rule Env)
 apply simp
 apply(erule_tac x="nata" in allE)
 apply(erule_tac x="nat" and P="λj. (s≤j) ⟶ (J j)" for s J in allE,simp)
 apply(subgoal_tac "(∀i. i < length xs ⟶ ((P, t) # xs) ! i -e→ xs ! i ⟶ (snd (((P, t) # xs) ! i), snd (xs ! i)) ∈ rely)")
  apply clarify
  apply(erule_tac x="Suc i" and P="λj. (H j) ⟶ (J j)∈etran" for H J in allE,simp)
 apply clarify
 apply(erule_tac x="Suc i" and P="λj. (H j) ⟶ (J j) ⟶ (T j)∈rely" for H J T in allE,simp)
apply(case_tac k,simp,simp)
apply(case_tac j)
 apply(erule_tac x=0 and P="λj. (H j) ⟶ (J j)∈etran" for H J in allE,simp)
 apply(erule etran.cases,simp)
apply(erule_tac x="nata" in allE)
apply(erule_tac x="nat" and P="λj. (s≤j) ⟶ (J j)" for s J in allE,simp)
apply(subgoal_tac "(∀i. i < length xs ⟶ ((Q, t) # xs) ! i -e→ xs ! i ⟶ (snd (((Q, t) # xs) ! i), snd (xs ! i)) ∈ rely)")
 apply clarify
 apply(erule_tac x="Suc i" and P="λj. (H j) ⟶ (J j)∈etran" for H J in allE,simp)
apply clarify
apply(erule_tac x="Suc i" and P="λj. (H j) ⟶ (J j) ⟶ (T j)∈rely" for H J T in allE,simp)
done

subsection ‹Soundness of the System for Component Programs›

subsubsection ‹Soundness of the Basic rule›

lemma unique_ctran_Basic [rule_format]:
  "∀s i. x ∈ cptn ⟶ x ! 0 = (Some (Basic f), s) ⟶
  Suc i<length x ⟶ x!i -c→ x!Suc i ⟶
  (∀j. Suc j<length x ⟶ i≠j ⟶ x!j -e→ x!Suc j)"
apply(induct x,simp)
apply simp
apply clarify
apply(erule cptn.cases,simp)
 apply(case_tac i,simp+)
 apply clarify
 apply(case_tac j,simp)
  apply(rule Env)
 apply simp
apply clarify
apply simp
apply(case_tac i)
 apply(case_tac j,simp,simp)
 apply(erule ctran.cases,simp_all)
 apply(force elim: not_ctran_None)
apply(ind_cases "((Some (Basic f), sa), Q, t) ∈ ctran" for sa Q t)
apply simp
apply(drule_tac i=nat in not_ctran_None,simp)
apply(erule etranE,simp)
done

lemma exists_ctran_Basic_None [rule_format]:
  "∀s i. x ∈ cptn ⟶ x ! 0 = (Some (Basic f), s)
  ⟶ i<length x ⟶ fst(x!i)=None ⟶ (∃j<i. x!j -c→ x!Suc j)"
apply(induct x,simp)
apply simp
apply clarify
apply(erule cptn.cases,simp)
 apply(case_tac i,simp,simp)
 apply(erule_tac x=nat in allE,simp)
 apply clarify
 apply(rule_tac x="Suc j" in exI,simp,simp)
apply clarify
apply(case_tac i,simp,simp)
apply(rule_tac x=0 in exI,simp)
done

lemma Basic_sound:
  " ⟦pre ⊆ {s. f s ∈ post}; {(s, t). s ∈ pre ∧ t = f s} ⊆ guar;
  stable pre rely; stable post rely⟧
  ⟹ ⊨ Basic f sat [pre, rely, guar, post]"
  supply [[simproc del: defined_all]]
apply(unfold com_validity_def)
apply clarify
apply(simp add:comm_def)
apply(rule conjI)
 apply clarify
 apply(simp add:cp_def assum_def)
 apply clarify
 apply(frule_tac j=0 and k=i and p=pre in stability)
       apply simp_all
   apply(erule_tac x=ia in allE,simp)
  apply(erule_tac i=i and f=f in unique_ctran_Basic,simp_all)
 apply(erule subsetD,simp)
 apply(case_tac "x!i")
 apply clarify
 apply(drule_tac s="Some (Basic f)" in sym,simp)
 apply(thin_tac "∀j. H j" for H)
 apply(force elim:ctran.cases)
apply clarify
apply(simp add:cp_def)
apply clarify
apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+)
  apply(case_tac x,simp+)
  apply(rule last_fst_esp,simp add:last_length)
 apply (case_tac x,simp+)
apply(simp add:assum_def)
apply clarify
apply(frule_tac j=0 and k="j" and p=pre in stability)
      apply simp_all
  apply(erule_tac x=i in allE,simp)
 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
apply(case_tac "x!j")
apply clarify
apply simp
apply(drule_tac s="Some (Basic f)" in sym,simp)
apply(case_tac "x!Suc j",simp)
apply(rule ctran.cases,simp)
apply(simp_all)
apply(drule_tac c=sa in subsetD,simp)
apply clarify
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
 apply(case_tac x,simp+)
 apply(erule_tac x=i in allE)
apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
  apply arith+
apply(case_tac x)
apply(simp add:last_length)+
done

subsubsection‹Soundness of the Await rule›

lemma unique_ctran_Await [rule_format]:
  "∀s i. x ∈ cptn ⟶ x ! 0 = (Some (Await b c), s) ⟶
  Suc i<length x ⟶ x!i -c→ x!Suc i ⟶
  (∀j. Suc j<length x ⟶ i≠j ⟶ x!j -e→ x!Suc j)"
apply(induct x,simp+)
apply clarify
apply(erule cptn.cases,simp)
 apply(case_tac i,simp+)
 apply clarify
 apply(case_tac j,simp)
  apply(rule Env)
 apply simp
apply clarify
apply simp
apply(case_tac i)
 apply(case_tac j,simp,simp)
 apply(erule ctran.cases,simp_all)
 apply(force elim: not_ctran_None)
apply(ind_cases "((Some (Await b c), sa), Q, t) ∈ ctran" for sa Q t,simp)
apply(drule_tac i=nat in not_ctran_None,simp)
apply(erule etranE,simp)
done

lemma exists_ctran_Await_None [rule_format]:
  "∀s i.  x ∈ cptn ⟶ x ! 0 = (Some (Await b c), s)
  ⟶ i<length x ⟶ fst(x!i)=None ⟶ (∃j<i. x!j -c→ x!Suc j)"
apply(induct x,simp+)
apply clarify
apply(erule cptn.cases,simp)
 apply(case_tac i,simp+)
 apply(erule_tac x=nat in allE,simp)
 apply clarify
 apply(rule_tac x="Suc j" in exI,simp,simp)
apply clarify
apply(case_tac i,simp,simp)
apply(rule_tac x=0 in exI,simp)
done

lemma Star_imp_cptn:
  "(P, s) -c*→ (R, t) ⟹ ∃l ∈ cp P s. (last l)=(R, t)
  ∧ (∀i. Suc i<length l ⟶ l!i -c→ l!Suc i)"
apply (erule converse_rtrancl_induct2)
 apply(rule_tac x="[(R,t)]" in bexI)
  apply simp
 apply(simp add:cp_def)
 apply(rule CptnOne)
apply clarify
apply(rule_tac x="(a, b)#l" in bexI)
 apply (rule conjI)
  apply(case_tac l,simp add:cp_def)
  apply(simp add:last_length)
 apply clarify
apply(case_tac i,simp)
apply(simp add:cp_def)
apply force
apply(simp add:cp_def)
 apply(case_tac l)
 apply(force elim:cptn.cases)
apply simp
apply(erule CptnComp)
apply clarify
done

lemma Await_sound:
  "⟦stable pre rely; stable post rely;
  ∀V. ⊢ P sat [pre ∩ b ∩ {s. s = V}, {(s, t). s = t},
                 UNIV, {s. (V, s) ∈ guar} ∩ post] ∧
  ⊨ P sat [pre ∩ b ∩ {s. s = V}, {(s, t). s = t},
                 UNIV, {s. (V, s) ∈ guar} ∩ post] ⟧
  ⟹ ⊨ Await b P sat [pre, rely, guar, post]"
apply(unfold com_validity_def)
apply clarify
apply(simp add:comm_def)
apply(rule conjI)
 apply clarify
 apply(simp add:cp_def assum_def)
 apply clarify
 apply(frule_tac j=0 and k=i and p=pre in stability,simp_all)
   apply(erule_tac x=ia in allE,simp)
  apply(subgoal_tac "x∈ cp (Some(Await b P)) s")
  apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
  apply(simp add:cp_def)
― ‹here starts the different part.›
 apply(erule ctran.cases,simp_all)
 apply(drule Star_imp_cptn)
 apply clarify
 apply(erule_tac x=sa in allE)
 apply clarify
 apply(erule_tac x=sa in allE)
 apply(drule_tac c=l in subsetD)
  apply (simp add:cp_def)
  apply clarify
  apply(erule_tac x=ia and P="λi. H i ⟶ (J i, I i)∈ctran" for H J I in allE,simp)
  apply(erule etranE,simp)
 apply simp
apply clarify
apply(simp add:cp_def)
apply clarify
apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
  apply (case_tac x,simp+)
 apply(rule last_fst_esp,simp add:last_length)
 apply(case_tac x, simp+)
apply clarify
apply(simp add:assum_def)
apply clarify
apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
  apply(erule_tac x=i in allE,simp)
 apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
apply(case_tac "x!j")
apply clarify
apply simp
apply(drule_tac s="Some (Await b P)" in sym,simp)
apply(case_tac "x!Suc j",simp)
apply(rule ctran.cases,simp)
apply(simp_all)
apply(drule Star_imp_cptn)
apply clarify
apply(erule_tac x=sa in allE)
apply clarify
apply(erule_tac x=sa in allE)
apply(drule_tac c=l in subsetD)
 apply (simp add:cp_def)
 apply clarify
 apply(erule_tac x=i and P="λi. H i ⟶ (J i, I i)∈ctran" for H J I in allE,simp)
 apply(erule etranE,simp)
apply simp
apply clarify
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
 apply(case_tac x,simp+)
 apply(erule_tac x=i in allE)
apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
 apply arith+
apply(case_tac x)
apply(simp add:last_length)+
done

subsubsection‹Soundness of the Conditional rule›

lemma Cond_sound:
  "⟦ stable pre rely; ⊨ P1 sat [pre ∩ b, rely, guar, post];
  ⊨ P2 sat [pre ∩ - b, rely, guar, post]; ∀s. (s,s)∈guar⟧
  ⟹ ⊨ (Cond b P1 P2) sat [pre, rely, guar, post]"
apply(unfold com_validity_def)
apply clarify
apply(simp add:cp_def comm_def)
apply(case_tac "∃i. Suc i<length x ∧ x!i -c→ x!Suc i")
 prefer 2
 apply simp
 apply clarify
 apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+)
     apply(case_tac x,simp+)
    apply(simp add:assum_def)
   apply(simp add:assum_def)
  apply(erule_tac m="length x" in etran_or_ctran,simp+)
 apply(case_tac x, (simp add:last_length)+)
apply(erule exE)
apply(drule_tac n=i and P="λi. H i ∧ (J i, I i) ∈ ctran" for H J I in Ex_first_occurrence)
apply clarify
apply (simp add:assum_def)
apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
 apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
apply(erule ctran.cases,simp_all)
 apply(erule_tac x="sa" in allE)
 apply(drule_tac c="drop (Suc m) x" in subsetD)
  apply simp
  apply clarify
 apply simp
 apply clarify
 apply(case_tac "i≤m")
  apply(drule le_imp_less_or_eq)
  apply(erule disjE)
   apply(erule_tac x=i in allE, erule impE, assumption)
   apply simp+
 apply(erule_tac x="i - (Suc m)" and P="λj. H j ⟶ J j ⟶ (I j)∈guar" for H J I in allE)
 apply(subgoal_tac "(Suc m)+(i - Suc m) ≤ length x")
  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) ≤ length x")
   apply(rotate_tac -2)
   apply simp
  apply arith
 apply arith
apply(case_tac "length (drop (Suc m) x)",simp)
apply(erule_tac x="sa" in allE)
back
apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
 apply clarify
apply simp
apply clarify
apply(case_tac "i≤m")
 apply(drule le_imp_less_or_eq)
 apply(erule disjE)
  apply(erule_tac x=i in allE, erule impE, assumption)
  apply simp
 apply simp
apply(erule_tac x="i - (Suc m)" and P="λj. H j ⟶ J j ⟶ (I j)∈guar" for H J I in allE)
apply(subgoal_tac "(Suc m)+(i - Suc m) ≤ length x")
 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) ≤ length x")
  apply(rotate_tac -2)
  apply simp
 apply arith
apply arith
done

subsubsection‹Soundness of the Sequential rule›

inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c→ t"

lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) ≠ None"
apply(subgoal_tac "length xs<length (x # xs)")
 apply(drule_tac Q=Q in  lift_nth)
 apply(erule ssubst)
 apply (simp add:lift_def)
 apply(case_tac "(x # xs) ! length xs",simp)
apply simp
done

lemma Seq_sound1 [rule_format]:
  "x∈ cptn_mod ⟹ ∀s P. x !0=(Some (Seq P Q), s) ⟶
  (∀i<length x. fst(x!i)≠Some Q) ⟶
  (∃xs∈ cp (Some P) s. x=map (lift Q) xs)"
  supply [[simproc del: defined_all]]
apply(erule cptn_mod.induct)
apply(unfold cp_def)
apply safe
apply simp_all
    apply(simp add:lift_def)
    apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne)
   apply(subgoal_tac "(∀i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) ≠ Some Q)")
    apply clarify
    apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
    apply(rule conjI,erule CptnEnv)
    apply(simp (no_asm_use) add:lift_def)
   apply clarify
   apply(erule_tac x="Suc i" in allE, simp)
  apply(ind_cases "((Some (Seq Pa Q), sa), None, t) ∈ ctran" for Pa sa t)
 apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
apply(erule_tac x="length xs" in allE, simp)
apply(simp only:Cons_lift_append)
apply(subgoal_tac "length xs < length ((Some P, sa) # xs)")
 apply(simp only :nth_append length_map last_length nth_map)
 apply(case_tac "last((Some P, sa) # xs)")
 apply(simp add:lift_def)
apply simp
done

lemma Seq_sound2 [rule_format]:
  "x ∈ cptn ⟹ ∀s P i. x!0=(Some (Seq P Q), s) ⟶ i<length x
  ⟶ fst(x!i)=Some Q ⟶
  (∀j<i. fst(x!j)≠(Some Q)) ⟶
  (∃xs ys. xs ∈ cp (Some P) s ∧ length xs=Suc i
   ∧ ys ∈ cp (Some Q) (snd(xs !i)) ∧ x=(map (lift Q) xs)@tl ys)"
  supply [[simproc del: defined_all]]
apply(erule cptn.induct)
apply(unfold cp_def)
apply safe
apply simp_all
 apply(case_tac i,simp+)
 apply(erule allE,erule impE,assumption,simp)
 apply clarify
 apply(subgoal_tac "(∀j < nat. fst (((Some (Seq Pa Q), t) # xs) ! j) ≠ Some Q)",clarify)
  prefer 2
  apply force
 apply(case_tac xsa,simp,simp)
 apply(rename_tac list)
 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
 apply(rule conjI,erule CptnEnv)
 apply(simp (no_asm_use) add:lift_def)
 apply(rule_tac x=ys in exI,simp)
apply(ind_cases "((Some (Seq Pa Q), sa), t) ∈ ctran" for Pa sa t)
 apply simp
 apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
 apply(rule conjI)
  apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp)
 apply(case_tac i, simp+)
 apply(case_tac nat,simp+)
 apply(rule_tac x="(Some Q,ta)#xs" in exI,simp add:lift_def)
 apply(case_tac nat,simp+)
 apply(force)
apply(case_tac i, simp+)
apply(case_tac nat,simp+)
apply(erule_tac x="Suc nata" in allE,simp)
apply clarify
apply(subgoal_tac "(∀j<Suc nata. fst (((Some (Seq P2 Q), ta) # xs) ! j) ≠ Some Q)",clarify)
 prefer 2
 apply clarify
 apply force
apply(rule_tac x="(Some Pa, sa)#(Some P2, ta)#(tl xsa)" in exI,simp)
apply(rule conjI,erule CptnComp)
apply(rule nth_tl_if,force,simp+)
apply(rule_tac x=ys in exI,simp)
apply(rule conjI)
apply(rule nth_tl_if,force,simp+)
 apply(rule tl_zero,simp+)
 apply force
apply(rule conjI,simp add:lift_def)
apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)")
 apply(simp add:Cons_lift del:list.map)
 apply(rule nth_tl_if)
   apply force
  apply simp+
apply(simp add:lift_def)
done
(*
lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) ≠ None"
apply(simp only:last_length [THEN sym])
apply(subgoal_tac "length xs<length (x # xs)")
 apply(drule_tac Q=Q in  lift_nth)
 apply(erule ssubst)
 apply (simp add:lift_def)
 apply(case_tac "(x # xs) ! length xs",simp)
apply simp
done
*)

lemma last_lift_not_None2: "fst ((lift Q) (last (x#xs))) ≠ None"
apply(simp only:last_length [THEN sym])
apply(subgoal_tac "length xs<length (x # xs)")
 apply(drule_tac Q=Q in  lift_nth)
 apply(erule ssubst)
 apply (simp add:lift_def)
 apply(case_tac "(x # xs) ! length xs",simp)
apply simp
done

lemma Seq_sound:
  "⟦⊨ P sat [pre, rely, guar, mid]; ⊨ Q sat [mid, rely, guar, post]⟧
  ⟹ ⊨ Seq P Q sat [pre, rely, guar, post]"
apply(unfold com_validity_def)
apply clarify
apply(case_tac "∃i<length x. fst(x!i)=Some Q")
 prefer 2
 apply (simp add:cp_def cptn_iff_cptn_mod)
 apply clarify
 apply(frule_tac Seq_sound1,force)
  apply force
 apply clarify
 apply(erule_tac x=s in allE,simp)
 apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod)
  apply(simp add:assum_def)
  apply clarify
  apply(erule_tac P="λj. H j ⟶ J j ⟶ I j" for H J I in allE,erule impE, assumption)
  apply(simp add:snd_lift)
  apply(erule mp)
  apply(force elim:etranE intro:Env simp add:lift_def)
 apply(simp add:comm_def)
 apply(rule conjI)
  apply clarify
  apply(erule_tac P="λj. H j ⟶ J j ⟶ I j" for H J I in allE,erule impE, assumption)
  apply(simp add:snd_lift)
  apply(erule mp)
  apply(case_tac "(xs!i)")
  apply(case_tac "(xs! Suc i)")
  apply(case_tac "fst(xs!i)")
   apply(erule_tac x=i in allE, simp add:lift_def)
  apply(case_tac "fst(xs!Suc i)")
   apply(force simp add:lift_def)
  apply(force simp add:lift_def)
 apply clarify
 apply(case_tac xs,simp add:cp_def)
 apply clarify
 apply (simp del:list.map)
 apply (rename_tac list)
 apply(subgoal_tac "(map (lift Q) ((a, b) # list))≠[]")
  apply(drule last_conv_nth)
  apply (simp del:list.map)
  apply(simp only:last_lift_not_None)
 apply simp
― ‹‹∃i<length x. fst (x ! i) = Some Q››
apply(erule exE)
apply(drule_tac n=i and P="λi. i < length x ∧ fst (x ! i) = Some Q" in Ex_first_occurrence)
apply clarify
apply (simp add:cp_def)
 apply clarify
 apply(frule_tac i=m in Seq_sound2,force)
  apply simp+
apply clarify
apply(simp add:comm_def)
apply(erule_tac x=s in allE)
apply(drule_tac c=xs in subsetD,simp)
 apply(case_tac "xs=[]",simp)
 apply(simp add:cp_def assum_def nth_append)
 apply clarify
 apply(erule_tac x=i in allE)
  back
 apply(simp add:snd_lift)
 apply(erule mp)
 apply(force elim:etranE intro:Env simp add:lift_def)
apply simp
apply clarify
apply(erule_tac x="snd(xs!m)" in allE)
apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
 apply(case_tac "xs≠[]")
 apply(drule last_conv_nth,simp)
 apply(rule conjI)
  apply(erule mp)
  apply(case_tac "xs!m")
  apply(case_tac "fst(xs!m)",simp)
  apply(simp add:lift_def nth_append)
 apply clarify
 apply(erule_tac x="m+i" in allE)
 back
 back
 apply(case_tac ys,(simp add:nth_append)+)
 apply (case_tac i, (simp add:snd_lift)+)
  apply(erule mp)
  apply(case_tac "xs!m")
  apply(force elim:etran.cases intro:Env simp add:lift_def)
 apply simp
apply simp
apply clarify
apply(rule conjI,clarify)
 apply(case_tac "i<m",simp add:nth_append)
  apply(simp add:snd_lift)
  apply(erule allE, erule impE, assumption, erule mp)
  apply(case_tac "(xs ! i)")
  apply(case_tac "(xs ! Suc i)")
  apply(case_tac "fst(xs ! i)",force simp add:lift_def)
  apply(case_tac "fst(xs ! Suc i)")
   apply (force simp add:lift_def)
  apply (force simp add:lift_def)
 apply(erule_tac x="i-m" in allE)
 back
 back
 apply(subgoal_tac "Suc (i - m) < length ys",simp)
  prefer 2
  apply arith
 apply(simp add:nth_append snd_lift)
 apply(rule conjI,clarify)
  apply(subgoal_tac "i=m")
   prefer 2
   apply arith
  apply clarify
  apply(simp add:cp_def)
  apply(rule tl_zero)
    apply(erule mp)
    apply(case_tac "lift Q (xs!m)",simp add:snd_lift)
    apply(case_tac "xs!m",case_tac "fst(xs!m)",simp add:lift_def snd_lift)
     apply(case_tac ys,simp+)
    apply(simp add:lift_def)
   apply simp
  apply force
 apply clarify
 apply(rule tl_zero)
   apply(rule tl_zero)
     apply (subgoal_tac "i-m=Suc(i-Suc m)")
      apply simp
      apply(erule mp)
      apply(case_tac ys,simp+)
   apply force
  apply arith
 apply force
apply clarify
apply(case_tac "(map (lift Q) xs @ tl ys)≠[]")
 apply(drule last_conv_nth)
 apply(simp add: snd_lift nth_append)
 apply(rule conjI,clarify)
  apply(case_tac ys,simp+)
 apply clarify
 apply(case_tac ys,simp+)
done

subsubsection‹Soundness of the While rule›

lemma last_append[rule_format]:
  "∀xs. ys≠[] ⟶ ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
apply(induct ys)
 apply simp
apply clarify
apply (simp add:nth_append)
done

lemma assum_after_body:
  "⟦ ⊨ P sat [pre ∩ b, rely, guar, pre];
  (Some P, s) # xs ∈ cptn_mod; fst (last ((Some P, s) # xs)) = None; s ∈ b;
  (Some (While b P), s) # (Some (Seq P (While b P)), s) #
   map (lift (While b P)) xs @ ys ∈ assum (pre, rely)⟧
  ⟹ (Some (While b P), snd (last ((Some P, s) # xs))) # ys ∈ assum (pre, rely)"
apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
apply clarify
apply(erule_tac x=s in allE)
apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
 apply clarify
 apply(erule_tac x="Suc i" in allE)
 apply simp
 apply(simp add:Cons_lift_append nth_append snd_lift del:list.map)
 apply(erule mp)
 apply(erule etranE,simp)
 apply(case_tac "fst(((Some P, s) # xs) ! i)")
  apply(force intro:Env simp add:lift_def)
 apply(force intro:Env simp add:lift_def)
apply(rule conjI)
 apply clarify
 apply(simp add:comm_def last_length)
apply clarify
apply(rule conjI)
 apply(simp add:comm_def)
apply clarify
apply(erule_tac x="Suc(length xs + i)" in allE,simp)
apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
apply(simp add:Cons_lift_append nth_append snd_lift)
done

lemma While_sound_aux [rule_format]:
  "⟦ pre ∩ - b ⊆ post; ⊨ P sat [pre ∩ b, rely, guar, pre]; ∀s. (s, s) ∈ guar;
   stable pre rely;  stable post rely; x ∈ cptn_mod ⟧
  ⟹  ∀s xs. x=(Some(While b P),s)#xs ⟶ x∈assum(pre, rely) ⟶ x ∈ comm (guar, post)"
  supply [[simproc del: defined_all]]
apply(erule cptn_mod.induct)
apply safe
apply (simp_all del:last.simps)
― ‹5 subgoals left›
apply(simp add:comm_def)
― ‹4 subgoals left›
apply(rule etran_in_comm)
apply(erule mp)
apply(erule tl_of_assum_in_assum,simp)
― ‹While-None›
apply(ind_cases "((Some (While b P), s), None, t) ∈ ctran" for s t)
apply(simp add:comm_def)
apply(simp add:cptn_iff_cptn_mod [THEN sym])
apply(rule conjI,clarify)
 apply(force simp add:assum_def)
apply clarify
apply(rule conjI, clarify)
 apply(case_tac i,simp,simp)
 apply(force simp add:not_ctran_None2)
apply(subgoal_tac "∀i. Suc i < length ((None, t) # xs) ⟶ (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)∈ etran")
 prefer 2
 apply clarify
 apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
 apply(erule not_ctran_None2,simp)
 apply simp+
apply(frule_tac j="0" and k="length ((None, s) # xs) - 1" and p=post in stability,simp+)
   apply(force simp add:assum_def subsetD)
  apply(simp add:assum_def)
  apply clarify
  apply(erule_tac x="i" in allE,simp)
  apply(erule_tac x="Suc i" in allE,simp)
 apply simp
apply clarify
apply (simp add:last_length)
― ‹WhileOne›
apply(rule ctran_in_comm,simp)
apply(simp add:Cons_lift del:list.map)
apply(simp add:comm_def del:list.map)
apply(rule conjI)
 apply clarify
 apply(case_tac "fst(((Some P, sa) # xs) ! i)")
  apply(case_tac "((Some P, sa) # xs) ! i")
  apply (simp add:lift_def)
  apply(ind_cases "(Some (While b P), ba) -c→ t" for ba t)
   apply simp
  apply simp
 apply(simp add:snd_lift del:list.map)
 apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
 apply(erule_tac x=sa in allE)
 apply(drule_tac c="(Some P, sa) # xs" in subsetD)
  apply (simp add:assum_def del:list.map)
  apply clarify
  apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:list.map)
  apply(erule mp)
  apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
   apply(erule etranE,simp add:lift_def)
   apply(rule Env)
  apply(erule etranE,simp add:lift_def)
  apply(rule Env)
 apply (simp add:comm_def del:list.map)
 apply clarify
 apply(erule allE,erule impE,assumption)
 apply(erule mp)
 apply(case_tac "((Some P, sa) # xs) ! i")
 apply(case_tac "xs!i")
 apply(simp add:lift_def)
 apply(case_tac "fst(xs!i)")
  apply force
 apply force
― ‹last=None›
apply clarify
apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))≠[]")
 apply(drule last_conv_nth)
 apply (simp del:list.map)
 apply(simp only:last_lift_not_None)
apply simp
― ‹WhileMore›
apply(rule ctran_in_comm,simp del:last.simps)
― ‹metiendo la hipotesis antes de dividir la conclusion.›
apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys ∈ assum (pre, rely)")
 apply (simp del:last.simps)
 prefer 2
 apply(erule assum_after_body)
  apply (simp del:last.simps)+
― ‹lo de antes.›
apply(simp add:comm_def del:list.map last.simps)
apply(rule conjI)
 apply clarify
 apply(simp only:Cons_lift_append)
 apply(case_tac "i<length xs")
  apply(simp add:nth_append del:list.map last.simps)
  apply(case_tac "fst(((Some P, sa) # xs) ! i)")
   apply(case_tac "((Some P, sa) # xs) ! i")
   apply (simp add:lift_def del:last.simps)
   apply(ind_cases "(Some (While b P), ba) -c→ t" for ba t)
    apply simp
   apply simp
  apply(simp add:snd_lift del:list.map last.simps)
  apply(thin_tac " ∀i. i < length ys ⟶ P i" for P)
  apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
  apply(erule_tac x=sa in allE)
  apply(drule_tac c="(Some P, sa) # xs" in subsetD)
   apply (simp add:assum_def del:list.map last.simps)
   apply clarify
   apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:list.map last.simps, erule mp)
   apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
    apply(erule etranE,simp add:lift_def)
    apply(rule Env)
   apply(erule etranE,simp add:lift_def)
   apply(rule Env)
  apply (simp add:comm_def del:list.map)
  apply clarify
  apply(erule allE,erule impE,assumption)
  apply(erule mp)
  apply(case_tac "((Some P, sa) # xs) ! i")
  apply(case_tac "xs!i")
  apply(simp add:lift_def)
  apply(case_tac "fst(xs!i)")
   apply force
 apply force
― ‹‹i ≥ length xs››
apply(subgoal_tac "i-length xs <length ys")
 prefer 2
 apply arith
apply(erule_tac x="i-length xs" in allE,clarify)
apply(case_tac "i=length xs")
 apply (simp add:nth_append snd_lift del:list.map last.simps)
 apply(simp add:last_length del:last.simps)
 apply(erule mp)
 apply(case_tac "last((Some P, sa) # xs)")
 apply(simp add:lift_def del:last.simps)
― ‹‹i>length xs››
apply(case_tac "i-length xs")
 apply arith
apply(simp add:nth_append del:list.map last.simps)
apply(rotate_tac -3)
apply(subgoal_tac "i- Suc (length xs)=nat")
 prefer 2
 apply arith
apply simp
― ‹last=None›
apply clarify
apply(case_tac ys)
 apply(simp add:Cons_lift del:list.map last.simps)
 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))≠[]")
  apply(drule last_conv_nth)
  apply (simp del:list.map)
  apply(simp only:last_lift_not_None)
 apply simp
apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)≠[]")
 apply(drule last_conv_nth)
 apply (simp del:list.map last.simps)
 apply(simp add:nth_append del:last.simps)
 apply(rename_tac a list)
 apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)≠[]")
  apply(drule last_conv_nth)
  apply (simp del:list.map last.simps)
 apply simp
apply simp
done

lemma While_sound:
  "⟦stable pre rely; pre ∩ - b ⊆ post; stable post rely;
    ⊨ P sat [pre ∩ b, rely, guar, pre]; ∀s. (s,s)∈guar⟧
  ⟹ ⊨ While b P sat [pre, rely, guar, post]"
apply(unfold com_validity_def)
apply clarify
apply(erule_tac xs="tl x" in While_sound_aux)
 apply(simp add:com_validity_def)
 apply force
 apply simp_all
apply(simp add:cptn_iff_cptn_mod cp_def)
apply(simp add:cp_def)
apply clarify
apply(rule nth_equalityI)
 apply simp_all
 apply(case_tac x,simp+)
apply(case_tac i,simp+)
apply(case_tac x,simp+)
done

subsubsection‹Soundness of the Rule of Consequence›

lemma Conseq_sound:
  "⟦pre ⊆ pre'; rely ⊆ rely'; guar' ⊆ guar; post' ⊆ post;
  ⊨ P sat [pre', rely', guar', post']⟧
  ⟹ ⊨ P sat [pre, rely, guar, post]"
apply(simp add:com_validity_def assum_def comm_def)
apply clarify
apply(erule_tac x=s in allE)
apply(drule_tac c=x in subsetD)
 apply force
apply force
done

subsubsection ‹Soundness of the system for sequential component programs›

theorem rgsound:
  "⊢ P sat [pre, rely, guar, post] ⟹ ⊨ P sat [pre, rely, guar, post]"
apply(erule rghoare.induct)
 apply(force elim:Basic_sound)
 apply(force elim:Seq_sound)
 apply(force elim:Cond_sound)
 apply(force elim:While_sound)
 apply(force elim:Await_sound)
apply(erule Conseq_sound,simp+)
done

subsection ‹Soundness of the System for Parallel Programs›

definition ParallelCom :: "('a rgformula) list ⇒ 'a par_com" where
  "ParallelCom Ps ≡ map (Some ∘ fst) Ps"

lemma two:
  "⟦ ∀i<length xs. rely ∪ (⋃j∈{j. j < length xs ∧ j ≠ i}. Guar (xs ! j))
     ⊆ Rely (xs ! i);
   pre ⊆ (⋂i∈{i. i < length xs}. Pre (xs ! i));
   ∀i<length xs.
   ⊨ Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   length xs=length clist; x ∈ par_cp (ParallelCom xs) s; x∈par_assum(pre, rely);
  ∀i<length clist. clist!i∈cp (Some(Com(xs!i))) s; x ∝ clist ⟧
  ⟹ ∀j i. i<length clist ∧ Suc j<length x ⟶ (clist!i!j) -c→ (clist!i!Suc j)
  ⟶ (snd(clist!i!j), snd(clist!i!Suc j)) ∈ Guar(xs!i)"
apply(unfold par_cp_def)
apply (rule ccontr)
― ‹By contradiction:›
apply simp
apply(erule exE)
― ‹the first c-tran that does not satisfy the guarantee-condition is from ‹σ_i› at step ‹m›.›
apply(drule_tac n=j and P="λj. ∃i. H i j" for H in Ex_first_occurrence)
apply(erule exE)
apply clarify
― ‹‹σ_i ∈ A(pre, rely_1)››
apply(subgoal_tac "take (Suc (Suc m)) (clist!i) ∈ assum(Pre(xs!i), Rely(xs!i))")
― ‹but this contradicts ‹⊨ σ_i sat [pre_i,rely_i,guar_i,post_i]››
 apply(erule_tac x=i and P="λi. H i ⟶ ⊨ (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
 apply(simp add:com_validity_def)
 apply(erule_tac x=s in allE)
 apply(simp add:cp_def comm_def)
 apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD)
  apply simp
  apply (blast intro: takecptn_is_cptn)
 apply simp
 apply clarify
 apply(erule_tac x=m and P="λj. I j ∧ J j ⟶ H j" for I J H in allE)
 apply (simp add:conjoin_def same_length_def)
apply(simp add:assum_def)
apply(rule conjI)
 apply(erule_tac x=i and P="λj. H j ⟶ I j ∈cp (K j) (J j)" for H I K J in allE)
 apply(simp add:cp_def par_assum_def)
 apply(drule_tac c="s" in subsetD,simp)
 apply simp
apply clarify
apply(erule_tac x=i and P="λj. H j ⟶ M ∪ ⋃((T j) ` (S j)) ⊆ (L j)" for H M S T L in allE)
apply simp
apply(erule subsetD)
apply simp
apply(simp add:conjoin_def compat_label_def)
apply clarify
apply(erule_tac x=ia and P="λj. H j ⟶ (P j) ∨ Q j" for H P Q in allE,simp)
― ‹each etran in ‹σ_1[0…m]› corresponds to›
apply(erule disjE)
― ‹a c-tran in some ‹σ_{ib}››
 apply clarify
 apply(case_tac "i=ib",simp)
  apply(erule etranE,simp)
 apply(erule_tac x="ib" and P="λi. H i ⟶ (I i) ∨ (J i)" for H I J in allE)
 apply (erule etranE)
 apply(case_tac "ia=m",simp)
 apply simp
 apply(erule_tac x=ia and P="λj. H j ⟶ (∀i. P i j)" for H P in allE)
 apply(subgoal_tac "ia<m",simp)
  prefer 2
  apply arith
 apply(erule_tac x=ib and P="λj. (I j, H j) ∈ ctran ⟶ P i j" for I H P in allE,simp)
 apply(simp add:same_state_def)
 apply(erule_tac x=i and P="λj. (T j) ⟶ (∀i. (H j i) ⟶ (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE)
 apply(erule_tac x=ib and P="λj. (T j) ⟶ (∀i. (H j i) ⟶ (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
― ‹or an e-tran in ‹σ›,
therefore it satisfies ‹rely ∨ guar_{ib}››
apply (force simp add:par_assum_def same_state_def)
done


lemma three [rule_format]:
  "⟦ xs≠[]; ∀i<length xs. rely ∪ (⋃j∈{j. j < length xs ∧ j ≠ i}. Guar (xs ! j))
   ⊆ Rely (xs ! i);
   pre ⊆ (⋂i∈{i. i < length xs}. Pre (xs ! i));
   ∀i<length xs.
    ⊨ Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   length xs=length clist; x ∈ par_cp (ParallelCom xs) s; x ∈ par_assum(pre, rely);
  ∀i<length clist. clist!i∈cp (Some(Com(xs!i))) s; x ∝ clist ⟧
  ⟹ ∀j i. i<length clist ∧ Suc j<length x ⟶ (clist!i!j) -e→ (clist!i!Suc j)
  ⟶ (snd(clist!i!j), snd(clist!i!Suc j)) ∈ rely ∪ (⋃j∈{j. j < length xs ∧ j ≠ i}. Guar (xs ! j))"
apply(drule two)
 apply simp_all
apply clarify
apply(simp add:conjoin_def compat_label_def)
apply clarify
apply(erule_tac x=j and P="λj. H j ⟶ (J j ∧ (∃i. P i j)) ∨ I j" for H J P I in allE,simp)
apply(erule disjE)
 prefer 2
 apply(force simp add:same_state_def par_assum_def)
apply clarify
apply(case_tac "i=ia",simp)
 apply(erule etranE,simp)
apply(erule_tac x="ia" and P="λi. H i ⟶ (I i) ∨ (J i)" for H I J in allE,simp)
apply(erule_tac x=j and P="λj. ∀i. S j i ⟶ (I j i, H j i) ∈ ctran ⟶ P i j" for S I H P in allE)
apply(erule_tac x=ia and P="λj. S j ⟶ (I j, H j) ∈ ctran ⟶ P j" for S I H P in allE)
apply(simp add:same_state_def)
apply(erule_tac x=i and P="λj. T j ⟶ (∀i. H j i ⟶ (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE)
apply(erule_tac x=ia and P="λj. T j ⟶ (∀i. H j i ⟶ (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
done

lemma four:
  "⟦xs≠[]; ∀i < length xs. rely ∪ (⋃j∈{j. j < length xs ∧ j ≠ i}. Guar (xs ! j))
    ⊆ Rely (xs ! i);
   (⋃j∈{j. j < length xs}. Guar (xs ! j)) ⊆ guar;
   pre ⊆ (⋂i∈{i. i < length xs}. Pre (xs ! i));
   ∀i < length xs.
    ⊨ Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   x ∈ par_cp (ParallelCom xs) s; x ∈ par_assum (pre, rely); Suc i < length x;
   x ! i -pc→ x ! Suc i⟧
  ⟹ (snd (x ! i), snd (x ! Suc i)) ∈ guar"
apply(simp add: ParallelCom_def)
apply(subgoal_tac "(map (Some ∘ fst) xs)≠[]")
 prefer 2
 apply simp
apply(frule rev_subsetD)
 apply(erule one [THEN equalityD1])
apply(erule subsetD)
apply simp
apply clarify
apply(drule_tac pre=pre and rely=rely and  x=x and s=s and xs=xs and clist=clist in two)
apply(assumption+)
     apply(erule sym)
    apply(simp add:ParallelCom_def)
   apply assumption
  apply(simp add:Com_def)
 apply assumption
apply(simp add:conjoin_def same_program_def)
apply clarify
apply(erule_tac x=i and P="λj. H j ⟶ fst(I j)=(J j)" for H I J in all_dupE)
apply(erule_tac x="Suc i" and P="λj. H j ⟶ fst(I j)=(J j)" for H I J in allE)
apply(erule par_ctranE,simp)
apply(erule_tac x=i and P="λj. ∀i. S j i ⟶ (I j i, H j i) ∈ ctran ⟶ P i j" for S I H P in allE)
apply(erule_tac x=ia and P="λj. S j ⟶ (I j, H j) ∈ ctran ⟶ P j" for S I H P in allE)
apply(rule_tac x=ia in exI)
apply(simp add:same_state_def)
apply(erule_tac x=ia and P="λj. T j ⟶ (∀i. H j i ⟶ (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE,simp)
apply(erule_tac x=ia and P="λj. T j ⟶ (∀i. H j i ⟶ (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
apply(erule_tac x=i and P="λj. H j ⟶ (snd (d j))=(snd (e j))" for H d e in all_dupE)
apply(erule_tac x=i and P="λj. H j ⟶ (snd (d j))=(snd (e j))" for H d e in all_dupE,simp)
apply(erule_tac x="Suc i" and P="λj. H j ⟶ (snd (d j))=(snd (e j))" for H d e in allE,simp)
apply(erule mp)
apply(subgoal_tac "r=fst(clist ! ia ! Suc i)",simp)
apply(drule_tac i=ia in list_eq_if)
back
apply simp_all
done

lemma parcptn_not_empty [simp]:"[] ∉ par_cptn"
apply(force elim:par_cptn.cases)
done

lemma five:
  "⟦xs≠[]; ∀i<length xs. rely ∪ (⋃j∈{j. j < length xs ∧ j ≠ i}. Guar (xs ! j))
   ⊆ Rely (xs ! i);
   pre ⊆ (⋂i∈{i. i < length xs}. Pre (xs ! i));
   (⋂i∈{i. i < length xs}. Post (xs ! i)) ⊆ post;
   ∀i < length xs.
    ⊨ Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
    x ∈ par_cp (ParallelCom xs) s; x ∈ par_assum (pre, rely);
   All_None (fst (last x)) ⟧ ⟹ snd (last x) ∈ post"
apply(simp add: ParallelCom_def)
apply(subgoal_tac "(map (Some ∘ fst) xs)≠[]")
 prefer 2
 apply simp
apply(frule rev_subsetD)
 apply(erule one [THEN equalityD1])
apply(erule subsetD)
apply simp
apply clarify
apply(subgoal_tac "∀i<length clist. clist!i∈assum(Pre(xs!i), Rely(xs!i))")
 apply(erule_tac x=xa and P="λi. H i ⟶ ⊨ (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
 apply(simp add:com_validity_def)
 apply(erule_tac x=s in allE)
 apply(erule_tac x=xa and P="λj. H j ⟶ (I j) ∈ cp (J j) s" for H I J in allE,simp)
 apply(drule_tac c="clist!xa" in subsetD)
  apply (force simp add:Com_def)
 apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
 apply clarify
 apply(erule_tac x="length x - 1" and P="λj. H j ⟶ fst(I j)=(J j)" for H I J in allE)
 apply (simp add:All_None_def same_length_def)
 apply(erule_tac x=xa and P="λj. H j ⟶ length(J j)=(K j)" for H J K in allE)
 apply(subgoal_tac "length x - 1 < length x",simp)
  apply(case_tac "x≠[]")
   apply(simp add: last_conv_nth)
   apply(erule_tac x="clist!xa" in ballE)
    apply(simp add:same_state_def)
    apply(subgoal_tac "clist!xa≠[]")
     apply(simp add: last_conv_nth)
    apply(case_tac x)
     apply (force simp add:par_cp_def)
    apply (force simp add:par_cp_def)
   apply force
  apply (force simp add:par_cp_def)
 apply(case_tac x)
  apply (force simp add:par_cp_def)
 apply (force simp add:par_cp_def)
apply clarify
apply(simp add:assum_def)
apply(rule conjI)
 apply(simp add:conjoin_def same_state_def par_cp_def)
 apply clarify
 apply(erule_tac x=i and P="λj. T j ⟶ (∀i. H j i ⟶ (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
 apply(erule_tac x=0 and P="λj. H j ⟶ (snd (d j))=(snd (e j))" for H d e in allE)
 apply(case_tac x,simp+)
 apply (simp add:par_assum_def)
 apply clarify
 apply(drule_tac c="snd (clist ! i ! 0)" in subsetD)
 apply assumption
 apply simp
apply clarify
apply(erule_tac x=i in all_dupE)
apply(rule subsetD, erule mp, assumption)
apply(erule_tac pre=pre and rely=rely and x=x and s=s in  three)
 apply(erule_tac x=ib in allE,erule mp)
 apply simp_all
 apply(simp add:ParallelCom_def)
 apply(force simp add:Com_def)
apply(simp add:conjoin_def same_length_def)
done

lemma ParallelEmpty [rule_format]:
  "∀i s. x ∈ par_cp (ParallelCom []) s ⟶
  Suc i < length x ⟶ (x ! i, x ! Suc i) ∉ par_ctran"
apply(induct_tac x)
 apply(simp add:par_cp_def ParallelCom_def)
apply clarify
apply(case_tac list,simp,simp)
apply(case_tac i)
 apply(simp add:par_cp_def ParallelCom_def)
 apply(erule par_ctranE,simp)
apply(simp add:par_cp_def ParallelCom_def)
apply clarify
apply(erule par_cptn.cases,simp)
 apply simp
apply(erule par_ctranE)
back
apply simp
done

theorem par_rgsound:
  "⊢ c SAT [pre, rely, guar, post] ⟹
   ⊨ (ParallelCom c) SAT [pre, rely, guar, post]"
apply(erule par_rghoare.induct)
apply(case_tac xs,simp)
 apply(simp add:par_com_validity_def par_comm_def)
 apply clarify
 apply(case_tac "post=UNIV",simp)
  apply clarify
  apply(drule ParallelEmpty)
   apply assumption
  apply simp
 apply clarify
 apply simp
apply(subgoal_tac "xs≠[]")
 prefer 2
 apply simp
apply(rename_tac a list)
apply(thin_tac "xs = a # list")
apply(simp add:par_com_validity_def par_comm_def)
apply clarify
apply(rule conjI)
 apply clarify
 apply(erule_tac pre=pre and rely=rely and guar=guar and x=x and s=s and xs=xs in four)
        apply(assumption+)
     apply clarify
     apply (erule allE, erule impE, assumption,erule rgsound)
    apply(assumption+)
apply clarify
apply(erule_tac pre=pre and rely=rely and post=post and x=x and s=s and xs=xs in five)
      apply(assumption+)
   apply clarify
   apply (erule allE, erule impE, assumption,erule rgsound)
  apply(assumption+)
done

end