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