src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 32687 27530efec97a
child 35416 d8d7d1b785af
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
prensani@13020
     1
prensani@13020
     2
header {* \section{The Multi-Mutator Case} *}
prensani@13020
     3
haftmann@16417
     4
theory Mul_Gar_Coll imports Graph OG_Syntax begin
prensani@13020
     5
prensani@13020
     6
text {*  The full theory takes aprox. 18 minutes.  *}
prensani@13020
     7
prensani@13020
     8
record mut =
prensani@13020
     9
  Z :: bool
prensani@13020
    10
  R :: nat
prensani@13020
    11
  T :: nat
prensani@13020
    12
prensani@13020
    13
text {* Declaration of variables: *}
prensani@13020
    14
prensani@13020
    15
record mul_gar_coll_state =
prensani@13020
    16
  M :: nodes
prensani@13020
    17
  E :: edges
prensani@13020
    18
  bc :: "nat set"
prensani@13020
    19
  obc :: "nat set"
prensani@13020
    20
  Ma :: nodes
prensani@13020
    21
  ind :: nat 
prensani@13020
    22
  k :: nat
prensani@13020
    23
  q :: nat
prensani@13020
    24
  l :: nat
prensani@13020
    25
  Muts :: "mut list"
prensani@13020
    26
prensani@13020
    27
subsection {* The Mutators *}
prensani@13020
    28
prensani@13020
    29
constdefs 
prensani@13020
    30
  Mul_mut_init :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
prensani@13020
    31
  "Mul_mut_init \<equiv> \<guillemotleft> \<lambda>n. n=length \<acute>Muts \<and> (\<forall>i<n. R (\<acute>Muts!i)<length \<acute>E 
prensani@13020
    32
                          \<and> T (\<acute>Muts!i)<length \<acute>M) \<guillemotright>"
prensani@13020
    33
prensani@13020
    34
  Mul_Redirect_Edge  :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com"
prensani@13020
    35
  "Mul_Redirect_Edge j n \<equiv>
prensani@13020
    36
  .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.
prensani@13020
    37
  \<langle>IF T(\<acute>Muts!j) \<in> Reach \<acute>E THEN  
prensani@13020
    38
  \<acute>E:= \<acute>E[R (\<acute>Muts!j):= (fst (\<acute>E!R(\<acute>Muts!j)), T (\<acute>Muts!j))] FI,, 
prensani@13020
    39
  \<acute>Muts:= \<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=False\<rparr>]\<rangle>"
prensani@13020
    40
prensani@13020
    41
  Mul_Color_Target :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com"
prensani@13020
    42
  "Mul_Color_Target j n \<equiv>
prensani@13020
    43
  .{\<acute>Mul_mut_init n \<and> \<not> Z (\<acute>Muts!j)}. 
prensani@13020
    44
  \<langle>\<acute>M:=\<acute>M[T (\<acute>Muts!j):=Black],, \<acute>Muts:=\<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=True\<rparr>]\<rangle>"
prensani@13020
    45
prensani@13020
    46
  Mul_Mutator :: "nat \<Rightarrow> nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
    47
  "Mul_Mutator j n \<equiv>
prensani@13020
    48
  .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.  
prensani@13020
    49
  WHILE True  
prensani@13020
    50
    INV .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.  
prensani@13020
    51
  DO Mul_Redirect_Edge j n ;; 
prensani@13020
    52
     Mul_Color_Target j n 
prensani@13020
    53
  OD"
prensani@13020
    54
prensani@13020
    55
lemmas mul_mutator_defs = Mul_mut_init_def Mul_Redirect_Edge_def Mul_Color_Target_def 
prensani@13020
    56
prensani@13020
    57
subsubsection {* Correctness of the proof outline of one mutator *}
prensani@13020
    58
prensani@13020
    59
lemma Mul_Redirect_Edge: "0\<le>j \<and> j<n \<Longrightarrow> 
prensani@13020
    60
  \<turnstile> Mul_Redirect_Edge j n 
prensani@13020
    61
     pre(Mul_Color_Target j n)"
prensani@13020
    62
apply (unfold mul_mutator_defs)
prensani@13020
    63
apply annhoare
prensani@13020
    64
apply(simp_all)
prensani@13020
    65
apply clarify
prensani@13020
    66
apply(simp add:nth_list_update)
prensani@13020
    67
done
prensani@13020
    68
prensani@13020
    69
lemma Mul_Color_Target: "0\<le>j \<and> j<n \<Longrightarrow> 
prensani@13020
    70
  \<turnstile>  Mul_Color_Target j n  
prensani@13020
    71
    .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}."
prensani@13020
    72
apply (unfold mul_mutator_defs)
prensani@13020
    73
apply annhoare
prensani@13020
    74
apply(simp_all)
prensani@13020
    75
apply clarify
prensani@13020
    76
apply(simp add:nth_list_update)
prensani@13020
    77
done
prensani@13020
    78
prensani@13020
    79
lemma Mul_Mutator: "0\<le>j \<and> j<n \<Longrightarrow>  
prensani@13020
    80
 \<turnstile> Mul_Mutator j n .{False}."
prensani@13020
    81
apply(unfold Mul_Mutator_def)
prensani@13020
    82
apply annhoare
prensani@13020
    83
apply(simp_all add:Mul_Redirect_Edge Mul_Color_Target)
prensani@13020
    84
apply(simp add:mul_mutator_defs Mul_Redirect_Edge_def)
prensani@13020
    85
done
prensani@13020
    86
prensani@13020
    87
subsubsection {* Interference freedom between mutators *}
prensani@13020
    88
prensani@13020
    89
lemma Mul_interfree_Redirect_Edge_Redirect_Edge: 
prensani@13020
    90
  "\<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow>  
prensani@13020
    91
  interfree_aux (Some (Mul_Redirect_Edge i n),{}, Some(Mul_Redirect_Edge j n))"
prensani@13020
    92
apply (unfold mul_mutator_defs)
prensani@13020
    93
apply interfree_aux
prensani@13020
    94
apply safe
prensani@13020
    95
apply(simp_all add: nth_list_update)
prensani@13020
    96
done
prensani@13020
    97
prensani@13020
    98
lemma Mul_interfree_Redirect_Edge_Color_Target: 
prensani@13020
    99
  "\<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow>  
prensani@13020
   100
  interfree_aux (Some(Mul_Redirect_Edge i n),{},Some(Mul_Color_Target j n))"
prensani@13020
   101
apply (unfold mul_mutator_defs)
prensani@13020
   102
apply interfree_aux
prensani@13020
   103
apply safe
prensani@13020
   104
apply(simp_all add: nth_list_update)
prensani@13020
   105
done
prensani@13020
   106
prensani@13020
   107
lemma Mul_interfree_Color_Target_Redirect_Edge: 
prensani@13020
   108
  "\<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow> 
prensani@13020
   109
  interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Redirect_Edge j n))"
prensani@13020
   110
apply (unfold mul_mutator_defs)
prensani@13020
   111
apply interfree_aux
prensani@13020
   112
apply safe
prensani@13020
   113
apply(simp_all add:nth_list_update)
prensani@13020
   114
done
prensani@13020
   115
prensani@13020
   116
lemma Mul_interfree_Color_Target_Color_Target: 
prensani@13020
   117
  " \<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow> 
prensani@13020
   118
  interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Color_Target j n))"
prensani@13020
   119
apply (unfold mul_mutator_defs)
prensani@13020
   120
apply interfree_aux
prensani@13020
   121
apply safe
prensani@13020
   122
apply(simp_all add: nth_list_update)
prensani@13020
   123
done
prensani@13020
   124
prensani@13020
   125
lemmas mul_mutator_interfree = 
prensani@13020
   126
  Mul_interfree_Redirect_Edge_Redirect_Edge Mul_interfree_Redirect_Edge_Color_Target
