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