src/HOL/Hoare_Parallel/OG_Tactics.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44928 7ef6505bde7f
child 51717 9e7d1c139569
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{Generation of Verification Conditions} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 23894
diff changeset
     3
theory OG_Tactics
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 23894
diff changeset
     4
imports OG_Hoare
15425
6356d2523f73 [ .. (] -> [ ..< ]
nipkow
parents: 13187
diff changeset
     5
begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     6
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     7
lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     8
lemmas oghoare_intros=Parallel Basic Seq Cond While Conseq
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     9
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    10
lemma ParallelConseqRule: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
 "\<lbrakk> p \<subseteq> (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i))));  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
  \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i)))) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
      (Parallel Ts) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
     (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i));  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    15
  (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i)) \<subseteq> q \<rbrakk>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
  \<Longrightarrow> \<parallel>- p (Parallel Ts) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
apply (rule Conseq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
prefer 2 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
 apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
apply assumption+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    21
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    23
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> \<parallel>- p (Basic id) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    24
apply(rule oghoare_intros)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    25
  prefer 2 apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    26
 prefer 2 apply(rule subset_refl)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    27
apply(simp add:Id_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    28
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    29
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    30
lemma BasicRule: "p \<subseteq> {s. (f s)\<in>q} \<Longrightarrow> \<parallel>- p (Basic f) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    31
apply(rule oghoare_intros)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    32
  prefer 2 apply(rule oghoare_intros)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    33
 prefer 2 apply(rule subset_refl)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    34
apply assumption
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    36
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    37
lemma SeqRule: "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    38
apply(rule Seq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    39
apply fast+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    40
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    41
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    42
lemma CondRule: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    43
 "\<lbrakk> p \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>w) \<and> (s\<notin>b \<longrightarrow> s\<in>w')}; \<parallel>- w c1 q; \<parallel>- w' c2 q \<rbrakk> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    44
  \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    45
apply(rule Cond)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    46
 apply(rule Conseq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    47
 prefer 4 apply(rule Conseq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    48
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    49
apply force+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    50
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    51
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    52
lemma WhileRule: "\<lbrakk> p \<subseteq> i; \<parallel>- (i \<inter> b) c i ; (i \<inter> (-b)) \<subseteq> q \<rbrakk>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    53
        \<Longrightarrow> \<parallel>- p (While b i c) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    54
apply(rule Conseq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    55
 prefer 2 apply(rule While)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    56
apply assumption+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    57
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    58
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    59
text {* Three new proof rules for special instances of the @{text
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    60
AnnBasic} and the @{text AnnAwait} commands when the transformation
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    61
performed on the state is the identity, and for an @{text AnnAwait}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    62
command where the boolean condition is @{text "{s. True}"}: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    63
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    64
lemma AnnatomRule:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    65
  "\<lbrakk> atom_com(c); \<parallel>- r c q \<rbrakk>  \<Longrightarrow> \<turnstile> (AnnAwait r {s. True} c) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    66
apply(rule AnnAwait)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    67
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    68
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    69
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    70
lemma AnnskipRule:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    71
  "r \<subseteq> q \<Longrightarrow> \<turnstile> (AnnBasic r id) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    72
apply(rule AnnBasic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    73
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    74
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    75
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    76
lemma AnnwaitRule:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    77
  "\<lbrakk> (r \<inter> b) \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b (Basic id)) q"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    78
apply(rule AnnAwait)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    79
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    80
apply(rule BasicRule)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    81
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    82
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    83
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    84
text {* Lemmata to avoid using the definition of @{text
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    85
map_ann_hoare}, @{text interfree_aux}, @{text interfree_swap} and
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    86
@{text interfree} by splitting it into different cases: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    87
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    88
lemma interfree_aux_rule1: "interfree_aux(co, q, None)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    89
by(simp add:interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    90
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    91
lemma interfree_aux_rule2: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    92
  "\<forall>(R,r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<Longrightarrow> interfree_aux(None, q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    93
apply(simp add:interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    94
apply(force elim:oghoare_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    95
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    96
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    97
lemma interfree_aux_rule3: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    98
  "(\<forall>(R, r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<and> (\<forall>p\<in>(assertions c). \<parallel>- (p \<inter> R) r p))
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    99
  \<Longrightarrow> interfree_aux(Some c, q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   100
apply(simp add:interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   101
apply(force elim:oghoare_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   102
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   103
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   104
lemma AnnBasic_assertions: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   105
  "\<lbrakk>interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk> \<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   106
    interfree_aux(Some (AnnBasic r f), q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   107
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   108
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   109
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   110
lemma AnnSeq_assertions: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   111
  "\<lbrakk> interfree_aux(Some c1, q, Some a); interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   112
   interfree_aux(Some (AnnSeq c1 c2), q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   113
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   114
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   115
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   116
lemma AnnCond1_assertions: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   117
  "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c1, q, Some a); 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   118
  interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   119
  interfree_aux(Some(AnnCond1 r b c1 c2), q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   120
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   121
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   122
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   123
lemma AnnCond2_assertions: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   124
  "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   125
  interfree_aux(Some (AnnCond2 r b c), q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   126
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   127
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   128
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   129
lemma AnnWhile_assertions: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   130
  "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, i, Some a); 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   131
  interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   132
  interfree_aux(Some (AnnWhile r b i c), q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   133
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   134
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   135
 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   136
lemma AnnAwait_assertions: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   137
  "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk>\<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   138
  interfree_aux(Some (AnnAwait r b c), q, Some a)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   139
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   140
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   141
 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   142
lemma AnnBasic_atomics: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   143
  "\<parallel>- (q \<inter> r) (Basic f) q \<Longrightarrow> interfree_aux(None, q, Some (AnnBasic r f))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   144
by(simp add: interfree_aux_def oghoare_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   145
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   146
lemma AnnSeq_atomics: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   147
  "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   148
  interfree_aux(Any, q, Some (AnnSeq a1 a2))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   149
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   150
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   151
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   152
lemma AnnCond1_atomics:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   153
  "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   154
   interfree_aux(Any, q, Some (AnnCond1 r b a1 a2))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   155
apply(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   156
by force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   157
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   158
lemma AnnCond2_atomics: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   159
  "interfree_aux (Any, q, Some a)\<Longrightarrow> interfree_aux(Any, q, Some (AnnCond2 r b a))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   160
by(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   161
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   162
lemma AnnWhile_atomics: "interfree_aux (Any, q, Some a) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   163
     \<Longrightarrow> interfree_aux(Any, q, Some (AnnWhile r b i a))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   164
by(simp add: interfree_aux_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   165
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   166
lemma Annatom_atomics: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   167
  "\<parallel>- (q \<inter> r) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r {x. True} a))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   168
by(simp add: interfree_aux_def oghoare_sound) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   169
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   170
lemma AnnAwait_atomics: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   171
  "\<parallel>- (q \<inter> (r \<inter> b)) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r b a))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   172
by(simp add: interfree_aux_def oghoare_sound)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   173
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32621
diff changeset
   174
definition interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   175
  "interfree_swap == \<lambda>(x, xs). \<forall>y\<in>set xs. interfree_aux (com x, post x, com y)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   176
  \<and> interfree_aux(com y, post y, com x)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   177
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   178
lemma interfree_swap_Empty: "interfree_swap (x, [])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   179
by(simp add:interfree_swap_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   180
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   181
lemma interfree_swap_List:  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   182
  "\<lbrakk> interfree_aux (com x, post x, com y); 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   183
  interfree_aux (com y, post y ,com x); interfree_swap (x, xs) \<rbrakk> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   184
  \<Longrightarrow> interfree_swap (x, y#xs)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   185
by(simp add:interfree_swap_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   186
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   187
lemma interfree_swap_Map: "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> interfree_aux (com x, post x, c k) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   188
 \<and> interfree_aux (c k, Q k, com x)   
15425
6356d2523f73 [ .. (] -> [ ..< ]
nipkow
parents: 13187
diff changeset
   189
 \<Longrightarrow> interfree_swap (x, map (\<lambda>k. (c k, Q k)) [i..<j])"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   190
by(force simp add: interfree_swap_def less_diff_conv)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   191
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   192
lemma interfree_Empty: "interfree []"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   193
by(simp add:interfree_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   194
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   195
lemma interfree_List: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   196
  "\<lbrakk> interfree_swap(x, xs); interfree xs \<rbrakk> \<Longrightarrow> interfree (x#xs)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   197
apply(simp add:interfree_def interfree_swap_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   198
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   199
apply(case_tac i)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   200
 apply(case_tac j)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   201
  apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   202
apply(case_tac j,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   203
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   204
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   205
lemma interfree_Map: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   206
  "(\<forall>i j. a\<le>i \<and> i<b \<and> a\<le>j \<and> j<b  \<and> i\<noteq>j \<longrightarrow> interfree_aux (c i, Q i, c j))  
15425
6356d2523f73 [ .. (] -> [ ..< ]
nipkow
parents: 13187
diff changeset
   207
  \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..<b])"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   208
by(force simp add: interfree_def less_diff_conv)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   209
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32621
diff changeset
   210
definition map_ann_hoare :: "(('a ann_com_op * 'a assn) list) \<Rightarrow> bool " ("[\<turnstile>] _" [0] 45) where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   211
  "[\<turnstile>] Ts == (\<forall>i<length Ts. \<exists>c q. Ts!i=(Some c, q) \<and> \<turnstile> c q)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   212
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   213
lemma MapAnnEmpty: "[\<turnstile>] []"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   214
by(simp add:map_ann_hoare_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   215
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   216
lemma MapAnnList: "\<lbrakk> \<turnstile> c q ; [\<turnstile>] xs \<rbrakk> \<Longrightarrow> [\<turnstile>] (Some c,q)#xs"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   217
apply(simp add:map_ann_hoare_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   218
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   219
apply(case_tac i,simp+)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   220
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   221
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   222
lemma MapAnnMap: 
15425
6356d2523f73 [ .. (] -> [ ..< ]
nipkow
parents: 13187
diff changeset
   223
  "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> \<turnstile> (c k) (Q k) \<Longrightarrow> [\<turnstile>] map (\<lambda>k. (Some (c k), Q k)) [i..<j]"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   224
apply(simp add: map_ann_hoare_def less_diff_conv)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   225
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   226
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   227
lemma ParallelRule:"\<lbrakk> [\<turnstile>] Ts ; interfree Ts \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   228
  \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i)))) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   229
          Parallel Ts 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   230
        (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   231
apply(rule Parallel)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   232
 apply(simp add:map_ann_hoare_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   233
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   234
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   235
(*
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   236
lemma ParamParallelRule:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   237
 "\<lbrakk> \<forall>k<n. \<turnstile> (c k) (Q k); 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   238
   \<forall>k l. k<n \<and> l<n  \<and> k\<noteq>l \<longrightarrow> interfree_aux (Some(c k), Q k, Some(c l)) \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   239
  \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<n} . pre(c i)) COBEGIN SCHEME [0\<le>i<n] (c i) (Q i) COEND  (\<Inter>i\<in>{i. i<n} . Q i )"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   240
apply(rule ParallelConseqRule)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   241
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   242
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   243
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   244
 apply(rule ParallelRule)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   245
  apply(rule MapAnnMap)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   246
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   247
 apply(rule interfree_Map)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   248
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   249
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   250
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   251
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   252
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   253
*)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   254
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   255
text {* The following are some useful lemmas and simplification
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   256
tactics to control which theorems are used to simplify at each moment,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   257
so that the original input does not suffer any unexpected
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   258
transformation. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   259
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   260
lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   261
by fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   262
lemma list_length: "length []=0 \<and> length (x#xs) = Suc(length xs)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   263
by simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   264
lemma list_lemmas: "length []=0 \<and> length (x#xs) = Suc(length xs) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   265
\<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   266
by simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   267
lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13020
diff changeset
   268
by auto
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   269
lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   270
lemmas my_simp_list = list_lemmas fst_conv snd_conv
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 23894
diff changeset
   271
not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   272
Collect_mem_eq ball_simps option.simps primrecdef_list
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 39159
diff changeset
   273
lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append list_length
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   274
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   275
ML {*
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 37136
diff changeset
   276
val before_interfree_simp_tac = simp_tac (HOL_basic_ss addsimps [@{thm com.simps}, @{thm post.simps}])
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   277
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 37136
diff changeset
   278
val  interfree_simp_tac = asm_simp_tac (HOL_ss addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list})
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   279
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 37136
diff changeset
   280
val ParallelConseq = simp_tac (HOL_basic_ss addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list})
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   281
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   282
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   283
text {* The following tactic applies @{text tac} to each conjunct in a
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   284
subgoal of the form @{text "A \<Longrightarrow> a1 \<and> a2 \<and> .. \<and> an"}  returning
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   285
@{text n} subgoals, one for each conjunct: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   286
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   287
ML {*
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   288
fun conjI_Tac tac i st = st |>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   289
       ( (EVERY [rtac conjI i,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   290
          conjI_Tac tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   291
          tac i]) ORELSE (tac i) )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   292
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   293
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   294
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   295
subsubsection {* Tactic for the generation of the verification conditions *} 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   296
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   297
text {* The tactic basically uses two subtactics:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   298
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   299
\begin{description}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   300
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   301
\item[HoareRuleTac] is called at the level of parallel programs, it        
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   302
 uses the ParallelTac to solve parallel composition of programs.         
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   303
 This verification has two parts, namely, (1) all component programs are 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   304
 correct and (2) they are interference free.  @{text HoareRuleTac} is
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   305
 also called at the level of atomic regions, i.e.  @{text "\<langle> \<rangle>"} and
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   306
 @{text "AWAIT b THEN _ END"}, and at each interference freedom test.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   307
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   308
\item[AnnHoareRuleTac] is for component programs which  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   309
 are annotated programs and so, there are not unknown assertions         
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   310
 (no need to use the parameter precond, see NOTE).
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   311
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   312
 NOTE: precond(::bool) informs if the subgoal has the form @{text "\<parallel>- ?p c q"},
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   313
 in this case we have precond=False and the generated  verification     
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   314
 condition would have the form @{text "?p \<subseteq> \<dots>"} which can be solved by        
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   315
 @{text "rtac subset_refl"}, if True we proceed to simplify it using
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   316
 the simplification tactics above.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   317
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   318
\end{description}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   319
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   320
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   321
ML {*
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   322
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   323
 fun WlpTac i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac false (i+1))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   324
and HoareRuleTac precond i st = st |>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   325
    ( (WlpTac i THEN HoareRuleTac precond i)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   326
      ORELSE
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   327
      (FIRST[rtac (@{thm SkipRule}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   328
             rtac (@{thm BasicRule}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   329
             EVERY[rtac (@{thm ParallelConseqRule}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   330
                   ParallelConseq (i+2),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   331
                   ParallelTac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   332
                   ParallelConseq i], 
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   333
             EVERY[rtac (@{thm CondRule}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   334
                   HoareRuleTac false (i+2),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   335
                   HoareRuleTac false (i+1)],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   336
             EVERY[rtac (@{thm WhileRule}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   337
                   HoareRuleTac true (i+1)],
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   338
             K all_tac i ]
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   339
       THEN (if precond then (K all_tac i) else (rtac (@{thm subset_refl}) i))))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   340
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   341
and  AnnWlpTac i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac (i+1))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   342
and AnnHoareRuleTac i st = st |>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   343
    ( (AnnWlpTac i THEN AnnHoareRuleTac i )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   344
     ORELSE
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   345
      (FIRST[(rtac (@{thm AnnskipRule}) i),
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   346
             EVERY[rtac (@{thm AnnatomRule}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   347
                   HoareRuleTac true (i+1)],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   348
             (rtac (@{thm AnnwaitRule}) i),
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   349
             rtac (@{thm AnnBasic}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   350
             EVERY[rtac (@{thm AnnCond1}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   351
                   AnnHoareRuleTac (i+3),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   352
                   AnnHoareRuleTac (i+1)],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   353
             EVERY[rtac (@{thm AnnCond2}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   354
                   AnnHoareRuleTac (i+1)],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   355
             EVERY[rtac (@{thm AnnWhile}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   356
                   AnnHoareRuleTac (i+2)],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   357
             EVERY[rtac (@{thm AnnAwait}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   358
                   HoareRuleTac true (i+1)],
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   359
             K all_tac i]))
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   360
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   361
and ParallelTac i = EVERY[rtac (@{thm ParallelRule}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   362
                          interfree_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   363
                           MapAnn_Tac i]
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   364
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   365
and MapAnn_Tac i st = st |>
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   366
    (FIRST[rtac (@{thm MapAnnEmpty}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   367
           EVERY[rtac (@{thm MapAnnList}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   368
                 MapAnn_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   369
                 AnnHoareRuleTac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   370
           EVERY[rtac (@{thm MapAnnMap}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   371
                 rtac (@{thm allI}) i,rtac (@{thm impI}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   372
                 AnnHoareRuleTac i]])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   373
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   374
and interfree_swap_Tac i st = st |>
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   375
    (FIRST[rtac (@{thm interfree_swap_Empty}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   376
           EVERY[rtac (@{thm interfree_swap_List}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   377
                 interfree_swap_Tac (i+2),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   378
                 interfree_aux_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   379
                 interfree_aux_Tac i ],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   380
           EVERY[rtac (@{thm interfree_swap_Map}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   381
                 rtac (@{thm allI}) i,rtac (@{thm impI}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   382
                 conjI_Tac (interfree_aux_Tac) i]])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   383
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   384
and interfree_Tac i st = st |> 
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   385
   (FIRST[rtac (@{thm interfree_Empty}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   386
          EVERY[rtac (@{thm interfree_List}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   387
                interfree_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   388
                interfree_swap_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   389
          EVERY[rtac (@{thm interfree_Map}) i,
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   390
                rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   391
                interfree_aux_Tac i ]])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   392
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   393
and interfree_aux_Tac i = (before_interfree_simp_tac i ) THEN 
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   394
        (FIRST[rtac (@{thm interfree_aux_rule1}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   395
               dest_assertions_Tac i])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   396
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   397
and dest_assertions_Tac i st = st |>
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   398
    (FIRST[EVERY[rtac (@{thm AnnBasic_assertions}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   399
                 dest_atomics_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   400
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   401
           EVERY[rtac (@{thm AnnSeq_assertions}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   402
                 dest_assertions_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   403
                 dest_assertions_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   404
           EVERY[rtac (@{thm AnnCond1_assertions}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   405
                 dest_assertions_Tac (i+2),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   406
                 dest_assertions_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   407
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   408
           EVERY[rtac (@{thm AnnCond2_assertions}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   409
                 dest_assertions_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   410
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   411
           EVERY[rtac (@{thm AnnWhile_assertions}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   412
                 dest_assertions_Tac (i+2),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   413
                 dest_atomics_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   414
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   415
           EVERY[rtac (@{thm AnnAwait_assertions}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   416
                 dest_atomics_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   417
                 dest_atomics_Tac i],
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   418
           dest_atomics_Tac i])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   419
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   420
and dest_atomics_Tac i st = st |>
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   421
    (FIRST[EVERY[rtac (@{thm AnnBasic_atomics}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   422
                 HoareRuleTac true i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   423
           EVERY[rtac (@{thm AnnSeq_atomics}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   424
                 dest_atomics_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   425
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   426
           EVERY[rtac (@{thm AnnCond1_atomics}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   427
                 dest_atomics_Tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   428
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   429
           EVERY[rtac (@{thm AnnCond2_atomics}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   430
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   431
           EVERY[rtac (@{thm AnnWhile_atomics}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   432
                 dest_atomics_Tac i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   433
           EVERY[rtac (@{thm Annatom_atomics}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   434
                 HoareRuleTac true i],
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   435
           EVERY[rtac (@{thm AnnAwait_atomics}) i,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   436
                 HoareRuleTac true i],
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   437
                 K all_tac i])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   438
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   439
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   440
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   441
text {* The final tactic is given the name @{text oghoare}: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   442
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   443
ML {* 
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   444
val oghoare_tac = SUBGOAL (fn (_, i) =>
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   445
   (HoareRuleTac true i))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   446
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   447
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   448
text {* Notice that the tactic for parallel programs @{text
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   449
"oghoare_tac"} is initially invoked with the value @{text true} for
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   450
the parameter @{text precond}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   451
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   452
Parts of the tactic can be also individually used to generate the
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   453
verification conditions for annotated sequential programs and to
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   454
generate verification conditions out of interference freedom tests: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   455
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   456
ML {* val annhoare_tac = SUBGOAL (fn (_, i) =>
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   457
  (AnnHoareRuleTac i))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   458
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   459
val interfree_aux_tac = SUBGOAL (fn (_, i) =>
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 21588
diff changeset
   460
   (interfree_aux_Tac i))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   461
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   462
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   463
text {* The so defined ML tactics are then ``exported'' to be used in
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   464
Isabelle proofs. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   465
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   466
method_setup oghoare = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   467
  Scan.succeed (K (SIMPLE_METHOD' oghoare_tac)) *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   468
  "verification condition generator for the oghoare logic"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   469
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   470
method_setup annhoare = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   471
  Scan.succeed (K (SIMPLE_METHOD' annhoare_tac)) *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   472
  "verification condition generator for the ann_hoare logic"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   473
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   474
method_setup interfree_aux = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   475
  Scan.succeed (K (SIMPLE_METHOD' interfree_aux_tac)) *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   476
  "verification condition generator for interference freedom tests"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   477
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   478
text {* Tactics useful for dealing with the generated verification conditions: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   479
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   480
method_setup conjI_tac = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   481
  Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac)))) *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   482
  "verification condition generator for interference freedom tests"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   483
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   484
ML {*
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   485
fun disjE_Tac tac i st = st |>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   486
       ( (EVERY [etac disjE i,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   487
          disjE_Tac tac (i+1),
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   488
          tac i]) ORELSE (tac i) )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   489
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   490
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   491
method_setup disjE_tac = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   492
  Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac)))) *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   493
  "verification condition generator for interference freedom tests"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   494
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13020
diff changeset
   495
end