src/HOL/Hoare_Parallel/OG_Hoare.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62390 842917225d56
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@59189
     1
section \<open>The Proof System\<close>
prensani@13020
     2
haftmann@16417
     3
theory OG_Hoare imports OG_Tran begin
prensani@13020
     4
haftmann@39246
     5
primrec assertions :: "'a ann_com \<Rightarrow> ('a assn) set" where
prensani@13020
     6
  "assertions (AnnBasic r f) = {r}"
haftmann@39246
     7
| "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
haftmann@39246
     8
| "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
haftmann@39246
     9
| "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
haftmann@39246
    10
| "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
wenzelm@59189
    11
| "assertions (AnnAwait r b c) = {r}"
prensani@13020
    12
haftmann@39246
    13
primrec atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set" where
prensani@13020
    14
  "atomics (AnnBasic r f) = {(r, Basic f)}"
haftmann@39246
    15
| "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
haftmann@39246
    16
| "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
haftmann@39246
    17
| "atomics (AnnCond2 r b c) = atomics c"
wenzelm@59189
    18
| "atomics (AnnWhile r b i c) = atomics c"
haftmann@39246
    19
| "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
prensani@13020
    20
haftmann@39246
    21
primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
haftmann@39246
    22
  "com (c, q) = c"
prensani@13020
    23
haftmann@39246
    24
primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where
haftmann@39246
    25
  "post (c, q) = q"
prensani@13020
    26
haftmann@35416
    27
definition interfree_aux :: "('a ann_com_op \<times> 'a assn \<times> 'a ann_com_op) \<Rightarrow> bool" where
wenzelm@59189
    28
  "interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or>
prensani@13020
    29
                    (\<forall>(r,a) \<in> atomics (the co'). \<parallel>= (q \<inter> r) a q \<and>
prensani@13020
    30
                    (co = None \<or> (\<forall>p \<in> assertions (the co). \<parallel>= (p \<inter> r) a p)))"
prensani@13020
    31
wenzelm@59189
    32
definition interfree :: "(('a ann_triple_op) list) \<Rightarrow> bool" where
wenzelm@59189
    33
  "interfree Ts \<equiv> \<forall>i j. i < length Ts \<and> j < length Ts \<and> i \<noteq> j \<longrightarrow>
prensani@13020
    34
                         interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) "
prensani@13020
    35
berghofe@23746
    36
inductive
berghofe@23746
    37
  oghoare :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(3\<parallel>- _//_//_)" [90,55,90] 50)
berghofe@23746
    38
  and ann_hoare :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(2\<turnstile> _// _)" [60,90] 45)
berghofe@23746
    39
where
prensani@13020
    40
  AnnBasic: "r \<subseteq> {s. f s \<in> q} \<Longrightarrow> \<turnstile> (AnnBasic r f) q"
prensani@13020
    41
berghofe@23746
    42
| AnnSeq:   "\<lbrakk> \<turnstile> c0 pre c1; \<turnstile> c1 q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnSeq c0 c1) q"
wenzelm@59189
    43
wenzelm@59189
    44
| AnnCond1: "\<lbrakk> r \<inter> b \<subseteq> pre c1; \<turnstile> c1 q; r \<inter> -b \<subseteq> pre c2; \<turnstile> c2 q\<rbrakk>
prensani@13020
    45
              \<Longrightarrow> \<turnstile> (AnnCond1 r b c1 c2) q"
berghofe@23746
    46
| AnnCond2: "\<lbrakk> r \<inter> b \<subseteq> pre c; \<turnstile> c q; r \<inter> -b \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnCond2 r b c) q"
wenzelm@59189
    47
wenzelm@59189
    48
| AnnWhile: "\<lbrakk> r \<subseteq> i; i \<inter> b \<subseteq> pre c; \<turnstile> c i; i \<inter> -b \<subseteq> q \<rbrakk>
prensani@13020
    49
              \<Longrightarrow> \<turnstile> (AnnWhile r b i c) q"
wenzelm@59189
    50
berghofe@23746
    51
| AnnAwait:  "\<lbrakk> atom_com c; \<parallel>- (r \<inter> b) c q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b c) q"
wenzelm@59189
    52
berghofe@23746
    53
| AnnConseq: "\<lbrakk>\<turnstile> c q; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<turnstile> c q'"
prensani@13020
    54
prensani@13020
    55
berghofe@23746
    56
| Parallel: "\<lbrakk> \<forall>i<length Ts. \<exists>c q. Ts!i = (Some c, q) \<and> \<turnstile> c q; interfree Ts \<rbrakk>
wenzelm@59189
    57
           \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i))))