prensani@13020
   127
  Mul_interfree_Color_Target_Redirect_Edge Mul_interfree_Color_Target_Color_Target
prensani@13020
   128
prensani@13020
   129
lemma Mul_interfree_Mutator_Mutator: "\<lbrakk>i < n; j < n; i \<noteq> j\<rbrakk> \<Longrightarrow> 
prensani@13020
   130
  interfree_aux (Some (Mul_Mutator i n), {}, Some (Mul_Mutator j n))"
prensani@13020
   131
apply(unfold Mul_Mutator_def)
prensani@13020
   132
apply(interfree_aux)
prensani@13020
   133
apply(simp_all add:mul_mutator_interfree)
prensani@13020
   134
apply(simp_all add: mul_mutator_defs)
prensani@13020
   135
apply(tactic {* TRYALL (interfree_aux_tac) *})
wenzelm@23894
   136
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
prensani@13020
   137
apply (simp_all add:nth_list_update)
prensani@13020
   138
done
prensani@13020
   139
prensani@13020
   140
subsubsection {* Modular Parameterized Mutators *}
prensani@13020
   141
prensani@13020
   142
lemma Mul_Parameterized_Mutators: "0<n \<Longrightarrow>
prensani@13020
   143
 \<parallel>- .{\<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))}.
prensani@13020
   144
 COBEGIN
prensani@13020
   145
 SCHEME  [0\<le> j< n]
prensani@13020
   146
  Mul_Mutator j n
prensani@13020
   147
 .{False}.
prensani@13020
   148
 COEND
prensani@13020
   149
 .{False}."
prensani@13020
   150
apply oghoare
prensani@13020
   151
apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
prensani@13020
   152
apply(erule Mul_Mutator)
nipkow@13187
   153
apply(simp add:Mul_interfree_Mutator_Mutator)
prensani@13020
   154
apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
prensani@13020
   155
done
prensani@13020
   156
prensani@13020
   157
subsection {* The Collector *}
prensani@13020
   158
prensani@13020
   159
constdefs
prensani@13020
   160
  Queue :: "mul_gar_coll_state \<Rightarrow> nat"
prensani@13020
   161
 "Queue \<equiv> \<guillemotleft> length (filter (\<lambda>i. \<not> Z i \<and> \<acute>M!(T i) \<noteq> Black) \<acute>Muts) \<guillemotright>"
prensani@13020
   162
prensani@13020
   163
consts  M_init :: nodes
prensani@13020
   164
prensani@13020
   165
constdefs
prensani@13020
   166
  Proper_M_init :: "mul_gar_coll_state \<Rightarrow> bool"
prensani@13020
   167
  "Proper_M_init \<equiv> \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>"
prensani@13020
   168
prensani@13020
   169
  Mul_Proper :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
prensani@13020
   170
  "Mul_Proper \<equiv> \<guillemotleft> \<lambda>n. Proper_Roots \<acute>M \<and> Proper_Edges (\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<and> n=length \<acute>Muts \<guillemotright>"
prensani@13020
   171
prensani@13020
   172
  Safe :: "mul_gar_coll_state \<Rightarrow> bool"
prensani@13020
   173
  "Safe \<equiv> \<guillemotleft> Reach \<acute>E \<subseteq> Blacks \<acute>M \<guillemotright>"
prensani@13020
   174
prensani@13020
   175
lemmas mul_collector_defs = Proper_M_init_def Mul_Proper_def Safe_def
prensani@13020
   176
prensani@13020
   177
subsubsection {* Blackening Roots *}
prensani@13020
   178
prensani@13020
   179
constdefs
prensani@13020
   180
  Mul_Blacken_Roots :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   181
  "Mul_Blacken_Roots n \<equiv>
prensani@13020
   182
  .{\<acute>Mul_Proper n}.
prensani@13020
   183
  \<acute>ind:=0;;
prensani@13020
   184
  .{\<acute>Mul_Proper n \<and> \<acute>ind=0}.
prensani@13020
   185
  WHILE \<acute>ind<length \<acute>M 
prensani@13020
   186
    INV .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M}.
prensani@13020
   187
  DO .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.
prensani@13020
   188
       IF \<acute>ind\<in>Roots THEN 
prensani@13020
   189
     .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots}. 
prensani@13020
   190
       \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;
prensani@13020
   191
     .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind+1. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.
prensani@13020
   192
       \<acute>ind:=\<acute>ind+1 
prensani@13020
   193
  OD"
prensani@13020
   194
prensani@13020
   195
lemma Mul_Blacken_Roots: 
prensani@13020
   196
  "\<turnstile> Mul_Blacken_Roots n  
prensani@13020
   197
  .{\<acute>Mul_Proper n \<and> Roots \<subseteq> Blacks \<acute>M}."
prensani@13020
   198
apply (unfold Mul_Blacken_Roots_def)
prensani@13020
   199
apply annhoare
prensani@13020
   200
apply(simp_all add:mul_collector_defs Graph_defs)
prensani@13020
   201
apply safe
prensani@13020
   202
apply(simp_all add:nth_list_update)
prensani@13020
   203
  apply (erule less_SucE)
prensani@13020
   204
   apply simp+
prensani@13020
   205
 apply force
prensani@13020
   206
apply force
prensani@13020
   207
done
prensani@13020
   208
prensani@13020
   209
subsubsection {* Propagating Black *} 
prensani@13020
   210
prensani@13020
   211
constdefs
prensani@13020
   212
  Mul_PBInv :: "mul_gar_coll_state \<Rightarrow> bool"
prensani@13020
   213
  "Mul_PBInv \<equiv>  \<guillemotleft>\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
prensani@13020
   214
                 \<or> (\<forall>i<\<acute>ind. \<not>BtoW(\<acute>E!i,\<acute>M)) \<and> \<acute>l\<le>\<acute>Queue\<guillemotright>"
prensani@13020
   215
prensani@13020
   216
  Mul_Auxk :: "mul_gar_coll_state \<Rightarrow> bool"
prensani@13020
   217
  "Mul_Auxk \<equiv> \<guillemotleft>\<acute>l<\<acute>Queue \<or> \<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or> \<acute>obc\<subset>Blacks \<acute>M\<guillemotright>"
prensani@13020
   218
prensani@13020
   219
constdefs
prensani@13020
   220
  Mul_Propagate_Black :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   221
  "Mul_Propagate_Black n \<equiv>
prensani@13020
   222
 .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   223
  \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)}. 
prensani@13020
   224
 \<acute>ind:=0;;
prensani@13020
   225
 .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   226
   \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> Blacks \<acute>M\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   227
   \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) \<and> \<acute>ind=0}. 
prensani@13020
   228
 WHILE \<acute>ind<length \<acute>E 
prensani@13020
   229
  INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   230
        \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   231
        \<and> \<acute>Mul_PBInv \<and> \<acute>ind\<le>length \<acute>E}.
prensani@13020
   232
 DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   233
     \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   234
     \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E}.
prensani@13020
   235
   IF \<acute>M!(fst (\<acute>E!\<acute>ind))=Black THEN 
prensani@13020
   236
   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   237
     \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   238
     \<and> \<acute>Mul_PBInv \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black \<and> \<acute>ind<length \<acute>E}.
prensani@13020
   239
    \<acute>k:=snd(\<acute>E!\<acute>ind);;
prensani@13020
   240
   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   241
     \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   242
     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue \<or> (\<forall>i<\<acute>ind. \<not>BtoW(\<acute>E!i,\<acute>M)) 
prensani@13020
   243
        \<and> \<acute>l\<le>\<acute>Queue \<and> \<acute>Mul_Auxk ) \<and> \<acute>k<length \<acute>M \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black 
