src/HOL/HoareParallel/Mul_Gar_Coll.thy
author wenzelm
Wed Dec 06 01:12:36 2006 +0100 (2006-12-06)
changeset 21669 c68717c16013
parent 20050 a2fb9d553aad
child 23880 64b9806e160b
permissions -rw-r--r--
removed legacy ML bindings;
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) *})
prensani@13020
   136
apply(tactic {* ALLGOALS Clarify_tac *})
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}.
prensani@13020
   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
--{* 3 subgoals left *}
prensani@13020
   280
apply force
prensani@13020
   281
--{* 2 subgoals left *}
prensani@13020
   282
apply clarify
prensani@13020
   283
apply(conjI_tac)
prensani@13020
   284
apply(disjE_tac)
prensani@13020
   285
 apply (simp_all)
prensani@13020
   286
apply clarify
prensani@13020
   287
apply(erule less_SucE)
prensani@13020
   288
 apply force
prensani@13020
   289
apply (simp add:BtoW_def)
prensani@13022
   290
--{* 1 subgoal left *}
prensani@13020
   291
apply clarify
prensani@13020
   292
apply simp
prensani@13020
   293
apply(disjE_tac)
prensani@13020
   294
apply (simp_all)
prensani@13020
   295
apply(rule disjI1 , rule Graph1)
prensani@13020
   296
 apply simp_all
prensani@13020
   297
done
prensani@13020
   298
prensani@13020
   299
subsubsection {* Counting Black Nodes *}
prensani@13020
   300
prensani@13020
   301
constdefs
prensani@13020
   302
  Mul_CountInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
prensani@13020
   303
 "Mul_CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
prensani@13020
   304
prensani@13020
   305
  Mul_Count :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   306
  "Mul_Count n \<equiv> 
prensani@13020
   307
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   308
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   309
    \<and> length \<acute>Ma=length \<acute>M 
prensani@13020
   310
    \<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
   311
    \<and> \<acute>q<n+1 \<and> \<acute>bc={}}.
prensani@13020
   312
  \<acute>ind:=0;;
prensani@13020
   313
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   314
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   315
    \<and> length \<acute>Ma=length \<acute>M 
prensani@13020
   316
    \<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
   317
    \<and> \<acute>q<n+1 \<and> \<acute>bc={} \<and> \<acute>ind=0}.
prensani@13020
   318
  WHILE \<acute>ind<length \<acute>M 
prensani@13020
   319
     INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   320
          \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M  
prensani@13020
   321
          \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
prensani@13020
   322
          \<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
   323
	  \<and> \<acute>q<n+1 \<and> \<acute>ind\<le>length \<acute>M}.
prensani@13020
   324
  DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   325
       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   326
       \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
prensani@13020
   327
       \<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
   328
       \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M}. 
prensani@13020
   329
     IF \<acute>M!\<acute>ind=Black 
prensani@13020
   330
     THEN .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   331
            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M  
prensani@13020
   332
            \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
prensani@13020
   333
            \<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
   334
            \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}.
prensani@13020
   335
          \<acute>bc:=insert \<acute>ind \<acute>bc
prensani@13020
   336
     FI;;
prensani@13020
   337
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   338
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   339
    \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv (\<acute>ind+1) 
prensani@13020
   340
    \<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
   341
    \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M}.
prensani@13020
   342
  \<acute>ind:=\<acute>ind+1
prensani@13020
   343
  OD"
prensani@13020
   344
 
prensani@13020
   345
lemma Mul_Count: 
prensani@13020
   346
  "\<turnstile> Mul_Count n  
prensani@13020
   347
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   348
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   349
    \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   350
    \<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
   351
    \<and> \<acute>q<n+1}."
prensani@13020
   352
apply (unfold Mul_Count_def)
prensani@13020
   353
apply annhoare
prensani@13020
   354
apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
prensani@13020
   355
--{* 7 subgoals left *}
prensani@13020
   356
apply force
prensani@13020
   357
apply force
prensani@13020
   358
apply force
prensani@13020
   359
--{* 4 subgoals left *}
prensani@13020
   360
apply clarify
prensani@13020
   361
apply(conjI_tac)
prensani@13020
   362
apply(disjE_tac)
prensani@13020
   363
 apply simp_all
prensani@13020
   364
apply(simp add:Blacks_def)
prensani@13020
   365
apply clarify
prensani@13020
   366
apply(erule less_SucE)
prensani@13020
   367
 back
prensani@13020
   368
 apply force
prensani@13020
   369
apply force
prensani@13020
   370
--{* 3 subgoals left *}
prensani@13020
   371
apply clarify
prensani@13020
   372
apply(conjI_tac)
prensani@13020
   373
apply(disjE_tac)
prensani@13020
   374
 apply simp_all
prensani@13020
   375
apply clarify
prensani@13020
   376
apply(erule less_SucE)
prensani@13020
   377
 back
prensani@13020
   378
 apply force
prensani@13020
   379
apply simp
prensani@13020
   380
apply(rotate_tac -1)
prensani@13020
   381
apply (force simp add:Blacks_def)
prensani@13020
   382
--{* 2 subgoals left *}
prensani@13020
   383
apply force
prensani@13022
   384
--{* 1 subgoal left *}
prensani@13020
   385
apply clarify
prensani@13020
   386
apply(drule le_imp_less_or_eq)
prensani@13020
   387
apply(disjE_tac)
prensani@13020
   388
apply (simp_all add:Blacks_def)
prensani@13020
   389
done
prensani@13020
   390
prensani@13020
   391
subsubsection {* Appending garbage nodes to the free list *}
prensani@13020
   392
prensani@13020
   393
consts  Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
prensani@13020
   394
prensani@13020
   395
