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