Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HoareParallel/RG_Hoare.thy
changeset 23746 a455e69c31cc
parent 20432 07ec57376051
equal deleted inserted replaced
23745:28df61d931e2 23746:a455e69c31cc 
     9 
     9 
    10 constdefs
 
    10 constdefs
 
    11   stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
    11   stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
    12   "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" 
    12   "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" 
    13 
    13 
    14 consts rghoare :: "('a rgformula) set" 
    14 inductive
 
    15 syntax 
    15   rghoare :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"  
    16   "_rghoare" :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"  
    16     ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
 
    17                 ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
 
    17 where
 
    18 translations 
       
    19   "\<turnstile> P sat [pre, rely, guar, post]" \<rightleftharpoons> "(P, pre, rely, guar, post) \<in> rghoare"
 
       
    20 
       
    21 inductive rghoare
 
       
    22 intros
 
       
    23   Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar; 
    18   Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar; 
    24             stable pre rely; stable post rely \<rbrakk> 
    19             stable pre rely; stable post rely \<rbrakk> 
    25            \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
 
    20            \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
 
    26 
    21 
    27   Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk> 
    22 | Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk> 
    28            \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"
 
    23            \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"
 
    29 
    24 
    30   Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
 
    25 | Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
 
    31            \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
 
    26            \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
 
    32           \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"
 
    27           \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"
 
    33 
    28 
    34   While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
 
    29 | While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
 
    35             \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
 
    30             \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
 
    36           \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
 
    31           \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
 
    37 
    32 
    38   Await: "\<lbrakk> stable pre rely; stable post rely; 
    33 | Await: "\<lbrakk> stable pre rely; stable post rely; 
    39             \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, 
    34             \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, 
    40                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
 
    35                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
 
    41            \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
 
    36            \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
 
    42   
    37   
    43   Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
 
    38 | Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
 
    44              \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
 
    39              \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
 
    45             \<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]"
 
    40             \<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]"
 
    46 
    41 
    47 constdefs 
    42 constdefs 
    48   Pre :: "'a rgformula \<Rightarrow> 'a set"
 
    43   Pre :: "'a rgformula \<Rightarrow> 'a set"
 
    58 
    53 
    59 subsection {* Proof System for Parallel Programs *}
 
    54 subsection {* Proof System for Parallel Programs *}
 
    60 
    55 
    61 types 'a par_rgformula = "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
 
    56 types 'a par_rgformula = "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
 
    62 
    57 
    63 consts par_rghoare :: "('a par_rgformula) set" 
    58 inductive
 
    64 syntax 
    59   par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
 
    65   "_par_rghoare" :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"    ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
 
    60     ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
 
    66 translations 
    61 where
 
    67   "\<turnstile> Ps SAT [pre, rely, guar, post]" \<rightleftharpoons> "(Ps, pre, rely, guar, post) \<in> par_rghoare"
 
       
    68 
       
    69 inductive par_rghoare
 
       
    70 intros
 
       
    71   Parallel: 
    62   Parallel: 
    72   "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j<length xs \<and> j\<noteq>i}. Guar(xs!j)) \<subseteq> Rely(xs!i);
 
    63   "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j<length xs \<and> j\<noteq>i}. Guar(xs!j)) \<subseteq> Rely(xs!i);
 
    73     (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
 
    64     (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
 
    74      pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i)); 
    65      pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i)); 
    75     (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post;
 
    66     (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post;
 
   111 done
 
   102 done
 
   112 
   103 
   113 lemma takecptn_is_cptn [rule_format, elim!]: 
   104 lemma takecptn_is_cptn [rule_format, elim!]: 
   114   "\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn"
 
   105   "\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn"
 
   115 apply(induct "c")
 
   106 apply(induct "c")
 
   116  apply(force elim: cptn.elims)
 
   107  apply(force elim: cptn.cases)
 
   117 apply clarify
 
   108 apply clarify
 
   118 apply(case_tac j) 
   109 apply(case_tac j) 
   119  apply simp
 
   110  apply simp
 
   120  apply(rule CptnOne)
 
   111  apply(rule CptnOne)
 
   121 apply simp
 
   112 apply simp
 
   122 apply(force intro:cptn.intros elim:cptn.elims)
 
   113 apply(force intro:cptn.intros elim:cptn.cases)
 
   123 done
 
   114 done
 
   124 
   115 
   125 lemma dropcptn_is_cptn [rule_format,elim!]: 
   116 lemma dropcptn_is_cptn [rule_format,elim!]: 
   126   "\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn"
 
   117   "\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn"
 
   127 apply(induct "c")
 
   118 apply(induct "c")
 
   128  apply(force elim: cptn.elims)
 
   119  apply(force elim: cptn.cases)
 
   129 apply clarify
 
   120 apply clarify
 
   130 apply(case_tac j,simp+) 
   121 apply(case_tac j,simp+) 
   131 apply(erule cptn.elims)
 
   122 apply(erule cptn.cases)
 
   132   apply simp
 
   123   apply simp
 
   133  apply force
 
   124  apply force
 
   134 apply force
 
   125 apply force
 
   135 done
 
   126 done
 
   136 
   127 
   137 lemma takepar_cptn_is_par_cptn [rule_format,elim]: 
   128 lemma takepar_cptn_is_par_cptn [rule_format,elim]: 
   138   "\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn"
 
   129   "\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn"
 
   139 apply(induct "c")
 
   130 apply(induct "c")
 
   140  apply(force elim: cptn.elims)
 
   131  apply(force elim: cptn.cases)
 
   141 apply clarify
 
   132 apply clarify
 
   142 apply(case_tac j,simp) 
   133 apply(case_tac j,simp) 
   143  apply(rule ParCptnOne)
 
   134  apply(rule ParCptnOne)
 
   144 apply(force intro:par_cptn.intros elim:par_cptn.elims)
 
   135 apply(force intro:par_cptn.intros elim:par_cptn.cases)
 
   145 done
 
   136 done
 
   146 
   137 
   147 lemma droppar_cptn_is_par_cptn [rule_format]:
 
   138 lemma droppar_cptn_is_par_cptn [rule_format]:
 
   148   "\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn"
 
   139   "\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn"
 
   149 apply(induct "c")
 
   140 apply(induct "c")
 
   150  apply(force elim: par_cptn.elims)
 
   141  apply(force elim: par_cptn.cases)
 
   151 apply clarify
 
   142 apply clarify
 
   152 apply(case_tac j,simp+) 
   143 apply(case_tac j,simp+) 
   153 apply(erule par_cptn.elims)
 
   144 apply(erule par_cptn.cases)
 
   154   apply simp
 
   145   apply simp
 
   155  apply force
 
   146  apply force
 
   156 apply force
 
   147 apply force
 
   157 done
 
   148 done
 
   158 
   149 
   163 
   154 
   164 lemma not_ctran_None [rule_format]: 
   155 lemma not_ctran_None [rule_format]: 
   165   "\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)"
 
   156   "\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)"
 
   166 apply(induct xs,simp+)
 
   157 apply(induct xs,simp+)
 
   167 apply clarify
 
   158 apply clarify
 
   168 apply(erule cptn.elims,simp)
 
   159 apply(erule cptn.cases,simp)
 
   169  apply simp
 
   160  apply simp
 
   170  apply(case_tac i,simp)
 
   161  apply(case_tac i,simp)
 
   171   apply(rule Env)
 
   162   apply(rule Env)
 
   172  apply simp
 
   163  apply simp
 
   173 apply(force elim:ctran.elims)
 
   164 apply(force elim:ctran.cases)
 
   174 done
 
   165 done
 
   175 
   166 
   176 lemma cptn_not_empty [simp]:"[] \<notin> cptn"
 
   167 lemma cptn_not_empty [simp]:"[] \<notin> cptn"
 
   177 apply(force elim:cptn.elims)
 
   168 apply(force elim:cptn.cases)
 
   178 done
 
   169 done
 
   179 
   170 
   180 lemma etran_or_ctran [rule_format]: 
   171 lemma etran_or_ctran [rule_format]: 
   181   "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x 
   172   "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x 
   182    \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m 
   173    \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m 
   183    \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
 
   174    \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
 
   184 apply(induct x,simp)
 
   175 apply(induct x,simp)
 
   185 apply clarify
 
   176 apply clarify
 
   186 apply(erule cptn.elims,simp)
 
   177 apply(erule cptn.cases,simp)
 
   187  apply(case_tac i,simp)
 
   178  apply(case_tac i,simp)
 
   188   apply(rule Env)
 
   179   apply(rule Env)
 
   189  apply simp
 
   180  apply simp
 
   190  apply(erule_tac x="m - 1" in allE)
 
   181  apply(erule_tac x="m - 1" in allE)
 
   191  apply(case_tac m,simp,simp)
 
   182  apply(case_tac m,simp,simp)
 
   200   "\<forall>i. Suc i<length x \<longrightarrow> x\<in>cptn \<longrightarrow> (x!i -c\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i)
 
   191   "\<forall>i. Suc i<length x \<longrightarrow> x\<in>cptn \<longrightarrow> (x!i -c\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i)
 
   201   \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i)"
 
   192   \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i)"
 
   202 apply(induct x)
 
   193 apply(induct x)
 
   203  apply simp
 
   194  apply simp
 
   204 apply clarify
 
   195 apply clarify
 
   205 apply(erule cptn.elims,simp)
 
   196 apply(erule cptn.cases,simp)
 
   206  apply(case_tac i,simp+)
 
   197  apply(case_tac i,simp+)
 
   207 apply(case_tac i,simp)
 
   198 apply(case_tac i,simp)
 
   208  apply(force elim:etran.elims)
 
   199  apply(force elim:etran.cases)
 
   209 apply simp
 
   200 apply simp
 
   210 done
 
   201 done
 
   211 
   202 
   212 lemma etran_or_ctran2_disjI1: 
   203 lemma etran_or_ctran2_disjI1: 
   213   "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -c\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i"
 
   204   "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -c\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i"
 
   219 
   210 
   220 lemma not_ctran_None2 [rule_format]: 
   211 lemma not_ctran_None2 [rule_format]: 
   221   "\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i"
 
   212   "\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i"
 
   222 apply(frule not_ctran_None,simp)
 
   213 apply(frule not_ctran_None,simp)
 
   223 apply(case_tac i,simp)
 
   214 apply(case_tac i,simp)
 
   224  apply(force elim:etran.elims)
 
   215  apply(force elim:etranE)
 
   225 apply simp
 
   216 apply simp
 
   226 apply(rule etran_or_ctran2_disjI2,simp_all)
 
   217 apply(rule etran_or_ctran2_disjI2,simp_all)
 
   227 apply(force intro:tl_of_cptn_is_cptn)
 
   218 apply(force intro:tl_of_cptn_is_cptn)
 
   228 done
 
   219 done
 
   229 
   220 
   239   (\<forall>i. (Suc i)<length x \<longrightarrow> 
   230   (\<forall>i. (Suc i)<length x \<longrightarrow> 
   240           (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow> 
   231           (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow> 
   241   (\<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)"
 
   232   (\<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)"
 
   242 apply(induct x)
 
   233 apply(induct x)
 
   243  apply clarify
 
   234  apply clarify
 
   244  apply(force elim:cptn.elims)
 
   235  apply(force elim:cptn.cases)
 
   245 apply clarify
 
   236 apply clarify
 
   246 apply(erule cptn.elims,simp)
 
   237 apply(erule cptn.cases,simp)
 
   247  apply simp
 
   238  apply simp
 
   248  apply(case_tac k,simp,simp)
 
   239  apply(case_tac k,simp,simp)
 
   249  apply(case_tac j,simp) 
   240  apply(case_tac j,simp) 
   250   apply(erule_tac x=0 in allE)
 
   241   apply(erule_tac x=0 in allE)
 
   251   apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (?J j)" in allE,simp)
 
   242   apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (?J j)" in allE,simp)
 
   272  apply clarify
 
   263  apply clarify
 
   273  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
 
   264  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
 
   274 apply(case_tac k,simp,simp)
 
   265 apply(case_tac k,simp,simp)
 
   275 apply(case_tac j)
 
   266 apply(case_tac j)
 
   276  apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
 
   267  apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
 
   277  apply(erule etran.elims,simp)
 
   268  apply(erule etran.cases,simp)
 
   278 apply(erule_tac x="nata" in allE)
 
   269 apply(erule_tac x="nata" in allE)
 
   279 apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
 
   270 apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
 
   280 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((Q, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((Q, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
 
   271 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((Q, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((Q, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
 
   281  apply clarify
 
   272  apply clarify
 
   282  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
 
   273  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
 
   293   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
   284   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
   294   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
 
   285   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
 
   295 apply(induct x,simp)
 
   286 apply(induct x,simp)
 
   296 apply simp
 
   287 apply simp
 
   297 apply clarify
 
   288 apply clarify
 
   298 apply(erule cptn.elims,simp)
 
   289 apply(erule cptn.cases,simp)
 
   299  apply(case_tac i,simp+)
 
   290  apply(case_tac i,simp+)
 
   300  apply clarify
 
   291  apply clarify
 
   301  apply(case_tac j,simp)
 
   292  apply(case_tac j,simp)
 
   302   apply(rule Env)
 
   293   apply(rule Env)
 
   303  apply simp
 
   294  apply simp
 
   304 apply clarify
 
   295 apply clarify
 
   305 apply simp
 
   296 apply simp
 
   306 apply(case_tac i)
 
   297 apply(case_tac i)
 
   307  apply(case_tac j,simp,simp)
 
   298  apply(case_tac j,simp,simp)
 
   308  apply(erule ctran.elims,simp_all)
 
   299  apply(erule ctran.cases,simp_all)
 
   309  apply(force elim: not_ctran_None)
 
   300  apply(force elim: not_ctran_None)
 
   310 apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran")
 
   301 apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran" for sa Q t)
 
   311 apply simp
 
   302 apply simp
 
   312 apply(drule_tac i=nat in not_ctran_None,simp)
 
   303 apply(drule_tac i=nat in not_ctran_None,simp)
 
   313 apply(erule etran.elims,simp)
 
   304 apply(erule etranE,simp)
 
   314 done
 
   305 done
 
   315 
   306 
   316 lemma exists_ctran_Basic_None [rule_format]: 
   307 lemma exists_ctran_Basic_None [rule_format]: 
   317   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) 
   308   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) 
   318   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
 
   309   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
 
   319 apply(induct x,simp)
 
   310 apply(induct x,simp)
 
   320 apply simp
 
   311 apply simp
 
   321 apply clarify
 
   312 apply clarify
 
   322 apply(erule cptn.elims,simp)
 
   313 apply(erule cptn.cases,simp)
 
   323  apply(case_tac i,simp,simp)
 
   314  apply(case_tac i,simp,simp)
 
   324  apply(erule_tac x=nat in allE,simp)
 
   315  apply(erule_tac x=nat in allE,simp)
 
   325  apply clarify
 
   316  apply clarify
 
   326  apply(rule_tac x="Suc j" in exI,simp,simp)
 
   317  apply(rule_tac x="Suc j" in exI,simp,simp)
 
   327 apply clarify
 
   318 apply clarify
 
   347  apply(erule subsetD,simp)
 
   338  apply(erule subsetD,simp)
 
   348  apply(case_tac "x!i")
 
   339  apply(case_tac "x!i")
 
   349  apply clarify
 
   340  apply clarify
 
   350  apply(drule_tac s="Some (Basic f)" in sym,simp)
 
   341  apply(drule_tac s="Some (Basic f)" in sym,simp)
 
   351  apply(thin_tac "\<forall>j. ?H j")
 
   342  apply(thin_tac "\<forall>j. ?H j")
 
   352  apply(force elim:ctran.elims)
 
   343  apply(force elim:ctran.cases)
 
   353 apply clarify
 
   344 apply clarify
 
   354 apply(simp add:cp_def)
 
   345 apply(simp add:cp_def)
 
   355 apply clarify
 
   346 apply clarify
 
   356 apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+)
 
   347 apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+)
 
   357   apply(case_tac x,simp+)
 
   348   apply(case_tac x,simp+)
 
   366 apply(case_tac "x!j")
 
   357 apply(case_tac "x!j")
 
   367 apply clarify
 
   358 apply clarify
 
   368 apply simp
 
   359 apply simp
 
   369 apply(drule_tac s="Some (Basic f)" in sym,simp)
 
   360 apply(drule_tac s="Some (Basic f)" in sym,simp)
 
   370 apply(case_tac "x!Suc j",simp)
 
   361 apply(case_tac "x!Suc j",simp)
 
   371 apply(rule ctran.elims,simp)
 
   362 apply(rule ctran.cases,simp)
 
   372 apply(simp_all)
 
   363 apply(simp_all)
 
   373 apply(drule_tac c=sa in subsetD,simp)
 
   364 apply(drule_tac c=sa in subsetD,simp)
 
   374 apply clarify
 
   365 apply clarify
 
   375 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
 
   366 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
 
   376  apply(case_tac x,simp+)
 
   367  apply(case_tac x,simp+)
 
   387   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow> 
   378   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow> 
   388   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
   379   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
   389   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
 
   380   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
 
   390 apply(induct x,simp+)
 
   381 apply(induct x,simp+)
 
   391 apply clarify
 
   382 apply clarify
 
   392 apply(erule cptn.elims,simp)
 
   383 apply(erule cptn.cases,simp)
 
   393  apply(case_tac i,simp+)
 
   384  apply(case_tac i,simp+)
 
   394  apply clarify
 
   385  apply clarify
 
   395  apply(case_tac j,simp)
 
   386  apply(case_tac j,simp)
 
   396   apply(rule Env)
 
   387   apply(rule Env)
 
   397  apply simp
 
   388  apply simp
 
   398 apply clarify
 
   389 apply clarify
 
   399 apply simp
 
   390 apply simp
 
   400 apply(case_tac i)
 
   391 apply(case_tac i)
 
   401  apply(case_tac j,simp,simp)
 
   392  apply(case_tac j,simp,simp)
 
   402  apply(erule ctran.elims,simp_all)
 
   393  apply(erule ctran.cases,simp_all)
 
   403  apply(force elim: not_ctran_None)
 
   394  apply(force elim: not_ctran_None)
 
   404 apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran",simp)
 
   395 apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran" for sa Q t,simp)
 
   405 apply(drule_tac i=nat in not_ctran_None,simp)
 
   396 apply(drule_tac i=nat in not_ctran_None,simp)
 
   406 apply(erule etran.elims,simp)
 
   397 apply(erule etranE,simp)
 
   407 done
 
   398 done
 
   408 
   399 
   409 lemma exists_ctran_Await_None [rule_format]: 
   400 lemma exists_ctran_Await_None [rule_format]: 
   410   "\<forall>s i.  x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) 
   401   "\<forall>s i.  x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) 
   411   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
 
   402   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
 
   412 apply(induct x,simp+)
 
   403 apply(induct x,simp+)
 
   413 apply clarify
 
   404 apply clarify
 
   414 apply(erule cptn.elims,simp)
 
   405 apply(erule cptn.cases,simp)
 
   415  apply(case_tac i,simp+)
 
   406  apply(case_tac i,simp+)
 
   416  apply(erule_tac x=nat in allE,simp)
 
   407  apply(erule_tac x=nat in allE,simp)
 
   417  apply clarify
 
   408  apply clarify
 
   418  apply(rule_tac x="Suc j" in exI,simp,simp)
 
   409  apply(rule_tac x="Suc j" in exI,simp,simp)
 
   419 apply clarify
 
   410 apply clarify
 
   438 apply(case_tac i,simp)
 
   429 apply(case_tac i,simp)
 
   439 apply(simp add:cp_def)
 
   430 apply(simp add:cp_def)
 
   440 apply force
 
   431 apply force
 
   441 apply(simp add:cp_def)
 
   432 apply(simp add:cp_def)
 
   442  apply(case_tac l)
 
   433  apply(case_tac l)
 
   443  apply(force elim:cptn.elims)
 
   434  apply(force elim:cptn.cases)
 
   444 apply simp
 
   435 apply simp
 
   445 apply(erule CptnComp)
 
   436 apply(erule CptnComp)
 
   446 apply clarify
 
   437 apply clarify
 
   447 done
 
   438 done
 
   448  
   439  
   464    apply(erule_tac x=ia in allE,simp)
 
   455    apply(erule_tac x=ia in allE,simp)
 
   465   apply(subgoal_tac "x\<in> cp (Some(Await b P)) s")
 
   456   apply(subgoal_tac "x\<in> cp (Some(Await b P)) s")
 
   466   apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
 
   457   apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
 
   467   apply(simp add:cp_def)
 
   458   apply(simp add:cp_def)
 
   468 --{* here starts the different part. *}
 
   459 --{* here starts the different part. *}
 
   469  apply(erule ctran.elims,simp_all)
 
   460  apply(erule ctran.cases,simp_all)
 
   470  apply(drule Star_imp_cptn) 
   461  apply(drule Star_imp_cptn) 
   471  apply clarify
 
   462  apply clarify
 
   472  apply(erule_tac x=sa in allE)
 
   463  apply(erule_tac x=sa in allE)
 
   473  apply clarify
 
   464  apply clarify
 
   474  apply(erule_tac x=sa in allE)
 
   465  apply(erule_tac x=sa in allE)
 
   475  apply(drule_tac c=l in subsetD)
 
   466  apply(drule_tac c=l in subsetD)
 
   476   apply (simp add:cp_def)
 
   467   apply (simp add:cp_def)
 
   477   apply clarify
 
   468   apply clarify
 
   478   apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
 
   469   apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
 
   479   apply(erule etran.elims,simp)
 
   470   apply(erule etranE,simp)
 
   480  apply simp
 
   471  apply simp
 
   481 apply clarify
 
   472 apply clarify
 
   482 apply(simp add:cp_def)
 
   473 apply(simp add:cp_def)
 
   483 apply clarify
 
   474 apply clarify
 
   484 apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
 
   475 apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
 
   494 apply(case_tac "x!j")
 
   485 apply(case_tac "x!j")
 
   495 apply clarify
 
   486 apply clarify
 
   496 apply simp
 
   487 apply simp
 
   497 apply(drule_tac s="Some (Await b P)" in sym,simp)
 
   488 apply(drule_tac s="Some (Await b P)" in sym,simp)
 
   498 apply(case_tac "x!Suc j",simp)
 
   489 apply(case_tac "x!Suc j",simp)
 
   499 apply(rule ctran.elims,simp)
 
   490 apply(rule ctran.cases,simp)
 
   500 apply(simp_all)
 
   491 apply(simp_all)
 
   501 apply(drule Star_imp_cptn) 
   492 apply(drule Star_imp_cptn) 
   502 apply clarify
 
   493 apply clarify
 
   503 apply(erule_tac x=sa in allE)
 
   494 apply(erule_tac x=sa in allE)
 
   504 apply clarify
 
   495 apply clarify
 
   505 apply(erule_tac x=sa in allE)
 
   496 apply(erule_tac x=sa in allE)
 
   506 apply(drule_tac c=l in subsetD)
 
   497 apply(drule_tac c=l in subsetD)
 
   507  apply (simp add:cp_def)
 
   498  apply (simp add:cp_def)
 
   508  apply clarify
 
   499  apply clarify
 
   509  apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
 
   500  apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
 
   510  apply(erule etran.elims,simp)
 
   501  apply(erule etranE,simp)
 
   511 apply simp
 
   502 apply simp
 
   512 apply clarify
 
   503 apply clarify
 
   513 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
 
   504 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
 
   514  apply(case_tac x,simp+)
 
   505  apply(case_tac x,simp+)
 
   515  apply(erule_tac x=i in allE)
 
   506  apply(erule_tac x=i in allE)
 
   542 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
 
   533 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
 
   543 apply clarify
 
   534 apply clarify
 
   544 apply (simp add:assum_def)
 
   535 apply (simp add:assum_def)
 
   545 apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
 
   536 apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
 
   546  apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
 
   537  apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
 
   547 apply(erule ctran.elims,simp_all)
 
   538 apply(erule ctran.cases,simp_all)
 
   548  apply(erule_tac x="sa" in allE)
 
   539  apply(erule_tac x="sa" in allE)
 
   549  apply(drule_tac c="drop (Suc m) x" in subsetD)
 
   540  apply(drule_tac c="drop (Suc m) x" in subsetD)
 
   550   apply simp
 
   541   apply simp
 
   551   apply clarify
 
   542   apply clarify
 
   552  apply simp
 
   543  apply simp
 
   614     apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
 
   605     apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
 
   615     apply(rule conjI,erule CptnEnv)
 
   606     apply(rule conjI,erule CptnEnv)
 
   616     apply(simp (no_asm_use) add:lift_def)
 
   607     apply(simp (no_asm_use) add:lift_def)
 
   617    apply clarify
 
   608    apply clarify
 
   618    apply(erule_tac x="Suc i" in allE, simp)
 
   609    apply(erule_tac x="Suc i" in allE, simp)
 
   619   apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran")
 
   610   apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran" for Pa sa t)
 
   620  apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
 
   611  apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
 
   621 apply(erule_tac x="length xs" in allE, simp)
 
   612 apply(erule_tac x="length xs" in allE, simp)
 
   622 apply(simp only:Cons_lift_append)
 
   613 apply(simp only:Cons_lift_append)
 
   623 apply(subgoal_tac "length xs < length ((Some P, sa) # xs)")
 
   614 apply(subgoal_tac "length xs < length ((Some P, sa) # xs)")
 
   624  apply(simp only :nth_append length_map last_length nth_map)
 
   615  apply(simp only :nth_append length_map last_length nth_map)
 
   647  apply(case_tac xsa,simp,simp)
 
   638  apply(case_tac xsa,simp,simp)
 
   648  apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
 
   639  apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
 
   649  apply(rule conjI,erule CptnEnv)
 
   640  apply(rule conjI,erule CptnEnv)
 
   650  apply(simp (no_asm_use) add:lift_def)
 
   641  apply(simp (no_asm_use) add:lift_def)
 
   651  apply(rule_tac x=ys in exI,simp)
 
   642  apply(rule_tac x=ys in exI,simp)
 
   652 apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran")
 
   643 apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran" for Pa sa t)
 
   653  apply simp
 
   644  apply simp
 
   654  apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
 
   645  apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
 
   655  apply(rule conjI)
 
   646  apply(rule conjI)
 
   656   apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp)
 
   647   apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp)
 
   657  apply(case_tac i, simp+)
 
   648  apply(case_tac i, simp+)
 
   722   apply(simp add:assum_def)
 
   713   apply(simp add:assum_def)
 
   723   apply clarify
 
   714   apply clarify
 
   724   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
 
   715   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
 
   725   apply(simp add:snd_lift)
 
   716   apply(simp add:snd_lift)
 
   726   apply(erule mp)
 
   717   apply(erule mp)
 
   727   apply(force elim:etran.elims intro:Env simp add:lift_def)
 
   718   apply(force elim:etranE intro:Env simp add:lift_def)
 
   728  apply(simp add:comm_def)
 
   719  apply(simp add:comm_def)
 
   729  apply(rule conjI)
 
   720  apply(rule conjI)
 
   730   apply clarify
 
   721   apply clarify
 
   731   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
 
   722   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
 
   732   apply(simp add:snd_lift)
 
   723   apply(simp add:snd_lift)
 
   764  apply clarify
 
   755  apply clarify
 
   765  apply(erule_tac x=i in allE)
 
   756  apply(erule_tac x=i in allE)
 
   766   back 
   757   back 
   767  apply(simp add:snd_lift)
 
   758  apply(simp add:snd_lift)
 
   768  apply(erule mp)
 
   759  apply(erule mp)
 
   769  apply(force elim:etran.elims intro:Env simp add:lift_def)
 
   760  apply(force elim:etranE intro:Env simp add:lift_def)
 
   770 apply simp
 
   761 apply simp
 
   771 apply clarify
 
   762 apply clarify
 
   772 apply(erule_tac x="snd(xs!m)" in allE)
 
   763 apply(erule_tac x="snd(xs!m)" in allE)
 
   773 apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
 
   764 apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
 
   774  apply(case_tac "xs\<noteq>[]")
 
   765  apply(case_tac "xs\<noteq>[]")
 
   784  back
 
   775  back
 
   785  apply(case_tac ys,(simp add:nth_append)+)
 
   776  apply(case_tac ys,(simp add:nth_append)+)
 
   786  apply (case_tac i, (simp add:snd_lift)+)
 
   777  apply (case_tac i, (simp add:snd_lift)+)
 
   787   apply(erule mp)
 
   778   apply(erule mp)
 
   788   apply(case_tac "xs!m")
 
   779   apply(case_tac "xs!m")
 
   789   apply(force elim:etran.elims intro:Env simp add:lift_def)
 
   780   apply(force elim:etran.cases intro:Env simp add:lift_def)
 
   790  apply simp 
   781  apply simp 
   791 apply simp
 
   782 apply simp
 
   792 apply clarify
 
   783 apply clarify
 
   793 apply(rule conjI,clarify)
 
   784 apply(rule conjI,clarify)
 
   794  apply(case_tac "i<m",simp add:nth_append)
 
   785  apply(case_tac "i<m",simp add:nth_append)
 
   864  apply clarify
 
   855  apply clarify
 
   865  apply(erule_tac x="Suc i" in allE)
 
   856  apply(erule_tac x="Suc i" in allE)
 
   866  apply simp
 
   857  apply simp
 
   867  apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
 
   858  apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
 
   868  apply(erule mp)
 
   859  apply(erule mp)
 
   869  apply(erule etran.elims,simp)
 
   860  apply(erule etranE,simp)
 
   870  apply(case_tac "fst(((Some P, s) # xs) ! i)")
 
   861  apply(case_tac "fst(((Some P, s) # xs) ! i)")
 
   871   apply(force intro:Env simp add:lift_def)
 
   862   apply(force intro:Env simp add:lift_def)
 
   872  apply(force intro:Env simp add:lift_def)
 
   863  apply(force intro:Env simp add:lift_def)
 
   873 apply(rule conjI)
 
   864 apply(rule conjI)
 
   874  apply clarify
 
   865  apply clarify
 
   898 --{* 4 subgoals left *}
 
   889 --{* 4 subgoals left *}
 
   899 apply(rule etran_in_comm)
 
   890 apply(rule etran_in_comm)
 
   900 apply(erule mp)
 
   891 apply(erule mp)
 
   901 apply(erule tl_of_assum_in_assum,simp)
 
   892 apply(erule tl_of_assum_in_assum,simp)
 
   902 --{* While-None *}
 
   893 --{* While-None *}
 
   903 apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran")
 
   894 apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran" for s t)
 
   904 apply(simp add:comm_def)
 
   895 apply(simp add:comm_def)
 
   905 apply(simp add:cptn_iff_cptn_mod [THEN sym])
 
   896 apply(simp add:cptn_iff_cptn_mod [THEN sym])
 
   906 apply(rule conjI,clarify)
 
   897 apply(rule conjI,clarify)
 
   907  apply(force simp add:assum_def)
 
   898  apply(force simp add:assum_def)
 
   908 apply clarify
 
   899 apply clarify
 
   909 apply(rule conjI, clarify)
 
   900 apply(rule conjI, clarify)
 
   910  apply(case_tac i,simp,simp)
 
   901  apply(case_tac i,simp,simp)
 
   911  apply(force simp add:not_ctran_None2)
 
   902  apply(force simp add:not_ctran_None2)
 
   912 apply(subgoal_tac "\<forall>i. Suc i < length ((None, sa) # xs) \<longrightarrow> (((None, sa) # xs) ! i, ((None, sa) # xs) ! Suc i)\<in> etran")
 
   903 apply(subgoal_tac "\<forall>i. Suc i < length ((None, t) # xs) \<longrightarrow> (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\<in> etran")
 
   913  prefer 2
 
   904  prefer 2
 
   914  apply clarify
 
   905  apply clarify
 
   915  apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
 
   906  apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
 
   916  apply(erule not_ctran_None2,simp)
 
   907  apply(erule not_ctran_None2,simp)
 
   917  apply simp+
 
   908  apply simp+
 
   932 apply(rule conjI)
 
   923 apply(rule conjI)
 
   933  apply clarify
 
   924  apply clarify
 
   934  apply(case_tac "fst(((Some P, sa) # xs) ! i)")
 
   925  apply(case_tac "fst(((Some P, sa) # xs) ! i)")
 
   935   apply(case_tac "((Some P, sa) # xs) ! i")
 
   926   apply(case_tac "((Some P, sa) # xs) ! i")
 
   936   apply (simp add:lift_def)
 
   927   apply (simp add:lift_def)
 
   937   apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t")
 
   928   apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
 
   938    apply simp
 
   929    apply simp
 
   939   apply simp
 
   930   apply simp
 
   940  apply(simp add:snd_lift del:map.simps)
 
   931  apply(simp add:snd_lift del:map.simps)
 
   941  apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
 
   932  apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
 
   942  apply(erule_tac x=sa in allE)
 
   933  apply(erule_tac x=sa in allE)
 
   944   apply (simp add:assum_def del:map.simps)
 
   935   apply (simp add:assum_def del:map.simps)
 
   945   apply clarify
 
   936   apply clarify
 
   946   apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps)
 
   937   apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps)
 
   947   apply(erule mp)
 
   938   apply(erule mp)
 
   948   apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
 
   939   apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
 
   949    apply(erule etran.elims,simp add:lift_def)
 
   940    apply(erule etranE,simp add:lift_def)
 
   950    apply(rule Env)
 
   941    apply(rule Env)
 
   951   apply(erule etran.elims,simp add:lift_def)
 
   942   apply(erule etranE,simp add:lift_def)
 
   952   apply(rule Env)
 
   943   apply(rule Env)
 
   953  apply (simp add:comm_def del:map.simps)
 
   944  apply (simp add:comm_def del:map.simps)
 
   954  apply clarify
 
   945  apply clarify
 
   955  apply(erule allE,erule impE,assumption)
 
   946  apply(erule allE,erule impE,assumption)
 
   956  apply(erule mp)
 
   947  apply(erule mp)
 
   984  apply(case_tac "i<length xs")
 
   975  apply(case_tac "i<length xs")
 
   985   apply(simp add:nth_append del:map.simps last.simps)
 
   976   apply(simp add:nth_append del:map.simps last.simps)
 
   986   apply(case_tac "fst(((Some P, sa) # xs) ! i)")
 
   977   apply(case_tac "fst(((Some P, sa) # xs) ! i)")
 
   987    apply(case_tac "((Some P, sa) # xs) ! i")
 
   978    apply(case_tac "((Some P, sa) # xs) ! i")
 
   988    apply (simp add:lift_def del:last.simps)
 
   979    apply (simp add:lift_def del:last.simps)
 
   989    apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t")
 
   980    apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
 
   990     apply simp
 
   981     apply simp
 
   991    apply simp
 
   982    apply simp
 
   992   apply(simp add:snd_lift del:map.simps last.simps)
 
   983   apply(simp add:snd_lift del:map.simps last.simps)
 
   993   apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i")
 
   984   apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i")
 
   994   apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
 
   985   apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
 
   996   apply(drule_tac c="(Some P, sa) # xs" in subsetD)
 
   987   apply(drule_tac c="(Some P, sa) # xs" in subsetD)
 
   997    apply (simp add:assum_def del:map.simps last.simps)
 
   988    apply (simp add:assum_def del:map.simps last.simps)
 
   998    apply clarify
 
   989    apply clarify
 
   999    apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp)
 
   990    apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp)
 
  1000    apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
 
   991    apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
 
  1001     apply(erule etran.elims,simp add:lift_def)
 
   992     apply(erule etranE,simp add:lift_def)
 
  1002     apply(rule Env)
 
   993     apply(rule Env)
 
  1003    apply(erule etran.elims,simp add:lift_def)
 
   994    apply(erule etranE,simp add:lift_def)
 
  1004    apply(rule Env)
 
   995    apply(rule Env)
 
  1005   apply (simp add:comm_def del:map.simps)
 
   996   apply (simp add:comm_def del:map.simps)
 
  1006   apply clarify
 
   997   apply clarify
 
  1007   apply(erule allE,erule impE,assumption)
 
   998   apply(erule allE,erule impE,assumption)
 
  1008   apply(erule mp)
 
   999   apply(erule mp)
 
  1156 --{* each etran in @{text "\<sigma>_1[0\<dots>m]"} corresponds to  *}
 
  1147 --{* each etran in @{text "\<sigma>_1[0\<dots>m]"} corresponds to  *}
 
  1157 apply(erule disjE)
 
  1148 apply(erule disjE)
 
  1158 --{* a c-tran in some @{text "\<sigma>_{ib}"}  *}
 
  1149 --{* a c-tran in some @{text "\<sigma>_{ib}"}  *}
 
  1159  apply clarify
 
  1150  apply clarify
 
  1160  apply(case_tac "i=ib",simp)
 
  1151  apply(case_tac "i=ib",simp)
 
  1161   apply(erule etran.elims,simp)
 
  1152   apply(erule etranE,simp)
 
  1162  apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
 
  1153  apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
 
  1163  apply (erule etran.elims)
 
  1154  apply (erule etranE)
 
  1164  apply(case_tac "ia=m",simp)
 
  1155  apply(case_tac "ia=m",simp)
 
  1165  apply simp
 
  1156  apply simp
 
  1166  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
 
  1157  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
 
  1167  apply(subgoal_tac "ia<m",simp)
 
  1158  apply(subgoal_tac "ia<m",simp)
 
  1168   prefer 2
 
  1159   prefer 2
 
  1196 apply(erule disjE)
 
  1187 apply(erule disjE)
 
  1197  prefer 2
 
  1188  prefer 2
 
  1198  apply(force simp add:same_state_def par_assum_def)
 
  1189  apply(force simp add:same_state_def par_assum_def)
 
  1199 apply clarify
 
  1190 apply clarify
 
  1200 apply(case_tac "i=ia",simp)
 
  1191 apply(case_tac "i=ia",simp)
 
  1201  apply(erule etran.elims,simp)
 
  1192  apply(erule etranE,simp)
 
  1202 apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
 
  1193 apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
 
  1203 apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
 
  1194 apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
 
  1204 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
 
  1195 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
 
  1205 apply(simp add:same_state_def)
 
  1196 apply(simp add:same_state_def)
 
  1206 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
 
  1197 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
 
  1235  apply assumption
 
  1226  apply assumption
 
  1236 apply(simp add:conjoin_def same_program_def)
 
  1227 apply(simp add:conjoin_def same_program_def)
 
  1237 apply clarify
 
  1228 apply clarify
 
  1238 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in all_dupE)
 
  1229 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in all_dupE)
 
  1239 apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
 
  1230 apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
 
  1240 apply(erule par_ctran.elims,simp)
 
  1231 apply(erule par_ctranE,simp)
 
  1241 apply(erule_tac x=i and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
 
  1232 apply(erule_tac x=i and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
 
  1242 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
 
  1233 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
 
  1243 apply(rule_tac x=ia in exI)
 
  1234 apply(rule_tac x=ia in exI)
 
  1244 apply(simp add:same_state_def)
 
  1235 apply(simp add:same_state_def)
 
  1245 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp)
 
  1236 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp)
 
  1253 back
 
  1244 back
 
  1254 apply simp_all
 
  1245 apply simp_all
 
  1255 done
 
  1246 done
 
  1256 
  1247 
  1257 lemma parcptn_not_empty [simp]:"[] \<notin> par_cptn"
 
  1248 lemma parcptn_not_empty [simp]:"[] \<notin> par_cptn"
 
  1258 apply(force elim:par_cptn.elims)
 
  1249 apply(force elim:par_cptn.cases)
 
  1259 done
 
  1250 done
 
  1260 
  1251 
  1261 lemma five: 
  1252 lemma five: 
  1262   "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
 
  1253   "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
 
  1263    \<subseteq> Rely (xs ! i);
 
  1254    \<subseteq> Rely (xs ! i);
 
  1334  apply(simp add:par_cp_def ParallelCom_def)
 
  1325  apply(simp add:par_cp_def ParallelCom_def)
 
  1335 apply clarify
 
  1326 apply clarify
 
  1336 apply(case_tac list,simp,simp)
 
  1327 apply(case_tac list,simp,simp)
 
  1337 apply(case_tac i)
 
  1328 apply(case_tac i)
 
  1338  apply(simp add:par_cp_def ParallelCom_def)
 
  1329  apply(simp add:par_cp_def ParallelCom_def)
 
  1339  apply(erule par_ctran.elims,simp)
 
  1330  apply(erule par_ctranE,simp)
 
  1340 apply(simp add:par_cp_def ParallelCom_def)
 
  1331 apply(simp add:par_cp_def ParallelCom_def)
 
  1341 apply clarify
 
  1332 apply clarify
 
  1342 apply(erule par_cptn.elims,simp)
 
  1333 apply(erule par_cptn.cases,simp)
 
  1343  apply simp
 
  1334  apply simp
 
  1344 apply(erule par_ctran.elims)
 
  1335 apply(erule par_ctranE)
 
  1345 back
 
  1336 back
 
  1346 apply simp
 
  1337 apply simp
 
  1347 done
 
  1338 done
 
  1348 
  1339 
  1349 theorem par_rgsound: 
  1340 theorem par_rgsound:
isabelle