prensani@13020
   244
     \<and> \<acute>ind<length \<acute>E}.
prensani@13020
   245
   \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],,\<acute>ind:=\<acute>ind+1\<rangle>
prensani@13020
   246
   ELSE .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   247
         \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   248
         \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E}.
wenzelm@32960
   249
         \<langle>IF \<acute>M!(fst (\<acute>E!\<acute>ind))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle> FI
prensani@13020
   250
 OD"
prensani@13020
   251
prensani@13020
   252
lemma Mul_Propagate_Black: 
prensani@13020
   253
  "\<turnstile> Mul_Propagate_Black n  
prensani@13020
   254
   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   255
     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))}."
prensani@13020
   256
apply(unfold Mul_Propagate_Black_def)
prensani@13020
   257
apply annhoare
prensani@13020
   258
apply(simp_all add:Mul_PBInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
prensani@13020
   259
--{* 8 subgoals left *}
prensani@13020
   260
apply force
prensani@13020
   261
apply force
prensani@13020
   262
apply force
prensani@13020
   263
apply(force simp add:BtoW_def Graph_defs)
prensani@13020
   264
--{* 4 subgoals left *}
prensani@13020
   265
apply clarify
prensani@13020
   266
apply(simp add: mul_collector_defs Graph12 Graph6 Graph7 Graph8)
prensani@13020
   267
apply(disjE_tac)
prensani@13020
   268
 apply(simp_all add:Graph12 Graph13)
prensani@13020
   269
 apply(case_tac "M x! k x=Black")
prensani@13020
   270
  apply(simp add: Graph10)
prensani@13020
   271
 apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
prensani@13020
   272
apply(case_tac "M x! k x=Black")
prensani@13020
   273
 apply(simp add: Graph10 BtoW_def)
prensani@13020
   274
 apply(rule disjI2, clarify, erule less_SucE, force)
prensani@13020
   275
 apply(case_tac "M x!snd(E x! ind x)=Black")
prensani@13020
   276
  apply(force)
prensani@13020
   277
 apply(force)
prensani@13020
   278
apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
prensani@13020
   279
--{* 2 subgoals left *}
prensani@13020
   280
apply clarify
prensani@13020
   281
apply(conjI_tac)
prensani@13020
   282
apply(disjE_tac)
prensani@13020
   283
 apply (simp_all)
prensani@13020
   284
apply clarify
prensani@13020
   285
apply(erule less_SucE)
prensani@13020
   286
 apply force
prensani@13020
   287
apply (simp add:BtoW_def)
prensani@13022
   288
--{* 1 subgoal left *}
prensani@13020
   289
apply clarify
prensani@13020
   290
apply simp
prensani@13020
   291
apply(disjE_tac)
prensani@13020
   292
apply (simp_all)
prensani@13020
   293
apply(rule disjI1 , rule Graph1)
prensani@13020
   294
 apply simp_all
prensani@13020
   295
done
prensani@13020
   296
prensani@13020
   297
subsubsection {* Counting Black Nodes *}
prensani@13020
   298
prensani@13020
   299
constdefs
prensani@13020
   300
  Mul_CountInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
prensani@13020
   301
 "Mul_CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
prensani@13020
   302
prensani@13020
   303
  Mul_Count :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   304
  "Mul_Count n \<equiv> 
prensani@13020
   305
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   306
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   307
    \<and> length \<acute>Ma=length \<acute>M 
prensani@13020
   308
    \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) ) 
prensani@13020
   309
    \<and> \<acute>q<n+1 \<and> \<acute>bc={}}.
prensani@13020
   310
  \<acute>ind:=0;;
prensani@13020
   311
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   312
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   313
    \<and> length \<acute>Ma=length \<acute>M 
prensani@13020
   314
    \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) ) 
prensani@13020
   315
    \<and> \<acute>q<n+1 \<and> \<acute>bc={} \<and> \<acute>ind=0}.
prensani@13020
   316
  WHILE \<acute>ind<length \<acute>M 
prensani@13020
   317
     INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   318
          \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M  
prensani@13020
   319
          \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
prensani@13020
   320
          \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
wenzelm@32960
   321
          \<and> \<acute>q<n+1 \<and> \<acute>ind\<le>length \<acute>M}.
prensani@13020
   322
  DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   323
       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   324
       \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
prensani@13020
   325
       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
prensani@13020
   326
       \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M}. 
prensani@13020
   327
     IF \<acute>M!\<acute>ind=Black 
prensani@13020
   328
     THEN .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   329
            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M  
prensani@13020
   330
            \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
prensani@13020
   331
            \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
prensani@13020
   332
            \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}.
prensani@13020
   333
          \<acute>bc:=insert \<acute>ind \<acute>bc
prensani@13020
   334
     FI;;
prensani@13020
   335
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   336
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   337
    \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv (\<acute>ind+1) 
prensani@13020
   338
    \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
prensani@13020
   339
    \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M}.
prensani@13020
   340
  \<acute>ind:=\<acute>ind+1
prensani@13020
   341
  OD"
prensani@13020
   342
 
prensani@13020
   343
lemma Mul_Count: 
prensani@13020
   344
  "\<turnstile> Mul_Count n  
prensani@13020
   345
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   346
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   347
    \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   348
    \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
prensani@13020
   349
    \<and> \<acute>q<n+1}."
prensani@13020
   350
apply (unfold Mul_Count_def)
prensani@13020
   351
apply annhoare
prensani@13020
   352
apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
prensani@13020
   353
--{* 7 subgoals left *}
prensani@13020
   354
apply force
prensani@13020
   355
apply force
prensani@13020
   356
apply force
prensani@13020
   357
--{* 4 subgoals left *}
prensani@13020
   358
apply clarify
prensani@13020
   359
apply(conjI_tac)
prensani@13020
   360
apply(disjE_tac)
prensani@13020
   361
 apply simp_all
prensani@13020
   362
apply(simp add:Blacks_def)
prensani@13020
   363
apply clarify
prensani@13020
   364
apply(erule less_SucE)
prensani@13020
   365
 back
prensani@13020
   366
 apply force
prensani@13020
   367
apply force
prensani@13020
   368
--{* 3 subgoals left *}
prensani@13020
   369
apply clarify
prensani@13020
   370
apply(conjI_tac)
prensani@13020
   371
apply(disjE_tac)
prensani@13020
   372
 apply simp_all
prensani@13020
   373
apply clarify
prensani@13020
   374
apply(erule less_SucE)
prensani@13020
   375
 back
prensani@13020
   376
 apply force
prensani@13020
   377
apply simp
prensani@13020
   378
apply(rotate_tac -1)
prensani@13020
   379
apply (force simp add:Blacks_def)
prensani@13020
   380
--{* 2 subgoals left *}
prensani@13020
   381
apply force
prensani@13022
   382
--{* 1 subgoal left *}
prensani@13020
   383
apply clarify
wenzelm@26316
   384
apply(drule_tac x = "ind x" in le_imp_less_or_eq)
prensani@13020
   385
apply (simp_all add:Blacks_def)
prensani@13020
   386
done
prensani@13020
   387
prensani@13020
   388
subsubsection {* Appending garbage nodes to the free list *}
prensani@13020
   389
prensani@13020
   390
consts  Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
prensani@13020
   391
prensani@13020
   392
axioms
prensani@13020
   393
  Append_to_free0: "length (Append_to_free (i, e)) = length e"
prensani@13020
   394
  Append_to_free1: "Proper_Edges (m, e) 
prensani@13020
   395
                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
prensani@13020
   396
  Append_to_free2: "i \<notin> Reach e 
prensani@13020
   397
           \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
prensani@13020
   398
prensani@13020
   399
constdefs
prensani@13020
   400
  Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
