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