src/HOL/Hoare_Parallel/RG_Hoare.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (8 months ago)
changeset 69313 b021008c5397
parent 68975 5ce4d117cea7
permissions -rw-r--r--
removed legacy input syntax
wenzelm@59189
     1
section \<open>The Proof System\<close>
prensani@13020
     2
haftmann@16417
     3
theory RG_Hoare imports RG_Tran begin
prensani@13020
     4
wenzelm@59189
     5
subsection \<open>Proof System for Component Programs\<close>
prensani@13020
     6
haftmann@54859
     7
declare Un_subset_iff [simp del] sup.bounded_iff [simp del]
paulson@15102
     8
wenzelm@59189
     9
definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
wenzelm@59189
    10
  "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)"
prensani@13020
    11
berghofe@23746
    12
inductive
wenzelm@59189
    13
  rghoare :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"
berghofe@23746
    14
    ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
berghofe@23746
    15
where
wenzelm@59189
    16
  Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar;
wenzelm@59189
    17
            stable pre rely; stable post rely \<rbrakk>
prensani@13020
    18
           \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
prensani@13020
    19
wenzelm@59189
    20
| Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk>
prensani@13020
    21
           \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"
prensani@13020
    22
berghofe@23746
    23
| Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
prensani@13020
    24
           \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
prensani@13020
    25
          \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"
prensani@13020
    26
berghofe@23746
    27
| While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
prensani@13020
    28
            \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
prensani@13020
    29
          \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
prensani@13020
    30
wenzelm@59189
    31
| Await: "\<lbrakk> stable pre rely; stable post rely;
wenzelm@59189
    32
            \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t},
prensani@13022
    33
                UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
prensani@13020
    34
           \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
wenzelm@59189
    35
berghofe@23746
    36
| Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
prensani@13020
    37
             \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
prensani@13020
    38
            \<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]"
prensani@13020
    39
haftmann@35416
    40
definition Pre :: "'a rgformula \<Rightarrow> 'a set" where
prensani@13020
    41
  "Pre x \<equiv> fst(snd x)"
haftmann@35416
    42
haftmann@35416
    43
definition Post :: "'a rgformula \<Rightarrow> 'a set" where
prensani@13020
    44
  "Post x \<equiv> snd(snd(snd(snd x)))"
haftmann@35416
    45
haftmann@35416
    46
definition Rely :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
prensani@13020
    47
  "Rely x \<equiv> fst(snd(snd x))"
haftmann@35416
    48
haftmann@35416
    49
definition Guar :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
prensani@13020
    50
  "Guar x \<equiv> fst(snd(snd(snd x)))"
haftmann@35416
    51
haftmann@35416
    52
definition Com :: "'a rgformula \<Rightarrow> 'a com" where
prensani@13020
    53
  "Com x \<equiv> fst x"
prensani@13020
    54
wenzelm@59189
    55
subsection \<open>Proof System for Parallel Programs\<close>
prensani@13020
    56
wenzelm@42174
    57
type_synonym 'a par_rgformula =
wenzelm@42174
    58
  "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
prensani@13020
    59
berghofe@23746
    60
inductive
berghofe@23746
    61
  par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
berghofe@23746
    62
    ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
berghofe@23746
    63
where
wenzelm@59189
    64
  Parallel:
prensani@13020
    65
  "\<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);
prensani@13020
    66
    (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
wenzelm@59189
    67
     pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i));
prensani@13020
    68
    (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post;
prensani@13020
    69
    \<forall>i<length xs. \<turnstile> Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] \<rbrakk>
prensani@13020
    70
   \<Longrightarrow>  \<turnstile> xs SAT [pre, rely, guar, post]"
prensani@13020
    71
wenzelm@59189
    72
section \<open>Soundness\<close>
prensani@13020
    73
wenzelm@59189
    74
subsubsection \<open>Some previous lemmas\<close>
prensani@13020
    75
wenzelm@59189
    76
lemma tl_of_assum_in_assum:
wenzelm@59189
    77
  "(P, s) # (P, t) # xs \<in> assum (pre, rely) \<Longrightarrow> stable pre rely
prensani@13020
    78
  \<Longrightarrow> (P, t) # xs \<in> assum (pre, rely)"
prensani@13020
    79
apply(simp add:assum_def)
prensani@13020
    80
apply clarify
prensani@13020
    81
apply(rule conjI)
prensani@13020
    82
 apply(erule_tac x=0 in allE)
prensani@13020
    83
 apply(simp (no_asm_use)only:stable_def)
prensani@13020
    84
 apply(erule allE,erule allE,erule impE,assumption,erule mp)
prensani@13020
    85
 apply(simp add:Env)
prensani@13020
    86
apply clarify
prensani@13020
    87
apply(erule_tac x="Suc i" in allE)
prensani@13020
    88
apply simp
prensani@13020
    89
done
prensani@13020
    90
wenzelm@59189
    91
lemma etran_in_comm:
prensani@13020
    92
  "(P, t) # xs \<in> comm(guar, post) \<Longrightarrow> (P, s) # (P, t) # xs \<in> comm(guar, post)"
prensani@13020
    93
apply(simp add:comm_def)
prensani@13020
    94
apply clarify
prensani@13020
    95
apply(case_tac i,simp+)
prensani@13020
    96
done
prensani@13020
    97
wenzelm@59189
    98
lemma ctran_in_comm:
wenzelm@59189
    99
  "\<lbrakk>(s, s) \<in> guar; (Q, s) # xs \<in> comm(guar, post)\<rbrakk>
prensani@13020
   100
  \<Longrightarrow> (P, s) # (Q, s) # xs \<in> comm(guar, post)"
prensani@13020
   101
apply(simp add:comm_def)
prensani@13020
   102
apply clarify
prensani@13020
   103
apply(case_tac i,simp+)
prensani@13020
   104
done
prensani@13020
   105
wenzelm@59189
   106
lemma takecptn_is_cptn [rule_format, elim!]:
prensani@13020
   107
  "\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn"
prensani@13020
   108
apply(induct "c")
berghofe@23746
   109
 apply(force elim: cptn.cases)
prensani@13020
   110
apply clarify
wenzelm@59189
   111
apply(case_tac j)
prensani@13020
   112
 apply simp
prensani@13020
   113
 apply(rule CptnOne)
prensani@13020
   114
apply simp
berghofe@23746
   115
apply(force intro:cptn.intros elim:cptn.cases)
prensani@13020
   116
done
prensani@13020
   117
wenzelm@59189
   118
lemma dropcptn_is_cptn [rule_format,elim!]:
prensani@13020
   119
  "\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn"
prensani@13020
   120
apply(induct "c")
berghofe@23746
   121
 apply(force elim: cptn.cases)
prensani@13020
   122
apply clarify
wenzelm@59189
   123
apply(case_tac j,simp+)
berghofe@23746
   124
apply(erule cptn.cases)
prensani@13020
   125
  apply simp
prensani@13020
   126
 apply force
prensani@13020
   127
apply force
prensani@13020
   128
done
prensani@13020
   129
wenzelm@59189
   130
lemma takepar_cptn_is_par_cptn [rule_format,elim]:
prensani@13020
   131
  "\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn"
prensani@13020
   132
apply(induct "c")
berghofe@23746
   133
 apply(force elim: cptn.cases)
prensani@13020
   134
apply clarify
wenzelm@59189
   135
apply(case_tac j,simp)
prensani@13020
   136
 apply(rule ParCptnOne)
berghofe@23746
   137
apply(force intro:par_cptn.intros elim:par_cptn.cases)
prensani@13020
   138
done
prensani@13020
   139
prensani@13020
   140
lemma droppar_cptn_is_par_cptn [rule_format]:
prensani@13020
   141
  "\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn"
prensani@13020
   142
apply(induct "c")
berghofe@23746
   143
 apply(force elim: par_cptn.cases)
prensani@13020
   144
apply clarify
wenzelm@59189
   145
apply(case_tac j,simp+)
berghofe@23746
   146
apply(erule par_cptn.cases)
prensani@13020
   147
  apply simp
prensani@13020
   148
 apply force
prensani@13020
   149
apply force
prensani@13020
   150
done
prensani@13020
   151
prensani@13020
   152
lemma tl_of_cptn_is_cptn: "\<lbrakk>x # xs \<in> cptn; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs  \<in> cptn"
wenzelm@59189
   153
apply(subgoal_tac "1 < length (x # xs)")
prensani@13020
   154
 apply(drule dropcptn_is_cptn,simp+)
prensani@13020
   155
done
prensani@13020
   156
wenzelm@59189
   157
lemma not_ctran_None [rule_format]:
prensani@13020
   158
  "\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)"
prensani@13020
   159
apply(induct xs,simp+)
prensani@13020
   160
apply clarify
berghofe@23746
   161
apply(erule cptn.cases,simp)
prensani@13020
   162
 apply simp
prensani@13020
   163
 apply(case_tac i,simp)
prensani@13020
   164
  apply(rule Env)
prensani@13020
   165
 apply simp
berghofe@23746
   166
apply(force elim:ctran.cases)
prensani@13020
   167
done
prensani@13020
   168
prensani@13020
   169
lemma cptn_not_empty [simp]:"[] \<notin> cptn"
berghofe@23746
   170
apply(force elim:cptn.cases)
prensani@13020
   171
done
prensani@13020
   172
wenzelm@59189
   173
lemma etran_or_ctran [rule_format]:
wenzelm@59189
   174
  "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x
wenzelm@59189
   175
   \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m
prensani@13022
   176
   \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
prensani@13020
   177
apply(induct x,simp)
prensani@13020
   178
apply clarify
berghofe@23746
   179
apply(erule cptn.cases,simp)
prensani@13020
   180
 apply(case_tac i,simp)
prensani@13020
   181
  apply(rule Env)
prensani@13020
   182
 apply simp
prensani@13020
   183
 apply(erule_tac x="m - 1" in allE)
prensani@13020
   184
 apply(case_tac m,simp,simp)
prensani@13020
   185
 apply(subgoal_tac "(\<forall>i. Suc i < nata \<longrightarrow> (((P, t) # xs) ! i, xs ! i) \<notin> ctran)")