prensani@13020
   401
  "Mul_AppendInv \<equiv> \<guillemotleft> \<lambda>ind. (\<forall>i. ind\<le>i \<longrightarrow> i<length \<acute>M \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black)\<guillemotright>"
prensani@13020
   402
prensani@13020
   403
  Mul_Append :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   404
  "Mul_Append n \<equiv> 
prensani@13020
   405
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
prensani@13020
   406
  \<acute>ind:=0;;
prensani@13020
   407
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}.
prensani@13020
   408
  WHILE \<acute>ind<length \<acute>M 
prensani@13020
   409
    INV .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}.
prensani@13020
   410
  DO .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}.
prensani@13020
   411
      IF \<acute>M!\<acute>ind=Black THEN 
prensani@13020
   412
     .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. 
prensani@13020
   413
      \<acute>M:=\<acute>M[\<acute>ind:=White] 
prensani@13020
   414
      ELSE 
prensani@13020
   415
     .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E}. 
prensani@13020
   416
      \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
prensani@13020
   417
      FI;;
prensani@13020
   418
  .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}. 
prensani@13020
   419
   \<acute>ind:=\<acute>ind+1
prensani@13020
   420
  OD"
prensani@13020
   421
prensani@13020
   422
lemma Mul_Append: 
prensani@13020
   423
  "\<turnstile> Mul_Append n  
prensani@13020
   424
     .{\<acute>Mul_Proper n}."
prensani@13020
   425
apply(unfold Mul_Append_def)
prensani@13020
   426
apply annhoare
prensani@13020
   427
apply(simp_all add: mul_collector_defs Mul_AppendInv_def 
prensani@13020
   428
      Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
   429
apply(force simp add:Blacks_def)
prensani@13020
   430
apply(force simp add:Blacks_def)
prensani@13020
   431
apply(force simp add:Blacks_def)
prensani@13020
   432
apply(force simp add:Graph_defs)
prensani@13020
   433
apply force
prensani@13020
   434
apply(force simp add:Append_to_free1 Append_to_free2)
prensani@13020
   435
apply force
prensani@13020
   436
apply force
prensani@13020
   437
done
prensani@13020
   438
prensani@13020
   439
subsubsection {* Collector *}
prensani@13020
   440
prensani@13020
   441
constdefs 
prensani@13020
   442
  Mul_Collector :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   443
  "Mul_Collector n \<equiv>
prensani@13020
   444
.{\<acute>Mul_Proper n}.  
prensani@13020
   445
WHILE True INV .{\<acute>Mul_Proper n}. 
prensani@13020
   446
DO  
prensani@13020
   447
Mul_Blacken_Roots n ;; 
prensani@13020
   448
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M}.  
prensani@13020
   449
 \<acute>obc:={};; 
prensani@13020
   450
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}.  
prensani@13020
   451
 \<acute>bc:=Roots;; 
prensani@13020
   452
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}. 
prensani@13020
   453
 \<acute>l:=0;; 
prensani@13020
   454
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>l=0}. 
prensani@13020
   455
 WHILE \<acute>l<n+1  
prensani@13020
   456
   INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and>  
prensani@13020
   457
         (\<acute>Safe \<or> (\<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M) \<and> \<acute>l<n+1)}. 
prensani@13020
   458
 DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   459
      \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M)}.
prensani@13020
   460
    \<acute>obc:=\<acute>bc;;
prensani@13020
   461
    Mul_Propagate_Black n;; 
prensani@13020
   462
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   463
      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   464
      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
prensani@13020
   465
      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))}. 
prensani@13020
   466
    \<acute>bc:={};;
prensani@13020
   467
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   468
      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   469
      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
prensani@13020
   470
      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) \<and> \<acute>bc={}}. 
prensani@13020
   471
       \<langle> \<acute>Ma:=\<acute>M,, \<acute>q:=\<acute>Queue \<rangle>;;
prensani@13020
   472
    Mul_Count n;; 
prensani@13020
   473
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   474
      \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   475
      \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   476
      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
prensani@13020
   477
      \<and> \<acute>q<n+1}. 
prensani@13020
   478
    IF \<acute>obc=\<acute>bc THEN
prensani@13020
   479
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   480
      \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   481
      \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   482
      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
prensani@13020
   483
      \<and> \<acute>q<n+1 \<and> \<acute>obc=\<acute>bc}.  
prensani@13020
   484
    \<acute>l:=\<acute>l+1  
prensani@13020
   485
    ELSE .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   486
          \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   487
          \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   488
          \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
prensani@13020
   489
          \<and> \<acute>q<n+1 \<and> \<acute>obc\<noteq>\<acute>bc}.  
prensani@13020
   490
        \<acute>l:=0 FI 
prensani@13020
   491
 OD;; 
prensani@13020
   492
 Mul_Append n  
prensani@13020
   493
OD"
prensani@13020
   494
prensani@13020
   495
lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def 
prensani@13020
   496
 Mul_Blacken_Roots_def Mul_Propagate_Black_def 
prensani@13020
   497
 Mul_Count_def Mul_Append_def
prensani@13020
   498
prensani@13020
   499
lemma Mul_Collector:
prensani@13020
   500
  "\<turnstile> Mul_Collector n 
prensani@13020
   501
  .{False}."
prensani@13020
   502
apply(unfold Mul_Collector_def)
prensani@13020
   503
apply annhoare
prensani@13020
   504
apply(simp_all only:pre.simps Mul_Blacken_Roots 
prensani@13020
   505
       Mul_Propagate_Black Mul_Count Mul_Append)
prensani@13020
   506
apply(simp_all add:mul_modules)
prensani@13020
   507
apply(simp_all add:mul_collector_defs Queue_def)
prensani@13020
   508
apply force
prensani@13020
   509
apply force
prensani@13020
   510
apply force
nipkow@15247
   511
apply (force simp add: less_Suc_eq_le)
prensani@13020
   512
apply force
prensani@13020
   513
apply (force dest:subset_antisym)
prensani@13020
   514
apply force
prensani@13020
   515
apply force
prensani@13020
   516
apply force
prensani@13020
   517
done
prensani@13020
   518
prensani@13020
   519
subsection {* Interference Freedom *}
prensani@13020
   520
prensani@13020
   521
lemma le_length_filter_update[rule_format]: 
prensani@13020
   522
 "\<forall>i. (\<not>P (list!i) \<or> P j) \<and> i<length list 
prensani@13020
   523
 \<longrightarrow> length(filter P list) \<le> length(filter P (list[i:=j]))"
prensani@13020
   524
apply(induct_tac "list")
prensani@13020
   525
 apply(simp)
prensani@13020
   526
apply(clarify)
prensani@13020
   527
apply(case_tac i)
prensani@13020
   528
 apply(simp)
prensani@13020
   529
apply(simp)
prensani@13020
   530
done
prensani@13020
   531
prensani@13020
   532
lemma less_length_filter_update [rule_format]: 
prensani@13020
   533
 "\<forall>i. P j \<and> \<not>(P (list!i)) \<and> i<length list 
prensani@13020
   534
 \<longrightarrow> length(filter P list) < length(filter P (list[i:=j]))"
prensani@13020
   535
apply(induct_tac "list")
prensani@13020
   536
 apply(simp)
prensani@13020
   537
apply(clarify)
prensani@13020
   538
apply(case_tac i)
prensani@13020
   539
 apply(simp)
prensani@13020
   540
apply(simp)
prensani@13020
   541
done
prensani@13020
   542
prensani@13020
   543
lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk> \<Longrightarrow>  
prensani@13020
   544
  interfree_aux (Some(Mul_Blacken_Roots n),{},Some(Mul_Redirect_Edge j n))"
prensani@13020
   545
apply (unfold mul_modules)
prensani@13020
   546
apply interfree_aux
prensani@13020
   547
apply safe
prensani@13020
   548
