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