src/HOL/Hoare_Parallel/OG_Tran.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62390 842917225d56
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@59189
     1
section \<open>Operational Semantics\<close>
prensani@13020
     2
haftmann@16417
     3
theory OG_Tran imports OG_Com begin
prensani@13020
     4
wenzelm@42174
     5
type_synonym 'a ann_com_op = "('a ann_com) option"
wenzelm@42174
     6
type_synonym 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
wenzelm@59189
     7
haftmann@35416
     8
primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
haftmann@35416
     9
  "com (c, q) = c"
prensani@13020
    10
haftmann@35416
    11
primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where
haftmann@35416
    12
  "post (c, q) = q"
prensani@13020
    13
haftmann@35416
    14
definition All_None :: "'a ann_triple_op list \<Rightarrow> bool" where
prensani@13020
    15
  "All_None Ts \<equiv> \<forall>(c, q) \<in> set Ts. c = None"
prensani@13020
    16
wenzelm@59189
    17
subsection \<open>The Transition Relation\<close>
prensani@13020
    18
berghofe@23746
    19
inductive_set
wenzelm@59189
    20
  ann_transition :: "(('a ann_com_op \<times> 'a) \<times> ('a ann_com_op \<times> 'a)) set"
berghofe@23746
    21
  and transition :: "(('a com \<times> 'a) \<times> ('a com \<times> 'a)) set"
berghofe@23746
    22
  and ann_transition' :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool"
berghofe@23746
    23
    ("_ -1\<rightarrow> _"[81,81] 100)
berghofe@23746
    24
  and transition' :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"
berghofe@23746
    25
    ("_ -P1\<rightarrow> _"[81,81] 100)
berghofe@23746
    26
  and transitions :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"
berghofe@23746
    27
    ("_ -P*\<rightarrow> _"[81,81] 100)
berghofe@23746
    28
where
berghofe@23746
    29
  "con_0 -1\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition"
berghofe@23746
    30
| "con_0 -P1\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition"
berghofe@23746
    31
| "con_0 -P*\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition\<^sup>*"
berghofe@23746
    32
berghofe@23746
    33
| AnnBasic:  "(Some (AnnBasic r f), s) -1\<rightarrow> (None, f s)"
berghofe@23746
    34
wenzelm@59189
    35
| AnnSeq1: "(Some c0, s) -1\<rightarrow> (None, t) \<Longrightarrow>
berghofe@23746
    36
               (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some c1, t)"
wenzelm@59189
    37
| AnnSeq2: "(Some c0, s) -1\<rightarrow> (Some c2, t) \<Longrightarrow>
berghofe@23746
    38
               (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some (AnnSeq c2 c1), t)"
berghofe@23746
    39
berghofe@23746
    40
| AnnCond1T: "s \<in> b  \<Longrightarrow> (Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (Some c1, s)"
berghofe@23746
    41
| AnnCond1F: "s \<notin> b \<Longrightarrow> (Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (Some c2, s)"
prensani@13020
    42
berghofe@23746
    43
| AnnCond2T: "s \<in> b  \<Longrightarrow> (Some (AnnCond2 r b c), s) -1\<rightarrow> (Some c, s)"
berghofe@23746
    44
| AnnCond2F: "s \<notin> b \<Longrightarrow> (Some (AnnCond2 r b c), s) -1\<rightarrow> (None, s)"
berghofe@23746
    45
berghofe@23746
    46
| AnnWhileF: "s \<notin> b \<Longrightarrow> (Some (AnnWhile r b i c), s) -1\<rightarrow> (None, s)"
wenzelm@59189
    47
| AnnWhileT: "s \<in> b  \<Longrightarrow> (Some (AnnWhile r b i c), s) -1\<rightarrow>
berghofe@23746
    48
                         (Some (AnnSeq c (AnnWhile i b i c)), s)"
berghofe@23746
    49
berghofe@23746
    50
| AnnAwait: "\<lbrakk> s \<in> b; atom_com c; (c, s) -P*\<rightarrow> (Parallel [], t) \<rbrakk> \<Longrightarrow>
wenzelm@59189
    51
                   (Some (AnnAwait r b c), s) -1\<rightarrow> (None, t)"
berghofe@23746
    52
berghofe@23746
    53
| Parallel: "\<lbrakk> i<length Ts; Ts!i = (Some c, q); (Some c, s) -1\<rightarrow> (r, t) \<rbrakk>
berghofe@23746
    54
              \<Longrightarrow> (Parallel Ts, s) -P1\<rightarrow> (Parallel (Ts [i:=(r, q)]), t)"