wenzelm@59189
    58
                     Parallel Ts
prensani@13020
    59
                  (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"
prensani@13020
    60
berghofe@23746
    61
| Basic:   "\<parallel>- {s. f s \<in>q} (Basic f) q"
wenzelm@59189
    62
berghofe@23746
    63
| Seq:    "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q "
prensani@13020
    64
berghofe@23746
    65
| Cond:   "\<lbrakk> \<parallel>- (p \<inter> b) c1 q; \<parallel>- (p \<inter> -b) c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q"
prensani@13020
    66
berghofe@23746
    67
| While:  "\<lbrakk> \<parallel>- (p \<inter> b) c p \<rbrakk> \<Longrightarrow> \<parallel>- p (While b i c) (p \<inter> -b)"
prensani@13020
    68
berghofe@23746
    69
| Conseq: "\<lbrakk> p' \<subseteq> p; \<parallel>- p c q ; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<parallel>- p' c q'"
wenzelm@32960
    70
wenzelm@59189
    71
section \<open>Soundness\<close>
prensani@13020
    72
(* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE
prensani@13020
    73
parts of conditional expressions (if P then x else y) are no longer
prensani@13020
    74
simplified.  (This allows the simplifier to unfold recursive
prensani@13020
    75
functional programs.)  To restore the old behaviour, we declare
prensani@13020
    76
@{text "lemmas [cong del] = if_weak_cong"}. *)
prensani@13020
    77
prensani@13020
    78
lemmas [cong del] = if_weak_cong
prensani@13020
    79
prensani@13020
    80
lemmas ann_hoare_induct = oghoare_ann_hoare.induct [THEN conjunct2]
prensani@13020
    81
lemmas oghoare_induct = oghoare_ann_hoare.induct [THEN conjunct1]
prensani@13020
    82
prensani@13020
    83
lemmas AnnBasic = oghoare_ann_hoare.AnnBasic
prensani@13020
    84
lemmas AnnSeq = oghoare_ann_hoare.AnnSeq
prensani@13020
    85
lemmas AnnCond1 = oghoare_ann_hoare.AnnCond1
prensani@13020
    86
lemmas AnnCond2 = oghoare_ann_hoare.AnnCond2
prensani@13020
    87
lemmas AnnWhile = oghoare_ann_hoare.AnnWhile
prensani@13020
    88
lemmas AnnAwait = oghoare_ann_hoare.AnnAwait
prensani@13020
    89
lemmas AnnConseq = oghoare_ann_hoare.AnnConseq
prensani@13020
    90
prensani@13020
    91
lemmas Parallel = oghoare_ann_hoare.Parallel
prensani@13020
    92
lemmas Basic = oghoare_ann_hoare.Basic
prensani@13020
    93
lemmas Seq = oghoare_ann_hoare.Seq
prensani@13020
    94
lemmas Cond = oghoare_ann_hoare.Cond
prensani@13020
    95
lemmas While = oghoare_ann_hoare.While
prensani@13020
    96
lemmas Conseq = oghoare_ann_hoare.Conseq
prensani@13020
    97
wenzelm@59189
    98
subsection \<open>Soundness of the System for Atomic Programs\<close>
prensani@13020
    99
wenzelm@59189
   100
lemma Basic_ntran [rule_format]:
prensani@13020
   101
 "(Basic f, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow> t = f s"
prensani@13020
   102
apply(induct "n")
prensani@13020
   103
 apply(simp (no_asm))
bulwahn@46362
   104
apply(fast dest: relpow_Suc_D2 Parallel_empty_lemma elim: transition_cases)
prensani@13020
   105
done
prensani@13020
   106
prensani@13020
   107
lemma SEM_fwhile: "SEM S (p \<inter> b) \<subseteq> p \<Longrightarrow> SEM (fwhile b S k) p \<subseteq> (p \<inter> -b)"
prensani@13020
   108
apply (induct "k")
prensani@13020
   109
 apply(simp (no_asm) add: L3_5v_lemma3)
prensani@13020
   110
apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty)
paulson@15102
   111
