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