prensani@13020
   186
  apply force
prensani@13020
   187
 apply clarify
prensani@13020
   188
 apply(erule_tac x="Suc ia" in allE,simp)
wenzelm@59807
   189
apply(erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (J j) \<notin> ctran" for H J in allE,simp)
prensani@13020
   190
done
prensani@13020
   191
wenzelm@59189
   192
lemma etran_or_ctran2 [rule_format]:
prensani@13020
   193
  "\<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)
prensani@13020
   194
  \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i)"
prensani@13020
   195
apply(induct x)
prensani@13020
   196
 apply simp
prensani@13020
   197
apply clarify
berghofe@23746
   198
apply(erule cptn.cases,simp)
prensani@13020
   199
 apply(case_tac i,simp+)
prensani@13020
   200
apply(case_tac i,simp)
berghofe@23746
   201
 apply(force elim:etran.cases)
prensani@13020
   202
apply simp
prensani@13020
   203
done
prensani@13020
   204
wenzelm@59189
   205
lemma etran_or_ctran2_disjI1:
prensani@13020
   206
  "\<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"
prensani@13020
   207
by(drule etran_or_ctran2,simp_all)
prensani@13020
   208
wenzelm@59189
   209
lemma etran_or_ctran2_disjI2:
prensani@13020
   210
  "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -e\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i"
prensani@13020
   211
by(drule etran_or_ctran2,simp_all)
prensani@13020
   212
wenzelm@59189
   213
lemma not_ctran_None2 [rule_format]:
prensani@13020
   214
  "\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i"
prensani@13020
   215
apply(frule not_ctran_None,simp)
prensani@13020
   216
apply(case_tac i,simp)
berghofe@23746
   217
 apply(force elim:etranE)
prensani@13020
   218
apply simp
prensani@13020
   219
apply(rule etran_or_ctran2_disjI2,simp_all)
prensani@13020
   220
apply(force intro:tl_of_cptn_is_cptn)
prensani@13020
   221
done
prensani@13020
   222
wenzelm@58860
   223
lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))"
prensani@13020
   224
apply(rule nat_less_induct)
prensani@13020
   225
apply clarify
prensani@13020
   226
apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
prensani@13020
   227
apply auto
prensani@13020
   228
done
wenzelm@59189
   229
wenzelm@59189
   230
lemma stability [rule_format]:
prensani@13020
   231
  "\<forall>j k. x \<in> cptn \<longrightarrow> stable p rely \<longrightarrow> j\<le>k \<longrightarrow> k<length x \<longrightarrow> snd(x!j)\<in>p  \<longrightarrow>
wenzelm@59189
   232
  (\<forall>i. (Suc i)<length x \<longrightarrow>
wenzelm@59189
   233
          (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow>
prensani@13020
   234
  (\<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)"
prensani@13020
   235
apply(induct x)
prensani@13020
   236
 apply clarify
berghofe@23746
   237
 apply(force elim:cptn.cases)
prensani@13020
   238
apply clarify
berghofe@23746
   239
apply(erule cptn.cases,simp)
prensani@13020
   240
 apply simp
prensani@13020
   241
 apply(case_tac k,simp,simp)
wenzelm@59189
   242
 apply(case_tac j,simp)
prensani@13020
   243
  apply(erule_tac x=0 in allE)
wenzelm@59807
   244
  apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (J j)" for J in allE,simp)
prensani@13020
   245
  apply(subgoal_tac "t\<in>p")
prensani@13020
   246
   apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
prensani@13020
   247
    apply clarify
wenzelm@59807
   248
    apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
prensani@13020
   249
   apply clarify
wenzelm@59807
   250
   apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
wenzelm@59807
   251
  apply(erule_tac x=0 and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran \<longrightarrow> T j" for H J T in allE,simp)
prensani@13020
   252
  apply(simp(no_asm_use) only:stable_def)
prensani@13020
   253
  apply(erule_tac x=s in allE)
prensani@13020
   254
  apply(erule_tac x=t in allE)
wenzelm@59189
   255
  apply simp
prensani@13020
   256
  apply(erule mp)
prensani@13020
   257
  apply(erule mp)
prensani@13020
   258
  apply(rule Env)
prensani@13020
   259
 apply simp
prensani@13020
   260
 apply(erule_tac x="nata" in allE)
wenzelm@59807
   261
 apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
prensani@13020
   262
 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
prensani@13020
   263
  apply clarify
wenzelm@59807
   264
  apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
prensani@13020
   265
 apply clarify
wenzelm@59807
   266
 apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
prensani@13020
   267
apply(case_tac k,simp,simp)
prensani@13020
   268
apply(case_tac j)
wenzelm@59807
   269
 apply(erule_tac x=0 and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
berghofe@23746
   270
 apply(erule etran.cases,simp)
prensani@13020
   271
apply(erule_tac x="nata" in allE)
wenzelm@59807
   272
apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
prensani@13020
   273
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)")
prensani@13020
   274
 apply clarify
wenzelm@59807
   275
 apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
prensani@13020
   276
apply clarify
wenzelm@59807
   277
apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
prensani@13020
   278
done
prensani@13020
   279
wenzelm@59189
   280
subsection \<open>Soundness of the System for Component Programs\<close>
prensani@13020
   281
wenzelm@59189
   282
subsubsection \<open>Soundness of the Basic rule\<close>
prensani@13020
   283
wenzelm@59189
   284
lemma unique_ctran_Basic [rule_format]:
wenzelm@59189
   285
  "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) \<longrightarrow>
wenzelm@59189
   286
  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow>
prensani@13022
   287
  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
prensani@13020
   288
apply(induct x,simp)
prensani@13020
   289
apply simp
prensani@13020
   290
apply clarify
berghofe@23746
   291
apply(erule cptn.cases,simp)
prensani@13020
   292
 apply(case_tac i,simp+)
prensani@13020
   293
 apply clarify
prensani@13020
   294
 apply(case_tac j,simp)
prensani@13020
   295
  apply(rule Env)
prensani@13020
   296
 apply simp
prensani@13020
   297
apply clarify
prensani@13020
   298
apply simp
prensani@13020
   299
apply(case_tac i)
prensani@13020
   300
 apply(case_tac j,simp,simp)
berghofe@23746
   301
 apply(erule ctran.cases,simp_all)
prensani@13020
   302
 apply(force elim: not_ctran_None)
berghofe@23746
   303
apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran" for sa Q t)
prensani@13020
   304
apply simp
prensani@13020
   305
apply(drule_tac i=nat in not_ctran_None,simp)
berghofe@23746
   306
apply(erule etranE,simp)
prensani@13020
   307
done
prensani@13020
   308
wenzelm@59189
   309
lemma exists_ctran_Basic_None [rule_format]:
wenzelm@59189
   310
  "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s)
prensani@13020
   311
  \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
prensani@13020
   312
apply(induct x,simp)
prensani@13020
   313
apply simp
prensani@13020
   314
apply clarify
berghofe@23746
   315
apply(erule cptn.cases,simp)
prensani@13020
   316
 apply(case_tac i,simp,simp)
prensani@13020
   317
 apply(erule_tac x=nat in allE,simp)
prensani@13020
   318
 apply clarify
prensani@13020
   319
 apply(rule_tac x="Suc j" in exI,simp,simp)
prensani@13020
   320
apply clarify
prensani@13020
   321
apply(case_tac i,simp,simp)
prensani@13020
   322
apply(rule_tac x=0 in exI,simp)
prensani@13020
   323
done
prensani@13020
   324
wenzelm@59189
   325
lemma Basic_sound:
wenzelm@59189
   326
  " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar;
prensani@13020
   327
  stable pre rely; stable post rely\<rbrakk>
prensani@13020
   328
  \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
prensani@13020
   329
apply(unfold com_validity_def)
prensani@13020
   330
apply clarify
prensani@13020
   331
apply(simp add:comm_def)
prensani@13020
   332
apply(rule conjI)
prensani@13020
   333
 apply clarify
prensani@13020
   334
 apply(simp add:cp_def assum_def)
prensani@13020
   335
 apply clarify
prensani@13020
   336
 apply(frule_tac j=0 and k=i and p=pre in stability)
prensani@13020
   337
       apply simp_all
prensani@13020
   338
   apply(erule_tac x=ia in allE,simp)
prensani@13020
   339
  apply(erule_tac i=i and f=f in unique_ctran_Basic,simp_all)
prensani@13020
   340
 apply(erule subsetD,simp)
prensani@13020
   341
 apply(case_tac "x!i")
prensani@13020
   342
 apply clarify
prensani@13020
   343
 apply(drule_tac s="Some (Basic f)" in sym,simp)
wenzelm@59807
   344
 apply(thin_tac "\<forall>j. H j" for H)
berghofe@23746
   345
 apply(force elim:ctran.cases)
prensani@13020
   346
apply clarify
prensani@13020
   347
apply(simp add:cp_def)
prensani@13020
   348
apply clarify
prensani@13020
   349
apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+)
prensani@13020
   350
  apply(case_tac x,simp+)
prensani@13020
   351
  apply(rule last_fst_esp,simp add:last_length)
prensani@13020
   352
 apply (case_tac x,simp+)
prensani@13020
   353
apply(simp add:assum_def)
prensani@13020
   354
apply clarify
prensani@13020
   355
apply(frule_tac j=0 and k="j" and p=pre in stability)
prensani@13020
   356
      apply simp_all
prensani@13020
   357
  apply(erule_tac x=i in allE,simp)
prensani@13020
   358
 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
prensani@13020
   359
apply(case_tac "x!j")
prensani@13020
   360
apply clarify
prensani@13020
   361
apply simp
prensani@13020
   362
apply(drule_tac s="Some (Basic f)" in sym,simp)
prensani@13020
   363
apply(case_tac "x!Suc j",simp)
berghofe@23746
   364
apply(rule ctran.cases,simp)
webertj@20432
   365
apply(simp_all)
prensani@13020
   366
apply(drule_tac c=sa in subsetD,simp)
prensani@13020
   367
apply clarify
prensani@13020
   368
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
webertj@20432
   369
 apply(case_tac x,simp+)
prensani@13020
   370
 apply(erule_tac x=i in allE)
webertj@20432
   371
apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
webertj@20432
   372
  apply arith+
prensani@13020
   373
apply(case_tac x)
webertj@20432
   374
apply(simp add:last_length)+
prensani@13020
   375
done
prensani@13020
   376
wenzelm@59189
   377
subsubsection\<open>Soundness of the Await rule\<close>
prensani@13020
   378
wenzelm@59189
   379
lemma unique_ctran_Await [rule_format]:
wenzelm@59189
   380
  "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow>
wenzelm@59189
   381
  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow>
prensani@13022
   382
  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
prensani@13020
   383
apply(induct x,simp+)
prensani@13020
   384
apply clarify
berghofe@23746
   385
apply(erule cptn.cases,simp)
prensani@13020
   386
 apply(case_tac i,simp+)
prensani@13020
   387
 apply clarify
prensani@13020
   388
 apply(case_tac j,simp)
prensani@13020
   389
  apply(rule Env)
prensani@13020
   390
 apply simp
prensani@13020
   391
apply clarify
prensani@13020
   392
apply simp
prensani@13020
   393
apply(case_tac i)
prensani@13020
   394
 apply(case_tac j,simp,simp)
berghofe@23746
   395
 apply(erule ctran.cases,simp_all)
prensani@13020
   396
 apply(force elim: not_ctran_None)
berghofe@23746
   397
apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran" for sa Q t,simp)
prensani@13020
   398
apply(drule_tac i=nat in not_ctran_None,simp)
berghofe@23746
   399
apply(erule etranE,simp)
prensani@13020
   400
done
prensani@13020
   401
wenzelm@59189
   402
lemma exists_ctran_Await_None [rule_format]:
wenzelm@59189
   403
  "\<forall>s i.  x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s)
prensani@13020
   404
  \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
prensani@13020
   405
apply(induct x,simp+)
prensani@13020
   406
apply clarify
berghofe@23746
   407
apply(erule cptn.cases,simp)
prensani@13020
   408
 apply(case_tac i,simp+)
prensani@13020
   409
 apply(erule_tac x=nat in allE,simp)
prensani@13020
   410
 apply clarify
prensani@13020
   411
 apply(rule_tac x="Suc j" in exI,simp,simp)
prensani@13020
   412
apply clarify
prensani@13020
   413
apply(case_tac i,simp,simp)
prensani@13020
   414
apply(rule_tac x=0 in exI,simp)
prensani@13020
   415
done
prensani@13020
   416
wenzelm@59189
   417
lemma Star_imp_cptn:
prensani@13020
   418
  "(P, s) -c*\<rightarrow> (R, t) \<Longrightarrow> \<exists>l \<in> cp P s. (last l)=(R, t)
prensani@13020
   419
  \<and> (\<forall>i. Suc i<length l \<longrightarrow> l!i -c\<rightarrow> l!Suc i)"
prensani@13020
   420
apply (erule converse_rtrancl_induct2)
prensani@13020
   421
 apply(rule_tac x="[(R,t)]" in bexI)
prensani@13020
   422
  apply simp
prensani@13020
   423
 apply(simp add:cp_def)
prensani@13020
   424
 apply(rule CptnOne)
prensani@13020
   425
apply clarify
prensani@13020
   426
apply(rule_tac x="(a, b)#l" in bexI)
prensani@13020
   427
 apply (rule conjI)
prensani@13020
   428
  apply(case_tac l,simp add:cp_def)
prensani@13020
   429
  apply(simp add:last_length)
prensani@13020
   430
 apply clarify
prensani@13020
   431
apply(case_tac i,simp)
prensani@13020
   432
apply(simp add:cp_def)
prensani@13020
   433
apply force
prensani@13020
   434
apply(simp add:cp_def)
prensani@13020
   435
 apply(case_tac l)
berghofe@23746
   436
 apply(force elim:cptn.cases)
prensani@13020
   437
apply simp
prensani@13020
   438
apply(erule CptnComp)
prensani@13020
   439
apply clarify
prensani@13020
   440
done
wenzelm@59189
   441
wenzelm@59189
   442
lemma Await_sound:
prensani@13020
   443
  "\<lbrakk>stable pre rely; stable post rely;
wenzelm@59189
   444
  \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t},
prensani@13022
   445
                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and>
wenzelm@59189
   446
  \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t},