apply(simp_all add:Graph6 Graph9 Graph12 nth_list_update mul_mutator_defs mul_collector_defs)
prensani@13020
   549
done
prensani@13020
   550
prensani@13020
   551
lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow> 
prensani@13020
   552
  interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Blacken_Roots n))"
prensani@13020
   553
apply (unfold mul_modules)
prensani@13020
   554
apply interfree_aux
prensani@13020
   555
apply safe
prensani@13020
   556
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   557
done
prensani@13020
   558
prensani@13020
   559
lemma Mul_interfree_Blacken_Roots_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   560
  interfree_aux (Some(Mul_Blacken_Roots n),{},Some (Mul_Color_Target j n ))"
prensani@13020
   561
apply (unfold mul_modules)
prensani@13020
   562
apply interfree_aux
prensani@13020
   563
apply safe
prensani@13020
   564
apply(simp_all add:mul_mutator_defs mul_collector_defs nth_list_update Graph7 Graph8 Graph9 Graph12)
prensani@13020
   565
done
prensani@13020
   566
prensani@13020
   567
lemma Mul_interfree_Color_Target_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   568
  interfree_aux (Some(Mul_Color_Target j n ),{},Some (Mul_Blacken_Roots n ))"
prensani@13020
   569
apply (unfold mul_modules)
prensani@13020
   570
apply interfree_aux
prensani@13020
   571
apply safe
prensani@13020
   572
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   573
done
prensani@13020
   574
prensani@13020
   575
lemma Mul_interfree_Propagate_Black_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   576
  interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Redirect_Edge j n ))"
prensani@13020
   577
apply (unfold mul_modules)
prensani@13020
   578
apply interfree_aux
prensani@13020
   579
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_PBInv_def nth_list_update Graph6)
prensani@13020
   580
--{* 7 subgoals left *}
prensani@13020
   581
apply clarify
prensani@13020
   582
apply(disjE_tac)
prensani@13020
   583
  apply(simp_all add:Graph6)
prensani@13020
   584
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   585
apply(rule conjI)
prensani@13020
   586
 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   587
apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   588
--{* 6 subgoals left *}
prensani@13020
   589
apply clarify
prensani@13020
   590
apply(disjE_tac)
prensani@13020
   591
  apply(simp_all add:Graph6)
prensani@13020
   592
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   593
apply(rule conjI)
prensani@13020
   594
 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   595
apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   596
--{* 5 subgoals left *}
prensani@13020
   597
apply clarify
prensani@13020
   598
apply(disjE_tac)
prensani@13020
   599
  apply(simp_all add:Graph6)
prensani@13020
   600
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   601
apply(rule conjI)
prensani@13020
   602
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   603
apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   604
apply(erule conjE)
prensani@13020
   605
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   606
 apply(rule conjI)
prensani@13020
   607
  apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   608
   apply clarify
prensani@13020
   609
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   610
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   611
   apply (force simp add: nth_list_update)
prensani@13020
   612
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   613
 apply(rule impI,(rule disjI2)+, erule le_trans)
prensani@13020
   614
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   615
apply(rule conjI)
prensani@13020
   616
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   617
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   618
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   619
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   620
--{* 4 subgoals left *}
prensani@13020
   621
apply clarify
prensani@13020
   622
apply(disjE_tac)
prensani@13020
   623
  apply(simp_all add:Graph6)
prensani@13020
   624
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   625
apply(rule conjI)
prensani@13020
   626
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   627
apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   628
apply(erule conjE)
prensani@13020
   629
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   630
 apply(rule conjI)
prensani@13020
   631
  apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   632
   apply clarify
prensani@13020
   633
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   634
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   635
   apply (force simp add: nth_list_update)
prensani@13020
   636
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   637
 apply(rule impI,(rule disjI2)+, erule le_trans)
prensani@13020
   638
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   639
apply(rule conjI)
prensani@13020
   640
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   641
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   642
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   643
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   644
--{* 3 subgoals left *}
prensani@13020
   645
apply clarify
prensani@13020
   646
apply(disjE_tac)
prensani@13020
   647
  apply(simp_all add:Graph6)
prensani@13020
   648
  apply (rule impI)
prensani@13020
   649
   apply(rule conjI)
prensani@13020
   650
    apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   651
   apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   652
    apply(simp add:nth_list_update)
prensani@13020
   653
   apply(simp add:nth_list_update)
prensani@13020
   654
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   655
   apply(simp add:nth_list_update)
prensani@13020
   656
  apply(simp add:nth_list_update)
prensani@13020
   657
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   658
  apply(rule conjI)
prensani@13020
   659
   apply(rule impI)
prensani@13020
   660
   apply(rule conjI)
prensani@13020
   661
    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   662
    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   663
   apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   664
    apply(simp add:nth_list_update)
prensani@13020
   665
   apply(simp add:nth_list_update)
prensani@13020
   666
  apply(rule impI)
prensani@13020
   667
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   668
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   669
 apply(rule conjI)
prensani@13020
   670
  apply(rule impI)
prensani@13020
   671
   apply(rule conjI)
prensani@13020
   672
    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   673
    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   674
   apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   675
    apply(simp add:nth_list_update)
prensani@13020
   676
   apply(simp add:nth_list_update)
prensani@13020
   677
  apply(rule impI)
prensani@13020
   678
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   679
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   680
 apply(erule conjE)
prensani@13020
   681
 apply(rule conjI)
prensani@13020
   682
  apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   683
   apply(rule impI,rule conjI,(rule disjI2)+,rule conjI)
prensani@13020
   684
    apply clarify
prensani@13020
   685
    apply(case_tac "R (Muts x! j)=i")
prensani@13020
   686
     apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   687
    apply (force simp add: nth_list_update)
prensani@13020
   688
   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   689
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   690
   apply(simp add:nth_list_update)
prensani@13020
   691
  apply(simp add:nth_list_update)
prensani@13020
   692
 apply(rule impI,rule conjI)
prensani@13020
   693
  apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   694
  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   695
 apply(case_tac "R (Muts x! j)=ind x")
prensani@13020
   696
  apply (force simp add: nth_list_update)
prensani@13020
   697
 apply (force simp add: nth_list_update)
prensani@13020
   698
apply(rule impI, (rule disjI2)+, erule le_trans)
prensani@13020
   699
apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   700
--{* 2 subgoals left *}
prensani@13020
   701
apply clarify
prensani@13020
   702
apply(rule conjI)
prensani@13020
   703
 apply(disjE_tac)
prensani@13020
   704
  apply(simp_all add:Mul_Auxk_def Graph6)
prensani@13020
   705
  apply (rule impI)
prensani@13020
   706
   apply(rule conjI)
prensani@13020
   707
    apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   708
   apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   709
    apply(simp add:nth_list_update)
prensani@13020
   710
   apply(simp add:nth_list_update)
prensani@13020
   711
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   712
   apply(simp add:nth_list_update)
prensani@13020
   713
  apply(simp add:nth_list_update)
prensani@13020
   714
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   715
  apply(rule impI)
prensani@13020
   716
  apply(rule conjI)
prensani@13020
   717
   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   718
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   719
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   720
   apply(simp add:nth_list_update)
prensani@13020
   721
  apply(simp add:nth_list_update)
prensani@13020
   722
 apply(rule impI)
prensani@13020
   723
 apply(rule conjI)
prensani@13020
   724
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   725
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   726
 apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   727
  apply(simp add:nth_list_update)
prensani@13020
   728
 apply(simp add:nth_list_update)
prensani@13020
   729
apply(rule impI)
prensani@13020
   730
apply(rule conjI)
prensani@13020
   731
 apply(erule conjE)+
prensani@13020
   732
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   733
  apply((rule disjI2)+,rule conjI)