axioms
prensani@13020
   396
  Append_to_free0: "length (Append_to_free (i, e)) = length e"
prensani@13020
   397
  Append_to_free1: "Proper_Edges (m, e) 
prensani@13020
   398
                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
prensani@13020
   399
  Append_to_free2: "i \<notin> Reach e 
prensani@13020
   400
           \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
prensani@13020
   401
prensani@13020
   402
constdefs
prensani@13020
   403
  Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
prensani@13020
   404
  "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
   405
prensani@13020
   406
  Mul_Append :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   407
  "Mul_Append n \<equiv> 
prensani@13020
   408
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
prensani@13020
   409
  \<acute>ind:=0;;
prensani@13020
   410
  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}.
prensani@13020
   411
  WHILE \<acute>ind<length \<acute>M 
prensani@13020
   412
    INV .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}.
prensani@13020
   413
  DO .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}.
prensani@13020
   414
      IF \<acute>M!\<acute>ind=Black THEN 
prensani@13020
   415
     .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. 
prensani@13020
   416
      \<acute>M:=\<acute>M[\<acute>ind:=White] 
prensani@13020
   417
      ELSE 
prensani@13020
   418
     .{\<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
   419
      \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
prensani@13020
   420
      FI;;
prensani@13020
   421
  .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}. 
prensani@13020
   422
   \<acute>ind:=\<acute>ind+1
prensani@13020
   423
  OD"
prensani@13020
   424
prensani@13020
   425
lemma Mul_Append: 
prensani@13020
   426
  "\<turnstile> Mul_Append n  
prensani@13020
   427
     .{\<acute>Mul_Proper n}."
prensani@13020
   428
apply(unfold Mul_Append_def)
prensani@13020
   429
apply annhoare
prensani@13020
   430
apply(simp_all add: mul_collector_defs Mul_AppendInv_def 
prensani@13020
   431
      Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
   432
apply(force simp add:Blacks_def)
prensani@13020
   433
apply(force simp add:Blacks_def)
prensani@13020
   434
apply(force simp add:Blacks_def)
prensani@13020
   435
apply(force simp add:Graph_defs)
prensani@13020
   436
apply force
prensani@13020
   437
apply(force simp add:Append_to_free1 Append_to_free2)
prensani@13020
   438
apply force
prensani@13020
   439
apply force
prensani@13020
   440
done
prensani@13020
   441
prensani@13020
   442
subsubsection {* Collector *}
prensani@13020
   443
prensani@13020
   444
constdefs 
prensani@13020
   445
  Mul_Collector :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
prensani@13020
   446
  "Mul_Collector n \<equiv>
prensani@13020
   447
.{\<acute>Mul_Proper n}.  
prensani@13020
   448
WHILE True INV .{\<acute>Mul_Proper n}. 
prensani@13020
   449
DO  
prensani@13020
   450
Mul_Blacken_Roots n ;; 
prensani@13020
   451
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M}.  
prensani@13020
   452
 \<acute>obc:={};; 
prensani@13020
   453
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}.  
prensani@13020
   454
 \<acute>bc:=Roots;; 
prensani@13020
   455
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}. 
prensani@13020
   456
 \<acute>l:=0;; 
prensani@13020
   457
.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>l=0}. 
prensani@13020
   458
 WHILE \<acute>l<n+1  
prensani@13020
   459
   INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and>  
prensani@13020
   460
         (\<acute>Safe \<or> (\<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M) \<and> \<acute>l<n+1)}. 
prensani@13020
   461
 DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   462
      \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M)}.
prensani@13020
   463
    \<acute>obc:=\<acute>bc;;
prensani@13020
   464
    Mul_Propagate_Black n;; 
prensani@13020
   465
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   466
      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   467
      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
prensani@13020
   468
      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))}. 
prensani@13020
   469
    \<acute>bc:={};;
prensani@13020
   470
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   471
      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   472
      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
prensani@13020
   473
      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) \<and> \<acute>bc={}}. 
prensani@13020
   474
       \<langle> \<acute>Ma:=\<acute>M,, \<acute>q:=\<acute>Queue \<rangle>;;
prensani@13020
   475
    Mul_Count n;; 
prensani@13020
   476
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   477
      \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   478
      \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   479
      \<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
   480
      \<and> \<acute>q<n+1}. 
prensani@13020
   481
    IF \<acute>obc=\<acute>bc THEN
prensani@13020
   482
    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   483
      \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   484
      \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   485
      \<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
   486
      \<and> \<acute>q<n+1 \<and> \<acute>obc=\<acute>bc}.  
prensani@13020
   487
    \<acute>l:=\<acute>l+1  
prensani@13020
   488
    ELSE .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
prensani@13020
   489
          \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
prensani@13020
   490
          \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
prensani@13020
   491
          \<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
   492
          \<and> \<acute>q<n+1 \<and> \<acute>obc\<noteq>\<acute>bc}.  
prensani@13020
   493
        \<acute>l:=0 FI 
prensani@13020
   494
 OD;; 
prensani@13020
   495
 Mul_Append n  
prensani@13020
   496
OD"
prensani@13020
   497
prensani@13020
   498
lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def 
prensani@13020
   499
 Mul_Blacken_Roots_def Mul_Propagate_Black_def 
prensani@13020
   500
 Mul_Count_def Mul_Append_def
prensani@13020
   501
prensani@13020
   502
lemma Mul_Collector:
prensani@13020
   503
  "\<turnstile> Mul_Collector n 
prensani@13020
   504
  .{False}."
prensani@13020
   505
apply(unfold Mul_Collector_def)
prensani@13020
   506
apply annhoare
prensani@13020
   507
apply(simp_all only:pre.simps Mul_Blacken_Roots 
prensani@13020
   508
       Mul_Propagate_Black Mul_Count Mul_Append)
prensani@13020
   509
