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