prensani@13020
   734
   apply clarify
prensani@13020
   735
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   736
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   737
   apply (force simp add: nth_list_update)
prensani@13020
   738
  apply(rule conjI)
prensani@13020
   739
   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   740
  apply(rule impI)
prensani@13020
   741
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   742
   apply(simp add:nth_list_update BtoW_def)
prensani@13020
   743
  apply (simp  add:nth_list_update)
prensani@13020
   744
  apply(rule impI)
prensani@13020
   745
  apply simp
prensani@13020
   746
  apply(disjE_tac)
prensani@13020
   747
   apply(rule disjI1, erule less_le_trans)
prensani@13020
   748
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   749
  apply force
prensani@13020
   750
 apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   751
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   752
 apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   753
  apply(simp add:nth_list_update)
prensani@13020
   754
 apply(simp add:nth_list_update)
prensani@13020
   755
apply(disjE_tac) 
prensani@13020
   756
apply simp_all
prensani@13020
   757
apply(conjI_tac)
prensani@13020
   758
 apply(rule impI)
prensani@13020
   759
 apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   760
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   761
apply(erule conjE)+
prensani@13020
   762
apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   763
 apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   764
apply(rule impI)+
prensani@13020
   765
apply simp
prensani@13020
   766
apply(disjE_tac)
prensani@13020
   767
 apply(rule disjI1, erule less_le_trans)
prensani@13020
   768
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   769
apply force
prensani@13022
   770
--{* 1 subgoal left *} 
prensani@13020
   771
apply clarify
prensani@13020
   772
apply(disjE_tac)
prensani@13020
   773
  apply(simp_all add:Graph6)
prensani@13020
   774
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   775
apply(rule conjI)
prensani@13020
   776
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   777
apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   778
apply(erule conjE)
prensani@13020
   779
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   780
 apply(rule conjI)
prensani@13020
   781
  apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   782
   apply clarify
prensani@13020
   783
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   784
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   785
   apply (force simp add: nth_list_update)
prensani@13020
   786
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   787
 apply(rule impI,(rule disjI2)+, erule le_trans)
prensani@13020
   788
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   789
apply(rule conjI)
prensani@13020
   790
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   791
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   792
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   793
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   794
done
prensani@13020
   795
prensani@13020
   796
lemma Mul_interfree_Redirect_Edge_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   797
  interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Propagate_Black n))"
prensani@13020
   798
apply (unfold mul_modules)
prensani@13020
   799
apply interfree_aux
prensani@13020
   800
apply safe
prensani@13020
   801
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   802
done
prensani@13020
   803
prensani@13020
   804
lemma Mul_interfree_Propagate_Black_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   805
  interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Color_Target j n ))"
prensani@13020
   806
apply (unfold mul_modules)
prensani@13020
   807
apply interfree_aux
prensani@13020
   808
apply(simp_all add: mul_collector_defs mul_mutator_defs)
prensani@13020
   809
--{* 7 subgoals left *}
prensani@13020
   810
apply clarify
prensani@13020
   811
apply (simp add:Graph7 Graph8 Graph12)
prensani@13020
   812
apply(disjE_tac)
prensani@13020
   813
  apply(simp add:Graph7 Graph8 Graph12)
prensani@13020
   814
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   815
  apply(rule disjI2,rule disjI1, erule le_trans)
prensani@13020
   816
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   817
 apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   818
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
   819
--{* 6 subgoals left *}
prensani@13020
   820
apply clarify
prensani@13020
   821
apply (simp add:Graph7 Graph8 Graph12)
prensani@13020
   822
apply(disjE_tac)
prensani@13020
   823
  apply(simp add:Graph7 Graph8 Graph12)
prensani@13020
   824
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   825
  apply(rule disjI2,rule disjI1, erule le_trans)
prensani@13020
   826
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   827
 apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   828
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
   829
--{* 5 subgoals left *}
prensani@13020
   830
apply clarify
prensani@13020
   831
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   832
apply(disjE_tac)
prensani@13020
   833
   apply(simp add:Graph7 Graph8 Graph12) 
prensani@13020
   834
  apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
prensani@13020
   835
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   836
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   837
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   838
 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
prensani@13020
   839
apply(erule conjE)
prensani@13020
   840
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   841
 apply((rule disjI2)+)
prensani@13020
   842
 apply (rule conjI)
prensani@13020
   843
  apply(simp add:Graph10)
prensani@13020
   844
 apply(erule le_trans)
prensani@13020
   845
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   846
apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   847
--{* 4 subgoals left *}
prensani@13020
   848
apply clarify
prensani@13020
   849
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   850
apply(disjE_tac)
prensani@13020
   851
   apply(simp add:Graph7 Graph8 Graph12)
prensani@13020
   852
  apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
prensani@13020
   853
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   854
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   855
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   856
 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
prensani@13020
   857
apply(erule conjE)
prensani@13020
   858
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   859
 apply((rule disjI2)+)
prensani@13020
   860
 apply (rule conjI)
prensani@13020
   861
  apply(simp add:Graph10)
prensani@13020
   862
 apply(erule le_trans)
prensani@13020
   863
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   864
apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   865
--{* 3 subgoals left *}
prensani@13020
   866
apply clarify
prensani@13020
   867
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   868
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   869
 apply(simp add:Graph10)
prensani@13020
   870
 apply(disjE_tac)
prensani@13020
   871
  apply simp_all
prensani@13020
   872
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
prensani@13020
   873
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   874
 apply(erule conjE)
prensani@13020
   875
 apply((rule disjI2)+,erule le_trans)
prensani@13020
   876
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   877
apply(rule conjI)
prensani@13020
   878
 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
prensani@13020
   879
apply (force simp add:nth_list_update)
prensani@13020
   880
--{* 2 subgoals left *}
prensani@13020
   881
apply clarify 
prensani@13020
   882
apply(simp add:Mul_Auxk_def Graph7 Graph8 Graph12)
prensani@13020
   883
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   884
 apply(simp add:Graph10)
prensani@13020
   885
 apply(disjE_tac)
prensani@13020
   886
  apply simp_all
prensani@13020
   887
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
prensani@13020
   888
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   889
 apply(erule conjE)+
prensani@13020
   890
 apply((rule disjI2)+,rule conjI, erule le_trans)
prensani@13020
   891
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   892
 apply((rule impI)+)
prensani@13020
   893
 apply simp
prensani@13020
   894
 apply(erule disjE)
prensani@13020
   895
  apply(rule disjI1, erule less_le_trans) 
prensani@13020
   896
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   897
 apply force
prensani@13020
   898
apply(rule conjI)
prensani@13020
   899
 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
prensani@13020
   900
apply (force simp add:nth_list_update)
prensani@13022
   901
--{* 1 subgoal left *}
prensani@13020
   902
apply clarify
prensani@13020
   903
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   904
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   905
 apply(simp add:Graph10)
prensani@13020
   906
 apply(disjE_tac)
prensani@13020
   907
  apply simp_all
prensani@13020
   908
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
prensani@13020
   909
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   910
 apply(erule conjE)
prensani@13020
   911
 apply((rule disjI2)+,erule le_trans)
prensani@13020
   912
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   913
apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
prensani@13020
   914
done
prensani@13020
   915
prensani@13020
   916
lemma Mul_interfree_Color_Target_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   917
  interfree_aux (Some(Mul_Color_Target j n),{},Some(Mul_Propagate_Black n ))"
prensani@13020
   918
apply (unfold mul_modules)
prensani@13020
   919
apply interfree_aux
prensani@13020
   920
apply safe
prensani@13020
   921
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   922
done
prensani@13020
   923
prensani@13020
   924
lemma Mul_interfree_Count_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   925
  interfree_aux (Some(Mul_Count n ),{},Some(Mul_Redirect_Edge j n))"