apply(simp_all add:mul_modules)
prensani@13020
   510
apply(simp_all add:mul_collector_defs Queue_def)
prensani@13020
   511
apply force
prensani@13020
   512
apply force
prensani@13020
   513
apply force
nipkow@15247
   514
apply (force simp add: less_Suc_eq_le)
prensani@13020
   515
apply force
prensani@13020
   516
apply (force dest:subset_antisym)
prensani@13020
   517
apply force
prensani@13020
   518
apply force
prensani@13020
   519
apply force
prensani@13020
   520
done
prensani@13020
   521
prensani@13020
   522
subsection {* Interference Freedom *}
prensani@13020
   523
prensani@13020
   524
lemma le_length_filter_update[rule_format]: 
prensani@13020
   525
 "\<forall>i. (\<not>P (list!i) \<or> P j) \<and> i<length list 
prensani@13020
   526
 \<longrightarrow> length(filter P list) \<le> length(filter P (list[i:=j]))"
prensani@13020
   527
apply(induct_tac "list")
prensani@13020
   528
 apply(simp)
prensani@13020
   529
apply(clarify)
prensani@13020
   530
apply(case_tac i)
prensani@13020
   531
 apply(simp)
prensani@13020
   532
apply(simp)
prensani@13020
   533
done
prensani@13020
   534
prensani@13020
   535
lemma less_length_filter_update [rule_format]: 
prensani@13020
   536
 "\<forall>i. P j \<and> \<not>(P (list!i)) \<and> i<length list 
prensani@13020
   537
 \<longrightarrow> length(filter P list) < length(filter P (list[i:=j]))"
prensani@13020
   538
apply(induct_tac "list")
prensani@13020
   539
 apply(simp)
prensani@13020
   540
apply(clarify)
prensani@13020
   541
apply(case_tac i)
prensani@13020
   542
 apply(simp)
prensani@13020
   543
apply(simp)
prensani@13020
   544
done
prensani@13020
   545
prensani@13020
   546
lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk> \<Longrightarrow>  
prensani@13020
   547
  interfree_aux (Some(Mul_Blacken_Roots n),{},Some(Mul_Redirect_Edge j n))"
prensani@13020
   548
apply (unfold mul_modules)
prensani@13020
   549
apply interfree_aux
prensani@13020
   550
apply safe
prensani@13020
   551
apply(simp_all add:Graph6 Graph9 Graph12 nth_list_update mul_mutator_defs mul_collector_defs)
prensani@13020
   552
done
prensani@13020
   553
prensani@13020
   554
lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow> 
prensani@13020
   555
  interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Blacken_Roots n))"
prensani@13020
   556
apply (unfold mul_modules)
prensani@13020
   557
apply interfree_aux
prensani@13020
   558
apply safe
prensani@13020
   559
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   560
done
prensani@13020
   561
prensani@13020
   562
lemma Mul_interfree_Blacken_Roots_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   563
  interfree_aux (Some(Mul_Blacken_Roots n),{},Some (Mul_Color_Target j n ))"
prensani@13020
   564
apply (unfold mul_modules)
prensani@13020
   565
apply interfree_aux
prensani@13020
   566
apply safe
prensani@13020
   567
apply(simp_all add:mul_mutator_defs mul_collector_defs nth_list_update Graph7 Graph8 Graph9 Graph12)
prensani@13020
   568
done
prensani@13020
   569
prensani@13020
   570
lemma Mul_interfree_Color_Target_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   571
  interfree_aux (Some(Mul_Color_Target j n ),{},Some (Mul_Blacken_Roots n ))"
prensani@13020
   572
apply (unfold mul_modules)
prensani@13020
   573
apply interfree_aux
prensani@13020
   574
apply safe
prensani@13020
   575
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   576
done
prensani@13020
   577
prensani@13020
   578
lemma Mul_interfree_Propagate_Black_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   579
  interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Redirect_Edge j n ))"
prensani@13020
   580
apply (unfold mul_modules)
prensani@13020
   581
apply interfree_aux
prensani@13020
   582
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_PBInv_def nth_list_update Graph6)
prensani@13020
   583
--{* 7 subgoals left *}
prensani@13020
   584
apply clarify
prensani@13020
   585
apply(disjE_tac)
prensani@13020
   586
  apply(simp_all add:Graph6)
prensani@13020
   587
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   588
apply(rule conjI)
prensani@13020
   589
 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
   590
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
   591
--{* 6 subgoals left *}
prensani@13020
   592
apply clarify
prensani@13020
   593
apply(disjE_tac)
prensani@13020
   594
  apply(simp_all add:Graph6)
prensani@13020
   595
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   596
apply(rule conjI)
prensani@13020
   597
 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
   598
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
   599
--{* 5 subgoals left *}
prensani@13020
   600
apply clarify
prensani@13020
   601
apply(disjE_tac)
prensani@13020
   602
  apply(simp_all add:Graph6)
prensani@13020
   603
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   604
apply(rule conjI)
prensani@13020
   605
 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
   606
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
   607
apply(erule conjE)
prensani@13020
   608
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   609
 apply(rule conjI)
prensani@13020
   610
  apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   611
   apply clarify
prensani@13020
   612
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   613
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   614
   apply (force simp add: nth_list_update)
prensani@13020
   615
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   616
 apply(rule impI,(rule disjI2)+, erule le_trans)
prensani@13020
   617
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   618
apply(rule conjI)
prensani@13020
   619
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   620
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   621
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   622
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   623
--{* 4 subgoals left *}
prensani@13020
   624
apply clarify
prensani@13020
   625
apply(disjE_tac)
prensani@13020
   626
  apply(simp_all add:Graph6)
prensani@13020
   627
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   628
apply(rule conjI)
prensani@13020
   629
 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
   630
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
   631