berghofe@23746
    55
berghofe@23746
    56
| Basic:  "(Basic f, s) -P1\<rightarrow> (Parallel [], f s)"
berghofe@23746
    57
berghofe@23746
    58
| Seq1:   "All_None Ts \<Longrightarrow> (Seq (Parallel Ts) c, s) -P1\<rightarrow> (c, s)"
berghofe@23746
    59
| Seq2:   "(c0, s) -P1\<rightarrow> (c2, t) \<Longrightarrow> (Seq c0 c1, s) -P1\<rightarrow> (Seq c2 c1, t)"
berghofe@23746
    60
berghofe@23746
    61
| CondT: "s \<in> b \<Longrightarrow> (Cond b c1 c2, s) -P1\<rightarrow> (c1, s)"
berghofe@23746
    62
| CondF: "s \<notin> b \<Longrightarrow> (Cond b c1 c2, s) -P1\<rightarrow> (c2, s)"
berghofe@23746
    63
berghofe@23746
    64
| WhileF: "s \<notin> b \<Longrightarrow> (While b i c, s) -P1\<rightarrow> (Parallel [], s)"
berghofe@23746
    65
| WhileT: "s \<in> b \<Longrightarrow> (While b i c, s) -P1\<rightarrow> (Seq c (While b i c), s)"
berghofe@23746
    66
berghofe@23746
    67
monos "rtrancl_mono"
prensani@13020
    68
wenzelm@59189
    69
text \<open>The corresponding abbreviations are:\<close>
prensani@13020
    70
berghofe@23746
    71
abbreviation
wenzelm@59189
    72
  ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a)
berghofe@23746
    73
                           \<Rightarrow> bool"  ("_ -_\<rightarrow> _"[81,81] 100)  where
haftmann@30952
    74
  "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition ^^ n"
prensani@13020
    75
berghofe@23746
    76
abbreviation
berghofe@23746
    77
  ann_transitions :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool"
berghofe@23746
    78
                           ("_ -*\<rightarrow> _"[81,81] 100)  where
berghofe@23746
    79
  "con_0 -*\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition\<^sup>*"
prensani@13020
    80
berghofe@23746
    81
abbreviation
wenzelm@59189
    82
  transition_n :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"
berghofe@23746
    83
                          ("_ -P_\<rightarrow> _"[81,81,81] 100)  where
haftmann@30952
    84
  "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition ^^ n"
prensani@13020
    85
wenzelm@59189
    86
subsection \<open>Definition of Semantics\<close>
prensani@13020
    87
haftmann@35416
    88
definition ann_sem :: "'a ann_com \<Rightarrow> 'a \<Rightarrow> 'a set" where
prensani@13020
    89
  "ann_sem c \<equiv> \<lambda>s. {t. (Some c, s) -*\<rightarrow> (None, t)}"
prensani@13020
    90
haftmann@35416
    91
definition ann_SEM :: "'a ann_com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@52141
    92
  "ann_SEM c S \<equiv> \<Union>(ann_sem c ` S)"
prensani@13020
    93
haftmann@35416
    94
definition sem :: "'a com \<Rightarrow> 'a \<Rightarrow> 'a set" where
prensani@13020
    95
  "sem c \<equiv> \<lambda>s. {t. \<exists>Ts. (c, s) -P*\<rightarrow> (Parallel Ts, t) \<and> All_None Ts}"
prensani@13020
    96
haftmann@35416
    97
definition SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@52141
    98
  "SEM c S \<equiv> \<Union>(sem c ` S)"
prensani@13020
    99
wenzelm@35107
   100
abbreviation Omega :: "'a com"    ("\<Omega>" 63)
wenzelm@35107
   101
  where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
prensani@13020
   102
haftmann@35416
   103
primrec fwhile :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> nat \<Rightarrow> 'a com" where
haftmann@35416
   104
    "fwhile b c 0 = \<Omega>"
haftmann@35416
   105
  | "fwhile b c (Suc n) = Cond b (Seq c (fwhile b c n)) (Basic id)"
prensani@13020
   106
wenzelm@59189
   107
subsubsection \<open>Proofs\<close>
prensani@13020
   108
prensani@13020
   109
declare ann_transition_transition.intros [intro]
wenzelm@59189
   110
inductive_cases transition_cases:
wenzelm@59189
   111
    "(Parallel T,s) -P1\<rightarrow> t"
prensani@13020
   112
    "(Basic f, s) -P1\<rightarrow> t"
