Quelle RG_Hoare.thy Sprache: Isabelle

section \<open>The Proof System\<close>

theory RG_Hoare imports RG_Tran begin

subsection \<open>Proof System for Component Programs\<close>

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"
    (\<open>\<turnstile> _ sat [_, _, _, _]\<close> [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 \<rbrakk>
           \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"

| Seq: "\ \ P sat [pre, rely, guar, mid]; \ Q sat [mid, rely, guar, post] \
           \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"

| Cond: "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post];
           \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
          \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"

| While: "\ stable pre rely; (pre \ -b) \ post; stable post rely;
            \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
          \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"

| Await: "\ stable pre rely; stable post rely;
            \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t},
                UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
           \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"

| Conseq: "\ pre \ pre'; rely \ rely'; guar' \ guar; post' \ post;
             \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
            \<Longrightarrow> \<turnstile> 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 \<open>Proof System for Parallel Programs\<close>

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"
    (\<open>\<turnstile> _ SAT [_, _, _, _]\<close> [60,0,0,0,0] 45)
where
  Parallel:
  "\ \i (\j\{j. j j\i}. Guar(xs!j)) \ Rely(xs!i);
    (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
     pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i));
    (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post;
    \<forall>i<length xs. \<turnstile> Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] \<rbrakk>
   \<Longrightarrow>  \<turnstile> xs SAT [pre, rely, guar, post]"

section \<open>Soundness\<close>

subsubsection \<open>Some previous lemmas\<close>

lemma tl_of_assum_in_assum:
  "(P, s) # (P, t) # xs \ assum (pre, rely) \ stable pre rely
  \<Longrightarrow> (P, t) # xs \<in> 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)\
  \<Longrightarrow> (P, s) # (Q, s) # xs \<in> 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 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 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 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
   \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m
   \<longrightarrow> x!i -e\<rightarrow> 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 x\cptn \ (x!i -c\ x!Suc i \ \ x!i -e\ x!Suc i)
  \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> 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 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 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 \ \ ((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 P i))"
apply(rule nat_less_induct)
apply clarify
apply(case_tac "\m. m \ P m")
apply auto
done

lemma stability [rule_format]:
  "\j k. x \ cptn \ stable p rely \ j\k \ k snd(x!j)\p \
  (\<forall>i. (Suc i)<length x \<longrightarrow>
          (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow>
  (\<forall>i. j\<le>i \<and> i<k \<longrightarrow> x!i -e\<rightarrow> x!Suc i) \<longrightarrow> snd(x!k)\<in>p \<and> 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 \<open>Soundness of the System for Component Programs\<close>

subsubsection \<open>Soundness of the Basic rule\<close>

lemma unique_ctran_Basic [rule_format]:
  "\s i. x \ cptn \ x ! 0 = (Some (Basic f), s) \
  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow>
  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> 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)
  \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> 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\<rbrakk>
  \<Longrightarrow> \<Turnstile> 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\<open>Soundness of the Await rule\<close>

lemma unique_ctran_Await [rule_format]:
  "\s i. x \ cptn \ x ! 0 = (Some (Await b c), s) \
  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow>
  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> 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)
  \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> 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)
  \<and> (\<forall>i. Suc i<length l \<longrightarrow> l!i -c\<rightarrow> 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;
  \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t},
                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and>
  \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t},
                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
  \<Longrightarrow> \<Turnstile> 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)
\<comment> \<open>here starts the different part.\<close>
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\<open>Soundness of the Conditional rule\<close>

lemma Cond_sound:
  "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post];
  \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
  \<Longrightarrow> \<Turnstile> (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 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\<open>Soundness of the Sequential rule\<close>

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)
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) \
  (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow>
  (\<exists>xs\<in> 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
  \<longrightarrow> fst(x!i)=Some Q \<longrightarrow>
  (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
  (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i
   \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> 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 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))) \<noteq> 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)
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]\
  \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