apply(rule conjI)
wenzelm@59189
   112
 apply (blast dest: L3_5i)
prensani@13020
   113
apply(simp add: SEM_def sem_def id_def)
haftmann@62343
   114
apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow)
haftmann@62343
   115
apply blast
prensani@13020
   116
done
prensani@13020
   117
wenzelm@59189
   118
lemma atom_hoare_sound [rule_format]:
prensani@13020
   119
 " \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q"
prensani@13020
   120
apply (unfold com_validity_def)
prensani@13020
   121
apply(rule oghoare_induct)
prensani@13020
   122
apply simp_all
wenzelm@62042
   123
\<comment>\<open>Basic\<close>
prensani@13020
   124
    apply(simp add: SEM_def sem_def)
bulwahn@46362
   125
    apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran)
wenzelm@62042
   126
\<comment>\<open>Seq\<close>
prensani@13020
   127
   apply(rule impI)
prensani@13020
   128
   apply(rule subset_trans)
prensani@13020
   129
    prefer 2 apply simp
prensani@13020
   130
   apply(simp add: L3_5ii L3_5i)
wenzelm@62042
   131
\<comment>\<open>Cond\<close>
prensani@13020
   132
  apply(simp add: L3_5iv)
wenzelm@62042
   133
\<comment>\<open>While\<close>
wenzelm@59189
   134
 apply (force simp add: L3_5v dest: SEM_fwhile)
wenzelm@62042
   135
\<comment>\<open>Conseq\<close>
paulson@15102
   136
apply(force simp add: SEM_def sem_def)
prensani@13020
   137
done
wenzelm@59189
   138
wenzelm@59189
   139
subsection \<open>Soundness of the System for Component Programs\<close>
prensani@13020
   140
prensani@13020
   141
inductive_cases ann_transition_cases:
berghofe@23746
   142
    "(None,s) -1\<rightarrow> (c', s')"
berghofe@23746
   143
    "(Some (AnnBasic r f),s) -1\<rightarrow> (c', s')"
berghofe@23746
   144
    "(Some (AnnSeq c1 c2), s) -1\<rightarrow> (c', s')"
berghofe@23746
   145
    "(Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (c', s')"
berghofe@23746
   146
    "(Some (AnnCond2 r b c), s) -1\<rightarrow> (c', s')"
berghofe@23746
   147
    "(Some (AnnWhile r b I c), s) -1\<rightarrow> (c', s')"
berghofe@23746
   148
    "(Some (AnnAwait r b c),s) -1\<rightarrow> (c', s')"
prensani@13020
   149
wenzelm@59189
   150
text \<open>Strong Soundness for Component Programs:\<close>
prensani@13020
   151
wenzelm@46008
   152
lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow>
wenzelm@59189
   153
  ((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
wenzelm@59189
   154
  (\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
wenzelm@59189
   155
  (\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
wenzelm@59189
   156
  r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and>
wenzelm@59189
   157
  (\<forall>r b c. C = AnnCond2 r b c \<longrightarrow>
wenzelm@59189
   158
  (\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c  \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and>
wenzelm@59189
   159
  (\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
wenzelm@59189
   160
  (\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and>
prensani@13020
   161
  (\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))"
prensani@13020
   162
apply(rule ann_hoare_induct)
wenzelm@46008
   163
apply simp_all
prensani@13020
   164
 apply(rule_tac x=q in exI,simp)+
prensani@13020
   165
apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
prensani@13020
   166
apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
prensani@13020
   167
done
prensani@13020
   168
berghofe@23746
   169
lemma Help: "(transition \<inter> {(x,y). True}) = (transition)"
prensani@13020
   170
apply force
prensani@13020
   171
done
prensani@13020
   172
wenzelm@59189
   173
lemma Strong_Soundness_aux_aux [rule_format]:
wenzelm@59189
   174
 "(co, s) -1\<rightarrow> (co', t) \<longrightarrow> (\<forall>c. co = Some c \<longrightarrow> s\<in> pre c \<longrightarrow>
prensani@13020
   175
 (\<forall>q. \<turnstile> c q \<longrightarrow> (if co' = None then t\<in>q else t \<in> pre(the co') \<and> \<turnstile> (the co') q )))"
prensani@13020
   176
apply(rule ann_transition_transition.induct [THEN conjunct1])
wenzelm@59189
   177
apply simp_all
wenzelm@62042
   178
\<comment>\<open>Basic\<close>
prensani@13020
   179
         apply clarify
prensani@13020
   180
         apply(frule ann_hoare_case_analysis)
prensani@13020
   181
         apply force
wenzelm@62042
   182
\<comment>\<open>Seq\<close>
prensani@13020
   183
        apply clarify
prensani@13020
   184
        apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   185
        apply(fast intro: AnnConseq)
prensani@13020
   186
       apply clarify
prensani@13020
   187
       apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   188
       apply clarify
prensani@13020
   189
       apply(rule conjI)
prensani@13020
   190
        apply force
prensani@13020
   191
       apply(rule AnnSeq,simp)
prensani@13020
   192
       apply(fast intro: AnnConseq)
wenzelm@62042
   193
\<comment>\<open>Cond1\<close>
prensani@13020
   194
      apply clarify
prensani@13020
   195
      apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   196
      apply(fast intro: AnnConseq)
prensani@13020
   197
     apply clarify
prensani@13020
   198
     apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   199
     apply(fast intro: AnnConseq)
wenzelm@62042
   200
\<comment>\<open>Cond2\<close>
prensani@13020
   201
    apply clarify
prensani@13020
   202
    apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   203
    apply(fast intro: AnnConseq)
prensani@13020
   204
   apply clarify
prensani@13020
   205
   apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   206
   apply(fast intro: AnnConseq)
wenzelm@62042
   207
\<comment>\<open>While\<close>
prensani@13020
   208
  apply clarify
prensani@13020
   209
  apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   210
  apply force
prensani@13020
   211
 apply clarify
prensani@13020
   212
 apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   213
 apply auto
prensani@13020
   214
 apply(rule AnnSeq)
prensani@13020
   215
  apply simp
prensani@13020
   216
 apply(rule AnnWhile)
prensani@13020
   217
  apply simp_all
wenzelm@62042
   218
\<comment>\<open>Await\<close>
prensani@13020
   219
apply(frule ann_hoare_case_analysis,simp)
prensani@13020
   220
apply clarify
prensani@13020
   221
apply(drule atom_hoare_sound)
wenzelm@59189
   222
 apply simp
prensani@13020
   223
apply(simp add: com_validity_def SEM_def sem_def)
prensani@13020
   224
apply(simp add: Help All_None_def)
prensani@13020
   225
apply force
prensani@13020
   226
done
prensani@13020
   227
wenzelm@59189
   228
lemma Strong_Soundness_aux: "\<lbrakk> (Some c, s) -*\<rightarrow> (co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
prensani@13020
   229
  \<Longrightarrow> if co = None then t \<in> q else t \<in> pre (the co) \<and> \<turnstile> (the co) q"
prensani@13020
   230
apply(erule rtrancl_induct2)
prensani@13020
   231
 apply simp
prensani@13020
   232
apply(case_tac "a")
prensani@13020
   233
 apply(fast elim: ann_transition_cases)
prensani@13020
   234
apply(erule Strong_Soundness_aux_aux)
prensani@13020
   235
 apply simp
prensani@13020
   236
apply simp_all
prensani@13020
   237
done
prensani@13020
   238
wenzelm@59189
   239
lemma Strong_Soundness: "\<lbrakk> (Some c, s)-*\<rightarrow>(co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
prensani@13020
   240
  \<Longrightarrow> if co = None then t\<in>q else t \<in> pre (the co)"
prensani@13020
   241
apply(force dest:Strong_Soundness_aux)
prensani@13020
   242
done
prensani@13020
   243
prensani@13020
   244
lemma ann_hoare_sound: "\<turnstile> c q  \<Longrightarrow> \<Turnstile> c q"
prensani@13020
   245
apply (unfold ann_com_validity_def ann_SEM_def ann_sem_def)
prensani@13020
   246
apply clarify
prensani@13020
   247
apply(drule Strong_Soundness)
prensani@13020
   248
apply simp_all
prensani@13020
   249
done
prensani@13020
   250
wenzelm@59189
   251
subsection \<open>Soundness of the System for Parallel Programs\<close>
prensani@13020
   252
wenzelm@59189
   253
lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\<rightarrow> (R', t) \<Longrightarrow>
prensani@13020
   254
  (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
prensani@13020
   255
  (\<forall>i. i<length Ts \<longrightarrow> post(Rs ! i) = post(Ts ! i)))"
prensani@13020
   256
apply(erule transition_cases)
prensani@13020
   257
apply simp
prensani@13020
   258
apply clarify
prensani@13020
   259
apply(case_tac "i=ia")
prensani@13020
   260
apply simp+
prensani@13020
   261
done
prensani@13020
   262
wenzelm@59189
   263
lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\<rightarrow> (R',t) \<Longrightarrow>
wenzelm@59189
   264
  (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
prensani@13020
   265
  (\<forall>i. i<length Ts \<longrightarrow> post(Ts ! i) = post(Rs ! i)))"
prensani@13020
   266
apply(erule rtrancl_induct2)
prensani@13020
   267
 apply(simp_all)
prensani@13020
   268
apply clarify
prensani@13020
   269
apply simp
prensani@13020
   270
apply(drule Parallel_length_post_P1)
prensani@13020
   271
apply auto
prensani@13020
   272
done
prensani@13020
   273
prensani@13020
   274
lemma assertions_lemma: "pre c \<in> assertions c"
prensani@13020
   275
apply(rule ann_com_com.induct [THEN conjunct1])
prensani@13020
   276
apply auto
prensani@13020
   277
done
prensani@13020
   278
wenzelm@59189
   279
lemma interfree_aux1 [rule_format]:
prensani@13020
   280
  "(c,s) -1\<rightarrow> (r,t)  \<longrightarrow> (interfree_aux(c1, q1, c) \<longrightarrow> interfree_aux(c1, q1, r))"
prensani@13020
   281
apply (rule ann_transition_transition.induct [THEN conjunct1])
prensani@13020
   282
apply(safe)
prensani@13020
   283
prefer 13
prensani@13020
   284
apply (rule TrueI)
prensani@13020
   285
apply (simp_all add:interfree_aux_def)
prensani@13020
   286
apply force+
prensani@13020
   287
done
prensani@13020
   288
wenzelm@59189
   289
lemma interfree_aux2 [rule_format]:
prensani@13020
   290
  "(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c, q, a)  \<longrightarrow> interfree_aux(r, q, a) )"
prensani@13020
   291
apply (rule ann_transition_transition.induct [THEN conjunct1])
prensani@13020
   292
apply(force simp add:interfree_aux_def)+
prensani@13020
   293
done
prensani@13020
   294
wenzelm@59189
   295
lemma interfree_lemma: "\<lbrakk> (Some c, s) -1\<rightarrow> (r, t);interfree Ts ; i<length Ts;
prensani@13020
   296
           Ts!i = (Some c, q) \<rbrakk> \<Longrightarrow> interfree (Ts[i:= (r, q)])"
prensani@13020
   297
apply(simp add: interfree_def)
prensani@13020
   298
apply clarify
prensani@13020
   299
apply(case_tac "i=j")
prensani@13020
   300
 apply(drule_tac t = "ia" in not_sym)
prensani@13020
   301
 apply simp_all
prensani@13020
   302
apply(force elim: interfree_aux1)
prensani@13020
   303
apply(force elim: interfree_aux2 simp add:nth_list_update)
prensani@13020
   304
done
prensani@13020
   305
wenzelm@59189
   306
text \<open>Strong Soundness Theorem for Parallel Programs:\<close>
prensani@13020
   307
wenzelm@59189
   308
lemma Parallel_Strong_Soundness_Seq_aux:
wenzelm@59189
   309
  "\<lbrakk>interfree Ts; i<length Ts; com(Ts ! i) = Some(AnnSeq c0 c1) \<rbrakk>
prensani@13020
   310
  \<Longrightarrow>  interfree (Ts[i:=(Some c0, pre c1)])"
prensani@13020
   311
apply(simp add: interfree_def)
prensani@13020
   312
apply clarify
prensani@13020
   313
apply(case_tac "i=j")
prensani@13020
   314
 apply(force simp add: nth_list_update interfree_aux_def)
prensani@13020
   315
apply(case_tac "i=ia")
prensani@13020
   316
 apply(erule_tac x=ia in allE)
prensani@13020
   317
 apply(force simp add:interfree_aux_def assertions_lemma)
prensani@13020
   318
apply simp
prensani@13020
   319
done
prensani@13020
   320
wenzelm@59189
   321
lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]:
wenzelm@59189
   322
 "\<lbrakk> \<forall>i<length Ts. (if com(Ts!i) = None then b \<in> post(Ts!i)
wenzelm@59189
   323
  else b \<in> pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i));
wenzelm@59189
   324
  com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts \<rbrakk> \<Longrightarrow>
wenzelm@59189
   325
 (\<forall>ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None
wenzelm@59189
   326
  then b \<in> post(Ts[i:=(Some c0, pre c1)]! ia)
wenzelm@59189
   327
 else b \<in> pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \<and>
wenzelm@59189
   328
 \<turnstile> the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia)))
prensani@13020
   329
  \<and> interfree (Ts[i:= (Some c0, pre c1)])"
prensani@13020
   330
apply(rule conjI)
prensani@13020
   331
 apply safe
prensani@13020
   332
 apply(case_tac "i=ia")
prensani@13020
   333
  apply simp
prensani@13020
   334
  apply(force dest: ann_hoare_case_analysis)
prensani@13020
   335
 apply simp
prensani@13020
   336
apply(fast elim: Parallel_Strong_Soundness_Seq_aux)
prensani@13020
   337
done
prensani@13020
   338
wenzelm@59189
   339
lemma Parallel_Strong_Soundness_aux_aux [rule_format]:
wenzelm@59189
   340
 "(Some c, b) -1\<rightarrow> (co, t) \<longrightarrow>
wenzelm@59189
   341
  (\<forall>Ts. i<length Ts \<longrightarrow> com(Ts ! i) = Some c \<longrightarrow>
wenzelm@59189
   342
  (\<forall>i<length Ts. (if com(Ts ! i) = None then b\<in>post(Ts!i)
wenzelm@59189
   343
  else b\<in>pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i))) \<longrightarrow>
wenzelm@59189
   344
 interfree Ts \<longrightarrow>
wenzelm@59189
   345
  (\<forall>j. j<length Ts \<and> i\<noteq>j \<longrightarrow> (if com(Ts!j) = None then t\<in>post(Ts!j)
prensani@13020
   346
  else t\<in>pre(the(com(Ts!j))) \<and> \<turnstile> the(com(Ts!j)) post(Ts!j))) )"
prensani@13020
   347
apply(rule ann_transition_transition.induct [THEN conjunct1])
prensani@13020
   348
apply safe
prensani@13020
   349
prefer 11
prensani@13020
   350
apply(rule TrueI)
prensani@13020
   351
apply simp_all
wenzelm@62042
   352
\<comment>\<open>Basic\<close>
prensani@13020
   353
   apply(erule_tac x = "i" in all_dupE, erule (1) notE impE)
prensani@13020
   354
   apply(erule_tac x = "j" in allE , erule (1) notE impE)
prensani@13020
   355
   apply(simp add: interfree_def)
prensani@13020
   356
   apply(erule_tac x = "j" in allE,simp)
prensani@13020
   357
   apply(erule_tac x = "i" in allE,simp)
prensani@13020
   358
   apply(drule_tac t = "i" in not_sym)
prensani@13020
   359
   apply(case_tac "com(Ts ! j)=None")
prensani@13020
   360
    apply(force intro: converse_rtrancl_into_rtrancl
prensani@13020
   361
          simp add: interfree_aux_def com_validity_def SEM_def sem_def All_None_def)
prensani@13020
   362
   apply(simp add:interfree_aux_def)
prensani@13020
   363
   apply clarify
prensani@13020
   364
   apply simp
prensani@13020
   365
   apply(erule_tac x="pre y" in ballE)
wenzelm@59189
   366
    apply(force intro: converse_rtrancl_into_rtrancl
prensani@13020
   367
          simp add: com_validity_def SEM_def sem_def All_None_def)
prensani@13020
   368
   apply(simp add:assertions_lemma)
wenzelm@62042
   369
\<comment>\<open>Seqs\<close>
prensani@13020
   370
  apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
prensani@13020
   371
  apply(drule  Parallel_Strong_Soundness_Seq,simp+)
prensani@13020
   372
 apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
prensani@13020
   373
 apply(drule  Parallel_Strong_Soundness_Seq,simp+)
wenzelm@62042
   374
\<comment>\<open>Await\<close>
prensani@13020
   375
apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE)
prensani@13020
   376
apply(erule_tac x = "j" in allE , erule (1) notE impE)
prensani@13020
   377
apply(simp add: interfree_def)
prensani@13020
   378
apply(erule_tac x = "j" in allE,simp)
prensani@13020
   379
apply(erule_tac x = "i" in allE,simp)
prensani@13020
   380
apply(drule_tac t = "i" in not_sym)
prensani@13020
   381
apply(case_tac "com(Ts ! j)=None")
wenzelm@59189
   382
 apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def
prensani@13020
   383
        com_validity_def SEM_def sem_def All_None_def Help)
prensani@13020
   384
apply(simp add:interfree_aux_def)
prensani@13020
   385
apply clarify
prensani@13020
   386
apply simp
prensani@13020
   387
apply(erule_tac x="pre y" in ballE)
wenzelm@59189
   388
 apply(force intro: converse_rtrancl_into_rtrancl
prensani@13020
   389
       simp add: com_validity_def SEM_def sem_def All_None_def Help)
prensani@13020
   390
apply(simp add:assertions_lemma)
prensani@13020
   391
done
prensani@13020
   392
wenzelm@59189
   393
lemma Parallel_Strong_Soundness_aux [rule_format]:
prensani@13020
   394
 "\<lbrakk>(Ts',s) -P*\<rightarrow> (Rs',t);  Ts' = (Parallel Ts); interfree Ts;
wenzelm@59189
   395
 \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. (Ts ! i) = (Some c, q) \<and> s\<in>(pre c) \<and> \<turnstile> c q ) \<rbrakk> \<Longrightarrow>
wenzelm@59189
   396
  \<forall>Rs. Rs' = (Parallel Rs) \<longrightarrow> (\<forall>j. j<length Rs \<longrightarrow>
wenzelm@59189
   397
  (if com(Rs ! j) = None then t\<in>post(Ts ! j)
prensani@13020
   398
  else t\<in>pre(the(com(Rs ! j))) \<and> \<turnstile> the(com(Rs ! j)) post(Ts ! j))) \<and> interfree Rs"
prensani@13020
   399
apply(erule rtrancl_induct2)
prensani@13020
   400
 apply clarify
wenzelm@62042
   401
\<comment>\<open>Base\<close>
prensani@13020
   402
 apply force
wenzelm@62042
   403
\<comment>\<open>Induction step\<close>
prensani@13020
   404
apply clarify
prensani@13020
   405
apply(drule Parallel_length_post_PStar)
prensani@13020
   406
apply clarify
berghofe@23746
   407
apply (ind_cases "(Parallel Ts, s) -P1\<rightarrow> (Parallel Rs, t)" for Ts s Rs t)
prensani@13020
   408
apply(rule conjI)
prensani@13020
   409
 apply clarify
prensani@13020
   410
 apply(case_tac "i=j")
nipkow@62390
   411
  apply(simp split del:if_split)
prensani@13020
   412
  apply(erule Strong_Soundness_aux_aux,simp+)
prensani@13020
   413
   apply force
prensani@13020
   414
  apply force
nipkow@62390
   415
 apply(simp split del: if_split)
prensani@13020
   416
 apply(erule Parallel_Strong_Soundness_aux_aux)
nipkow@62390
   417
 apply(simp_all add: split del:if_split)
prensani@13020
   418
 apply force
prensani@13020
   419
apply(rule interfree_lemma)
prensani@13020
   420
apply simp_all
prensani@13020
   421
done
prensani@13020
   422
wenzelm@59189
   423
lemma Parallel_Strong_Soundness:
wenzelm@59189
   424
 "\<lbrakk>(Parallel Ts, s) -P*\<rightarrow> (Parallel Rs, t); interfree Ts; j<length Rs;
wenzelm@59189
   425
  \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. Ts ! i = (Some c, q) \<and> s\<in>pre c \<and> \<turnstile> c q) \<rbrakk> \<Longrightarrow>