wenzelm@59189
   113
    "(Seq c1 c2, s) -P1\<rightarrow> t"
prensani@13020
   114
    "(Cond b c1 c2, s) -P1\<rightarrow> t"
prensani@13020
   115
    "(While b i c, s) -P1\<rightarrow> t"
prensani@13020
   116
wenzelm@59189
   117
lemma Parallel_empty_lemma [rule_format (no_asm)]:
prensani@13020
   118
  "(Parallel [],s) -Pn\<rightarrow> (Parallel Ts,t) \<longrightarrow> Ts=[] \<and> n=0 \<and> s=t"
prensani@13020
   119
apply(induct n)
prensani@13020
   120
 apply(simp (no_asm))
prensani@13020
   121
apply clarify
bulwahn@46362
   122
apply(drule relpow_Suc_D2)
prensani@13020
   123
apply(force elim:transition_cases)
prensani@13020
   124
done
prensani@13020
   125
wenzelm@59189
   126
lemma Parallel_AllNone_lemma [rule_format (no_asm)]:
prensani@13020
   127
 "All_None Ss \<longrightarrow> (Parallel Ss,s) -Pn\<rightarrow> (Parallel Ts,t) \<longrightarrow> Ts=Ss \<and> n=0 \<and> s=t"
prensani@13020
   128
apply(induct "n")
prensani@13020
   129
 apply(simp (no_asm))
prensani@13020
   130
apply clarify
bulwahn@46362
   131
apply(drule relpow_Suc_D2)
prensani@13020
   132
apply clarify
prensani@13020
   133
apply(erule transition_cases,simp_all)
prensani@13020
   134
apply(force dest:nth_mem simp add:All_None_def)
prensani@13020
   135
done
prensani@13020
   136
prensani@13020
   137
lemma Parallel_AllNone: "All_None Ts \<Longrightarrow> (SEM (Parallel Ts) X) = X"
prensani@13020
   138
apply (unfold SEM_def sem_def)
prensani@13020
   139
apply auto
bulwahn@46362
   140
apply(drule rtrancl_imp_UN_relpow)
prensani@13020
   141
apply clarify
prensani@13020
   142
apply(drule Parallel_AllNone_lemma)
prensani@13020
   143
apply auto
prensani@13020
   144
done
prensani@13020
   145
prensani@13020
   146
lemma Parallel_empty: "Ts=[] \<Longrightarrow> (SEM (Parallel Ts) X) = X"
prensani@13020
   147
apply(rule Parallel_AllNone)
prensani@13020
   148
apply(simp add:All_None_def)
prensani@13020
   149
done
prensani@13020
   150
wenzelm@59189
   151
text \<open>Set of lemmas from Apt and Olderog "Verification of sequential
wenzelm@59189
   152
and concurrent programs", page 63.\<close>
prensani@13020
   153
wenzelm@59189
   154
lemma L3_5i: "X\<subseteq>Y \<Longrightarrow> SEM c X \<subseteq> SEM c Y"
prensani@13020
   155
apply (unfold SEM_def)
prensani@13020
   156
apply force
prensani@13020
   157
done
prensani@13020
   158
wenzelm@59189
   159
lemma L3_5ii_lemma1:
wenzelm@59189
   160
 "\<lbrakk> (c1, s1) -P*\<rightarrow> (Parallel Ts, s2); All_None Ts;
wenzelm@59189
   161
  (c2, s2) -P*\<rightarrow> (Parallel Ss, s3); All_None Ss \<rbrakk>
prensani@13020
   162
 \<Longrightarrow> (Seq c1 c2, s1) -P*\<rightarrow> (Parallel Ss, s3)"
prensani@13020
   163
apply(erule converse_rtrancl_induct2)
prensani@13020
   164
apply(force intro:converse_rtrancl_into_rtrancl)+
prensani@13020
   165
done
prensani@13020
   166
wenzelm@59189
   167
lemma L3_5ii_lemma2 [rule_format (no_asm)]:
wenzelm@59189
   168
 "\<forall>c1 c2 s t. (Seq c1 c2, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow>
wenzelm@59189
   169
  (All_None Ts) \<longrightarrow> (\<exists>y m Rs. (c1,s) -P*\<rightarrow> (Parallel Rs, y) \<and>
prensani@13020
   170
  (All_None Rs) \<and> (c2, y) -Pm\<rightarrow> (Parallel Ts, t) \<and>  m \<le> n)"
prensani@13020
   171
apply(induct "n")
prensani@13020
   172
 apply(force)
