src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
changeset 35416 d8d7d1b785af
parent 32960 69916a850301
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -26,24 +26,23 @@
     1.4  
     1.5  subsection {* The Mutators *}
     1.6  
     1.7 -constdefs 
     1.8 -  Mul_mut_init :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
     1.9 +definition Mul_mut_init :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
    1.10    "Mul_mut_init \<equiv> \<guillemotleft> \<lambda>n. n=length \<acute>Muts \<and> (\<forall>i<n. R (\<acute>Muts!i)<length \<acute>E 
    1.11                            \<and> T (\<acute>Muts!i)<length \<acute>M) \<guillemotright>"
    1.12  
    1.13 -  Mul_Redirect_Edge  :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com"
    1.14 +definition Mul_Redirect_Edge  :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com" where
    1.15    "Mul_Redirect_Edge j n \<equiv>
    1.16    .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.
    1.17    \<langle>IF T(\<acute>Muts!j) \<in> Reach \<acute>E THEN  
    1.18    \<acute>E:= \<acute>E[R (\<acute>Muts!j):= (fst (\<acute>E!R(\<acute>Muts!j)), T (\<acute>Muts!j))] FI,, 
    1.19    \<acute>Muts:= \<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=False\<rparr>]\<rangle>"
    1.20  
    1.21 -  Mul_Color_Target :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com"
    1.22 +definition Mul_Color_Target :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com" where
    1.23    "Mul_Color_Target j n \<equiv>
    1.24    .{\<acute>Mul_mut_init n \<and> \<not> Z (\<acute>Muts!j)}. 
    1.25    \<langle>\<acute>M:=\<acute>M[T (\<acute>Muts!j):=Black],, \<acute>Muts:=\<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=True\<rparr>]\<rangle>"
    1.26  
    1.27 -  Mul_Mutator :: "nat \<Rightarrow> nat \<Rightarrow>  mul_gar_coll_state ann_com"
    1.28 +definition Mul_Mutator :: "nat \<Rightarrow> nat \<Rightarrow>  mul_gar_coll_state ann_com" where
    1.29    "Mul_Mutator j n \<equiv>
    1.30    .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.  
    1.31    WHILE True  
    1.32 @@ -156,28 +155,25 @@
    1.33  
    1.34  subsection {* The Collector *}
    1.35  
    1.36 -constdefs
    1.37 -  Queue :: "mul_gar_coll_state \<Rightarrow> nat"
    1.38 +definition Queue :: "mul_gar_coll_state \<Rightarrow> nat" where
    1.39   "Queue \<equiv> \<guillemotleft> length (filter (\<lambda>i. \<not> Z i \<and> \<acute>M!(T i) \<noteq> Black) \<acute>Muts) \<guillemotright>"
    1.40  
    1.41  consts  M_init :: nodes
    1.42  
    1.43 -constdefs
    1.44 -  Proper_M_init :: "mul_gar_coll_state \<Rightarrow> bool"
    1.45 +definition Proper_M_init :: "mul_gar_coll_state \<Rightarrow> bool" where
    1.46    "Proper_M_init \<equiv> \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>"
    1.47  
    1.48 -  Mul_Proper :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
    1.49 +definition Mul_Proper :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
    1.50    "Mul_Proper \<equiv> \<guillemotleft> \<lambda>n. Proper_Roots \<acute>M \<and> Proper_Edges (\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<and> n=length \<acute>Muts \<guillemotright>"
    1.51  
    1.52 -  Safe :: "mul_gar_coll_state \<Rightarrow> bool"
    1.53 +definition Safe :: "mul_gar_coll_state \<Rightarrow> bool" where
    1.54    "Safe \<equiv> \<guillemotleft> Reach \<acute>E \<subseteq> Blacks \<acute>M \<guillemotright>"
    1.55  
    1.56  lemmas mul_collector_defs = Proper_M_init_def Mul_Proper_def Safe_def
    1.57  
    1.58  subsubsection {* Blackening Roots *}
    1.59  
    1.60 -constdefs
    1.61 -  Mul_Blacken_Roots :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
    1.62 +definition Mul_Blacken_Roots :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
    1.63    "Mul_Blacken_Roots n \<equiv>
    1.64    .{\<acute>Mul_Proper n}.
    1.65    \<acute>ind:=0;;
    1.66 @@ -208,16 +204,14 @@
    1.67  
    1.68  subsubsection {* Propagating Black *} 
    1.69  
    1.70 -constdefs
    1.71 -  Mul_PBInv :: "mul_gar_coll_state \<Rightarrow> bool"
    1.72 +definition Mul_PBInv :: "mul_gar_coll_state \<Rightarrow> bool" where
    1.73    "Mul_PBInv \<equiv>  \<guillemotleft>\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
    1.74                   \<or> (\<forall>i<\<acute>ind. \<not>BtoW(\<acute>E!i,\<acute>M)) \<and> \<acute>l\<le>\<acute>Queue\<guillemotright>"
    1.75  
    1.76 -  Mul_Auxk :: "mul_gar_coll_state \<Rightarrow> bool"
    1.77 +definition Mul_Auxk :: "mul_gar_coll_state \<Rightarrow> bool" where
    1.78    "Mul_Auxk \<equiv> \<guillemotleft>\<acute>l<\<acute>Queue \<or> \<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or> \<acute>obc\<subset>Blacks \<acute>M\<guillemotright>"
    1.79  
    1.80 -constdefs
    1.81 -  Mul_Propagate_Black :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
    1.82 +definition Mul_Propagate_Black :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
    1.83    "Mul_Propagate_Black n \<equiv>
    1.84   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
    1.85    \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)}. 
    1.86 @@ -296,11 +290,10 @@
    1.87  
    1.88  subsubsection {* Counting Black Nodes *}
    1.89  
    1.90 -constdefs
    1.91 -  Mul_CountInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
    1.92 - "Mul_CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
    1.93 +definition Mul_CountInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
    1.94 +  "Mul_CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
    1.95  
    1.96 -  Mul_Count :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
    1.97 +definition Mul_Count :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
    1.98    "Mul_Count n \<equiv> 
    1.99    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
   1.100      \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
   1.101 @@ -396,11 +389,10 @@
   1.102    Append_to_free2: "i \<notin> Reach e 
   1.103             \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
   1.104  
   1.105 -constdefs
   1.106 -  Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool"
   1.107 +definition Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
   1.108    "Mul_AppendInv \<equiv> \<guillemotleft> \<lambda>ind. (\<forall>i. ind\<le>i \<longrightarrow> i<length \<acute>M \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black)\<guillemotright>"
   1.109  
   1.110 -  Mul_Append :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
   1.111 +definition Mul_Append :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   1.112    "Mul_Append n \<equiv> 
   1.113    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
   1.114    \<acute>ind:=0;;
   1.115 @@ -438,8 +430,7 @@
   1.116  
   1.117  subsubsection {* Collector *}
   1.118  
   1.119 -constdefs 
   1.120 -  Mul_Collector :: "nat \<Rightarrow>  mul_gar_coll_state ann_com"
   1.121 +definition Mul_Collector :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   1.122    "Mul_Collector n \<equiv>
   1.123  .{\<acute>Mul_Proper n}.  
   1.124  WHILE True INV .{\<acute>Mul_Proper n}.