apply(erule conjE)
prensani@13020
   632
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   633
 apply(rule conjI)
prensani@13020
   634
  apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   635
   apply clarify
prensani@13020
   636
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   637
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   638
   apply (force simp add: nth_list_update)
prensani@13020
   639
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   640
 apply(rule impI,(rule disjI2)+, erule le_trans)
prensani@13020
   641
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   642
apply(rule conjI)
prensani@13020
   643
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   644
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   645
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   646
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   647
--{* 3 subgoals left *}
prensani@13020
   648
apply clarify
prensani@13020
   649
apply(disjE_tac)
prensani@13020
   650
  apply(simp_all add:Graph6)
prensani@13020
   651
  apply (rule impI)
prensani@13020
   652
   apply(rule conjI)
prensani@13020
   653
    apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
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 "R (Muts x ! j)= ind x")
prensani@13020
   658
   apply(simp add:nth_list_update)
prensani@13020
   659
  apply(simp add:nth_list_update)
prensani@13020
   660
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   661
  apply(rule conjI)
prensani@13020
   662
   apply(rule impI)
prensani@13020
   663
   apply(rule conjI)
prensani@13020
   664
    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   665
    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   666
   apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   667
    apply(simp add:nth_list_update)
prensani@13020
   668
   apply(simp add:nth_list_update)
prensani@13020
   669
  apply(rule impI)
prensani@13020
   670
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   671
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   672
 apply(rule conjI)
prensani@13020
   673
  apply(rule impI)
prensani@13020
   674
   apply(rule conjI)
prensani@13020
   675
    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   676
    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   677
   apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   678
    apply(simp add:nth_list_update)
prensani@13020
   679
   apply(simp add:nth_list_update)
prensani@13020
   680
  apply(rule impI)
prensani@13020
   681
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   682
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   683
 apply(erule conjE)
prensani@13020
   684
 apply(rule conjI)
prensani@13020
   685
  apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   686
   apply(rule impI,rule conjI,(rule disjI2)+,rule conjI)
prensani@13020
   687
    apply clarify
prensani@13020
   688
    apply(case_tac "R (Muts x! j)=i")
prensani@13020
   689
     apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   690
    apply (force simp add: nth_list_update)
prensani@13020
   691
   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   692
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   693
   apply(simp add:nth_list_update)
prensani@13020
   694
  apply(simp add:nth_list_update)
prensani@13020
   695
 apply(rule impI,rule conjI)
prensani@13020
   696
  apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   697
  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   698
 apply(case_tac "R (Muts x! j)=ind x")
prensani@13020
   699
  apply (force simp add: nth_list_update)
prensani@13020
   700
 apply (force simp add: nth_list_update)
prensani@13020
   701
apply(rule impI, (rule disjI2)+, erule le_trans)
prensani@13020
   702
apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   703
--{* 2 subgoals left *}
prensani@13020
   704
apply clarify
prensani@13020
   705
apply(rule conjI)
prensani@13020
   706
 apply(disjE_tac)
prensani@13020
   707
  apply(simp_all add:Mul_Auxk_def Graph6)
prensani@13020
   708
  apply (rule impI)
prensani@13020
   709
   apply(rule conjI)
prensani@13020
   710
    apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
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 "R (Muts x ! j)= ind x")
prensani@13020
   715
   apply(simp add:nth_list_update)
prensani@13020
   716
  apply(simp add:nth_list_update)
prensani@13020
   717
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   718
  apply(rule impI)
prensani@13020
   719
  apply(rule conjI)
prensani@13020
   720
   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   721
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   722
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   723
   apply(simp add:nth_list_update)
prensani@13020
   724
  apply(simp add:nth_list_update)
prensani@13020
   725
 apply(rule impI)
prensani@13020
   726
 apply(rule conjI)
prensani@13020
   727
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   728
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   729
 apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   730
  apply(simp add:nth_list_update)
prensani@13020
   731
 apply(simp add:nth_list_update)
prensani@13020
   732
apply(rule impI)
prensani@13020
   733
apply(rule conjI)
prensani@13020
   734
 apply(erule conjE)+
prensani@13020
   735
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   736
  apply((rule disjI2)+,rule conjI)
prensani@13020
   737
   apply clarify
prensani@13020
   738
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   739
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   740
   apply (force simp add: nth_list_update)
prensani@13020
   741
  apply(rule conjI)
prensani@13020
   742
   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   743
  apply(rule impI)
prensani@13020
   744
  apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   745
   apply(simp add:nth_list_update BtoW_def)
prensani@13020
   746
  apply (simp  add:nth_list_update)
prensani@13020
   747
  apply(rule impI)
prensani@13020
   748
  apply simp
prensani@13020
   749
  apply(disjE_tac)
prensani@13020
   750
   apply(rule disjI1, erule less_le_trans)
prensani@13020
   751
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   752
  apply force
prensani@13020
   753
 apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   754
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   755
 apply(case_tac "R (Muts x ! j)= ind x")
prensani@13020
   756
  apply(simp add:nth_list_update)
prensani@13020
   757
 apply(simp add:nth_list_update)
prensani@13020
   758
apply(disjE_tac) 
prensani@13020
   759
apply simp_all
prensani@13020
   760
apply(conjI_tac)
prensani@13020
   761
 apply(rule impI)
prensani@13020
   762
 apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   763
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   764
apply(erule conjE)+
prensani@13020
   765
apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   766
 apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   767
apply(rule impI)+
prensani@13020
   768
apply simp
prensani@13020
   769
apply(disjE_tac)
prensani@13020
   770
 apply(rule disjI1, erule less_le_trans)
prensani@13020
   771
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   772
apply force
prensani@13022
   773