prensani@13020
   926
apply (unfold mul_modules)
prensani@13020
   927
apply interfree_aux
prensani@13020
   928
--{* 9 subgoals left *}
prensani@13020
   929
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def Graph6)
prensani@13020
   930
apply clarify
prensani@13020
   931
apply disjE_tac
prensani@13020
   932
   apply(simp add:Graph6)
prensani@13020
   933
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   934
 apply(simp add:Graph6)
prensani@13020
   935
apply clarify
prensani@13020
   936
apply disjE_tac
prensani@13020
   937
 apply(simp add:Graph6)
prensani@13020
   938
 apply(rule conjI)
prensani@13020
   939
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   940
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   941
apply(simp add:Graph6)
prensani@13020
   942
--{* 8 subgoals left *}
prensani@13020
   943
apply(simp add:mul_mutator_defs nth_list_update)
prensani@13020
   944
--{* 7 subgoals left *}
prensani@13020
   945
apply(simp add:mul_mutator_defs mul_collector_defs)
prensani@13020
   946
apply clarify
prensani@13020
   947
apply disjE_tac
prensani@13020
   948
   apply(simp add:Graph6)
prensani@13020
   949
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   950
 apply(simp add:Graph6)
prensani@13020
   951
apply clarify
prensani@13020
   952
apply disjE_tac
prensani@13020
   953
 apply(simp add:Graph6)
prensani@13020
   954
 apply(rule conjI)
prensani@13020
   955
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   956
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   957
apply(simp add:Graph6)
prensani@13020
   958
--{* 6 subgoals left *}
prensani@13020
   959
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
   960
apply clarify
prensani@13020
   961
apply disjE_tac
prensani@13020
   962
   apply(simp add:Graph6 Queue_def)
prensani@13020
   963
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   964
 apply(simp add:Graph6)
prensani@13020
   965
apply clarify
prensani@13020
   966
apply disjE_tac
prensani@13020
   967
 apply(simp add:Graph6)
prensani@13020
   968
 apply(rule conjI)
prensani@13020
   969
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   970
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   971
apply(simp add:Graph6)
prensani@13020
   972
--{* 5 subgoals left *}
prensani@13020
   973
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
   974
apply clarify
prensani@13020
   975
apply disjE_tac
prensani@13020
   976
   apply(simp add:Graph6)
prensani@13020
   977
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   978
 apply(simp add:Graph6)
prensani@13020
   979
apply clarify
prensani@13020
   980
apply disjE_tac
prensani@13020
   981
 apply(simp add:Graph6)
prensani@13020
   982
 apply(rule conjI)
prensani@13020
   983
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   984
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   985
apply(simp add:Graph6)
prensani@13020
   986
--{* 4 subgoals left *}
prensani@13020
   987
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
   988
apply clarify
prensani@13020
   989
apply disjE_tac
prensani@13020
   990
   apply(simp add:Graph6)
prensani@13020
   991
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   992
 apply(simp add:Graph6)
prensani@13020
   993
apply clarify
prensani@13020
   994
apply disjE_tac
prensani@13020
   995
 apply(simp add:Graph6)
prensani@13020
   996
 apply(rule conjI)
prensani@13020
   997
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   998
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   999
apply(simp add:Graph6)
prensani@13020
  1000
--{* 3 subgoals left *}
prensani@13020
  1001
apply(simp add:mul_mutator_defs nth_list_update)
prensani@13020
  1002
--{* 2 subgoals left *}
prensani@13020
  1003
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
  1004
apply clarify
prensani@13020
  1005
apply disjE_tac
prensani@13020
  1006
   apply(simp add:Graph6)
prensani@13020
  1007
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
  1008
 apply(simp add:Graph6)
prensani@13020
  1009
apply clarify
prensani@13020
  1010
apply disjE_tac
prensani@13020
  1011
 apply(simp add:Graph6)
prensani@13020
  1012
 apply(rule conjI)
prensani@13020
  1013
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
  1014
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
  1015
apply(simp add:Graph6)
prensani@13022
  1016
--{* 1 subgoal left *}
prensani@13020
  1017
apply(simp add:mul_mutator_defs nth_list_update)
prensani@13020
  1018
done
prensani@13020
  1019
prensani@13020
  1020
lemma Mul_interfree_Redirect_Edge_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1021
  interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Count n ))"
prensani@13020
  1022
apply (unfold mul_modules)
prensani@13020
  1023
apply interfree_aux
prensani@13020
  1024
apply safe
prensani@13020
  1025
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
  1026
done
prensani@13020
  1027
prensani@13020
  1028
lemma Mul_interfree_Count_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1029
  interfree_aux (Some(Mul_Count n ),{},Some(Mul_Color_Target j n))"
prensani@13020
  1030
apply (unfold mul_modules)
prensani@13020
  1031
apply interfree_aux
prensani@13020
  1032
apply(simp_all add:mul_collector_defs mul_mutator_defs Mul_CountInv_def)
prensani@13020
  1033
--{* 6 subgoals left *}
prensani@13020
  1034
apply clarify
prensani@13020
  1035
apply disjE_tac
prensani@13020
  1036
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1037
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1038
apply clarify
prensani@13020
  1039
apply disjE_tac
prensani@13020
  1040
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1041
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1042
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1043
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1044
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1045
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1046
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1047
--{* 5 subgoals left *}
prensani@13020
  1048
apply clarify
prensani@13020
  1049
apply disjE_tac
prensani@13020
  1050
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1051
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1052
apply clarify
prensani@13020
  1053
apply disjE_tac
prensani@13020
  1054
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1055
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1056
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1057
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1058
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1059
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1060
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1061
--{* 4 subgoals left *}
prensani@13020
  1062
apply clarify
prensani@13020
  1063
apply disjE_tac
prensani@13020
  1064
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1065
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1066
apply clarify
prensani@13020
  1067
apply disjE_tac
prensani@13020
  1068
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1069
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1070
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1071
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1072
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1073
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1074
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1075
--{* 3 subgoals left *}
prensani@13020
  1076
apply clarify
prensani@13020
  1077
apply disjE_tac
prensani@13020
  1078
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1079
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1080
apply clarify
prensani@13020
  1081
apply disjE_tac
prensani@13020
  1082
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1083
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1084
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1085
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1086
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1087
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1088
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1089
--{* 2 subgoals left *}
prensani@13020
  1090
apply clarify
prensani@13020
  1091
apply disjE_tac
prensani@13020
  1092
  apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
prensani@13020
  1093
 apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
prensani@13020
  1094
apply clarify
prensani@13020
  1095
apply disjE_tac
prensani@13020
  1096
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1097
 apply(rule conjI)
prensani@13020
  1098
  apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1099
   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1100
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1101
  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1102
 apply (simp add: nth_list_update)
prensani@13020
  1103
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1104
apply(rule conjI)
prensani@13020
  1105
 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1106
apply (simp add: nth_list_update)
prensani@13022
  1107
--{* 1 subgoal left *}
prensani@13020
  1108
apply clarify
prensani@13020
  1109
apply disjE_tac
prensani@13020
  1110
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1111
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1112
apply clarify
prensani@13020
  1113
apply disjE_tac
prensani@13020
  1114
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1115
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1116
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1117
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1118
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1119
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1120
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1121
done
prensani@13020
  1122
prensani@13020
  1123
lemma Mul_interfree_Color_Target_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1124
  interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Count n ))"
prensani@13020
  1125
apply (unfold mul_modules)
prensani@13020
  1126
apply interfree_aux
prensani@13020
  1127
apply safe
prensani@13020
  1128
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
  1129
done
prensani@13020
  1130
prensani@13020
  1131
lemma Mul_interfree_Append_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1132
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
prensani@13020
  1133