prensani@13022
   447
                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
prensani@13020
   448
  \<Longrightarrow> \<Turnstile> Await b P sat [pre, rely, guar, post]"
prensani@13020
   449
apply(unfold com_validity_def)
prensani@13020
   450
apply clarify
prensani@13020
   451
apply(simp add:comm_def)
prensani@13020
   452
apply(rule conjI)
prensani@13020
   453
 apply clarify
prensani@13020
   454
 apply(simp add:cp_def assum_def)
prensani@13020
   455
 apply clarify
prensani@13020
   456
 apply(frule_tac j=0 and k=i and p=pre in stability,simp_all)
prensani@13020
   457
   apply(erule_tac x=ia in allE,simp)
prensani@13020
   458
  apply(subgoal_tac "x\<in> cp (Some(Await b P)) s")
prensani@13020
   459
  apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
prensani@13020
   460
  apply(simp add:cp_def)
wenzelm@67443
   461
\<comment> \<open>here starts the different part.\<close>
berghofe@23746
   462
 apply(erule ctran.cases,simp_all)
wenzelm@59189
   463
 apply(drule Star_imp_cptn)
prensani@13020
   464
 apply clarify
prensani@13020
   465
 apply(erule_tac x=sa in allE)
prensani@13020
   466
 apply clarify
prensani@13020
   467
 apply(erule_tac x=sa in allE)
prensani@13020
   468
 apply(drule_tac c=l in subsetD)
prensani@13020
   469
  apply (simp add:cp_def)
prensani@13020
   470
  apply clarify
wenzelm@59807
   471
  apply(erule_tac x=ia and P="\<lambda>i. H i \<longrightarrow> (J i, I i)\<in>ctran" for H J I in allE,simp)
berghofe@23746
   472
  apply(erule etranE,simp)
prensani@13020
   473
 apply simp
prensani@13020
   474
apply clarify
prensani@13020
   475
apply(simp add:cp_def)
prensani@13020
   476
apply clarify
prensani@13020
   477
apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
prensani@13020
   478
  apply (case_tac x,simp+)
prensani@13020
   479
 apply(rule last_fst_esp,simp add:last_length)
wenzelm@52597
   480
 apply(case_tac x, simp+)
prensani@13020
   481
apply clarify
prensani@13020
   482
apply(simp add:assum_def)
prensani@13020
   483
apply clarify
prensani@13020
   484
apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
prensani@13020
   485
  apply(erule_tac x=i in allE,simp)
prensani@13020
   486
 apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
prensani@13020
   487
apply(case_tac "x!j")
prensani@13020
   488
apply clarify
prensani@13020
   489
apply simp
prensani@13020
   490
apply(drule_tac s="Some (Await b P)" in sym,simp)
prensani@13020
   491
apply(case_tac "x!Suc j",simp)
berghofe@23746
   492
apply(rule ctran.cases,simp)
webertj@20432
   493
apply(simp_all)
wenzelm@59189
   494
apply(drule Star_imp_cptn)
prensani@13020
   495
apply clarify
prensani@13020
   496
apply(erule_tac x=sa in allE)
prensani@13020
   497
apply clarify
prensani@13020
   498
apply(erule_tac x=sa in allE)
prensani@13020
   499
apply(drule_tac c=l in subsetD)
prensani@13020
   500
 apply (simp add:cp_def)
prensani@13020
   501
 apply clarify
wenzelm@59807
   502
 apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> (J i, I i)\<in>ctran" for H J I in allE,simp)
berghofe@23746
   503
 apply(erule etranE,simp)
prensani@13020
   504
apply simp
prensani@13020
   505
apply clarify
prensani@13020
   506
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
webertj@20432
   507
 apply(case_tac x,simp+)
prensani@13020
   508
 apply(erule_tac x=i in allE)
webertj@20432
   509
apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
webertj@20432
   510
 apply arith+
prensani@13020
   511
apply(case_tac x)
webertj@20432
   512
apply(simp add:last_length)+
prensani@13020
   513
done
prensani@13020
   514
wenzelm@59189
   515
subsubsection\<open>Soundness of the Conditional rule\<close>
prensani@13020
   516
wenzelm@59189
   517
lemma Cond_sound:
wenzelm@59189
   518
  "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post];
prensani@13020
   519
  \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
prensani@13020
   520
  \<Longrightarrow> \<Turnstile> (Cond b P1 P2) sat [pre, rely, guar, post]"
prensani@13020
   521
apply(unfold com_validity_def)
prensani@13020
   522
apply clarify
prensani@13020
   523
apply(simp add:cp_def comm_def)
prensani@13020
   524
apply(case_tac "\<exists>i. Suc i<length x \<and> x!i -c\<rightarrow> x!Suc i")
prensani@13020
   525
 prefer 2
prensani@13020
   526
 apply simp
prensani@13020
   527
 apply clarify
prensani@13020
   528
 apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+)
prensani@13020
   529
     apply(case_tac x,simp+)
prensani@13020
   530
    apply(simp add:assum_def)
prensani@13020
   531
   apply(simp add:assum_def)
prensani@13020
   532
  apply(erule_tac m="length x" in etran_or_ctran,simp+)
prensani@13020
   533
 apply(case_tac x, (simp add:last_length)+)
prensani@13020
   534
apply(erule exE)
wenzelm@59807
   535
apply(drule_tac n=i and P="\<lambda>i. H i \<and> (J i, I i) \<in> ctran" for H J I in Ex_first_occurrence)
prensani@13020
   536
apply clarify
prensani@13020
   537
apply (simp add:assum_def)
prensani@13020
   538
apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
prensani@13020
   539
 apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
berghofe@23746
   540
apply(erule ctran.cases,simp_all)
prensani@13020
   541
 apply(erule_tac x="sa" in allE)
prensani@13020
   542
 apply(drule_tac c="drop (Suc m) x" in subsetD)
prensani@13020
   543
  apply simp