--{* 1 subgoal left *} 
prensani@13020
   774
apply clarify
prensani@13020
   775
apply(disjE_tac)
prensani@13020
   776
  apply(simp_all add:Graph6)
prensani@13020
   777
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   778
apply(rule conjI)
prensani@13020
   779
 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
   780
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
   781
apply(erule conjE)
prensani@13020
   782
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   783
 apply(rule conjI)
prensani@13020
   784
  apply(rule impI,(rule disjI2)+,rule conjI)
prensani@13020
   785
   apply clarify
prensani@13020
   786
   apply(case_tac "R (Muts x! j)=i")
prensani@13020
   787
    apply (force simp add: nth_list_update BtoW_def)
prensani@13020
   788
   apply (force simp add: nth_list_update)
prensani@13020
   789
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   790
 apply(rule impI,(rule disjI2)+, erule le_trans)
prensani@13020
   791
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
   792
apply(rule conjI)
prensani@13020
   793
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   794
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   795
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
prensani@13020
   796
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
prensani@13020
   797
done
prensani@13020
   798
prensani@13020
   799
lemma Mul_interfree_Redirect_Edge_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   800
  interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Propagate_Black n))"
prensani@13020
   801
apply (unfold mul_modules)
prensani@13020
   802
apply interfree_aux
prensani@13020
   803
apply safe
prensani@13020
   804
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   805
done
prensani@13020
   806
prensani@13020
   807
lemma Mul_interfree_Propagate_Black_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   808
  interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Color_Target j n ))"
prensani@13020
   809
apply (unfold mul_modules)
prensani@13020
   810
apply interfree_aux
prensani@13020
   811
apply(simp_all add: mul_collector_defs mul_mutator_defs)
prensani@13020
   812
--{* 7 subgoals left *}
prensani@13020
   813
apply clarify
prensani@13020
   814
apply (simp add:Graph7 Graph8 Graph12)
prensani@13020
   815
apply(disjE_tac)
prensani@13020
   816
  apply(simp add:Graph7 Graph8 Graph12)
prensani@13020
   817
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   818
  apply(rule disjI2,rule disjI1, erule le_trans)
prensani@13020
   819
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   820
 apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   821
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
   822
--{* 6 subgoals left *}
prensani@13020
   823
apply clarify
prensani@13020
   824
apply (simp add:Graph7 Graph8 Graph12)
prensani@13020
   825
apply(disjE_tac)
prensani@13020
   826
  apply(simp add:Graph7 Graph8 Graph12)
prensani@13020
   827
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   828
  apply(rule disjI2,rule disjI1, erule le_trans)
prensani@13020
   829
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   830
 apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   831
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
   832
--{* 5 subgoals left *}
prensani@13020
   833
apply clarify
prensani@13020
   834
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   835
apply(disjE_tac)
prensani@13020
   836
   apply(simp add:Graph7 Graph8 Graph12) 
prensani@13020
   837
  apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
prensani@13020
   838
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   839
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   840
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   841
 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
prensani@13020
   842
apply(erule conjE)
prensani@13020
   843
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   844
 apply((rule disjI2)+)
prensani@13020
   845
 apply (rule conjI)
prensani@13020
   846
  apply(simp add:Graph10)
prensani@13020
   847
 apply(erule le_trans)
prensani@13020
   848
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   849
apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   850
--{* 4 subgoals left *}
prensani@13020
   851
apply clarify
prensani@13020
   852
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   853
apply(disjE_tac)
prensani@13020
   854
   apply(simp add:Graph7 Graph8 Graph12)
prensani@13020
   855
  apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
prensani@13020
   856
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   857
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
prensani@13020
   858
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   859
 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
prensani@13020
   860
apply(erule conjE)
prensani@13020
   861
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   862
 apply((rule disjI2)+)
prensani@13020
   863
 apply (rule conjI)
prensani@13020
   864
  apply(simp add:Graph10)
prensani@13020
   865
 apply(erule le_trans)
prensani@13020
   866
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   867
apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) 
prensani@13020
   868
--{* 3 subgoals left *}
prensani@13020
   869
apply clarify
prensani@13020
   870
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   871
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   872
 apply(simp add:Graph10)
prensani@13020
   873
 apply(disjE_tac)
prensani@13020
   874
  apply simp_all
prensani@13020
   875
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
prensani@13020
   876
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   877
 apply(erule conjE)
prensani@13020
   878
 apply((rule disjI2)+,erule le_trans)
prensani@13020
   879
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   880
apply(rule conjI)
prensani@13020
   881
 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
prensani@13020
   882
apply (force simp add:nth_list_update)
prensani@13020
   883
--{* 2 subgoals left *}
prensani@13020
   884
apply clarify 
prensani@13020
   885
apply(simp add:Mul_Auxk_def Graph7 Graph8 Graph12)
prensani@13020
   886
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   887
 apply(simp add:Graph10)
prensani@13020
   888
 apply(disjE_tac)
prensani@13020
   889
  apply simp_all
prensani@13020
   890
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
prensani@13020
   891
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   892
 apply(erule conjE)+
prensani@13020
   893
 apply((rule disjI2)+,rule conjI, erule le_trans)
prensani@13020
   894
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   895
 apply((rule impI)+)
prensani@13020
   896
 apply simp
prensani@13020
   897
 apply(erule disjE)
prensani@13020
   898
  apply(rule disjI1, erule less_le_trans) 
prensani@13020
   899
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   900
 apply force
prensani@13020
   901
apply(rule conjI)
prensani@13020
   902
 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
prensani@13020
   903
apply (force simp add:nth_list_update)
prensani@13022
   904
--{* 1 subgoal left *}
prensani@13020
   905
apply clarify
prensani@13020
   906
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
prensani@13020
   907
apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
   908
 apply(simp add:Graph10)
prensani@13020
   909
 apply(disjE_tac)
prensani@13020
   910
  apply simp_all
prensani@13020
   911
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
prensani@13020
   912
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   913
 apply(erule conjE)
prensani@13020
   914
 apply((rule disjI2)+,erule le_trans)
prensani@13020
   915
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
   916
apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
prensani@13020
   917
done
prensani@13020
   918
prensani@13020
   919
lemma Mul_interfree_Color_Target_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   920
  interfree_aux (Some(Mul_Color_Target j n),{},Some(Mul_Propagate_Black n ))"
prensani@13020
   921
apply (unfold mul_modules)
prensani@13020
   922
apply interfree_aux
prensani@13020
   923
apply safe
prensani@13020
   924
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
   925
done
prensani@13020
   926
prensani@13020
   927
lemma Mul_interfree_Count_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
   928
  interfree_aux (Some(Mul_Count n ),{},Some(Mul_Redirect_Edge j n))"
prensani@13020
   929
apply (unfold mul_modules)
prensani@13020
   930
apply interfree_aux
prensani@13020
   931
--{* 9 subgoals left *}
prensani@13020
   932
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def Graph6)
prensani@13020
   933
apply clarify
prensani@13020
   934
apply disjE_tac
prensani@13020
   935
   apply(simp add:Graph6)
prensani@13020
   936
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   937
 apply(simp add:Graph6)
prensani@13020
   938
apply clarify
prensani@13020
   939
apply disjE_tac
prensani@13020
   940
 apply(simp add:Graph6)
prensani@13020
   941
 apply(rule conjI)
prensani@13020
   942
  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
   943
 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
   944
apply(simp add:Graph6)
prensani@13020
   945
--{* 8 subgoals left *}
prensani@13020
   946
apply(simp add:mul_mutator_defs nth_list_update)
prensani@13020
   947
--{* 7 subgoals left *}
prensani@13020
   948
apply(simp add:mul_mutator_defs mul_collector_defs)
prensani@13020
   949
apply clarify
prensani@13020
   950
apply disjE_tac
prensani@13020
   951
   apply(simp add:Graph6)
prensani@13020
   952
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   953
 apply(simp add:Graph6)
prensani@13020
   954
apply clarify
prensani@13020
   955
apply disjE_tac
prensani@13020
   956
 apply(simp add:Graph6)
prensani@13020
   957
 apply(rule conjI)
prensani@13020
   958
  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
   959
 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
   960
apply(simp add:Graph6)
prensani@13020
   961
--{* 6 subgoals left *}
prensani@13020
   962
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
   963
apply clarify
prensani@13020
   964
apply disjE_tac
prensani@13020
   965
   apply(simp add:Graph6 Queue_def)
prensani@13020
   966
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   967
 apply(simp add:Graph6)
prensani@13020
   968
apply clarify
prensani@13020
   969
apply disjE_tac
prensani@13020
   970
 apply(simp add:Graph6)
prensani@13020
   971
 apply(rule conjI)
prensani@13020
   972
  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
   973
 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
   974
apply(simp add:Graph6)
prensani@13020
   975
--{* 5 subgoals left *}
prensani@13020
   976
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
   977
apply clarify
prensani@13020
   978
apply disjE_tac
prensani@13020
   979
   apply(simp add:Graph6)
prensani@13020
   980
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   981
 apply(simp add:Graph6)
prensani@13020
   982
apply clarify
prensani@13020
   983
apply disjE_tac
prensani@13020
   984
 apply(simp add:Graph6)
prensani@13020
   985
 apply(rule conjI)
prensani@13020
   986
  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
   987
 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
   988
apply(simp add:Graph6)
prensani@13020
   989
--{* 4 subgoals left *}
prensani@13020
   990
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
   991
apply clarify
prensani@13020
   992
apply disjE_tac
prensani@13020
   993
   apply(simp add:Graph6)
prensani@13020
   994
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
   995
 apply(simp add:Graph6)
prensani@13020
   996
apply clarify
prensani@13020
   997
apply disjE_tac
prensani@13020
   998
 apply(simp add:Graph6)
prensani@13020
   999
 apply(rule conjI)
prensani@13020
  1000
  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
  1001
 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
  1002
apply(simp add:Graph6)
prensani@13020
  1003
--{* 3 subgoals left *}
prensani@13020
  1004
apply(simp add:mul_mutator_defs nth_list_update)
prensani@13020
  1005
--{* 2 subgoals left *}
prensani@13020
  1006
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
prensani@13020
  1007
apply clarify
prensani@13020
  1008
apply disjE_tac
prensani@13020
  1009
   apply(simp add:Graph6)
prensani@13020
  1010
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
prensani@13020
  1011
 apply(simp add:Graph6)
prensani@13020
  1012
apply clarify
prensani@13020
  1013
apply disjE_tac
prensani@13020
  1014
 apply(simp add:Graph6)
prensani@13020
  1015
 apply(rule conjI)
prensani@13020
  1016
  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
  1017
 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
  1018
apply(simp add:Graph6)
prensani@13022
  1019
--{* 1 subgoal left *}
prensani@13020
  1020
apply(simp add:mul_mutator_defs nth_list_update)
prensani@13020
  1021
done
prensani@13020
  1022
prensani@13020
  1023
lemma Mul_interfree_Redirect_Edge_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1024
  interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Count n ))"
prensani@13020
  1025
apply (unfold mul_modules)
prensani@13020
  1026
apply interfree_aux
prensani@13020
  1027
apply safe
prensani@13020
  1028
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
  1029
done
prensani@13020
  1030
prensani@13020
  1031
lemma Mul_interfree_Count_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1032
  interfree_aux (Some(Mul_Count n ),{},Some(Mul_Color_Target j n))"