apply (unfold mul_modules)
prensani@13020
  1134
apply interfree_aux
wenzelm@23894
  1135
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
prensani@13020
  1136
apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
prensani@13020
  1137
apply(erule_tac x=j in allE, force dest:Graph3)+
prensani@13020
  1138
done
prensani@13020
  1139
prensani@13020
  1140
lemma Mul_interfree_Redirect_Edge_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1141
  interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
prensani@13020
  1142
apply (unfold mul_modules)
prensani@13020
  1143
apply interfree_aux
wenzelm@23894
  1144
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
prensani@13020
  1145
apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def  mul_mutator_defs nth_list_update)
prensani@13020
  1146
done
prensani@13020
  1147
prensani@13020
  1148
lemma Mul_interfree_Append_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1149
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
prensani@13020
  1150
apply (unfold mul_modules)
prensani@13020
  1151
apply interfree_aux
wenzelm@23894
  1152
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
prensani@13020
  1153
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1 
prensani@13020
  1154
              Graph12 nth_list_update)
prensani@13020
  1155
done
prensani@13020
  1156
prensani@13020
  1157
lemma Mul_interfree_Color_Target_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1158
  interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
prensani@13020
  1159
apply (unfold mul_modules)
prensani@13020
  1160
apply interfree_aux
wenzelm@23894
  1161
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
prensani@13020
  1162
apply(simp_all add: mul_mutator_defs nth_list_update)
prensani@13020
  1163
apply(simp add:Mul_AppendInv_def Append_to_free0)
prensani@13020
  1164
done
prensani@13020
  1165
prensani@13020
  1166
subsubsection {* Interference freedom Collector-Mutator *}
prensani@13020
  1167
prensani@13020
  1168
lemmas mul_collector_mutator_interfree =  
prensani@13020
  1169
 Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target 
prensani@13020
  1170
 Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target  
prensani@13020
  1171
 Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target 
prensani@13020
  1172
 Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target 
prensani@13020
  1173
 Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots 
prensani@13020
  1174
 Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black  
prensani@13020
  1175
 Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count 
prensani@13020
  1176
 Mul_interfree_Redirect_Edge_Append Mul_interfree_Color_Target_Append
prensani@13020
  1177
prensani@13020
  1178
lemma Mul_interfree_Collector_Mutator: "j<n  \<Longrightarrow> 
prensani@13020
  1179
  interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))"
prensani@13020
  1180
apply(unfold Mul_Collector_def Mul_Mutator_def)
prensani@13020
  1181
apply interfree_aux
prensani@13020
  1182
apply(simp_all add:mul_collector_mutator_interfree)
prensani@13020
  1183
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
prensani@13020
  1184
apply(tactic  {* TRYALL (interfree_aux_tac) *})
prensani@13020
  1185
--{* 42 subgoals left *}
prensani@13020
  1186
apply (clarify,simp add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)+
prensani@13020
  1187
--{* 24 subgoals left *}
prensani@13020
  1188
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
  1189
--{* 14 subgoals left *}
wenzelm@23894
  1190
apply(tactic {* TRYALL (clarify_tac @{claset}) *})
prensani@13020
  1191
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
  1192
apply(tactic {* TRYALL (rtac conjI) *})
prensani@13020
  1193
apply(tactic {* TRYALL (rtac impI) *})
prensani@13020
  1194
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1195
apply(tactic {* TRYALL (etac conjE) *})
prensani@13020
  1196
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1197
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1198
--{* 72 subgoals left *}
prensani@13020
  1199
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
  1200
--{* 35 subgoals left *}
wenzelm@26342
  1201
apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
prensani@13020
  1202
--{* 28 subgoals left *}
prensani@13020
  1203
apply(tactic {* TRYALL (etac conjE) *})
prensani@13020
  1204
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1205
--{* 34 subgoals left *}
prensani@13020
  1206
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
  1207
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
wenzelm@27095
  1208
apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
prensani@13020
  1209
apply(simp_all add:Graph10)
prensani@13020
  1210
--{* 47 subgoals left *}
wenzelm@26342
  1211
apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
prensani@13020
  1212
--{* 41 subgoals left *}
wenzelm@26342
  1213
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
prensani@13020
  1214
--{* 35 subgoals left *}
wenzelm@26342
  1215
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
prensani@13020
  1216
--{* 31 subgoals left *}
wenzelm@26342
  1217
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
prensani@13020
  1218
--{* 29 subgoals left *}
wenzelm@26342
  1219
apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
prensani@13020
  1220
--{* 25 subgoals left *}
wenzelm@26342
  1221
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
prensani@13020
  1222
--{* 10 subgoals left *}
prensani@13020
  1223
apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
prensani@13020
  1224
done
prensani@13020
  1225
prensani@13020
  1226
subsubsection {* Interference freedom Mutator-Collector *}
prensani@13020
  1227
prensani@13020
  1228
lemma Mul_interfree_Mutator_Collector: " j < n \<Longrightarrow> 
prensani@13020
  1229
  interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))"
prensani@13020
  1230
apply(unfold Mul_Collector_def Mul_Mutator_def)
prensani@13020
  1231
apply interfree_aux
prensani@13020
  1232
apply(simp_all add:mul_collector_mutator_interfree)
prensani@13020
  1233
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
prensani@13020
  1234
apply(tactic  {* TRYALL (interfree_aux_tac) *})
prensani@13020
  1235
--{* 76 subgoals left *}
haftmann@32687
  1236
apply (clarsimp simp add: nth_list_update)+
prensani@13020
  1237
--{* 56 subgoals left *}
haftmann@32687
  1238
apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
prensani@13020
  1239
done
prensani@13020
  1240
prensani@13020
  1241
subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
prensani@13020
  1242
prensani@13020
  1243
text {* The total number of verification conditions is 328 *}
prensani@13020
  1244
prensani@13020
  1245
lemma Mul_Gar_Coll: 
prensani@13020
  1246
 "\<parallel>- .{\<acute>Mul_Proper n \<and> \<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))}.  
prensani@13020
  1247
 COBEGIN  
prensani@13020
  1248
  Mul_Collector n
prensani@13020
  1249
 .{False}.
prensani@13020
  1250
 \<parallel>  
prensani@13020
  1251
 SCHEME  [0\<le> j< n]
prensani@13020
  1252
  Mul_Mutator j n
prensani@13020
  1253
 .{False}.  
prensani@13020
  1254
 COEND  
prensani@13020
  1255
 .{False}."
prensani@13020
  1256
apply oghoare
prensani@13020
  1257
--{* Strengthening the precondition *}
prensani@13020
  1258
apply(rule Int_greatest)
prensani@13020
  1259
 apply (case_tac n)
prensani@13020
  1260
  apply(force simp add: Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1261
 apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
prensani@13020
  1262
 apply force
prensani@13020
  1263
apply clarify
haftmann@32133
  1264
apply(case_tac i)
prensani@13020
  1265
 apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1266
apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
prensani@13020
  1267
--{* Collector *}
prensani@13020
  1268
apply(rule Mul_Collector)
prensani@13020
  1269
--{* Mutator *}
prensani@13020
  1270
apply(erule Mul_Mutator)
prensani@13020
  1271
--{* Interference freedom *}
prensani@13020
  1272
apply(simp add:Mul_interfree_Collector_Mutator)
prensani@13020
  1273
apply(simp add:Mul_interfree_Mutator_Collector)
prensani@13020
  1274
apply(simp add:Mul_interfree_Mutator_Mutator)
prensani@13020
  1275
--{* Weakening of the postcondition *}
prensani@13020
  1276
apply(case_tac n)
prensani@13020
  1277
 apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1278
apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1279
done
prensani@13020
  1280
nipkow@13187
  1281
end