prensani@13020
   544
  apply clarify
prensani@13020
   545
 apply simp
wenzelm@17528
   546
 apply clarify
wenzelm@17528
   547
 apply(case_tac "i\<le>m")
wenzelm@17528
   548
  apply(drule le_imp_less_or_eq)
wenzelm@17528
   549
  apply(erule disjE)
wenzelm@17528
   550
   apply(erule_tac x=i in allE, erule impE, assumption)
wenzelm@17528
   551
   apply simp+
wenzelm@59807
   552
 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> (I j)\<in>guar" for H J I in allE)
webertj@20432
   553
 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
webertj@20432
   554
  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
webertj@20432
   555
   apply(rotate_tac -2)
prensani@13020
   556
   apply simp
prensani@13020
   557
  apply arith
prensani@13020
   558
 apply arith
webertj@20432
   559
apply(case_tac "length (drop (Suc m) x)",simp)
webertj@20432
   560
apply(erule_tac x="sa" in allE)
webertj@20432
   561
back
webertj@20432
   562
apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
webertj@20432
   563
 apply clarify
webertj@20432
   564
apply simp
webertj@20432
   565
apply clarify
webertj@20432
   566
apply(case_tac "i\<le>m")
webertj@20432
   567
 apply(drule le_imp_less_or_eq)
webertj@20432
   568
 apply(erule disjE)
webertj@20432
   569
  apply(erule_tac x=i in allE, erule impE, assumption)
webertj@20432
   570
  apply simp
webertj@20432
   571
 apply simp
wenzelm@59807
   572
apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> (I j)\<in>guar" for H J I in allE)
webertj@20432
   573
apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
webertj@20432
   574
 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
webertj@20432
   575
  apply(rotate_tac -2)
webertj@20432
   576
  apply simp
webertj@20432
   577
 apply arith
webertj@20432
   578
apply arith
webertj@20217
   579
done
prensani@13020
   580
wenzelm@59189
   581
subsubsection\<open>Soundness of the Sequential rule\<close>
prensani@13020
   582
prensani@13020
   583
inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
prensani@13020
   584
prensani@13020
   585
lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None"
prensani@13020
   586
apply(subgoal_tac "length xs<length (x # xs)")
prensani@13020
   587
 apply(drule_tac Q=Q in  lift_nth)
prensani@13020
   588
 apply(erule ssubst)
prensani@13020
   589
 apply (simp add:lift_def)
prensani@13020
   590
 apply(case_tac "(x # xs) ! length xs",simp)
prensani@13020
   591
apply simp
prensani@13020
   592
done
prensani@13020
   593
wenzelm@59189
   594
lemma Seq_sound1 [rule_format]:
wenzelm@59189
   595
  "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow>
wenzelm@59189
   596
  (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow>
prensani@13020
   597
  (\<exists>xs\<in> cp (Some P) s. x=map (lift Q) xs)"
prensani@13020
   598
apply(erule cptn_mod.induct)
prensani@13020
   599
apply(unfold cp_def)
prensani@13020
   600
apply safe
prensani@13020
   601
apply simp_all
prensani@13020
   602
    apply(simp add:lift_def)
prensani@13020
   603
    apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne)
prensani@13020
   604
   apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)")
prensani@13020
   605
    apply clarify
nipkow@14025
   606
    apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
prensani@13020
   607
    apply(rule conjI,erule CptnEnv)
berghofe@13601
   608
    apply(simp (no_asm_use) add:lift_def)
prensani@13020
   609
   apply clarify
prensani@13020
   610
   apply(erule_tac x="Suc i" in allE, simp)
berghofe@23746
   611
  apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran" for Pa sa t)
prensani@13020
   612
 apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
prensani@13020
   613
apply(erule_tac x="length xs" in allE, simp)
prensani@13020
   614
apply(simp only:Cons_lift_append)
prensani@13020
   615
apply(subgoal_tac "length xs < length ((Some P, sa) # xs)")
prensani@13020
   616
 apply(simp only :nth_append length_map last_length nth_map)
prensani@13020
   617
 apply(case_tac "last((Some P, sa) # xs)")
prensani@13020
   618
 apply(simp add:lift_def)
prensani@13020
   619
apply simp
prensani@13020
   620
done
prensani@13020
   621
wenzelm@59189
   622
lemma Seq_sound2 [rule_format]:
wenzelm@59189
   623
  "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x
prensani@13022
   624
  \<longrightarrow> fst(x!i)=Some Q \<longrightarrow>
prensani@13020
   625
  (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
wenzelm@59189
   626
  (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i
prensani@13022
   627
   \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)"
prensani@13020
   628
apply(erule cptn.induct)
prensani@13020
   629
apply(unfold cp_def)
prensani@13020
   630
apply safe
prensani@13020
   631
apply simp_all
prensani@13020
   632
 apply(case_tac i,simp+)
prensani@13020
   633
 apply(erule allE,erule impE,assumption,simp)
prensani@13020
   634
 apply clarify
prensani@13020
   635
 apply(subgoal_tac "(\<forall>j < nat. fst (((Some (Seq Pa Q), t) # xs) ! j) \<noteq> Some Q)",clarify)
prensani@13020
   636
  prefer 2
prensani@13020
   637
  apply force
prensani@13020
   638
 apply(case_tac xsa,simp,simp)
blanchet@55417
   639
 apply(rename_tac list)
prensani@13020
   640
 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
prensani@13020
   641
 apply(rule conjI,erule CptnEnv)
berghofe@13601
   642
 apply(simp (no_asm_use) add:lift_def)
prensani@13020
   643
 apply(rule_tac x=ys in exI,simp)
berghofe@23746
   644
apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran" for Pa sa t)
prensani@13020
   645
 apply simp
prensani@13020
   646
 apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
prensani@13020
   647
 apply(rule conjI)
prensani@13020
   648
  apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp)
prensani@13020
   649
 apply(case_tac i, simp+)
prensani@13020
   650
 apply(case_tac nat,simp+)
prensani@13020
   651
 apply(rule_tac x="(Some Q,ta)#xs" in exI,simp add:lift_def)
prensani@13020
   652
 apply(case_tac nat,simp+)
prensani@13020
   653
 apply(force)
prensani@13020
   654
apply(case_tac i, simp+)
prensani@13020
   655
apply(case_tac nat,simp+)
prensani@13020
   656
apply(erule_tac x="Suc nata" in allE,simp)
prensani@13020
   657
apply clarify
prensani@13020
   658
apply(subgoal_tac "(\<forall>j<Suc nata. fst (((Some (Seq P2 Q), ta) # xs) ! j) \<noteq> Some Q)",clarify)
prensani@13020
   659
 prefer 2
prensani@13020
   660
 apply clarify
prensani@13020
   661
 apply force
prensani@13020
   662
apply(rule_tac x="(Some Pa, sa)#(Some P2, ta)#(tl xsa)" in exI,simp)
prensani@13020
   663
apply(rule conjI,erule CptnComp)
prensani@13020
   664
apply(rule nth_tl_if,force,simp+)
prensani@13020
   665
apply(rule_tac x=ys in exI,simp)
prensani@13020
   666
apply(rule conjI)
prensani@13020
   667
apply(rule nth_tl_if,force,simp+)
prensani@13020
   668
 apply(rule tl_zero,simp+)
prensani@13020
   669
 apply force
prensani@13020
   670
apply(rule conjI,simp add:lift_def)
wenzelm@59189
   671
apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)")
blanchet@55465
   672
 apply(simp add:Cons_lift del:list.map)
prensani@13020
   673
 apply(rule nth_tl_if)
prensani@13020
   674
   apply force
prensani@13020
   675
  apply simp+
prensani@13020
   676
apply(simp add:lift_def)
prensani@13020
   677
done
prensani@13020
   678
(*
prensani@13020
   679
lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
prensani@13020
   680
apply(simp only:last_length [THEN sym])
prensani@13020
   681
apply(subgoal_tac "length xs<length (x # xs)")
prensani@13020
   682
 apply(drule_tac Q=Q in  lift_nth)
prensani@13020
   683
 apply(erule ssubst)
prensani@13020
   684
 apply (simp add:lift_def)
prensani@13020
   685
 apply(case_tac "(x # xs) ! length xs",simp)
prensani@13020
   686
apply simp
prensani@13020
   687
done
prensani@13020
   688
*)
prensani@13020
   689
prensani@13020
   690
lemma last_lift_not_None2: "fst ((lift Q) (last (x#xs))) \<noteq> None"
prensani@13020
   691
apply(simp only:last_length [THEN sym])
prensani@13020
   692
apply(subgoal_tac "length xs<length (x # xs)")
prensani@13020
   693
 apply(drule_tac Q=Q in  lift_nth)
prensani@13020
   694
 apply(erule ssubst)
prensani@13020
   695
 apply (simp add:lift_def)
prensani@13020
   696
 apply(case_tac "(x # xs) ! length xs",simp)
prensani@13020
   697
apply simp
prensani@13020
   698
done
prensani@13020
   699
wenzelm@59189
   700
lemma Seq_sound:
prensani@13020
   701
  "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
prensani@13020
   702
  \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
prensani@13020
   703
apply(unfold com_validity_def)
prensani@13020
   704
apply clarify
prensani@13020
   705
apply(case_tac "\<exists>i<length x. fst(x!i)=Some Q")
prensani@13020
   706
 prefer 2
prensani@13020
   707
 apply (simp add:cp_def cptn_iff_cptn_mod)
prensani@13020
   708
 apply clarify
prensani@13020
   709
 apply(frule_tac Seq_sound1,force)
prensani@13020
   710
  apply force
prensani@13020
   711
 apply clarify
prensani@13020
   712
 apply(erule_tac x=s in allE,simp)
prensani@13020
   713
 apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod)
prensani@13020
   714
  apply(simp add:assum_def)
prensani@13020
   715
  apply clarify
wenzelm@59807
   716
  apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
prensani@13020
   717
  apply(simp add:snd_lift)
prensani@13020
   718
  apply(erule mp)
berghofe@23746
   719
  apply(force elim:etranE intro:Env simp add:lift_def)