prensani@13020
  1033
apply (unfold mul_modules)
prensani@13020
  1034
apply interfree_aux
prensani@13020
  1035
apply(simp_all add:mul_collector_defs mul_mutator_defs Mul_CountInv_def)
prensani@13020
  1036
--{* 6 subgoals left *}
prensani@13020
  1037
apply clarify
prensani@13020
  1038
apply disjE_tac
prensani@13020
  1039
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1040
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1041
apply clarify
prensani@13020
  1042
apply disjE_tac
prensani@13020
  1043
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1044
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1045
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1046
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1047
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1048
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1049
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1050
--{* 5 subgoals left *}
prensani@13020
  1051
apply clarify
prensani@13020
  1052
apply disjE_tac
prensani@13020
  1053
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1054
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1055
apply clarify
prensani@13020
  1056
apply disjE_tac
prensani@13020
  1057
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1058
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1059
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1060
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1061
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1062
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1063
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1064
--{* 4 subgoals left *}
prensani@13020
  1065
apply clarify
prensani@13020
  1066
apply disjE_tac
prensani@13020
  1067
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1068
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1069
apply clarify
prensani@13020
  1070
apply disjE_tac
prensani@13020
  1071
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1072
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1073
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1074
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1075
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1076
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1077
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1078
--{* 3 subgoals left *}
prensani@13020
  1079
apply clarify
prensani@13020
  1080
apply disjE_tac
prensani@13020
  1081
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1082
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1083
apply clarify
prensani@13020
  1084
apply disjE_tac
prensani@13020
  1085
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1086
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1087
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1088
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1089
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1090
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1091
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1092
--{* 2 subgoals left *}
prensani@13020
  1093
apply clarify
prensani@13020
  1094
apply disjE_tac
prensani@13020
  1095
  apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
prensani@13020
  1096
 apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
prensani@13020
  1097
apply clarify
prensani@13020
  1098
apply disjE_tac
prensani@13020
  1099
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1100
 apply(rule conjI)
prensani@13020
  1101
  apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1102
   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1103
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1104
  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1105
 apply (simp add: nth_list_update)
prensani@13020
  1106
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1107
apply(rule conjI)
prensani@13020
  1108
 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1109
apply (simp add: nth_list_update)
prensani@13022
  1110
--{* 1 subgoal left *}
prensani@13020
  1111
apply clarify
prensani@13020
  1112
apply disjE_tac
prensani@13020
  1113
  apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1114
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1115
apply clarify
prensani@13020
  1116
apply disjE_tac
prensani@13020
  1117
 apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1118
 apply(case_tac "M x!(T (Muts x!j))=Black")
prensani@13020
  1119
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
prensani@13020
  1120
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
prensani@13020
  1121
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
prensani@13020
  1122
apply (simp add: Graph7 Graph8 Graph12)
prensani@13020
  1123
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
prensani@13020
  1124
done
prensani@13020
  1125
prensani@13020
  1126
lemma Mul_interfree_Color_Target_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1127
  interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Count n ))"
prensani@13020
  1128
apply (unfold mul_modules)
prensani@13020
  1129
apply interfree_aux
prensani@13020
  1130
apply safe
prensani@13020
  1131
apply(simp_all add:mul_mutator_defs nth_list_update)
prensani@13020
  1132
done
prensani@13020
  1133
prensani@13020
  1134
lemma Mul_interfree_Append_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1135
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
prensani@13020
  1136
apply (unfold mul_modules)
prensani@13020
  1137
apply interfree_aux
prensani@13020
  1138
apply(tactic {* ALLGOALS Clarify_tac *})
prensani@13020
  1139
apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
prensani@13020
  1140
apply(erule_tac x=j in allE, force dest:Graph3)+
prensani@13020
  1141
done
prensani@13020
  1142
prensani@13020
  1143
lemma Mul_interfree_Redirect_Edge_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1144
  interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
prensani@13020
  1145
apply (unfold mul_modules)
prensani@13020
  1146
apply interfree_aux
prensani@13020
  1147
apply(tactic {* ALLGOALS Clarify_tac *})
prensani@13020
  1148
apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def  mul_mutator_defs nth_list_update)
prensani@13020
  1149
done
prensani@13020
  1150
prensani@13020
  1151
lemma Mul_interfree_Append_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1152
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
prensani@13020
  1153
apply (unfold mul_modules)
prensani@13020
  1154
apply interfree_aux
prensani@13020
  1155
apply(tactic {* ALLGOALS Clarify_tac *})
prensani@13020
  1156
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1 
prensani@13020
  1157
              Graph12 nth_list_update)
prensani@13020
  1158
done
prensani@13020
  1159
prensani@13020
  1160
lemma Mul_interfree_Color_Target_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
prensani@13020
  1161
  interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
prensani@13020
  1162
apply (unfold mul_modules)
prensani@13020
  1163
apply interfree_aux
prensani@13020
  1164
apply(tactic {* ALLGOALS Clarify_tac *})
prensani@13020
  1165
apply(simp_all add: mul_mutator_defs nth_list_update)
prensani@13020
  1166
apply(simp add:Mul_AppendInv_def Append_to_free0)
prensani@13020
  1167
done
prensani@13020
  1168
prensani@13020
  1169
subsubsection {* Interference freedom Collector-Mutator *}
prensani@13020
  1170
prensani@13020
  1171
lemmas mul_collector_mutator_interfree =  
prensani@13020
  1172
 Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target 
prensani@13020
  1173
 Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target  
prensani@13020
  1174
 Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target 
prensani@13020
  1175
 Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target 
prensani@13020
  1176
 Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots 
prensani@13020
  1177
 Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black  
prensani@13020
  1178
 Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count 