apply(unfold com_validity_def)
apply clarify
apply(case_tac "\i
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
\<comment> \<open>\<open>\<exists>i<length x. fst (x ! i) = Some Q\<close>\<close>
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,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\<open>Soundness of the While rule\<close>

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 \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b;
  (Some (While b P), s) # (Some (Seq P (While b P)), s) #
   map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
  \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> 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 \<in> cptn_mod \<rbrakk>
  \<Longrightarrow>  \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"
  supply [[simproc del: defined_all]]
apply(erule cptn_mod.induct)
apply safe
apply (simp_all del:last.simps)
\<comment> \<open>5 subgoals left\<close>
apply(simp add:comm_def)
\<comment> \<open>4 subgoals left\<close>
apply(rule etran_in_comm)
apply(erule mp)
apply(erule tl_of_assum_in_assum,simp)
\<comment> \<open>While-None\<close>
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)
\<comment> \<open>WhileOne\<close>
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
\<comment> \<open>last=None\<close>
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
\<comment> \<open>WhileMore\<close>
apply(rule ctran_in_comm,simp del:last.simps)
\<comment> \<open>metiendo la hipotesis antes de dividir la conclusion.\<close>
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)+
\<comment> \<open>lo de antes.\<close>
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)
  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
\<comment> \<open>\<open>i \<ge> length xs\<close>\<close>
apply(subgoal_tac "i-length xs )
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)
\<comment> \<open>\<open>i>length xs\<close>\<close>
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
\<comment> \<open>last=None\<close>
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;
    \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
  \<Longrightarrow> \<Turnstile> 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\<open>Soundness of the Rule of Consequence\<close>

lemma Conseq_sound:
  "\pre \ pre'; rely \ rely'; guar' \ guar; post' \ post;
  \<Turnstile> P sat [pre', rely', guar', post']\<rbrakk>
  \<Longrightarrow> \<Turnstile> 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 \<open>Soundness of the system for sequential component programs\<close>

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 \<open>Soundness of the System for Parallel Programs\<close>

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

lemma two:
  "\ \i (\j\{j. j < length xs \ j \ i}. Guar (xs ! j))
     \<subseteq> Rely (xs ! i);
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   \<forall>i<length xs.
   \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
  \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
  \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j)
  \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
apply(unfold par_cp_def)
apply (rule ccontr)
\<comment> \<open>By contradiction:\<close>
apply simp
apply(erule exE)
\<comment> \<open>the first c-tran that does not satisfy the guarantee-condition is from \<open>\<sigma>_i\<close> at step \<open>m\<close>.\<close>
apply(drule_tac n=j and P="\j. \i. H i j" for H in Ex_first_occurrence)
apply(erule exE)
apply clarify
\<comment> \<open>\<open>\<sigma>_i \<in> A(pre, rely_1)\<close>\<close>
apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \ assum(Pre(xs!i), Rely(xs!i))")
\<comment> \<open>but this contradicts \<open>\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]\<close>\<close>
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)
\<comment> \<open>each etran in \<open>\<sigma>_1[0\<dots>m]\<close> corresponds to\<close>
apply(erule disjE)
\<comment> \<open>a c-tran in some \<open>\<sigma>_{ib}\<close>\<close>
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,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)
\<comment> \<open>or an e-tran in \<open>\<sigma>\<close>,
therefore it satisfies \<open>rely \<or> guar_{ib}\<close>\<close>
apply (force simp add:par_assum_def same_state_def)
done

lemma three [rule_format]:
  "\ xs\[]; \i (\j\{j. j < length xs \ j \ i}. Guar (xs ! j))
   \<subseteq> Rely (xs ! i);
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   \<forall>i<length xs.
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum(pre, rely);
  \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
  \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -e\<rightarrow> (clist!i!Suc j)
  \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> 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))
    \<subseteq> Rely (xs ! i);
   (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar;
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   \<forall>i < length xs.
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x;
   x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
  \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> 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 (\j\{j. j < length xs \ j \ i}. Guar (xs ! j))
   \<subseteq> Rely (xs ! i);
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
   \<forall>i < length xs.
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
    x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely);
   All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> 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 "\iassum(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 \<longrightarrow> (x ! i, x ! Suc i) \<notin> 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] \
   \<Turnstile> (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

quality100%

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.