prensani@13020
   720
 apply(simp add:comm_def)
prensani@13020
   721
 apply(rule conjI)
prensani@13020
   722
  apply clarify
wenzelm@59807
   723
  apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
prensani@13020
   724
  apply(simp add:snd_lift)
prensani@13020
   725
  apply(erule mp)
prensani@13020
   726
  apply(case_tac "(xs!i)")
prensani@13020
   727
  apply(case_tac "(xs! Suc i)")
prensani@13020
   728
  apply(case_tac "fst(xs!i)")
prensani@13020
   729
   apply(erule_tac x=i in allE, simp add:lift_def)
prensani@13020
   730
  apply(case_tac "fst(xs!Suc i)")
prensani@13020
   731
   apply(force simp add:lift_def)
prensani@13020
   732
  apply(force simp add:lift_def)
prensani@13020
   733
 apply clarify
prensani@13020
   734
 apply(case_tac xs,simp add:cp_def)
prensani@13020
   735
 apply clarify
blanchet@55465
   736
 apply (simp del:list.map)
blanchet@55417
   737
 apply (rename_tac list)
prensani@13020
   738
 apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]")
nipkow@17588
   739
  apply(drule last_conv_nth)
blanchet@55465
   740
  apply (simp del:list.map)
prensani@13020
   741
  apply(simp only:last_lift_not_None)
prensani@13020
   742
 apply simp
wenzelm@67443
   743
\<comment> \<open>\<open>\<exists>i<length x. fst (x ! i) = Some Q\<close>\<close>
prensani@13020
   744
apply(erule exE)
prensani@13020
   745
apply(drule_tac n=i and P="\<lambda>i. i < length x \<and> fst (x ! i) = Some Q" in Ex_first_occurrence)
prensani@13020
   746
apply clarify
prensani@13020
   747
apply (simp add:cp_def)
prensani@13020
   748
 apply clarify
prensani@13020
   749
 apply(frule_tac i=m in Seq_sound2,force)
prensani@13020
   750
  apply simp+
prensani@13020
   751
apply clarify
prensani@13020
   752
apply(simp add:comm_def)
prensani@13020
   753
apply(erule_tac x=s in allE)
prensani@13020
   754
apply(drule_tac c=xs in subsetD,simp)
prensani@13020
   755
 apply(case_tac "xs=[]",simp)
prensani@13020
   756
 apply(simp add:cp_def assum_def nth_append)
prensani@13020
   757
 apply clarify
prensani@13020
   758
 apply(erule_tac x=i in allE)
wenzelm@59189
   759
  back
prensani@13020
   760
 apply(simp add:snd_lift)
prensani@13020
   761
 apply(erule mp)
berghofe@23746
   762
 apply(force elim:etranE intro:Env simp add:lift_def)
prensani@13020
   763
apply simp
prensani@13020
   764
apply clarify
prensani@13020
   765
apply(erule_tac x="snd(xs!m)" in allE)
prensani@13020
   766
apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
prensani@13020
   767
 apply(case_tac "xs\<noteq>[]")
nipkow@17588
   768
 apply(drule last_conv_nth,simp)
prensani@13020
   769
 apply(rule conjI)
prensani@13020
   770
  apply(erule mp)
prensani@13020
   771
  apply(case_tac "xs!m")
prensani@13020
   772
  apply(case_tac "fst(xs!m)",simp)
prensani@13020
   773
  apply(simp add:lift_def nth_append)
prensani@13020
   774
 apply clarify
prensani@13020
   775
 apply(erule_tac x="m+i" in allE)
prensani@13020
   776
 back
prensani@13020
   777
 back
prensani@13020
   778
 apply(case_tac ys,(simp add:nth_append)+)
prensani@13020
   779
 apply (case_tac i, (simp add:snd_lift)+)
prensani@13020
   780
  apply(erule mp)
prensani@13020
   781
  apply(case_tac "xs!m")
berghofe@23746
   782
  apply(force elim:etran.cases intro:Env simp add:lift_def)
wenzelm@59189
   783
 apply simp
prensani@13020
   784
apply simp
prensani@13020
   785
apply clarify
prensani@13020
   786
apply(rule conjI,clarify)
prensani@13020
   787
 apply(case_tac "i<m",simp add:nth_append)
prensani@13020
   788
  apply(simp add:snd_lift)
prensani@13020
   789
  apply(erule allE, erule impE, assumption, erule mp)
prensani@13020
   790
  apply(case_tac "(xs ! i)")
wenzelm@59189
   791
  apply(case_tac "(xs ! Suc i)")
wenzelm@59189
   792
  apply(case_tac "fst(xs ! i)",force simp add:lift_def)
prensani@13020
   793
  apply(case_tac "fst(xs ! Suc i)")
prensani@13020
   794
   apply (force simp add:lift_def)
prensani@13020
   795
  apply (force simp add:lift_def)
wenzelm@59189
   796
 apply(erule_tac x="i-m" in allE)
prensani@13020
   797
 back
prensani@13020
   798
 back
prensani@13020
   799
 apply(subgoal_tac "Suc (i - m) < length ys",simp)
prensani@13020
   800
  prefer 2
prensani@13020
   801
  apply arith
prensani@13020
   802
 apply(simp add:nth_append snd_lift)
prensani@13020
   803
 apply(rule conjI,clarify)
prensani@13020
   804
  apply(subgoal_tac "i=m")
prensani@13020
   805
   prefer 2
prensani@13020
   806
   apply arith
prensani@13020
   807
  apply clarify
prensani@13020
   808
  apply(simp add:cp_def)
prensani@13020
   809
  apply(rule tl_zero)
prensani@13020
   810
    apply(erule mp)
prensani@13020
   811
    apply(case_tac "lift Q (xs!m)",simp add:snd_lift)
prensani@13020
   812
    apply(case_tac "xs!m",case_tac "fst(xs!m)",simp add:lift_def snd_lift)
prensani@13020
   813
     apply(case_tac ys,simp+)
prensani@13020
   814
    apply(simp add:lift_def)
wenzelm@59189
   815
   apply simp
prensani@13020
   816
  apply force
prensani@13020
   817
 apply clarify
prensani@13020
   818
 apply(rule tl_zero)
prensani@13020
   819
   apply(rule tl_zero)
prensani@13020
   820
     apply (subgoal_tac "i-m=Suc(i-Suc m)")
prensani@13020
   821
      apply simp
prensani@13020
   822
      apply(erule mp)
prensani@13020
   823
      apply(case_tac ys,simp+)
prensani@13020
   824
   apply force
prensani@13020
   825
  apply arith
prensani@13020
   826
 apply force
prensani@13020
   827
apply clarify
prensani@13020
   828
apply(case_tac "(map (lift Q) xs @ tl ys)\<noteq>[]")
nipkow@17588
   829
 apply(drule last_conv_nth)
prensani@13020
   830
 apply(simp add: snd_lift nth_append)
prensani@13020
   831
 apply(rule conjI,clarify)
prensani@13020
   832
  apply(case_tac ys,simp+)
prensani@13020
   833
 apply clarify
prensani@13020
   834
 apply(case_tac ys,simp+)
prensani@13020
   835
done
prensani@13020
   836
wenzelm@59189
   837
subsubsection\<open>Soundness of the While rule\<close>
prensani@13020
   838
prensani@13020
   839
lemma last_append[rule_format]:
prensani@13020
   840
  "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
prensani@13020
   841
apply(induct ys)
prensani@13020
   842
 apply simp
prensani@13020
   843
apply clarify
wenzelm@52597
   844
apply (simp add:nth_append)
prensani@13020
   845
done
prensani@13020
   846
wenzelm@59189
   847
lemma assum_after_body:
wenzelm@59189
   848
  "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre];
prensani@13020
   849
  (Some P, s) # xs \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b;
wenzelm@59189
   850
  (Some (While b P), s) # (Some (Seq P (While b P)), s) #
prensani@13022
   851
   map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
prensani@13020
   852
  \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> assum (pre, rely)"
prensani@13020
   853
apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
prensani@13020
   854
apply clarify
prensani@13020
   855
apply(erule_tac x=s in allE)
prensani@13020
   856
apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
prensani@13020
   857
 apply clarify
prensani@13020
   858
 apply(erule_tac x="Suc i" in allE)
prensani@13020
   859
 apply simp
blanchet@55465
   860
 apply(simp add:Cons_lift_append nth_append snd_lift del:list.map)
prensani@13020
   861
 apply(erule mp)
berghofe@23746
   862
 apply(erule etranE,simp)
prensani@13020
   863
 apply(case_tac "fst(((Some P, s) # xs) ! i)")
prensani@13020
   864
  apply(force intro:Env simp add:lift_def)
prensani@13020
   865
 apply(force intro:Env simp add:lift_def)
prensani@13020
   866
apply(rule conjI)
prensani@13020
   867
 apply clarify
prensani@13020
   868
 apply(simp add:comm_def last_length)
prensani@13020
   869
apply clarify
prensani@13020
   870
apply(rule conjI)
prensani@13020
   871
 apply(simp add:comm_def)
prensani@13020
   872
apply clarify
prensani@13020
   873
apply(erule_tac x="Suc(length xs + i)" in allE,simp)
nipkow@41842
   874
apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
nipkow@41842
   875
apply(simp add:Cons_lift_append nth_append snd_lift)
prensani@13020
   876
done
prensani@13020
   877
wenzelm@59189
   878
lemma While_sound_aux [rule_format]:
prensani@13020
   879
  "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
wenzelm@59189
   880
   stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk>
prensani@13020
   881
  \<Longrightarrow>  \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"
prensani@13020
   882
apply(erule cptn_mod.induct)
prensani@13020
   883
apply safe
prensani@13020
   884
apply (simp_all del:last.simps)
wenzelm@67443
   885
\<comment> \<open>5 subgoals left\<close>
prensani@13020
   886
apply(simp add:comm_def)
wenzelm@67443
   887
\<comment> \<open>4 subgoals left\<close>
prensani@13020
   888
apply(rule etran_in_comm)
prensani@13020
   889
apply(erule mp)
prensani@13020
   890
apply(erule tl_of_assum_in_assum,simp)
wenzelm@67443
   891