prensani@13020
   426
  if com(Rs ! j) = None then t\<in>post(Ts ! j) else t\<in>pre (the(com(Rs ! j)))"
prensani@13020
   427
apply(drule  Parallel_Strong_Soundness_aux)
prensani@13020
   428
apply simp+
prensani@13020
   429
done
prensani@13020
   430
paulson@15102
   431
lemma oghoare_sound [rule_format]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q"
prensani@13020
   432
apply (unfold com_validity_def)
prensani@13020
   433
apply(rule oghoare_induct)
prensani@13020
   434
apply(rule TrueI)+
wenzelm@62042
   435
\<comment>\<open>Parallel\<close>
prensani@13020
   436
      apply(simp add: SEM_def sem_def)
huffman@44535
   437
      apply(clarify, rename_tac x y i Ts')
prensani@13020
   438
      apply(frule Parallel_length_post_PStar)
prensani@13020
   439
      apply clarify
huffman@44535
   440
      apply(drule_tac j=i in Parallel_Strong_Soundness)
prensani@13020
   441
         apply clarify
prensani@13020
   442
        apply simp
prensani@13020
   443
       apply force
prensani@13020
   444
      apply simp
wenzelm@59807
   445
      apply(erule_tac V = "\<forall>i. P i" for P in thin_rl)
prensani@13020
   446
      apply(drule_tac s = "length Rs" in sym)
prensani@13020
   447
      apply(erule allE, erule impE, assumption)
prensani@13020
   448
      apply(force dest: nth_mem simp add: All_None_def)
wenzelm@62042
   449
\<comment>\<open>Basic\<close>
prensani@13020
   450
    apply(simp add: SEM_def sem_def)
bulwahn@46362
   451
    apply(force dest: rtrancl_imp_UN_relpow Basic_ntran)
wenzelm@62042
   452
\<comment>\<open>Seq\<close>
prensani@13020
   453
   apply(rule subset_trans)
prensani@13020
   454
    prefer 2 apply assumption
prensani@13020
   455
   apply(simp add: L3_5ii L3_5i)
wenzelm@62042
   456
\<comment>\<open>Cond\<close>
prensani@13020
   457
  apply(simp add: L3_5iv)
wenzelm@62042
   458
\<comment>\<open>While\<close>
prensani@13020
   459
 apply(simp add: L3_5v)
wenzelm@59189
   460
 apply (blast dest: SEM_fwhile)
wenzelm@62042
   461
\<comment>\<open>Conseq\<close>
paulson@15102
   462
apply(auto simp add: SEM_def sem_def)
prensani@13020
   463
done
prensani@13020
   464
haftmann@39246
   465
end