bulwahn@46362
   173
apply(safe dest!: relpow_Suc_D2)
prensani@13020
   174
apply(erule transition_cases,simp_all)
prensani@13020
   175
 apply (fast intro!: le_SucI)
bulwahn@46362
   176
apply (fast intro!: le_SucI elim!: relpow_imp_rtrancl converse_rtrancl_into_rtrancl)
prensani@13020
   177
done
prensani@13020
   178
wenzelm@59189
   179
lemma L3_5ii_lemma3:
wenzelm@59189
   180
 "\<lbrakk>(Seq c1 c2,s) -P*\<rightarrow> (Parallel Ts,t); All_None Ts\<rbrakk> \<Longrightarrow>
wenzelm@59189
   181
    (\<exists>y Rs. (c1,s) -P*\<rightarrow> (Parallel Rs,y) \<and> All_None Rs
prensani@13020
   182
   \<and> (c2,y) -P*\<rightarrow> (Parallel Ts,t))"
bulwahn@46362
   183
apply(drule rtrancl_imp_UN_relpow)
bulwahn@46362
   184
apply(fast dest: L3_5ii_lemma2 relpow_imp_rtrancl)
prensani@13020
   185
done
prensani@13020
   186
prensani@13020
   187
lemma L3_5ii: "SEM (Seq c1 c2) X = SEM c2 (SEM c1 X)"
prensani@13020
   188
apply (unfold SEM_def sem_def)
prensani@13020
   189
apply auto
prensani@13020
   190
 apply(fast dest: L3_5ii_lemma3)
prensani@13020
   191
apply(fast elim: L3_5ii_lemma1)
prensani@13020
   192
done
prensani@13020
   193
prensani@13020
   194
lemma L3_5iii: "SEM (Seq (Seq c1 c2) c3) X = SEM (Seq c1 (Seq c2 c3)) X"
prensani@13020
   195
apply (simp (no_asm) add: L3_5ii)
prensani@13020
   196
done
prensani@13020
   197
prensani@13020
   198
lemma L3_5iv:
prensani@13020
   199
 "SEM (Cond b c1 c2) X = (SEM c1 (X \<inter> b)) Un (SEM c2 (X \<inter> (-b)))"
prensani@13020
   200
apply (unfold SEM_def sem_def)
prensani@13020
   201
apply auto
prensani@13020
   202
apply(erule converse_rtranclE)
prensani@13020
   203
 prefer 2
prensani@13020
   204
 apply (erule transition_cases,simp_all)
prensani@13020
   205
  apply(fast intro: converse_rtrancl_into_rtrancl elim: transition_cases)+
prensani@13020
   206
done
prensani@13020
   207
prensani@13020
   208
wenzelm@59189
   209
lemma  L3_5v_lemma1[rule_format]:
prensani@13020
   210
 "(S,s) -Pn\<rightarrow> (T,t) \<longrightarrow> S=\<Omega> \<longrightarrow> (\<not>(\<exists>Rs. T=(Parallel Rs) \<and> All_None Rs))"
prensani@13020
   211
apply (unfold UNIV_def)
prensani@13020
   212
apply(rule nat_less_induct)
prensani@13020
   213
apply safe
bulwahn@46362
   214
apply(erule relpow_E2)
prensani@13020
   215
 apply simp_all
prensani@13020
   216
apply(erule transition_cases)
prensani@13020
   217
 apply simp_all
bulwahn@46362
   218
apply(erule relpow_E2)
prensani@13020
   219
 apply(simp add: Id_def)
prensani@13020
   220
apply(erule transition_cases,simp_all)
prensani@13020
   221
apply clarify
prensani@13020
   222
apply(erule transition_cases,simp_all)
bulwahn@46362
   223
apply(erule relpow_E2,simp)
prensani@13020
   224
apply clarify
prensani@13020
   225
apply(erule transition_cases)
prensani@13020
   226
 apply simp+
prensani@13020
   227
    apply clarify
prensani@13020
   228
    apply(erule transition_cases)
prensani@13020
   229
apply simp_all
prensani@13020
   230
done
prensani@13020
   231
prensani@13020
   232
lemma L3_5v_lemma2: "\<lbrakk>(\<Omega>, s) -P*\<rightarrow> (Parallel Ts, t); All_None Ts \<rbrakk> \<Longrightarrow> False"
bulwahn@46362
   233
apply(fast dest: rtrancl_imp_UN_relpow L3_5v_lemma1)
prensani@13020
   234
done
prensani@13020
   235
prensani@13020
   236