\<comment> \<open>While-None\<close>
berghofe@23746
   892
apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran" for s t)
prensani@13020
   893
apply(simp add:comm_def)
prensani@13020
   894
apply(simp add:cptn_iff_cptn_mod [THEN sym])
prensani@13020
   895
apply(rule conjI,clarify)
prensani@13020
   896
 apply(force simp add:assum_def)
prensani@13020
   897
apply clarify
prensani@13020
   898
apply(rule conjI, clarify)
prensani@13020
   899
 apply(case_tac i,simp,simp)
prensani@13020
   900
 apply(force simp add:not_ctran_None2)
berghofe@23746
   901
apply(subgoal_tac "\<forall>i. Suc i < length ((None, t) # xs) \<longrightarrow> (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\<in> etran")
prensani@13020
   902
 prefer 2
prensani@13020
   903
 apply clarify
prensani@13020
   904
 apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
prensani@13020
   905
 apply(erule not_ctran_None2,simp)
prensani@13020
   906
 apply simp+
prensani@13020
   907
apply(frule_tac j="0" and k="length ((None, s) # xs) - 1" and p=post in stability,simp+)
prensani@13020
   908
   apply(force simp add:assum_def subsetD)
prensani@13020
   909
  apply(simp add:assum_def)
prensani@13020
   910
  apply clarify
wenzelm@59189
   911
  apply(erule_tac x="i" in allE,simp)
wenzelm@59189
   912
  apply(erule_tac x="Suc i" in allE,simp)
prensani@13020
   913
 apply simp
prensani@13020
   914
apply clarify
prensani@13020
   915
apply (simp add:last_length)
wenzelm@67443
   916
\<comment> \<open>WhileOne\<close>
wenzelm@59807
   917
apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
prensani@13020
   918
apply(rule ctran_in_comm,simp)
blanchet@55465
   919
apply(simp add:Cons_lift del:list.map)
blanchet@55465
   920
apply(simp add:comm_def del:list.map)
prensani@13020
   921
apply(rule conjI)
prensani@13020
   922
 apply clarify
prensani@13020
   923
 apply(case_tac "fst(((Some P, sa) # xs) ! i)")
prensani@13020
   924
  apply(case_tac "((Some P, sa) # xs) ! i")
prensani@13020
   925
  apply (simp add:lift_def)
berghofe@23746
   926
  apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
prensani@13020
   927
   apply simp
prensani@13020
   928
  apply simp
blanchet@55465
   929
 apply(simp add:snd_lift del:list.map)
prensani@13020
   930
 apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
prensani@13020
   931
 apply(erule_tac x=sa in allE)
prensani@13020
   932
 apply(drule_tac c="(Some P, sa) # xs" in subsetD)
blanchet@55465
   933
  apply (simp add:assum_def del:list.map)
prensani@13020
   934
  apply clarify
blanchet@55465
   935
  apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:list.map)
prensani@13020
   936
  apply(erule mp)
prensani@13020
   937
  apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
berghofe@23746
   938
   apply(erule etranE,simp add:lift_def)
prensani@13020
   939
   apply(rule Env)
berghofe@23746
   940
  apply(erule etranE,simp add:lift_def)
prensani@13020
   941
  apply(rule Env)
blanchet@55465
   942
 apply (simp add:comm_def del:list.map)
prensani@13020
   943
 apply clarify
prensani@13020
   944
 apply(erule allE,erule impE,assumption)
prensani@13020
   945
 apply(erule mp)
prensani@13020
   946
 apply(case_tac "((Some P, sa) # xs) ! i")
prensani@13020
   947
 apply(case_tac "xs!i")
prensani@13020
   948
 apply(simp add:lift_def)
prensani@13020
   949
 apply(case_tac "fst(xs!i)")
prensani@13020
   950
  apply force
prensani@13020
   951
 apply force
wenzelm@67443
   952
\<comment> \<open>last=None\<close>
prensani@13020
   953
apply clarify
prensani@13020
   954
apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
nipkow@17588
   955
 apply(drule last_conv_nth)
blanchet@55465
   956
 apply (simp del:list.map)
prensani@13020
   957
 apply(simp only:last_lift_not_None)
prensani@13020
   958
apply simp
wenzelm@67443
   959
\<comment> \<open>WhileMore\<close>
wenzelm@59807
   960
apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
prensani@13020
   961
apply(rule ctran_in_comm,simp del:last.simps)
wenzelm@67443
   962
\<comment> \<open>metiendo la hipotesis antes de dividir la conclusion.\<close>
prensani@13020
   963
apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)")
prensani@13020
   964
 apply (simp del:last.simps)
prensani@13020
   965
 prefer 2
prensani@13020
   966
 apply(erule assum_after_body)
prensani@13020
   967
  apply (simp del:last.simps)+
wenzelm@67443
   968
\<comment> \<open>lo de antes.\<close>
blanchet@55465
   969
apply(simp add:comm_def del:list.map last.simps)
prensani@13020
   970
apply(rule conjI)
prensani@13020
   971
 apply clarify
prensani@13020
   972
 apply(simp only:Cons_lift_append)
prensani@13020
   973
 apply(case_tac "i<length xs")
blanchet@55465
   974
  apply(simp add:nth_append del:list.map last.simps)
prensani@13020
   975
  apply(case_tac "fst(((Some P, sa) # xs) ! i)")
prensani@13020
   976
   apply(case_tac "((Some P, sa) # xs) ! i")
prensani@13020
   977
   apply (simp add:lift_def del:last.simps)
berghofe@23746
   978
   apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
prensani@13020
   979
    apply simp
prensani@13020
   980
   apply simp
blanchet@55465
   981
  apply(simp add:snd_lift del:list.map last.simps)
wenzelm@59807
   982
  apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> P i" for P)
prensani@13020
   983
  apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
prensani@13020
   984
  apply(erule_tac x=sa in allE)
prensani@13020
   985
  apply(drule_tac c="(Some P, sa) # xs" in subsetD)
blanchet@55465
   986
   apply (simp add:assum_def del:list.map last.simps)
prensani@13020
   987
   apply clarify
blanchet@55465
   988
   apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:list.map last.simps, erule mp)
prensani@13020
   989
   apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
berghofe@23746
   990
    apply(erule etranE,simp add:lift_def)
prensani@13020
   991
    apply(rule Env)
berghofe@23746
   992
   apply(erule etranE,simp add:lift_def)
prensani@13020
   993
   apply(rule Env)
blanchet@55465
   994
  apply (simp add:comm_def del:list.map)
prensani@13020
   995
  apply clarify
prensani@13020
   996
  apply(erule allE,erule impE,assumption)
prensani@13020
   997
  apply(erule mp)
prensani@13020
   998
  apply(case_tac "((Some P, sa) # xs) ! i")
prensani@13020
   999
  apply(case_tac "xs!i")
prensani@13020
  1000
  apply(simp add:lift_def)
prensani@13020
  1001
  apply(case_tac "fst(xs!i)")
prensani@13020
  1002
   apply force
prensani@13020
  1003
 apply force
wenzelm@67443
  1004
\<comment> \<open>\<open>i \<ge> length xs\<close>\<close>
wenzelm@59189
  1005
apply(subgoal_tac "i-length xs <length ys")
prensani@13020
  1006
 prefer 2
prensani@13020
  1007
 apply arith
prensani@13020
  1008
apply(erule_tac x="i-length xs" in allE,clarify)
prensani@13020
  1009
apply(case_tac "i=length xs")
blanchet@55465
  1010
 apply (simp add:nth_append snd_lift del:list.map last.simps)
prensani@13020
  1011
 apply(simp add:last_length del:last.simps)
prensani@13020
  1012
 apply(erule mp)
prensani@13020
  1013
 apply(case_tac "last((Some P, sa) # xs)")
prensani@13020
  1014
 apply(simp add:lift_def del:last.simps)
wenzelm@67443
  1015
\<comment> \<open>\<open>i>length xs\<close>\<close>
prensani@13020
  1016
apply(case_tac "i-length xs")
prensani@13020
  1017
 apply arith
blanchet@55465
  1018
apply(simp add:nth_append del:list.map last.simps)
nipkow@13187
  1019
apply(rotate_tac -3)
prensani@13020
  1020
apply(subgoal_tac "i- Suc (length xs)=nat")
prensani@13020
  1021
 prefer 2
prensani@13020
  1022
 apply arith
prensani@13020
  1023
apply simp
wenzelm@67443
  1024
\<comment> \<open>last=None\<close>
prensani@13020
  1025
apply clarify
prensani@13020
  1026
apply(case_tac ys)
blanchet@55465
  1027
 apply(simp add:Cons_lift del:list.map last.simps)
prensani@13020
  1028
 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
nipkow@17588
  1029
  apply(drule last_conv_nth)
blanchet@55465
  1030
  apply (simp del:list.map)
prensani@13020
  1031
  apply(simp only:last_lift_not_None)
prensani@13020
  1032
 apply simp
prensani@13020
  1033
apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)\<noteq>[]")
nipkow@17588
  1034
 apply(drule last_conv_nth)
blanchet@55465
  1035
 apply (simp del:list.map last.simps)
prensani@13020
  1036
 apply(simp add:nth_append del:last.simps)
blanchet@55417
  1037
 apply(rename_tac a list)
prensani@13020
  1038
 apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\<noteq>[]")
nipkow@17588
  1039
  apply(drule last_conv_nth)
blanchet@55465
  1040
  apply (simp del:list.map last.simps)
prensani@13020
  1041
 apply simp
prensani@13020
  1042
apply simp
prensani@13020
  1043
done
prensani@13020
  1044
wenzelm@59189
  1045
lemma While_sound:
prensani@13020
  1046
  "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely;
prensani@13020
  1047
    \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
prensani@13020
  1048
  \<Longrightarrow> \<Turnstile> While b P sat [pre, rely, guar, post]"
prensani@13020
  1049
apply(unfold com_validity_def)
prensani@13020
  1050
apply clarify
prensani@13020
  1051
apply(erule_tac xs="tl x" in While_sound_aux)
prensani@13020
  1052
 apply(simp add:com_validity_def)
