src/HOL/Hoare_Parallel/RG_Hoare.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42174 d0be2722ce9f
child 52597 a8a81453833d
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
header {* \section{The Proof System} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15236
diff changeset
     3
theory RG_Hoare imports RG_Tran begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     4
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     5
subsection {* Proof System for Component Programs *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     6
32687
27530efec97a tuned proofs; be more cautios wrt. default simp rules
haftmann
parents: 32621
diff changeset
     7
declare Un_subset_iff [simp del] le_sup_iff [simp del]
27530efec97a tuned proofs; be more cautios wrt. default simp rules
haftmann
parents: 32621
diff changeset
     8
declare Cons_eq_map_conv [iff]
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
     9
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    10
definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where  
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
  "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    13
inductive
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    14
  rghoare :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"  
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    15
    ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    16
where
13099
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13022
diff changeset
    17
  Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar; 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
            stable pre rely; stable post rely \<rbrakk> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
           \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    21
| Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk> 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
           \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    23
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    24
| Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    25
           \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    26
          \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    27
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    28
| While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    29
            \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    30
          \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    31
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    32
| Await: "\<lbrakk> stable pre rely; stable post rely; 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
    33
            \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
    34
                UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
           \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    36
  
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    37
| Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    38
             \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    39
            \<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    40
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    41
definition Pre :: "'a rgformula \<Rightarrow> 'a set" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    42
  "Pre x \<equiv> fst(snd x)"
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    43
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    44
definition Post :: "'a rgformula \<Rightarrow> 'a set" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    45
  "Post x \<equiv> snd(snd(snd(snd x)))"
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    46
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    47
definition Rely :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    48
  "Rely x \<equiv> fst(snd(snd x))"
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    49
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    50
definition Guar :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    51
  "Guar x \<equiv> fst(snd(snd(snd x)))"
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    52
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
    53
definition Com :: "'a rgformula \<Rightarrow> 'a com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    54
  "Com x \<equiv> fst x"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    55
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    56
subsection {* Proof System for Parallel Programs *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    57
42174
d0be2722ce9f modernized specifications;
wenzelm
parents: 41842
diff changeset
    58
type_synonym 'a par_rgformula =
d0be2722ce9f modernized specifications;
wenzelm
parents: 41842
diff changeset
    59
  "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    60
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    61
inductive
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    62
  par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    63
    ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
    64
where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    65
  Parallel: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    66
  "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j<length xs \<and> j\<noteq>i}. Guar(xs!j)) \<subseteq> Rely(xs!i);
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    67
    (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    68
     pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i)); 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    69
    (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    70
    \<forall>i<length xs. \<turnstile> Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    71
   \<Longrightarrow>  \<turnstile> xs SAT [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    72
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    73
section {* Soundness*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    74
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    75
subsubsection {* Some previous lemmas *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    76
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    77
lemma tl_of_assum_in_assum: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    78
  "(P, s) # (P, t) # xs \<in> assum (pre, rely) \<Longrightarrow> stable pre rely 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    79
  \<Longrightarrow> (P, t) # xs \<in> assum (pre, rely)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    80
apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    81
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    82
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    83
 apply(erule_tac x=0 in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    84
 apply(simp (no_asm_use)only:stable_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    85
 apply(erule allE,erule allE,erule impE,assumption,erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    86
 apply(simp add:Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    87
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    88
apply(erule_tac x="Suc i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    89
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    90
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    91
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    92
lemma etran_in_comm: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    93
  "(P, t) # xs \<in> comm(guar, post) \<Longrightarrow> (P, s) # (P, t) # xs \<in> comm(guar, post)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    94
apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    95
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    96
apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    97
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    98
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    99
lemma ctran_in_comm: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   100
  "\<lbrakk>(s, s) \<in> guar; (Q, s) # xs \<in> comm(guar, post)\<rbrakk> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   101
  \<Longrightarrow> (P, s) # (Q, s) # xs \<in> comm(guar, post)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   102
apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   103
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   104
apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   105
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   106
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   107
lemma takecptn_is_cptn [rule_format, elim!]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   108
  "\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   109
apply(induct "c")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   110
 apply(force elim: cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   111
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   112
apply(case_tac j) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   113
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   114
 apply(rule CptnOne)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   115
apply simp
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   116
apply(force intro:cptn.intros elim:cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   117
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   118
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   119
lemma dropcptn_is_cptn [rule_format,elim!]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   120
  "\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   121
apply(induct "c")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   122
 apply(force elim: cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   123
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   124
apply(case_tac j,simp+) 
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   125
apply(erule cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   126
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   127
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   128
apply force
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 takepar_cptn_is_par_cptn [rule_format,elim]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   132
  "\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   133
apply(induct "c")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   134
 apply(force elim: cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   135
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   136
apply(case_tac j,simp) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   137
 apply(rule ParCptnOne)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   138
apply(force intro:par_cptn.intros elim:par_cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   139
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   140
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   141
lemma droppar_cptn_is_par_cptn [rule_format]:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   142
  "\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   143
apply(induct "c")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   144
 apply(force elim: par_cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   145
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   146
apply(case_tac j,simp+) 
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   147
apply(erule par_cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   148
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   149
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   150
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   151
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   152
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   153
lemma tl_of_cptn_is_cptn: "\<lbrakk>x # xs \<in> cptn; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs  \<in> cptn"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   154
apply(subgoal_tac "1 < length (x # xs)") 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   155
 apply(drule dropcptn_is_cptn,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   156
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   157
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   158
lemma not_ctran_None [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   159
  "\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   160
apply(induct xs,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   161
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   162
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   163
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   164
 apply(case_tac i,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   165
  apply(rule Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   166
 apply simp
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   167
apply(force elim:ctran.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   168
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   169
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   170
lemma cptn_not_empty [simp]:"[] \<notin> cptn"
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   171
apply(force elim:cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   172
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   173
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   174
lemma etran_or_ctran [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   175
  "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   176
   \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   177
   \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   178
apply(induct x,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   179
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   180
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   181
 apply(case_tac i,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   182
  apply(rule Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   183
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   184
 apply(erule_tac x="m - 1" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   185
 apply(case_tac m,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   186
 apply(subgoal_tac "(\<forall>i. Suc i < nata \<longrightarrow> (((P, t) # xs) ! i, xs ! i) \<notin> ctran)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   187
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   188
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   189
 apply(erule_tac x="Suc ia" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   190
apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?J j) \<notin> ctran" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   191
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   192
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   193
lemma etran_or_ctran2 [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   194
  "\<forall>i. Suc i<length x \<longrightarrow> x\<in>cptn \<longrightarrow> (x!i -c\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   195
  \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   196
apply(induct x)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   197
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   198
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   199
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   200
 apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   201
apply(case_tac i,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   202
 apply(force elim:etran.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   203
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   204
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   205
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   206
lemma etran_or_ctran2_disjI1: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   207
  "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -c\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   208
by(drule etran_or_ctran2,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   209
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   210
lemma etran_or_ctran2_disjI2: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   211
  "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -e\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   212
by(drule etran_or_ctran2,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   213
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   214
lemma not_ctran_None2 [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   215
  "\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   216
apply(frule not_ctran_None,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   217
apply(case_tac i,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   218
 apply(force elim:etranE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   219
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   220
apply(rule etran_or_ctran2_disjI2,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   221
apply(force intro:tl_of_cptn_is_cptn)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   222
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   223
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   224
lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))";
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   225
apply(rule nat_less_induct)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   226
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   227
apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   228
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   229
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   230
 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   231
lemma stability [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   232
  "\<forall>j k. x \<in> cptn \<longrightarrow> stable p rely \<longrightarrow> j\<le>k \<longrightarrow> k<length x \<longrightarrow> snd(x!j)\<in>p  \<longrightarrow>
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   233
  (\<forall>i. (Suc i)<length x \<longrightarrow> 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   234
          (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow> 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   235
  (\<forall>i. j\<le>i \<and> i<k \<longrightarrow> x!i -e\<rightarrow> x!Suc i) \<longrightarrow> snd(x!k)\<in>p \<and> fst(x!j)=fst(x!k)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   236
apply(induct x)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   237
 apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   238
 apply(force elim:cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   239
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   240
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   241
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   242
 apply(case_tac k,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   243
 apply(case_tac j,simp) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   244
  apply(erule_tac x=0 in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   245
  apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (?J j)" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   246
  apply(subgoal_tac "t\<in>p")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   247
   apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   248
    apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   249
    apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   250
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   251
   apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   252
  apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran \<longrightarrow> ?T j" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   253
  apply(simp(no_asm_use) only:stable_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   254
  apply(erule_tac x=s in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   255
  apply(erule_tac x=t in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   256
  apply simp 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   257
  apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   258
  apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   259
  apply(rule Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   260
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   261
 apply(erule_tac x="nata" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   262
 apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   263
 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   264
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   265
  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   266
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   267
 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   268
apply(case_tac k,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   269
apply(case_tac j)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   270
 apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   271
 apply(erule etran.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   272
apply(erule_tac x="nata" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   273
apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   274
apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((Q, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((Q, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   275
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   276
 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   277
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   278
apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   279
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   280
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   281
subsection {* Soundness of the System for Component Programs *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   282
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   283
subsubsection {* Soundness of the Basic rule *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   284
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   285
lemma unique_ctran_Basic [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   286
  "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) \<longrightarrow> 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   287
  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   288
  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   289
apply(induct x,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   290
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   291
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   292
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   293
 apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   294
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   295
 apply(case_tac j,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   296
  apply(rule Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   297
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   298
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   299
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   300
apply(case_tac i)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   301
 apply(case_tac j,simp,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   302
 apply(erule ctran.cases,simp_all)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   303
 apply(force elim: not_ctran_None)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   304
apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran" for sa Q t)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   305
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   306
apply(drule_tac i=nat in not_ctran_None,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   307
apply(erule etranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   308
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   309
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   310
lemma exists_ctran_Basic_None [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   311
  "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   312
  \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   313
apply(induct x,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   314
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   315
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   316
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   317
 apply(case_tac i,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   318
 apply(erule_tac x=nat in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   319
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   320
 apply(rule_tac x="Suc j" in exI,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   321
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   322
apply(case_tac i,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   323
apply(rule_tac x=0 in exI,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   324
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   325
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   326
lemma Basic_sound: 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   327
  " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   328
  stable pre rely; stable post rely\<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   329
  \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   330
apply(unfold com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   331
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   332
apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   333
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   334
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   335
 apply(simp add:cp_def assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   336
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   337
 apply(frule_tac j=0 and k=i and p=pre in stability)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   338
       apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   339
   apply(erule_tac x=ia in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   340
  apply(erule_tac i=i and f=f in unique_ctran_Basic,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   341
 apply(erule subsetD,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   342
 apply(case_tac "x!i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   343
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   344
 apply(drule_tac s="Some (Basic f)" in sym,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   345
 apply(thin_tac "\<forall>j. ?H j")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   346
 apply(force elim:ctran.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   347
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   348
apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   349
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   350
apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   351
  apply(case_tac x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   352
  apply(rule last_fst_esp,simp add:last_length)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   353
 apply (case_tac x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   354
apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   355
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   356
apply(frule_tac j=0 and k="j" and p=pre in stability)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   357
      apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   358
  apply(erule_tac x=i in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   359
 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   360
apply(case_tac "x!j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   361
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   362
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   363
apply(drule_tac s="Some (Basic f)" in sym,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   364
apply(case_tac "x!Suc j",simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   365
apply(rule ctran.cases,simp)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   366
apply(simp_all)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   367
apply(drule_tac c=sa in subsetD,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   368
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   369
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   370
 apply(case_tac x,simp+)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   371
 apply(erule_tac x=i in allE)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   372
apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   373
  apply arith+
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   374
apply(case_tac x)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   375
apply(simp add:last_length)+
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   376
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   377
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   378
subsubsection{* Soundness of the Await rule *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   379
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   380
lemma unique_ctran_Await [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   381
  "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow> 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   382
  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   383
  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   384
apply(induct x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   385
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   386
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   387
 apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   388
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   389
 apply(case_tac j,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   390
  apply(rule Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   391
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   392
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   393
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   394
apply(case_tac i)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   395
 apply(case_tac j,simp,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   396
 apply(erule ctran.cases,simp_all)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   397
 apply(force elim: not_ctran_None)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   398
apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran" for sa Q t,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   399
apply(drule_tac i=nat in not_ctran_None,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   400
apply(erule etranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   401
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   402
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   403
lemma exists_ctran_Await_None [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   404
  "\<forall>s i.  x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   405
  \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   406
apply(induct x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   407
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   408
apply(erule cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   409
 apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   410
 apply(erule_tac x=nat in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   411
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   412
 apply(rule_tac x="Suc j" in exI,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   413
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   414
apply(case_tac i,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   415
apply(rule_tac x=0 in exI,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   416
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   417
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   418
lemma Star_imp_cptn: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   419
  "(P, s) -c*\<rightarrow> (R, t) \<Longrightarrow> \<exists>l \<in> cp P s. (last l)=(R, t)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   420
  \<and> (\<forall>i. Suc i<length l \<longrightarrow> l!i -c\<rightarrow> l!Suc i)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   421
apply (erule converse_rtrancl_induct2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   422
 apply(rule_tac x="[(R,t)]" in bexI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   423
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   424
 apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   425
 apply(rule CptnOne)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   426
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   427
apply(rule_tac x="(a, b)#l" in bexI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   428
 apply (rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   429
  apply(case_tac l,simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   430
  apply(simp add:last_length)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   431
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   432
apply(case_tac i,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   433
apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   434
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   435
apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   436
 apply(case_tac l)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   437
 apply(force elim:cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   438
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   439
apply(erule CptnComp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   440
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   441
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   442
 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   443
lemma Await_sound: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   444
  "\<lbrakk>stable pre rely; stable post rely;
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   445
  \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   446
                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and>
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   447
  \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   448
                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   449
  \<Longrightarrow> \<Turnstile> Await b P sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   450
apply(unfold com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   451
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   452
apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   453
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   454
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   455
 apply(simp add:cp_def assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   456
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   457
 apply(frule_tac j=0 and k=i and p=pre in stability,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   458
   apply(erule_tac x=ia in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   459
  apply(subgoal_tac "x\<in> cp (Some(Await b P)) s")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   460
  apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   461
  apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   462
--{* here starts the different part. *}
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   463
 apply(erule ctran.cases,simp_all)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   464
 apply(drule Star_imp_cptn) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   465
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   466
 apply(erule_tac x=sa in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   467
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   468
 apply(erule_tac x=sa in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   469
 apply(drule_tac c=l in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   470
  apply (simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   471
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   472
  apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   473
  apply(erule etranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   474
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   475
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   476
apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   477
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   478
apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   479
  apply (case_tac x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   480
 apply(rule last_fst_esp,simp add:last_length)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   481
 apply(case_tac x, (simp add:cptn_not_empty)+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   482
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   483
apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   484
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   485
apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   486
  apply(erule_tac x=i in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   487
 apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   488
apply(case_tac "x!j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   489
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   490
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   491
apply(drule_tac s="Some (Await b P)" in sym,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   492
apply(case_tac "x!Suc j",simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   493
apply(rule ctran.cases,simp)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   494
apply(simp_all)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   495
apply(drule Star_imp_cptn) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   496
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   497
apply(erule_tac x=sa in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   498
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   499
apply(erule_tac x=sa in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   500
apply(drule_tac c=l in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   501
 apply (simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   502
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   503
 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   504
 apply(erule etranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   505
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   506
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   507
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   508
 apply(case_tac x,simp+)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   509
 apply(erule_tac x=i in allE)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   510
apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   511
 apply arith+
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   512
apply(case_tac x)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   513
apply(simp add:last_length)+
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   514
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   515
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   516
subsubsection{* Soundness of the Conditional rule *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   517
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   518
lemma Cond_sound: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   519
  "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   520
  \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   521
  \<Longrightarrow> \<Turnstile> (Cond b P1 P2) sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   522
apply(unfold com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   523
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   524
apply(simp add:cp_def comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   525
apply(case_tac "\<exists>i. Suc i<length x \<and> x!i -c\<rightarrow> x!Suc i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   526
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   527
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   528
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   529
 apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   530
     apply(case_tac x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   531
    apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   532
   apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   533
  apply(erule_tac m="length x" in etran_or_ctran,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   534
 apply(case_tac x, (simp add:last_length)+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   535
apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   536
apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   537
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   538
apply (simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   539
apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   540
 apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   541
apply(erule ctran.cases,simp_all)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   542
 apply(erule_tac x="sa" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   543
 apply(drule_tac c="drop (Suc m) x" in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   544
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   545
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   546
 apply simp
17528
2a602a8462d5 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
wenzelm
parents: 16417
diff changeset
   547
 apply clarify
2a602a8462d5 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
wenzelm
parents: 16417
diff changeset
   548
 apply(case_tac "i\<le>m")
2a602a8462d5 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
wenzelm
parents: 16417
diff changeset
   549
  apply(drule le_imp_less_or_eq)
2a602a8462d5 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
wenzelm
parents: 16417
diff changeset
   550
  apply(erule disjE)
2a602a8462d5 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
wenzelm
parents: 16417
diff changeset
   551
   apply(erule_tac x=i in allE, erule impE, assumption)
2a602a8462d5 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
wenzelm
parents: 16417
diff changeset
   552
   apply simp+
2a602a8462d5 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
wenzelm
parents: 16417
diff changeset
   553
 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   554
 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   555
  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   556
   apply(rotate_tac -2)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   557
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   558
  apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   559
 apply arith
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   560
apply(case_tac "length (drop (Suc m) x)",simp)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   561
apply(erule_tac x="sa" in allE)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   562
back
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   563
apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   564
 apply clarify
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   565
apply simp
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   566
apply clarify
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   567
apply(case_tac "i\<le>m")
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   568
 apply(drule le_imp_less_or_eq)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   569
 apply(erule disjE)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   570
  apply(erule_tac x=i in allE, erule impE, assumption)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   571
  apply simp
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   572
 apply simp
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   573
apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   574
apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   575
 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   576
  apply(rotate_tac -2)
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   577
  apply simp
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   578
 apply arith
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20272
diff changeset
   579
apply arith
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 18576
diff changeset
   580
done
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   581
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   582
subsubsection{* Soundness of the Sequential rule *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   583
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   584
inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   585
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   586
lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   587
apply(subgoal_tac "length xs<length (x # xs)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   588
 apply(drule_tac Q=Q in  lift_nth)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   589
 apply(erule ssubst)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   590
 apply (simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   591
 apply(case_tac "(x # xs) ! length xs",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   592
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   593
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   594
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13601
diff changeset
   595
declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   596
lemma Seq_sound1 [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   597
  "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   598
  (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   599
  (\<exists>xs\<in> cp (Some P) s. x=map (lift Q) xs)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   600
apply(erule cptn_mod.induct)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   601
apply(unfold cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   602
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   603
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   604
    apply(simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   605
    apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   606
   apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   607
    apply clarify
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13601
diff changeset
   608
    apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   609
    apply(rule conjI,erule CptnEnv)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
   610
    apply(simp (no_asm_use) add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   611
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   612
   apply(erule_tac x="Suc i" in allE, simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   613
  apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran" for Pa sa t)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   614
 apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   615
apply(erule_tac x="length xs" in allE, simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   616
apply(simp only:Cons_lift_append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   617
apply(subgoal_tac "length xs < length ((Some P, sa) # xs)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   618
 apply(simp only :nth_append length_map last_length nth_map)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   619
 apply(case_tac "last((Some P, sa) # xs)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   620
 apply(simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   621
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   622
done
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13601
diff changeset
   623
declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   624
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   625
lemma Seq_sound2 [rule_format]: 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   626
  "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   627
  \<longrightarrow> fst(x!i)=Some Q \<longrightarrow>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   628
  (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   629
  (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   630
   \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   631
apply(erule cptn.induct)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   632
apply(unfold cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   633
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   634
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   635
 apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   636
 apply(erule allE,erule impE,assumption,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   637
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   638
 apply(subgoal_tac "(\<forall>j < nat. fst (((Some (Seq Pa Q), t) # xs) ! j) \<noteq> Some Q)",clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   639
  prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   640
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   641
 apply(case_tac xsa,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   642
 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   643
 apply(rule conjI,erule CptnEnv)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
   644
 apply(simp (no_asm_use) add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   645
 apply(rule_tac x=ys in exI,simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   646
apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran" for Pa sa t)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   647
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   648
 apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   649
 apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   650
  apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   651
 apply(case_tac i, simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   652
 apply(case_tac nat,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   653
 apply(rule_tac x="(Some Q,ta)#xs" in exI,simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   654
 apply(case_tac nat,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   655
 apply(force)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   656
apply(case_tac i, simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   657
apply(case_tac nat,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   658
apply(erule_tac x="Suc nata" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   659
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   660
apply(subgoal_tac "(\<forall>j<Suc nata. fst (((Some (Seq P2 Q), ta) # xs) ! j) \<noteq> Some Q)",clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   661
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   662
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   663
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   664
apply(rule_tac x="(Some Pa, sa)#(Some P2, ta)#(tl xsa)" in exI,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   665
apply(rule conjI,erule CptnComp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   666
apply(rule nth_tl_if,force,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   667
apply(rule_tac x=ys in exI,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   668
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   669
apply(rule nth_tl_if,force,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   670
 apply(rule tl_zero,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   671
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   672
apply(rule conjI,simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   673
apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)") 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   674
 apply(simp add:Cons_lift del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   675
 apply(rule nth_tl_if)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   676
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   677
  apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   678
apply(simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   679
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   680
(*
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   681
lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   682
apply(simp only:last_length [THEN sym])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   683
apply(subgoal_tac "length xs<length (x # xs)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   684
 apply(drule_tac Q=Q in  lift_nth)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   685
 apply(erule ssubst)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   686
 apply (simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   687
 apply(case_tac "(x # xs) ! length xs",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   688
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   689
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   690
*)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   691
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   692
lemma last_lift_not_None2: "fst ((lift Q) (last (x#xs))) \<noteq> None"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   693
apply(simp only:last_length [THEN sym])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   694
apply(subgoal_tac "length xs<length (x # xs)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   695
 apply(drule_tac Q=Q in  lift_nth)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   696
 apply(erule ssubst)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   697
 apply (simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   698
 apply(case_tac "(x # xs) ! length xs",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   699
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   700
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   701
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   702
lemma Seq_sound: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   703
  "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   704
  \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   705
apply(unfold com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   706
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   707
apply(case_tac "\<exists>i<length x. fst(x!i)=Some Q")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   708
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   709
 apply (simp add:cp_def cptn_iff_cptn_mod)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   710
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   711
 apply(frule_tac Seq_sound1,force)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   712
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   713
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   714
 apply(erule_tac x=s in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   715
 apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   716
  apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   717
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   718
  apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   719
  apply(simp add:snd_lift)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   720
  apply(erule mp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   721
  apply(force elim:etranE intro:Env simp add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   722
 apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   723
 apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   724
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   725
  apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   726
  apply(simp add:snd_lift)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   727
  apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   728
  apply(case_tac "(xs!i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   729
  apply(case_tac "(xs! Suc i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   730
  apply(case_tac "fst(xs!i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   731
   apply(erule_tac x=i in allE, simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   732
  apply(case_tac "fst(xs!Suc i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   733
   apply(force simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   734
  apply(force simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   735
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   736
 apply(case_tac xs,simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   737
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   738
 apply (simp del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   739
 apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
   740
  apply(drule last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   741
  apply (simp del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   742
  apply(simp only:last_lift_not_None)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   743
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   744
--{* @{text "\<exists>i<length x. fst (x ! i) = Some Q"} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   745
apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   746
apply(drule_tac n=i and P="\<lambda>i. i < length x \<and> fst (x ! i) = Some Q" in Ex_first_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   747
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   748
apply (simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   749
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   750
 apply(frule_tac i=m in Seq_sound2,force)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   751
  apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   752
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   753
apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   754
apply(erule_tac x=s in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   755
apply(drule_tac c=xs in subsetD,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   756
 apply(case_tac "xs=[]",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   757
 apply(simp add:cp_def assum_def nth_append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   758
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   759
 apply(erule_tac x=i in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   760
  back 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   761
 apply(simp add:snd_lift)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   762
 apply(erule mp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   763
 apply(force elim:etranE intro:Env simp add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   764
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   765
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   766
apply(erule_tac x="snd(xs!m)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   767
apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   768
 apply(case_tac "xs\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
   769
 apply(drule last_conv_nth,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   770
 apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   771
  apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   772
  apply(case_tac "xs!m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   773
  apply(case_tac "fst(xs!m)",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   774
  apply(simp add:lift_def nth_append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   775
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   776
 apply(erule_tac x="m+i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   777
 back
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   778
 back
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   779
 apply(case_tac ys,(simp add:nth_append)+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   780
 apply (case_tac i, (simp add:snd_lift)+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   781
  apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   782
  apply(case_tac "xs!m")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   783
  apply(force elim:etran.cases intro:Env simp add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   784
 apply simp 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   785
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   786
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   787
apply(rule conjI,clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   788
 apply(case_tac "i<m",simp add:nth_append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   789
  apply(simp add:snd_lift)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   790
  apply(erule allE, erule impE, assumption, erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   791
  apply(case_tac "(xs ! i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   792
  apply(case_tac "(xs ! Suc i)")   
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   793
  apply(case_tac "fst(xs ! i)",force simp add:lift_def)   
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   794
  apply(case_tac "fst(xs ! Suc i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   795
   apply (force simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   796
  apply (force simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   797
 apply(erule_tac x="i-m" in allE) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   798
 back
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   799
 back
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   800
 apply(subgoal_tac "Suc (i - m) < length ys",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   801
  prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   802
  apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   803
 apply(simp add:nth_append snd_lift)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   804
 apply(rule conjI,clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   805
  apply(subgoal_tac "i=m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   806
   prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   807
   apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   808
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   809
  apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   810
  apply(rule tl_zero)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   811
    apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   812
    apply(case_tac "lift Q (xs!m)",simp add:snd_lift)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   813
    apply(case_tac "xs!m",case_tac "fst(xs!m)",simp add:lift_def snd_lift)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   814
     apply(case_tac ys,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   815
    apply(simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   816
   apply simp 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   817
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   818
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   819
 apply(rule tl_zero)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   820
   apply(rule tl_zero)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   821
     apply (subgoal_tac "i-m=Suc(i-Suc m)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   822
      apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   823
      apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   824
      apply(case_tac ys,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   825
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   826
  apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   827
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   828
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   829
apply(case_tac "(map (lift Q) xs @ tl ys)\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
   830
 apply(drule last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   831
 apply(simp add: snd_lift nth_append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   832
 apply(rule conjI,clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   833
  apply(case_tac ys,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   834
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   835
 apply(case_tac ys,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   836
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   837
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   838
subsubsection{* Soundness of the While rule *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   839
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   840
lemma last_append[rule_format]:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   841
  "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   842
apply(induct ys)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   843
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   844
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   845
apply (simp add:nth_append length_append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   846
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   847
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   848
lemma assum_after_body: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   849
  "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   850
  (Some P, s) # xs \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b;
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   851
  (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   852
   map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   853
  \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> assum (pre, rely)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   854
apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   855
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   856
apply(erule_tac x=s in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   857
apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   858
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   859
 apply(erule_tac x="Suc i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   860
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   861
 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   862
 apply(erule mp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   863
 apply(erule etranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   864
 apply(case_tac "fst(((Some P, s) # xs) ! i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   865
  apply(force intro:Env simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   866
 apply(force intro:Env simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   867
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   868
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   869
 apply(simp add:comm_def last_length)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   870
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   871
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   872
 apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   873
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   874
apply(erule_tac x="Suc(length xs + i)" in allE,simp)
41842
d8f76db6a207 added simp lemma nth_Cons_pos to List
nipkow
parents: 35416
diff changeset
   875
apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
d8f76db6a207 added simp lemma nth_Cons_pos to List
nipkow
parents: 35416
diff changeset
   876
apply(simp add:Cons_lift_append nth_append snd_lift)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   877
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   878
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   879
lemma While_sound_aux [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   880
  "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   881
   stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   882
  \<Longrightarrow>  \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   883
apply(erule cptn_mod.induct)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   884
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   885
apply (simp_all del:last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   886
--{* 5 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   887
apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   888
--{* 4 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   889
apply(rule etran_in_comm)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   890
apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   891
apply(erule tl_of_assum_in_assum,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   892
--{* While-None *}
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   893
apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran" for s t)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   894
apply(simp add:comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   895
apply(simp add:cptn_iff_cptn_mod [THEN sym])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   896
apply(rule conjI,clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   897
 apply(force simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   898
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   899
apply(rule conjI, clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   900
 apply(case_tac i,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   901
 apply(force simp add:not_ctran_None2)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   902
apply(subgoal_tac "\<forall>i. Suc i < length ((None, t) # xs) \<longrightarrow> (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\<in> etran")
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   903
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   904
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   905
 apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   906
 apply(erule not_ctran_None2,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   907
 apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   908
apply(frule_tac j="0" and k="length ((None, s) # xs) - 1" and p=post in stability,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   909
   apply(force simp add:assum_def subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   910
  apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   911
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   912
  apply(erule_tac x="i" in allE,simp) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   913
  apply(erule_tac x="Suc i" in allE,simp) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   914
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   915
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   916
apply (simp add:last_length)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   917
--{* WhileOne *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   918
apply(thin_tac "P = While b P \<longrightarrow> ?Q")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   919
apply(rule ctran_in_comm,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   920
apply(simp add:Cons_lift del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   921
apply(simp add:comm_def del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   922
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   923
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   924
 apply(case_tac "fst(((Some P, sa) # xs) ! i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   925
  apply(case_tac "((Some P, sa) # xs) ! i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   926
  apply (simp add:lift_def)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   927
  apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   928
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   929
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   930
 apply(simp add:snd_lift del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   931
 apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   932
 apply(erule_tac x=sa in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   933
 apply(drule_tac c="(Some P, sa) # xs" in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   934
  apply (simp add:assum_def del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   935
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   936
  apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   937
  apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   938
  apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   939
   apply(erule etranE,simp add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   940
   apply(rule Env)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   941
  apply(erule etranE,simp add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   942
  apply(rule Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   943
 apply (simp add:comm_def del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   944
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   945
 apply(erule allE,erule impE,assumption)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   946
 apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   947
 apply(case_tac "((Some P, sa) # xs) ! i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   948
 apply(case_tac "xs!i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   949
 apply(simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   950
 apply(case_tac "fst(xs!i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   951
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   952
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   953
--{* last=None *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   954
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   955
apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
   956
 apply(drule last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   957
 apply (simp del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   958
 apply(simp only:last_lift_not_None)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   959
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   960
--{* WhileMore *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   961
apply(thin_tac "P = While b P \<longrightarrow> ?Q")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   962
apply(rule ctran_in_comm,simp del:last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   963
--{* metiendo la hipotesis antes de dividir la conclusion. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   964
apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   965
 apply (simp del:last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   966
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   967
 apply(erule assum_after_body)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   968
  apply (simp del:last.simps)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   969
--{* lo de antes. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   970
apply(simp add:comm_def del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   971
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   972
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   973
 apply(simp only:Cons_lift_append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   974
 apply(case_tac "i<length xs")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   975
  apply(simp add:nth_append del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   976
  apply(case_tac "fst(((Some P, sa) # xs) ! i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   977
   apply(case_tac "((Some P, sa) # xs) ! i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   978
   apply (simp add:lift_def del:last.simps)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   979
   apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   980
    apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   981
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   982
  apply(simp add:snd_lift del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   983
  apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   984
  apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   985
  apply(erule_tac x=sa in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   986
  apply(drule_tac c="(Some P, sa) # xs" in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   987
   apply (simp add:assum_def del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   988
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   989
   apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   990
   apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   991
    apply(erule etranE,simp add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   992
    apply(rule Env)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
   993
   apply(erule etranE,simp add:lift_def)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   994
   apply(rule Env)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   995
  apply (simp add:comm_def del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   996
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   997
  apply(erule allE,erule impE,assumption)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   998
  apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   999
  apply(case_tac "((Some P, sa) # xs) ! i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1000
  apply(case_tac "xs!i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1001
  apply(simp add:lift_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1002
  apply(case_tac "fst(xs!i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1003
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1004
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1005
--{*  @{text "i \<ge> length xs"} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1006
apply(subgoal_tac "i-length xs <length ys") 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1007
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1008
 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1009
apply(erule_tac x="i-length xs" in allE,clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1010
apply(case_tac "i=length xs")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1011
 apply (simp add:nth_append snd_lift del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1012
 apply(simp add:last_length del:last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1013
 apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1014
 apply(case_tac "last((Some P, sa) # xs)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1015
 apply(simp add:lift_def del:last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1016
--{* @{text "i>length xs"} *} 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1017
apply(case_tac "i-length xs")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1018
 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1019
apply(simp add:nth_append del:map.simps last.simps)
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13099
diff changeset
  1020
apply(rotate_tac -3)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1021
apply(subgoal_tac "i- Suc (length xs)=nat")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1022
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1023
 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1024
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1025
--{* last=None *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1026
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1027
apply(case_tac ys)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1028
 apply(simp add:Cons_lift del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1029
 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
  1030
  apply(drule last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1031
  apply (simp del:map.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1032
  apply(simp only:last_lift_not_None)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1033
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1034
apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
  1035
 apply(drule last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1036
 apply (simp del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1037
 apply(simp add:nth_append del:last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1038
 apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
  1039
  apply(drule last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1040
  apply (simp del:map.simps last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1041
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1042
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1043
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1044
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1045
lemma While_sound: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1046
  "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1047
    \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1048
  \<Longrightarrow> \<Turnstile> While b P sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1049
apply(unfold com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1050
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1051
apply(erule_tac xs="tl x" in While_sound_aux)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1052
 apply(simp add:com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1053
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1054
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1055
apply(simp add:cptn_iff_cptn_mod cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1056
apply(simp add:cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1057
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1058
apply(rule nth_equalityI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1059
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1060
 apply(case_tac x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1061
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1062
apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1063
apply(case_tac x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1064
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1065
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1066
subsubsection{* Soundness of the Rule of Consequence *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1067
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1068
lemma Conseq_sound: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1069
  "\<lbrakk>pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1070
  \<Turnstile> P sat [pre', rely', guar', post']\<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1071
  \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1072
apply(simp add:com_validity_def assum_def comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1073
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1074
apply(erule_tac x=s in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1075
apply(drule_tac c=x in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1076
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1077
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1078
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1079
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1080
subsubsection {* Soundness of the system for sequential component programs *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1081
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1082
theorem rgsound: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1083
  "\<turnstile> P sat [pre, rely, guar, post] \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1084
apply(erule rghoare.induct)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1085
 apply(force elim:Basic_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1086
 apply(force elim:Seq_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1087
 apply(force elim:Cond_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1088
 apply(force elim:While_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1089
 apply(force elim:Await_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1090
apply(erule Conseq_sound,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1091
done     
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1092
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1093
subsection {* Soundness of the System for Parallel Programs *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1094
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32687
diff changeset
  1095
definition ParallelCom :: "('a rgformula) list \<Rightarrow> 'a par_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1096
  "ParallelCom Ps \<equiv> map (Some \<circ> fst) Ps" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1097
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1098
lemma two: 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1099
  "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1100
     \<subseteq> Rely (xs ! i);
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1101
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1102
   \<forall>i<length xs. 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1103
   \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1104
   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1105
  \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1106
  \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1107
  \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1108
apply(unfold par_cp_def)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1109
apply (rule ccontr) 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1110
--{* By contradiction: *}
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1111
apply (simp del: Un_subset_iff)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1112
apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1113
--{* the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1114
apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1115
apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1116
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1117
--{* @{text "\<sigma>_i \<in> A(pre, rely_1)"} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1118
apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \<in> assum(Pre(xs!i), Rely(xs!i))")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1119
--{* but this contradicts @{text "\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]"} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1120
 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1121
 apply(simp add:com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1122
 apply(erule_tac x=s in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1123
 apply(simp add:cp_def comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1124
 apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1125
  apply simp
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1126
  apply (blast intro: takecptn_is_cptn) 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1127
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1128
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1129
 apply(erule_tac x=m and P="\<lambda>j. ?I j \<and> ?J j \<longrightarrow> ?H j" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1130
 apply (simp add:conjoin_def same_length_def)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1131
apply(simp add:assum_def del: Un_subset_iff)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1132
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1133
 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow>  ?I j \<in>cp (?K j) (?J j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1134
 apply(simp add:cp_def par_assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1135
 apply(drule_tac c="s" in subsetD,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1136
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1137
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1138
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?M \<union> UNION (?S j) (?T j) \<subseteq>  (?L j)" in allE)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1139
apply(simp del: Un_subset_iff)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1140
apply(erule subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1141
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1142
apply(simp add:conjoin_def compat_label_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1143
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1144
apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j) \<or> ?Q j" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1145
--{* each etran in @{text "\<sigma>_1[0\<dots>m]"} corresponds to  *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1146
apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1147
--{* a c-tran in some @{text "\<sigma>_{ib}"}  *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1148
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1149
 apply(case_tac "i=ib",simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1150
  apply(erule etranE,simp)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
  1151
 apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1152
 apply (erule etranE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1153
 apply(case_tac "ia=m",simp)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
  1154
 apply simp
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1155
 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1156
 apply(subgoal_tac "ia<m",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1157
  prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1158
  apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1159
 apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1160
 apply(simp add:same_state_def)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
  1161
 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1162
 apply(erule_tac x=ib and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1163
--{* or an e-tran in @{text "\<sigma>"}, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1164
therefore it satisfies @{text "rely \<or> guar_{ib}"} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1165
apply (force simp add:par_assum_def same_state_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1166
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1167
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1168
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1169
lemma three [rule_format]: 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1170
  "\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1171
   \<subseteq> Rely (xs ! i);
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1172
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1173
   \<forall>i<length xs. 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1174
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1175
   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum(pre, rely);
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1176
  \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1177
  \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -e\<rightarrow> (clist!i!Suc j) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1178
  \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1179
apply(drule two)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1180
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1181
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1182
apply(simp add:conjoin_def compat_label_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1183
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1184
apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (?J j \<and> (\<exists>i. ?P i j)) \<or> ?I j" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1185
apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1186
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1187
 apply(force simp add:same_state_def par_assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1188
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1189
apply(case_tac "i=ia",simp)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1190
 apply(erule etranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1191
apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1192
apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1193
apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1194
apply(simp add:same_state_def)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
  1195
apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1196
apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1197
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1198
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1199
lemma four: 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1200
  "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1201
    \<subseteq> Rely (xs ! i);
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1202
   (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar; 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1203
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1204
   \<forall>i < length xs.
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1205
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1206
   x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x; 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1207
   x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1208
  \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1209
apply(simp add: ParallelCom_def del: Un_subset_iff)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1210
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1211
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1212
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1213
apply(frule rev_subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1214
 apply(erule one [THEN equalityD1])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1215
apply(erule subsetD)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1216
apply (simp del: Un_subset_iff)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1217
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1218
apply(drule_tac pre=pre and rely=rely and  x=x and s=s and xs=xs and clist=clist in two)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1219
apply(assumption+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1220
     apply(erule sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1221
    apply(simp add:ParallelCom_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1222
   apply assumption
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1223
  apply(simp add:Com_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1224
 apply assumption
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1225
apply(simp add:conjoin_def same_program_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1226
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1227
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in all_dupE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1228
apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1229
apply(erule par_ctranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1230
apply(erule_tac x=i and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1231
apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1232
apply(rule_tac x=ia in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1233
apply(simp add:same_state_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1234
apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1235
apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1236
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1237
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1238
apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1239
apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1240
apply(subgoal_tac "r=fst(clist ! ia ! Suc i)",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1241
apply(drule_tac i=ia in list_eq_if)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1242
back
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1243
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1244
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1245
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1246
lemma parcptn_not_empty [simp]:"[] \<notin> par_cptn"
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1247
apply(force elim:par_cptn.cases)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1248
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1249
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1250
lemma five: 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1251
  "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1252
   \<subseteq> Rely (xs ! i);
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1253
   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1254
   (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1255
   \<forall>i < length xs.
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1256
    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1257
    x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1258
   All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1259
apply(simp add: ParallelCom_def del: Un_subset_iff)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1260
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1261
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1262
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1263
apply(frule rev_subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1264
 apply(erule one [THEN equalityD1])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1265
apply(erule subsetD)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14315
diff changeset
  1266
apply(simp del: Un_subset_iff)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1267
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1268
apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1269
 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1270
 apply(simp add:com_validity_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1271
 apply(erule_tac x=s in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1272
 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I j) \<in> cp (?J j) s" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1273
 apply(drule_tac c="clist!i" in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1274
  apply (force simp add:Com_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1275
 apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1276
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1277
 apply(erule_tac x="length x - 1" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1278
 apply (simp add:All_None_def same_length_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1279
 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1280
 apply(subgoal_tac "length x - 1 < length x",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1281
  apply(case_tac "x\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
  1282
   apply(simp add: last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1283
   apply(erule_tac x="clist!i" in ballE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1284
    apply(simp add:same_state_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1285
    apply(subgoal_tac "clist!i\<noteq>[]")
17588
f2bd501398ee fix because of list lemmas
nipkow
parents: 17582
diff changeset
  1286
     apply(simp add: last_conv_nth)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1287
    apply(case_tac x)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1288
     apply (force simp add:par_cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1289
    apply (force simp add:par_cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1290
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1291
  apply (force simp add:par_cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1292
 apply(case_tac x)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1293
  apply (force simp add:par_cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1294
 apply (force simp add:par_cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1295
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1296
apply(simp add:assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1297
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1298
 apply(simp add:conjoin_def same_state_def par_cp_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1299
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1300
 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1301
 apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1302
 apply(case_tac x,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1303
 apply (simp add:par_assum_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1304
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1305
 apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1306
 apply assumption
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1307
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1308
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1309
apply(erule_tac x=ia in all_dupE)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
  1310
apply(rule subsetD, erule mp, assumption)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1311
apply(erule_tac pre=pre and rely=rely and x=x and s=s in  three)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1312
 apply(erule_tac x=ic in allE,erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1313
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1314
 apply(simp add:ParallelCom_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1315
 apply(force simp add:Com_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1316
apply(simp add:conjoin_def same_length_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1317
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1318
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1319
lemma ParallelEmpty [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1320
  "\<forall>i s. x \<in> par_cp (ParallelCom []) s \<longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1321
  Suc i < length x \<longrightarrow> (x ! i, x ! Suc i) \<notin> par_ctran"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1322
apply(induct_tac x)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1323
 apply(simp add:par_cp_def ParallelCom_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1324
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1325
apply(case_tac list,simp,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1326
apply(case_tac i)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1327
 apply(simp add:par_cp_def ParallelCom_def)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1328
 apply(erule par_ctranE,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1329
apply(simp add:par_cp_def ParallelCom_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1330
apply clarify
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1331
apply(erule par_cptn.cases,simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1332
 apply simp
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 20432
diff changeset
  1333
apply(erule par_ctranE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1334
back
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1335
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1336
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1337
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1338
theorem par_rgsound: 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1339
  "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow> 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
  1340
   \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1341
apply(erule par_rghoare.induct)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1342
apply(case_tac xs,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1343
 apply(simp add:par_com_validity_def par_comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1344
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1345
 apply(case_tac "post=UNIV",simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1346
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1347
  apply(drule ParallelEmpty)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1348
   apply assumption
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1349
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1350
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1351
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1352
apply(subgoal_tac "xs\<noteq>[]")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1353
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1354
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1355
apply(thin_tac "xs = a # list")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1356
apply(simp add:par_com_validity_def par_comm_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1357
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1358
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1359
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1360
 apply(erule_tac pre=pre and rely=rely and guar=guar and x=x and s=s and xs=xs in four)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1361
        apply(assumption+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1362
     apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1363
     apply (erule allE, erule impE, assumption,erule rgsound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1364
    apply(assumption+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1365
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1366
apply(erule_tac pre=pre and rely=rely and post=post and x=x and s=s and xs=xs in five)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1367
      apply(assumption+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1368
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1369
   apply (erule allE, erule impE, assumption,erule rgsound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1370
  apply(assumption+) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1371
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
  1372
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13099
diff changeset
  1373
end