lemma L3_5v_lemma3: "SEM (\<Omega>) S = {}"
prensani@13020
   237
apply (unfold SEM_def sem_def)
prensani@13020
   238
apply(fast dest: L3_5v_lemma2)
prensani@13020
   239
done
prensani@13020
   240
wenzelm@59189
   241
lemma L3_5v_lemma4 [rule_format]:
wenzelm@59189
   242
 "\<forall>s. (While b i c, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow>
prensani@13020
   243
  (\<exists>k. (fwhile b c k, s) -P*\<rightarrow> (Parallel Ts, t))"
prensani@13020
   244
apply(rule nat_less_induct)
prensani@13020
   245
apply safe
bulwahn@46362
   246
apply(erule relpow_E2)
prensani@13020
   247
 apply safe
prensani@13020
   248
apply(erule transition_cases,simp_all)
prensani@13020
   249
 apply (rule_tac x = "1" in exI)
prensani@13020
   250
 apply(force dest: Parallel_empty_lemma intro: converse_rtrancl_into_rtrancl simp add: Id_def)
prensani@13020
   251
apply safe
prensani@13020
   252
apply(drule L3_5ii_lemma2)
prensani@13020
   253
 apply safe
prensani@13020
   254
apply(drule le_imp_less_Suc)
prensani@13020
   255
apply (erule allE , erule impE,assumption)
prensani@13020
   256
apply (erule allE , erule impE, assumption)
prensani@13020
   257
apply safe
prensani@13020
   258
apply (rule_tac x = "k+1" in exI)
prensani@13020
   259
apply(simp (no_asm))
prensani@13020
   260
apply(rule converse_rtrancl_into_rtrancl)
prensani@13020
   261
 apply fast
prensani@13020
   262
apply(fast elim: L3_5ii_lemma1)
prensani@13020
   263
done
prensani@13020
   264
wenzelm@59189
   265
lemma L3_5v_lemma5 [rule_format]:
wenzelm@59189
   266
 "\<forall>s. (fwhile b c k, s) -P*\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow>
prensani@13020
   267
  (While b i c, s) -P*\<rightarrow> (Parallel Ts,t)"
prensani@13020
   268
apply(induct "k")
prensani@13020
   269
 apply(force dest: L3_5v_lemma2)
prensani@13020
   270
apply safe
prensani@13020
   271
apply(erule converse_rtranclE)
prensani@13020
   272
 apply simp_all
prensani@13020
   273
apply(erule transition_cases,simp_all)
prensani@13020
   274
 apply(rule converse_rtrancl_into_rtrancl)
prensani@13020
   275
  apply(fast)
prensani@13020
   276
 apply(fast elim!: L3_5ii_lemma1 dest: L3_5ii_lemma3)
bulwahn@46362
   277
apply(drule rtrancl_imp_UN_relpow)
prensani@13020
   278
apply clarify
bulwahn@46362
   279
apply(erule relpow_E2)
prensani@13020
   280
 apply simp_all
prensani@13020
   281
apply(erule transition_cases,simp_all)
prensani@13020
   282
apply(fast dest: Parallel_empty_lemma)
prensani@13020
   283
done
prensani@13020
   284
prensani@13020
   285
lemma L3_5v: "SEM (While b i c) = (\<lambda>x. (\<Union>k. SEM (fwhile b c k) x))"
prensani@13020
   286
apply(rule ext)
prensani@13020
   287
apply (simp add: SEM_def sem_def)
prensani@13020
   288
apply safe
bulwahn@46362
   289
 apply(drule rtrancl_imp_UN_relpow,simp)
prensani@13020
   290
 apply clarify
prensani@13020
   291
 apply(fast dest:L3_5v_lemma4)
prensani@13020
   292
apply(fast intro: L3_5v_lemma5)
prensani@13020
   293
done
prensani@13020
   294
wenzelm@59189
   295
section \<open>Validity of Correctness Formulas\<close>
prensani@13020
   296
haftmann@35416
   297
definition com_validity :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a assn \<Rightarrow> bool" ("(3\<parallel>= _// _//_)" [90,55,90] 50) where
prensani@13020
   298
  "\<parallel>= p c q \<equiv> SEM c p \<subseteq> q"
prensani@13020
   299
haftmann@35416
   300
definition ann_com_validity :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool" ("\<Turnstile> _ _" [60,90] 45) where
prensani@13020
   301
  "\<Turnstile> c q \<equiv> ann_SEM c (pre c) \<subseteq> q"
prensani@13020
   302
nipkow@62390
   303
end