prensani@13020
  1053
 apply force
prensani@13020
  1054
 apply simp_all
prensani@13020
  1055
apply(simp add:cptn_iff_cptn_mod cp_def)
prensani@13020
  1056
apply(simp add:cp_def)
prensani@13020
  1057
apply clarify
prensani@13020
  1058
apply(rule nth_equalityI)
prensani@13020
  1059
 apply simp_all
prensani@13020
  1060
 apply(case_tac x,simp+)
prensani@13020
  1061
apply(case_tac i,simp+)
prensani@13020
  1062
apply(case_tac x,simp+)
prensani@13020
  1063
done
prensani@13020
  1064
wenzelm@59189
  1065
subsubsection\<open>Soundness of the Rule of Consequence\<close>
prensani@13020
  1066
wenzelm@59189
  1067
lemma Conseq_sound:
wenzelm@59189
  1068
  "\<lbrakk>pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
prensani@13020
  1069
  \<Turnstile> P sat [pre', rely', guar', post']\<rbrakk>
prensani@13020
  1070
  \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]"
prensani@13020
  1071
apply(simp add:com_validity_def assum_def comm_def)
prensani@13020
  1072
apply clarify
prensani@13020
  1073
apply(erule_tac x=s in allE)
prensani@13020
  1074
apply(drule_tac c=x in subsetD)
prensani@13020
  1075
 apply force
prensani@13020
  1076
apply force
prensani@13020
  1077
done
prensani@13020
  1078
wenzelm@59189
  1079
subsubsection \<open>Soundness of the system for sequential component programs\<close>
prensani@13020
  1080
wenzelm@59189
  1081
theorem rgsound:
prensani@13020
  1082
  "\<turnstile> P sat [pre, rely, guar, post] \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]"
prensani@13020
  1083
apply(erule rghoare.induct)
prensani@13020
  1084
 apply(force elim:Basic_sound)
prensani@13020
  1085
 apply(force elim:Seq_sound)
prensani@13020
  1086
 apply(force elim:Cond_sound)
prensani@13020
  1087
 apply(force elim:While_sound)
prensani@13020
  1088
 apply(force elim:Await_sound)
prensani@13020
  1089
apply(erule Conseq_sound,simp+)
wenzelm@59189
  1090
done
prensani@13020
  1091
wenzelm@59189
  1092
subsection \<open>Soundness of the System for Parallel Programs\<close>
prensani@13020
  1093
haftmann@35416
  1094
definition ParallelCom :: "('a rgformula) list \<Rightarrow> 'a par_com" where
wenzelm@59189
  1095
  "ParallelCom Ps \<equiv> map (Some \<circ> fst) Ps"
prensani@13020
  1096
wenzelm@59189
  1097
lemma two:
wenzelm@59189
  1098
  "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
prensani@13022
  1099
     \<subseteq> Rely (xs ! i);
prensani@13022
  1100
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
wenzelm@59189
  1101
   \<forall>i<length xs.
prensani@13022
  1102
   \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
prensani@13022
  1103
   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
prensani@13020
  1104
  \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
wenzelm@59189
  1105
  \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j)
prensani@13020
  1106
  \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
prensani@13020
  1107
apply(unfold par_cp_def)
wenzelm@59189
  1108
apply (rule ccontr)
wenzelm@67443
  1109
\<comment> \<open>By contradiction:\<close>
wenzelm@52597
  1110
apply simp
prensani@13020
  1111
apply(erule exE)
wenzelm@67443
  1112
\<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>
wenzelm@59807
  1113
apply(drule_tac n=j and P="\<lambda>j. \<exists>i. H i j" for H in Ex_first_occurrence)
prensani@13020
  1114
apply(erule exE)
prensani@13020
  1115
apply clarify
wenzelm@67443
  1116
\<comment> \<open>\<open>\<sigma>_i \<in> A(pre, rely_1)\<close>\<close>
prensani@13020
  1117
apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \<in> assum(Pre(xs!i), Rely(xs!i))")
wenzelm@67443
  1118
\<comment> \<open>but this contradicts \<open>\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]\<close>\<close>
wenzelm@59807
  1119
 apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
prensani@13020
  1120
 apply(simp add:com_validity_def)
prensani@13020
  1121
 apply(erule_tac x=s in allE)
prensani@13020
  1122
 apply(simp add:cp_def comm_def)
prensani@13020
  1123
 apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD)
prensani@13020
  1124
  apply simp
wenzelm@59189
  1125
  apply (blast intro: takecptn_is_cptn)
prensani@13020
  1126
 apply simp
prensani@13020
  1127
 apply clarify
wenzelm@59807
  1128
 apply(erule_tac x=m and P="\<lambda>j. I j \<and> J j \<longrightarrow> H j" for I J H in allE)
prensani@13020
  1129
 apply (simp add:conjoin_def same_length_def)
wenzelm@52597
  1130
apply(simp add:assum_def)
prensani@13020
  1131
apply(rule conjI)
wenzelm@59807
  1132
 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> I j \<in>cp (K j) (J j)" for H I K J in allE)
prensani@13020
  1133
 apply(simp add:cp_def par_assum_def)
prensani@13020
  1134
 apply(drule_tac c="s" in subsetD,simp)
prensani@13020
  1135
 apply simp
prensani@13020
  1136
apply clarify
haftmann@69313
  1137
apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> M \<union> \<Union>((T j) ` (S j)) \<subseteq> (L j)" for H M S T L in allE)
wenzelm@52597
  1138
apply simp
prensani@13020
  1139
apply(erule subsetD)
prensani@13020
  1140
apply simp
prensani@13020
  1141
apply(simp add:conjoin_def compat_label_def)
prensani@13020
  1142
apply clarify
wenzelm@59807
  1143
apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (P j) \<or> Q j" for H P Q in allE,simp)
wenzelm@67443
  1144
\<comment> \<open>each etran in \<open>\<sigma>_1[0\<dots>m]\<close> corresponds to\<close>
prensani@13020
  1145
apply(erule disjE)
wenzelm@67443
  1146
\<comment> \<open>a c-tran in some \<open>\<sigma>_{ib}\<close>\<close>
prensani@13020
  1147
 apply clarify
prensani@13020
  1148
 apply(case_tac "i=ib",simp)
berghofe@23746
  1149
  apply(erule etranE,simp)
wenzelm@59807
  1150
 apply(erule_tac x="ib" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE)
berghofe@23746
  1151
 apply (erule etranE)
prensani@13020
  1152
 apply(case_tac "ia=m",simp)
berghofe@13601
  1153
 apply simp
wenzelm@59807
  1154
 apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (\<forall>i. P i j)" for H P in allE)
prensani@13020
  1155
 apply(subgoal_tac "ia<m",simp)
prensani@13020
  1156
  prefer 2
prensani@13020
  1157
  apply arith
wenzelm@59807
  1158
 apply(erule_tac x=ib and P="\<lambda>j. (I j, H j) \<in> ctran \<longrightarrow> P i j" for I H P in allE,simp)
prensani@13020
  1159
 apply(simp add:same_state_def)
wenzelm@59807
  1160
 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)))" for T H d e in all_dupE)
wenzelm@59807
  1161
 apply(erule_tac x=ib and P="\<lambda>j. (T j) \<longrightarrow> (\<forall>i. (H j i) \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
wenzelm@67443
  1162
\<comment> \<open>or an e-tran in \<open>\<sigma>\<close>,
wenzelm@62042
  1163
therefore it satisfies \<open>rely \<or> guar_{ib}\<close>\<close>
prensani@13020
  1164
apply (force simp add:par_assum_def same_state_def)
prensani@13020
  1165
done
prensani@13020
  1166
paulson@15102
  1167
wenzelm@59189
  1168
lemma three [rule_format]:
wenzelm@59189
  1169
  "\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
prensani@13022
  1170
   \<subseteq> Rely (xs ! i);
prensani@13022
  1171
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
wenzelm@59189
  1172
   \<forall>i<length xs.
prensani@13022
  1173
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
prensani@13022
  1174
   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum(pre, rely);
prensani@13020
  1175
  \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
wenzelm@59189
  1176
  \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -e\<rightarrow> (clist!i!Suc j)
prensani@13020
  1177
  \<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))"
prensani@13020
  1178
apply(drule two)
prensani@13020
  1179
 apply simp_all
prensani@13020
  1180
apply clarify
prensani@13020
  1181
apply(simp add:conjoin_def compat_label_def)
prensani@13020
  1182
apply clarify
wenzelm@59807
  1183
apply(erule_tac x=j and P="\<lambda>j. H j \<longrightarrow> (J j \<and> (\<exists>i. P i j)) \<or> I j" for H J P I in allE,simp)
prensani@13020
  1184
apply(erule disjE)
prensani@13020
  1185
 prefer 2
prensani@13020
  1186
 apply(force simp add:same_state_def par_assum_def)
prensani@13020
  1187
apply clarify
prensani@13020
  1188
apply(case_tac "i=ia",simp)
berghofe@23746
  1189
 apply(erule etranE,simp)
wenzelm@59807
  1190
apply(erule_tac x="ia" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE,simp)
wenzelm@59807
  1191
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" for S I H P in allE)
wenzelm@59807
  1192
apply(erule_tac x=ia and P="\<lambda>j. S j \<longrightarrow> (I j, H j) \<in> ctran \<longrightarrow> P j" for S I H P in allE)
prensani@13020
  1193
apply(simp add:same_state_def)
wenzelm@59807
  1194
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)))" for T H d e in all_dupE)
wenzelm@59807
  1195
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)))" for T H d e in allE,simp)
prensani@13020
  1196
done
prensani@13020
  1197
wenzelm@59189
  1198
lemma four:
wenzelm@59189
  1199
  "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
prensani@13022
  1200
    \<subseteq> Rely (xs ! i);
wenzelm@59189
  1201
   (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar;
prensani@13022
  1202
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
prensani@13022
  1203
   \<forall>i < length xs.
prensani@13022
  1204
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
wenzelm@59189
  1205
   x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x;
prensani@13022
  1206
   x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
prensani@13020
  1207
  \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
wenzelm@52597
  1208
apply(simp add: ParallelCom_def)
prensani@13020
  1209
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
prensani@13020
  1210
 prefer 2
prensani@13020
  1211
 apply simp
prensani@13020
  1212
apply(frule rev_subsetD)
prensani@13020
  1213
 apply(erule one [THEN equalityD1])
prensani@13020
  1214
apply(erule subsetD)
wenzelm@52597
  1215
apply simp
prensani@13020
  1216
apply clarify
prensani@13020
  1217
apply(drule_tac pre=pre and rely=rely and  x=x and s=s and xs=xs and clist=clist in two)
prensani@13020
  1218
apply(assumption+)
prensani@13020
  1219
     apply(erule sym)
prensani@13020
  1220
    apply(simp add:ParallelCom_def)
prensani@13020
  1221
   apply assumption
prensani@13020
  1222
  apply(simp add:Com_def)
prensani@13020
  1223
 apply assumption
prensani@13020
  1224
apply(simp add:conjoin_def same_program_def)
prensani@13020
  1225
apply clarify
wenzelm@59807
  1226
apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in all_dupE)
wenzelm@59807
  1227
apply(erule_tac x="Suc i" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
berghofe@23746
  1228
apply(erule par_ctranE,simp)
wenzelm@59807
  1229
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" for S I H P in allE)
wenzelm@59807
  1230
apply(erule_tac x=ia and P="\<lambda>j. S j \<longrightarrow> (I j, H j) \<in> ctran \<longrightarrow> P j" for S I H P in allE)
prensani@13020
  1231
apply(rule_tac x=ia in exI)
prensani@13020
  1232
apply(simp add:same_state_def)
wenzelm@59807
  1233
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)))" for T H d e in all_dupE,simp)
wenzelm@59807
  1234
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)))" for T H d e in allE,simp)
wenzelm@59807
  1235
apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in all_dupE)
wenzelm@59807
  1236
apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in all_dupE,simp)
wenzelm@59807
  1237
apply(erule_tac x="Suc i" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
prensani@13020
  1238
apply(erule mp)
prensani@13020
  1239
apply(subgoal_tac "r=fst(clist ! ia ! Suc i)",simp)
prensani@13020
  1240
apply(drule_tac i=ia in list_eq_if)
prensani@13020
  1241
back
prensani@13020
  1242
apply simp_all
prensani@13020
  1243
done
prensani@13020
  1244
prensani@13020
  1245
lemma parcptn_not_empty [simp]:"[] \<notin> par_cptn"
berghofe@23746
  1246
apply(force elim:par_cptn.cases)
prensani@13020
  1247
done
prensani@13020
  1248
wenzelm@59189
  1249
lemma five:
prensani@13022
  1250
  "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
prensani@13022
  1251
   \<subseteq> Rely (xs ! i);
wenzelm@59189
  1252
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
prensani@13022
  1253
   (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
prensani@13022
  1254
   \<forall>i < length xs.
prensani@13022
  1255
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
wenzelm@59189
  1256
    x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely);
prensani@13022
  1257
   All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
wenzelm@52597
  1258
apply(simp add: ParallelCom_def)
prensani@13020
  1259
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
prensani@13020
  1260
 prefer 2
prensani@13020
  1261
 apply simp
prensani@13020
  1262
apply(frule rev_subsetD)
prensani@13020
  1263
 apply(erule one [THEN equalityD1])
prensani@13020
  1264
apply(erule subsetD)
wenzelm@52597
  1265
apply simp
prensani@13020
  1266
apply clarify
prensani@13020
  1267
apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
haftmann@62343
  1268
 apply(erule_tac x=xa and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
prensani@13020
  1269
 apply(simp add:com_validity_def)
prensani@13020
  1270
 apply(erule_tac x=s in allE)
haftmann@62343
  1271
 apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp)
haftmann@62343
  1272
 apply(drule_tac c="clist!xa" in subsetD)
prensani@13020
  1273
  apply (force simp add:Com_def)
prensani@13020
  1274
 apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
prensani@13020
  1275
 apply clarify
wenzelm@59807
  1276
 apply(erule_tac x="length x - 1" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
prensani@13020
  1277
 apply (simp add:All_None_def same_length_def)
haftmann@62343
  1278
 apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
prensani@13020
  1279
 apply(subgoal_tac "length x - 1 < length x",simp)
prensani@13020
  1280
  apply(case_tac "x\<noteq>[]")
nipkow@17588
  1281
   apply(simp add: last_conv_nth)
haftmann@62343
  1282
   apply(erule_tac x="clist!xa" in ballE)
prensani@13020
  1283
    apply(simp add:same_state_def)
haftmann@62343
  1284
    apply(subgoal_tac "clist!xa\<noteq>[]")
nipkow@17588
  1285
     apply(simp add: last_conv_nth)
prensani@13020
  1286
    apply(case_tac x)
prensani@13020
  1287
     apply (force simp add:par_cp_def)
prensani@13020
  1288
    apply (force simp add:par_cp_def)
prensani@13020
  1289
   apply force
prensani@13020
  1290
  apply (force simp add:par_cp_def)
prensani@13020
  1291
 apply(case_tac x)
prensani@13020
  1292
  apply (force simp add:par_cp_def)
prensani@13020
  1293
 apply (force simp add:par_cp_def)
prensani@13020
  1294
apply clarify
prensani@13020
  1295
apply(simp add:assum_def)
prensani@13020
  1296
apply(rule conjI)
prensani@13020
  1297
 apply(simp add:conjoin_def same_state_def par_cp_def)
prensani@13020
  1298
 apply clarify
haftmann@62343
  1299
 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)))" for T H d e in allE,simp)
wenzelm@59807
  1300
 apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
prensani@13020
  1301
 apply(case_tac x,simp+)
prensani@13020
  1302
 apply (simp add:par_assum_def)
prensani@13020
  1303
 apply clarify
haftmann@62343
  1304
 apply(drule_tac c="snd (clist ! i ! 0)" in subsetD)
prensani@13020
  1305
 apply assumption
prensani@13020
  1306
 apply simp
prensani@13020
  1307
apply clarify
haftmann@62343
  1308
apply(erule_tac x=i in all_dupE)
berghofe@13601
  1309
apply(rule subsetD, erule mp, assumption)
prensani@13020
  1310
apply(erule_tac pre=pre and rely=rely and x=x and s=s in  three)
haftmann@62343
  1311
 apply(erule_tac x=ib in allE,erule mp)
prensani@13020
  1312
 apply simp_all
prensani@13020
  1313
 apply(simp add:ParallelCom_def)
prensani@13020
  1314
 apply(force simp add:Com_def)
prensani@13020
  1315
apply(simp add:conjoin_def same_length_def)
prensani@13020
  1316
done
prensani@13020
  1317
wenzelm@59189
  1318
lemma ParallelEmpty [rule_format]:
wenzelm@59189
  1319
  "\<forall>i s. x \<in> par_cp (ParallelCom []) s \<longrightarrow>
prensani@13020
  1320
  Suc i < length x \<longrightarrow> (x ! i, x ! Suc i) \<notin> par_ctran"
prensani@13020
  1321
apply(induct_tac x)
prensani@13020
  1322
 apply(simp add:par_cp_def ParallelCom_def)
prensani@13020
  1323
apply clarify
prensani@13020
  1324
apply(case_tac list,simp,simp)
prensani@13020
  1325
apply(case_tac i)
prensani@13020
  1326
 apply(simp add:par_cp_def ParallelCom_def)
berghofe@23746
  1327
 apply(erule par_ctranE,simp)
prensani@13020
  1328
apply(simp add:par_cp_def ParallelCom_def)
prensani@13020
  1329
apply clarify
berghofe@23746
  1330
apply(erule par_cptn.cases,simp)
prensani@13020
  1331
 apply simp
berghofe@23746
  1332
apply(erule par_ctranE)
prensani@13020
  1333
back
prensani@13020
  1334
apply simp
prensani@13020
  1335
done
prensani@13020
  1336
wenzelm@59189
  1337
theorem par_rgsound:
wenzelm@59189
  1338
  "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow>
prensani@13022
  1339
   \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]"
prensani@13020
  1340
apply(erule par_rghoare.induct)
prensani@13020
  1341
apply(case_tac xs,simp)
prensani@13020
  1342
 apply(simp add:par_com_validity_def par_comm_def)
prensani@13020
  1343
 apply clarify
prensani@13020
  1344
 apply(case_tac "post=UNIV",simp)
prensani@13020
  1345
  apply clarify
prensani@13020
  1346
  apply(drule ParallelEmpty)
prensani@13020
  1347
   apply assumption
prensani@13020
  1348
  apply simp
prensani@13020
  1349
 apply clarify
prensani@13020
  1350
 apply simp
prensani@13020
  1351
apply(subgoal_tac "xs\<noteq>[]")
prensani@13020
  1352
 prefer 2
prensani@13020
  1353
 apply simp
blanchet@55417
  1354
apply(rename_tac a list)
prensani@13020
  1355
apply(thin_tac "xs = a # list")
prensani@13020
  1356
apply(simp add:par_com_validity_def par_comm_def)
prensani@13020
  1357
apply clarify
prensani@13020
  1358
apply(rule conjI)
prensani@13020
  1359
 apply clarify
prensani@13020
  1360
 apply(erule_tac pre=pre and rely=rely and guar=guar and x=x and s=s and xs=xs in four)
prensani@13020
  1361
        apply(assumption+)
prensani@13020
  1362
     apply clarify
prensani@13020
  1363
     apply (erule allE, erule impE, assumption,erule rgsound)
prensani@13020
  1364
    apply(assumption+)
prensani@13020
  1365
apply clarify
prensani@13020
  1366
apply(erule_tac pre=pre and rely=rely and post=post and x=x and s=s and xs=xs in five)
prensani@13020
  1367
      apply(assumption+)
prensani@13020
  1368
   apply clarify
prensani@13020
  1369
   apply (erule allE, erule impE, assumption,erule rgsound)
wenzelm@59189
  1370
  apply(assumption+)
prensani@13020
  1371
done
prensani@13020
  1372
nipkow@13187
  1373
end