prensani@13020
  1179
 Mul_interfree_Redirect_Edge_Append Mul_interfree_Color_Target_Append
prensani@13020
  1180
prensani@13020
  1181
lemma Mul_interfree_Collector_Mutator: "j<n  \<Longrightarrow> 
prensani@13020
  1182
  interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))"
prensani@13020
  1183
apply(unfold Mul_Collector_def Mul_Mutator_def)
prensani@13020
  1184
apply interfree_aux
prensani@13020
  1185
apply(simp_all add:mul_collector_mutator_interfree)
prensani@13020
  1186
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
prensani@13020
  1187
apply(tactic  {* TRYALL (interfree_aux_tac) *})
prensani@13020
  1188
--{* 42 subgoals left *}
prensani@13020
  1189
apply (clarify,simp add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)+
prensani@13020
  1190
--{* 24 subgoals left *}
prensani@13020
  1191
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
  1192
--{* 14 subgoals left *}
prensani@13020
  1193
apply(tactic {* TRYALL Clarify_tac *})
prensani@13020
  1194
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
  1195
apply(tactic {* TRYALL (rtac conjI) *})
prensani@13020
  1196
apply(tactic {* TRYALL (rtac impI) *})
prensani@13020
  1197
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1198
apply(tactic {* TRYALL (etac conjE) *})
prensani@13020
  1199
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1200
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1201
--{* 72 subgoals left *}
prensani@13020
  1202
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
prensani@13020
  1203
--{* 35 subgoals left *}
wenzelm@20050
  1204
apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
prensani@13020
  1205
--{* 28 subgoals left *}
prensani@13020
  1206
apply(tactic {* TRYALL (etac conjE) *})
prensani@13020
  1207
apply(tactic {* TRYALL (etac disjE) *})
prensani@13020
  1208
--{* 34 subgoals left *}
prensani@13020
  1209
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
  1210
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
prensani@13020
  1211
apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
prensani@13020
  1212
apply(simp_all add:Graph10)
prensani@13020
  1213
--{* 47 subgoals left *}
wenzelm@21669
  1214
apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
prensani@13020
  1215
--{* 41 subgoals left *}
prensani@13020
  1216
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
prensani@13020
  1217
--{* 35 subgoals left *}
wenzelm@21669
  1218
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
prensani@13020
  1219
--{* 31 subgoals left *}
wenzelm@21669
  1220
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
prensani@13020
  1221
--{* 29 subgoals left *}
wenzelm@21669
  1222
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
  1223
--{* 25 subgoals left *}
prensani@13020
  1224
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
prensani@13020
  1225
--{* 10 subgoals left *}
prensani@13020
  1226
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
  1227
done
prensani@13020
  1228
prensani@13020
  1229
subsubsection {* Interference freedom Mutator-Collector *}
prensani@13020
  1230
prensani@13020
  1231
lemma Mul_interfree_Mutator_Collector: " j < n \<Longrightarrow> 
prensani@13020
  1232
  interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))"
prensani@13020
  1233
apply(unfold Mul_Collector_def Mul_Mutator_def)
prensani@13020
  1234
apply interfree_aux
prensani@13020
  1235
apply(simp_all add:mul_collector_mutator_interfree)
prensani@13020
  1236
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
prensani@13020
  1237
apply(tactic  {* TRYALL (interfree_aux_tac) *})
prensani@13020
  1238
--{* 76 subgoals left *}
prensani@13020
  1239
apply (clarify,simp add: nth_list_update)+
prensani@13020
  1240
--{* 56 subgoals left *}
prensani@13020
  1241
apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
prensani@13020
  1242
done
prensani@13020
  1243
prensani@13020
  1244
subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
prensani@13020
  1245
prensani@13020
  1246
text {* The total number of verification conditions is 328 *}
prensani@13020
  1247
prensani@13020
  1248
lemma Mul_Gar_Coll: 
prensani@13020
  1249
 "\<parallel>- .{\<acute>Mul_Proper n \<and> \<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))}.  
prensani@13020
  1250
 COBEGIN  
prensani@13020
  1251
  Mul_Collector n
prensani@13020
  1252
 .{False}.
prensani@13020
  1253
 \<parallel>  
prensani@13020
  1254
 SCHEME  [0\<le> j< n]
prensani@13020
  1255
  Mul_Mutator j n
prensani@13020
  1256
 .{False}.  
prensani@13020
  1257
 COEND  
prensani@13020
  1258
 .{False}."
prensani@13020
  1259
apply oghoare
prensani@13020
  1260
--{* Strengthening the precondition *}
prensani@13020
  1261
apply(rule Int_greatest)
prensani@13020
  1262
 apply (case_tac n)
prensani@13020
  1263
  apply(force simp add: Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1264
 apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
prensani@13020
  1265
 apply force
prensani@13020
  1266
apply clarify
prensani@13020
  1267
apply(case_tac xa)
prensani@13020
  1268
 apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1269
apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
prensani@13020
  1270
--{* Collector *}
prensani@13020
  1271
apply(rule Mul_Collector)
prensani@13020
  1272
--{* Mutator *}
prensani@13020
  1273
apply(erule Mul_Mutator)
prensani@13020
  1274
--{* Interference freedom *}
prensani@13020
  1275
apply(simp add:Mul_interfree_Collector_Mutator)
prensani@13020
  1276
apply(simp add:Mul_interfree_Mutator_Collector)
prensani@13020
  1277
apply(simp add:Mul_interfree_Mutator_Mutator)
prensani@13020
  1278
--{* Weakening of the postcondition *}
prensani@13020
  1279
apply(case_tac n)
prensani@13020
  1280
 apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1281
apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
prensani@13020
  1282
done
prensani@13020
  1283
nipkow@13187
  1284
end