src/HOL/Hoare_Parallel/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
header {* \section{The Single Mutator Case} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15197
diff changeset
     3
theory Gar_Coll imports Graph OG_Syntax begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     4
13624
17684cf64fda added the new elim rule psubsetE
paulson
parents: 13601
diff changeset
     5
declare psubsetE [rule del]
17684cf64fda added the new elim rule psubsetE
paulson
parents: 13601
diff changeset
     6
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     7
text {* Declaration of variables: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     8
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     9
record gar_coll_state =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    10
  M :: nodes
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
  E :: edges
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
  bc :: "nat set"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
  obc :: "nat set"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
  Ma :: nodes
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    15
  ind :: nat 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
  k :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
  z :: bool
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
subsection {* The Mutator *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    21
text {* The mutator first redirects an arbitrary edge @{text "R"} from
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
an arbitrary accessible node towards an arbitrary accessible node
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    23
@{text "T"}.  It then colors the new target @{text "T"} black. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    24
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    25
We declare the arbitrarily selected node and edge as constants:*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    26
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    27
consts R :: nat  T :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    28
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    29
text {* \noindent The following predicate states, given a list of
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    30
nodes @{text "m"} and a list of edges @{text "e"}, the conditions
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    31
under which the selected edge @{text "R"} and node @{text "T"} are
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    32
valid: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    33
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
    34
definition Mut_init :: "gar_coll_state \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
  "Mut_init \<equiv> \<guillemotleft> T \<in> Reach \<acute>E \<and> R < length \<acute>E \<and> T < length \<acute>M \<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    36
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    37
text {* \noindent For the mutator we
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    38
consider two modules, one for each action.  An auxiliary variable
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    39
@{text "\<acute>z"} is set to false if the mutator has already redirected an
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    40
edge but has not yet colored the new target.   *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    41
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
    42
definition Redirect_Edge :: "gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    43
  "Redirect_Edge \<equiv> .{\<acute>Mut_init \<and> \<acute>z}. \<langle>\<acute>E:=\<acute>E[R:=(fst(\<acute>E!R), T)],, \<acute>z:= (\<not>\<acute>z)\<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: 34233
diff changeset
    45
definition Color_Target :: "gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    46
  "Color_Target \<equiv> .{\<acute>Mut_init \<and> \<not>\<acute>z}. \<langle>\<acute>M:=\<acute>M[T:=Black],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    47
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
    48
definition Mutator :: "gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    49
  "Mutator \<equiv>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    50
  .{\<acute>Mut_init \<and> \<acute>z}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    51
  WHILE True INV .{\<acute>Mut_init \<and> \<acute>z}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    52
  DO  Redirect_Edge ;; Color_Target  OD"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    53
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    54
subsubsection {* Correctness of the mutator *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    55
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    56
lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    57
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    58
lemma Redirect_Edge: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    59
  "\<turnstile> Redirect_Edge pre(Color_Target)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    60
apply (unfold mutator_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    61
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    62
apply(simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    63
apply(force elim:Graph2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    64
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    65
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    66
lemma Color_Target:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    67
  "\<turnstile> Color_Target .{\<acute>Mut_init \<and> \<acute>z}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    68
apply (unfold mutator_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    69
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    70
apply(simp_all)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    71
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    72
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    73
lemma Mutator: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    74
 "\<turnstile> Mutator .{False}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    75
apply(unfold Mutator_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    76
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    77
apply(simp_all add:Redirect_Edge Color_Target)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    78
apply(simp add:mutator_defs Redirect_Edge_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    79
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    80
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    81
subsection {* The Collector *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    82
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    83
text {* \noindent A constant @{text "M_init"} is used to give @{text "\<acute>Ma"} a
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    84
suitable first value, defined as a list of nodes where only the @{text
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    85
"Roots"} are black. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    86
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    87
consts  M_init :: nodes
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    88
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
    89
definition Proper_M_init :: "gar_coll_state \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    90
  "Proper_M_init \<equiv>  \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    91
 
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
    92
definition Proper :: "gar_coll_state \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    93
  "Proper \<equiv> \<guillemotleft> Proper_Roots \<acute>M \<and> Proper_Edges(\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    94
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
    95
definition Safe :: "gar_coll_state \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    96
  "Safe \<equiv> \<guillemotleft> Reach \<acute>E \<subseteq> Blacks \<acute>M \<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    97
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    98
lemmas collector_defs = Proper_M_init_def Proper_def Safe_def
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    99
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   100
subsubsection {* Blackening the roots *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   101
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   102
definition Blacken_Roots :: " gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   103
  "Blacken_Roots \<equiv> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   104
  .{\<acute>Proper}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   105
  \<acute>ind:=0;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   106
  .{\<acute>Proper \<and> \<acute>ind=0}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   107
  WHILE \<acute>ind<length \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   108
   INV .{\<acute>Proper \<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
   109
  DO .{\<acute>Proper \<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
   110
   IF \<acute>ind\<in>Roots THEN 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   111
   .{\<acute>Proper \<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
   112
    \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   113
   .{\<acute>Proper \<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
   114
    \<acute>ind:=\<acute>ind+1 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   115
  OD"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   116
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   117
lemma Blacken_Roots: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   118
 "\<turnstile> Blacken_Roots .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   119
apply (unfold Blacken_Roots_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   120
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   121
apply(simp_all add:collector_defs Graph_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   122
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   123
apply(simp_all add:nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   124
  apply (erule less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   125
   apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   126
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   127
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   128
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   129
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   130
subsubsection {* Propagating black *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   131
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   132
definition PBInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   133
  "PBInv \<equiv> \<guillemotleft> \<lambda>ind. \<acute>obc < Blacks \<acute>M \<or> (\<forall>i <ind. \<not>BtoW (\<acute>E!i, \<acute>M) \<or>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   134
   (\<not>\<acute>z \<and> i=R \<and> (snd(\<acute>E!R)) = T \<and> (\<exists>r. ind \<le> r \<and> r < length \<acute>E \<and> BtoW(\<acute>E!r,\<acute>M))))\<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   135
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   136
definition Propagate_Black_aux :: "gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   137
  "Propagate_Black_aux \<equiv>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   138
  .{\<acute>Proper \<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
   139
  \<acute>ind:=0;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   140
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   141
  WHILE \<acute>ind<length \<acute>E 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   142
   INV .{\<acute>Proper \<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
   143
         \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   144
  DO .{\<acute>Proper \<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
   145
       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   146
   IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   147
    .{\<acute>Proper \<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
   148
       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   149
     \<acute>M:=\<acute>M[snd(\<acute>E!\<acute>ind):=Black];;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   150
    .{\<acute>Proper \<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
   151
       \<and> \<acute>PBInv (\<acute>ind + 1) \<and> \<acute>ind<length \<acute>E}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   152
     \<acute>ind:=\<acute>ind+1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   153
   FI
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   154
  OD"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   155
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   156
lemma Propagate_Black_aux: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   157
  "\<turnstile>  Propagate_Black_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   158
  .{\<acute>Proper \<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
   159
    \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   160
apply (unfold Propagate_Black_aux_def  PBInv_def collector_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   161
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   162
apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   163
      apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   164
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   165
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   166
--{* 4 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   167
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   168
apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   169
apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   170
 apply(rule disjI1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   171
 apply(erule Graph13)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   172
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   173
apply (case_tac "M x ! snd (E x ! ind x)=Black")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   174
 apply (simp add: Graph10 BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   175
 apply (rule disjI2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   176
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   177
 apply (erule less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   178
  apply (erule_tac x=i in allE , erule (1) notE impE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   179
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   180
  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
   181
  apply (drule_tac y = r in le_imp_less_or_eq)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   182
  apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   183
   apply (subgoal_tac "Suc (ind x)\<le>r")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   184
    apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   185
   apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   186
  apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   187
 apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   188
apply(rule disjI1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   189
apply(erule subset_psubset_trans)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   190
apply(erule Graph11)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   191
apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   192
--{* 3 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   193
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   194
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   195
--{* last *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   196
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   197
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   198
apply(subgoal_tac "ind x = length (E x)")
34233
156c42518cfc removed more asm_rl's - unfortunately slowdown of 1 min.
nipkow
parents: 32687
diff changeset
   199
 apply (simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   200
 apply(drule Graph1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   201
   apply simp
34233
156c42518cfc removed more asm_rl's - unfortunately slowdown of 1 min.
nipkow
parents: 32687
diff changeset
   202
  apply clarify
156c42518cfc removed more asm_rl's - unfortunately slowdown of 1 min.
nipkow
parents: 32687
diff changeset
   203
  apply(erule allE, erule impE, assumption)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   204
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   205
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   206
apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   207
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   208
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   209
subsubsection {* Refining propagating black *}
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: 34233
diff changeset
   211
definition Auxk :: "gar_coll_state \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   212
  "Auxk \<equiv> \<guillemotleft>\<acute>k<length \<acute>M \<and> (\<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   213
          \<acute>obc<Blacks \<acute>M \<or> (\<not>\<acute>z \<and> \<acute>ind=R \<and> snd(\<acute>E!R)=T  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   214
          \<and> (\<exists>r. \<acute>ind<r \<and> r<length \<acute>E \<and> BtoW(\<acute>E!r, \<acute>M))))\<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   215
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   216
definition Propagate_Black :: " gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   217
  "Propagate_Black \<equiv>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   218
  .{\<acute>Proper \<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
   219
  \<acute>ind:=0;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   220
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   221
  WHILE \<acute>ind<length \<acute>E 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   222
   INV .{\<acute>Proper \<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
   223
         \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   224
  DO .{\<acute>Proper \<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
   225
       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   226
   IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   227
    .{\<acute>Proper \<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
   228
      \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   229
     \<acute>k:=(snd(\<acute>E!\<acute>ind));;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   230
    .{\<acute>Proper \<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
   231
      \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   232
      \<and> \<acute>Auxk}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   233
     \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],, \<acute>ind:=\<acute>ind+1\<rangle>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   234
   ELSE .{\<acute>Proper \<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
   235
          \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   236
         \<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   237
   FI
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   238
  OD"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   239
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   240
lemma Propagate_Black: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   241
  "\<turnstile>  Propagate_Black
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   242
  .{\<acute>Proper \<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
   243
    \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   244
apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   245
apply annhoare
32687
27530efec97a tuned proofs; be more cautios wrt. default simp rules
haftmann
parents: 32621
diff changeset
   246
apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   247
       apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   248
      apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   249
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   250
--{* 5 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   251
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   252
apply(simp add:BtoW_def Proper_Edges_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   253
--{* 4 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   254
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   255
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   256
apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   257
 apply (rule disjI1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   258
 apply (erule psubset_subset_trans)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   259
 apply (erule Graph9)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   260
apply (case_tac "M x!k x=Black")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   261
 apply (case_tac "M x ! snd (E x ! ind x)=Black")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   262
  apply (simp add: Graph10 BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   263
  apply (rule disjI2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   264
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   265
  apply (erule less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   266
   apply (erule_tac x=i in allE , erule (1) notE impE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   267
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   268
   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
   269
   apply (drule_tac y = r in le_imp_less_or_eq)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   270
   apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   271
    apply (subgoal_tac "Suc (ind x)\<le>r")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   272
     apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   273
    apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   274
   apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   275
  apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   276
 apply (simp add: Graph10 BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   277
 apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   278
  apply (erule disjI1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   279
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   280
 apply (erule less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   281
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   282
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   283
 apply (subgoal_tac "Suc R\<le>r")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   284
  apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   285
 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   286
apply(rule disjI1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   287
apply(erule subset_psubset_trans)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   288
apply(erule Graph11)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   289
apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   290
--{* 2 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   291
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   292
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   293
apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   294
 apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   295
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   296
apply (erule less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   297
 apply (erule_tac x=i in allE , erule (1) notE impE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   298
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   299
 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
   300
 apply (drule_tac y = r in le_imp_less_or_eq)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   301
 apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   302
  apply (subgoal_tac "Suc (ind x)\<le>r")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   303
   apply fast
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   304
  apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   305
 apply (simp add: BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   306
apply (simp add: BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   307
--{* last *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   308
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   309
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   310
apply(subgoal_tac "ind x = length (E x)")
34233
156c42518cfc removed more asm_rl's - unfortunately slowdown of 1 min.
nipkow
parents: 32687
diff changeset
   311
 apply (simp)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   312
 apply(drule Graph1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   313
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   314
  apply clarify  
34233
156c42518cfc removed more asm_rl's - unfortunately slowdown of 1 min.
nipkow
parents: 32687
diff changeset
   315
  apply(erule allE, erule impE, assumption)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   316
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   317
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   318
apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   319
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   320
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   321
subsubsection {* Counting black nodes *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   322
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   323
definition CountInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   324
  "CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   325
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   326
definition Count :: " gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   327
  "Count \<equiv>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   328
  .{\<acute>Proper \<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>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   331
  \<acute>ind:=0;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   332
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   333
    \<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
   334
   \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={} 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   335
   \<and> \<acute>ind=0}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   336
   WHILE \<acute>ind<length \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   337
     INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   338
           \<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
   339
           \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   340
           \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind\<le>length \<acute>M}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   341
   DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   342
         \<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
   343
         \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   344
         \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   345
       IF \<acute>M!\<acute>ind=Black 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   346
          THEN .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   347
                 \<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
   348
                 \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   349
                 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   350
          \<acute>bc:=insert \<acute>ind \<acute>bc
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   351
       FI;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   352
      .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   353
        \<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
   354
        \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv (\<acute>ind+1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   355
        \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   356
      \<acute>ind:=\<acute>ind+1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   357
   OD"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   358
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   359
lemma Count: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   360
  "\<turnstile> Count 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   361
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   362
   \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   363
   \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   364
apply(unfold Count_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   365
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   366
apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   367
      apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   368
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   369
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   370
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   371
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   372
   apply(fast elim:less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   373
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   374
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   375
  apply(fast elim:less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   376
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   377
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   378
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   379
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   380
subsubsection {* Appending garbage nodes to the free list *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   381
45827
66c68453455c modernized specifications;
wenzelm
parents: 42793
diff changeset
   382
axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
66c68453455c modernized specifications;
wenzelm
parents: 42793
diff changeset
   383
where
66c68453455c modernized specifications;
wenzelm
parents: 42793
diff changeset
   384
  Append_to_free0: "length (Append_to_free (i, e)) = length e" and
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   385
  Append_to_free1: "Proper_Edges (m, e) 
45827
66c68453455c modernized specifications;
wenzelm
parents: 42793
diff changeset
   386
                   \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   387
  Append_to_free2: "i \<notin> Reach e 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   388
     \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   389
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   390
definition AppendInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   391
  "AppendInv \<equiv> \<guillemotleft>\<lambda>ind. \<forall>i<length \<acute>M. ind\<le>i \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black\<guillemotright>"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   392
45827
66c68453455c modernized specifications;
wenzelm
parents: 42793
diff changeset
   393
definition Append :: "gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   394
   "Append \<equiv>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   395
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   396
  \<acute>ind:=0;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   397
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   398
    WHILE \<acute>ind<length \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   399
      INV .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   400
    DO .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   401
       IF \<acute>M!\<acute>ind=Black THEN 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   402
          .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   403
          \<acute>M:=\<acute>M[\<acute>ind:=White] 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   404
       ELSE .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   405
              \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   406
       FI;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   407
     .{\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   408
       \<acute>ind:=\<acute>ind+1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   409
    OD"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   410
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   411
lemma Append: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   412
  "\<turnstile> Append .{\<acute>Proper}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   413
apply(unfold Append_def AppendInv_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   414
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   415
apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   416
       apply(force simp:Blacks_def nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   417
      apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   418
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   419
    apply(force simp add:Graph_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   420
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   421
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   422
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   423
  apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   424
   apply (erule Append_to_free1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   425
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   426
  apply (drule_tac n = "i" in Append_to_free2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   427
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   428
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   429
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   430
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   431
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   432
subsubsection {* Correctness of the Collector *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   433
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 34233
diff changeset
   434
definition Collector :: " gar_coll_state ann_com" where
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   435
  "Collector \<equiv>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   436
.{\<acute>Proper}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   437
 WHILE True INV .{\<acute>Proper}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   438
 DO  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   439
  Blacken_Roots;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   440
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   441
   \<acute>obc:={};; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   442
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   443
   \<acute>bc:=Roots;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   444
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   445
   \<acute>Ma:=M_init;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   446
  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   447
   WHILE \<acute>obc\<noteq>\<acute>bc  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   448
     INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   449
           \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   450
           \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   451
   DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   452
       \<acute>obc:=\<acute>bc;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   453
       Propagate_Black;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   454
      .{\<acute>Proper \<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
   455
        \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   456
       \<acute>Ma:=\<acute>M;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   457
      .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   458
        \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   459
        \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   460
       \<acute>bc:={};;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   461
       Count 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   462
   OD;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   463
  Append  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   464
 OD"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   465
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   466
lemma Collector: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   467
  "\<turnstile> Collector .{False}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   468
apply(unfold Collector_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   469
apply annhoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   470
apply(simp_all add: Blacken_Roots Propagate_Black Count Append)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   471
apply(simp_all add:Blacken_Roots_def Propagate_Black_def Count_def Append_def collector_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   472
   apply (force simp add: Proper_Roots_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   473
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   474
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   475
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   476
apply (erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   477
apply(simp add:psubsetI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   478
 apply(force dest:subset_antisym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   479
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   480
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   481
subsection {* Interference Freedom *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   482
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   483
lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   484
                 Propagate_Black_def Count_def Append_def
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   485
lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   486
lemmas abbrev = collector_defs mutator_defs Invariants
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   487
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   488
lemma interfree_Blacken_Roots_Redirect_Edge: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   489
 "interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   490
apply (unfold modules)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   491
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   492
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   493
apply (simp_all add:Graph6 Graph12 abbrev)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   494
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   495
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   496
lemma interfree_Redirect_Edge_Blacken_Roots: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   497
  "interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   498
apply (unfold modules)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   499
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   500
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   501
apply(simp add:abbrev)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   502
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   503
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   504
lemma interfree_Blacken_Roots_Color_Target: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   505
  "interfree_aux (Some Blacken_Roots, {}, Some Color_Target)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   506
apply (unfold modules)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   507
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   508
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   509
apply(simp_all add:Graph7 Graph8 nth_list_update abbrev)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   510
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   511
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   512
lemma interfree_Color_Target_Blacken_Roots: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   513
  "interfree_aux (Some Color_Target, {}, Some Blacken_Roots)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   514
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   515
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   516
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   517
apply(simp add:abbrev)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   518
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   519
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   520
lemma interfree_Propagate_Black_Redirect_Edge: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   521
  "interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   522
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   523
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   524
--{* 11 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   525
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   526
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   527
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   528
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   529
apply(erule conjE)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   530
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   531
 apply(erule Graph4) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   532
   apply(simp)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   533
  apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   534
 apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   535
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   536
 apply (force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   537
apply(erule Graph4)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   538
   apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   539
--{* 7 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   540
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   541
apply(erule conjE)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   542
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   543
 apply(erule Graph4) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   544
   apply(simp)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   545
  apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   546
 apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   547
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   548
 apply (force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   549
apply(erule Graph4)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   550
   apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   551
--{* 6 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   552
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   553
apply(erule conjE)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   554
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   555
 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   556
  apply(erule Graph4) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   557
    apply(simp)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   558
   apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   559
  apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   560
 apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   561
  apply (force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   562
 apply(erule Graph4)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   563
    apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   564
apply(simp add:BtoW_def nth_list_update) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   565
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   566
--{* 5 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   567
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   568
--{* 4 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   569
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   570
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   571
 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   572
  apply(erule Graph4) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   573
    apply(simp)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   574
   apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   575
  apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   576
 apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   577
  apply (force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   578
 apply(erule Graph4)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   579
    apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   580
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   581
 apply(simp add:nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   582
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   583
apply(rule impI, rule impI, erule disjE, erule disjI1, case_tac "R = (ind x)" ,case_tac "M x ! T = Black")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   584
  apply(force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   585
 apply(case_tac "M x !snd (E x ! ind x)=Black")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   586
  apply(rule disjI2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   587
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   588
  apply (erule Graph5)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   589
  apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   590
 apply(force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   591
apply(force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   592
--{* 3 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   593
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   594
--{* 2 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   595
apply(clarify, simp add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   596
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   597
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   598
 apply(erule Graph4) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   599
   apply(simp)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   600
  apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   601
 apply (simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   602
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   603
 apply (force simp add:BtoW_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   604
apply(erule Graph4)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   605
   apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   606
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   607
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   608
lemma interfree_Redirect_Edge_Propagate_Black: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   609
  "interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   610
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   611
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   612
apply(clarify, simp add:abbrev)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   613
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   614
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   615
lemma interfree_Propagate_Black_Color_Target: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   616
  "interfree_aux (Some Propagate_Black, {}, Some Color_Target)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   617
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   618
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   619
--{* 11 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   620
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   621
apply(erule conjE)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   622
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   623
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   624
      erule allE, erule impE, assumption, erule impE, assumption, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   625
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   626
--{* 7 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   627
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   628
apply(erule conjE)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   629
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   630
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   631
      erule allE, erule impE, assumption, erule impE, assumption, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   632
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   633
--{* 6 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   634
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   635
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   636
apply (rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   637
 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   638
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   639
      erule allE, erule impE, assumption, erule impE, assumption, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   640
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   641
apply(simp add:nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   642
--{* 5 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   643
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   644
--{* 4 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   645
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   646
apply (rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   647
 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   648
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   649
      erule allE, erule impE, assumption, erule impE, assumption, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   650
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   651
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   652
apply(simp add:nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   653
apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   654
      erule subset_psubset_trans, erule Graph11, force)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   655
--{* 3 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   656
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   657
--{* 2 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   658
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   659
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   660
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   661
      erule allE, erule impE, assumption, erule impE, assumption, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   662
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   663
--{* 3 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   664
apply(simp add:abbrev)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   665
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   666
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   667
lemma interfree_Color_Target_Propagate_Black: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   668
  "interfree_aux (Some Color_Target, {}, Some Propagate_Black)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   669
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   670
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   671
apply(clarify, simp add:abbrev)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   672
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   673
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   674
lemma interfree_Count_Redirect_Edge: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   675
  "interfree_aux (Some Count, {}, Some Redirect_Edge)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   676
apply (unfold modules)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   677
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   678
--{* 9 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   679
apply(simp_all add:abbrev Graph6 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   680
--{* 6 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   681
apply(clarify, simp add:abbrev Graph6 Graph12,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   682
      erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   683
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   684
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   685
lemma interfree_Redirect_Edge_Count: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   686
  "interfree_aux (Some Redirect_Edge, {}, Some Count)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   687
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   688
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   689
apply(clarify,simp add:abbrev)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   690
apply(simp add:abbrev)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   691
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   692
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   693
lemma interfree_Count_Color_Target: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   694
  "interfree_aux (Some Count, {}, Some Color_Target)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   695
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   696
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   697
--{* 9 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   698
apply(simp_all add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   699
--{* 6 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   700
apply(clarify,simp add:abbrev Graph7 Graph8 Graph12,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   701
      erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   702
--{* 2 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   703
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   704
apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   705
 apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   706
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
   707
--{* 1 subgoal left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   708
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   709
      erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   710
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   711
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   712
lemma interfree_Color_Target_Count: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   713
  "interfree_aux (Some Color_Target, {}, Some Count)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   714
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   715
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   716
apply(clarify, simp add:abbrev)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   717
apply(simp add:abbrev)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   718
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   719
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   720
lemma interfree_Append_Redirect_Edge: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   721
  "interfree_aux (Some Append, {}, Some Redirect_Edge)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   722
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   723
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   724
apply( simp_all add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   725
apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   726
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   727
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   728
lemma interfree_Redirect_Edge_Append: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   729
  "interfree_aux (Some Redirect_Edge, {}, Some Append)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   730
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   731
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   732
apply(clarify, simp add:abbrev Append_to_free0)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   733
apply (force simp add: Append_to_free2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   734
apply(clarify, simp add:abbrev Append_to_free0)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   735
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   736
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   737
lemma interfree_Append_Color_Target: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   738
  "interfree_aux (Some Append, {}, Some Color_Target)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   739
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   740
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   741
apply(clarify, simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   742
apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   743
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   744
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   745
lemma interfree_Color_Target_Append: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   746
  "interfree_aux (Some Color_Target, {}, Some Append)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   747
apply (unfold modules )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   748
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   749
apply(clarify, simp add:abbrev Append_to_free0)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   750
apply (force simp add: Append_to_free2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   751
apply(clarify,simp add:abbrev Append_to_free0)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   752
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   753
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   754
lemmas collector_mutator_interfree = 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   755
 interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   756
 interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   757
 interfree_Count_Redirect_Edge interfree_Count_Color_Target 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   758
 interfree_Append_Redirect_Edge interfree_Append_Color_Target 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   759
 interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   760
 interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   761
 interfree_Redirect_Edge_Count interfree_Color_Target_Count 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   762
 interfree_Redirect_Edge_Append interfree_Color_Target_Append
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   763
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   764
subsubsection {* Interference freedom Collector-Mutator *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   765
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   766
lemma interfree_Collector_Mutator:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   767
 "interfree_aux (Some Collector, {}, Some Mutator)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   768
apply(unfold Collector_def Mutator_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   769
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   770
apply(simp_all add:collector_mutator_interfree)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   771
apply(unfold modules collector_defs mutator_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   772
apply(tactic  {* TRYALL (interfree_aux_tac) *})
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   773
--{* 32 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   774
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   775
--{* 20 subgoals left *}
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35416
diff changeset
   776
apply(tactic{* TRYALL (clarify_tac @{context}) *})
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   777
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   778
apply(tactic {* TRYALL (etac disjE) *})
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   779
apply simp_all
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35416
diff changeset
   780
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35416
diff changeset
   781
apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35416
diff changeset
   782
apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   783
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   784
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   785
subsubsection {* Interference freedom Mutator-Collector *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   786
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   787
lemma interfree_Mutator_Collector:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   788
 "interfree_aux (Some Mutator, {}, Some Collector)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   789
apply(unfold Collector_def Mutator_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   790
apply interfree_aux
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   791
apply(simp_all add:collector_mutator_interfree)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   792
apply(unfold modules collector_defs mutator_defs)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   793
apply(tactic  {* TRYALL (interfree_aux_tac) *})
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   794
--{* 64 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   795
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35416
diff changeset
   796
apply(tactic{* TRYALL (clarify_tac @{context}) *})
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   797
--{* 4 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   798
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   799
apply(simp add:Append_to_free2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   800
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   801
apply(simp add:Append_to_free2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   802
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   803
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   804
subsubsection {* The Garbage Collection algorithm *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   805
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   806
text {* In total there are 289 verification conditions.  *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   807
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   808
lemma Gar_Coll: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   809
  "\<parallel>- .{\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   810
  COBEGIN  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   811
   Collector
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   812
  .{False}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   813
 \<parallel>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   814
   Mutator
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   815
  .{False}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   816
 COEND 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   817
  .{False}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   818
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   819
apply(force simp add: Mutator_def Collector_def modules)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   820
apply(rule Collector)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   821
apply(rule Mutator)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   822
apply(simp add:interfree_Collector_Mutator)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   823
apply(simp add:interfree_Mutator_Collector)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   824
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   825
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   826
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   827
end