src/HOL/Hoare_Parallel/Graph.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 42174 d0be2722ce9f child 54863 82acc20ded73 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 prensani@13020 ` 1` ```header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms} ``` prensani@13020 ` 2` prensani@13020 ` 3` ```\section {Formalization of the Memory} *} ``` prensani@13020 ` 4` haftmann@16417 ` 5` ```theory Graph imports Main begin ``` prensani@13020 ` 6` prensani@13020 ` 7` ```datatype node = Black | White ``` prensani@13020 ` 8` wenzelm@42174 ` 9` ```type_synonym nodes = "node list" ``` wenzelm@42174 ` 10` ```type_synonym edge = "nat \ nat" ``` wenzelm@42174 ` 11` ```type_synonym edges = "edge list" ``` prensani@13020 ` 12` prensani@13020 ` 13` ```consts Roots :: "nat set" ``` prensani@13020 ` 14` haftmann@35416 ` 15` ```definition Proper_Roots :: "nodes \ bool" where ``` prensani@13020 ` 16` ``` "Proper_Roots M \ Roots\{} \ Roots \ {i. i edges) \ bool" where ``` prensani@13020 ` 19` ``` "Proper_Edges \ (\(M,E). \i snd(E!i) nodes) \ bool" where ``` prensani@13020 ` 22` ``` "BtoW \ (\(e,M). (M!fst e)=Black \ (M!snd e)\Black)" ``` prensani@13020 ` 23` haftmann@35416 ` 24` ```definition Blacks :: "nodes \ nat set" where ``` prensani@13020 ` 25` ``` "Blacks M \ {i. i M!i=Black}" ``` prensani@13020 ` 26` haftmann@35416 ` 27` ```definition Reach :: "edges \ nat set" where ``` prensani@13020 ` 28` ``` "Reach E \ {x. (\path. 1 path!(length path - 1)\Roots \ x=path!0 ``` prensani@13020 ` 29` ``` \ (\ij x\Roots}" ``` prensani@13020 ` 31` prensani@13020 ` 32` ```text{* Reach: the set of reachable nodes is the set of Roots together with the ``` prensani@13020 ` 33` ```nodes reachable from some Root by a path represented by a list of ``` prensani@13020 ` 34` ``` nodes (at least two since we traverse at least one edge), where two ``` prensani@13020 ` 35` ```consecutive nodes correspond to an edge in E. *} ``` prensani@13020 ` 36` prensani@13020 ` 37` ```subsection {* Proofs about Graphs *} ``` prensani@13020 ` 38` prensani@13020 ` 39` ```lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def ``` prensani@13020 ` 40` ```declare Graph_defs [simp] ``` prensani@13020 ` 41` prensani@13022 ` 42` ```subsubsection{* Graph 1 *} ``` prensani@13020 ` 43` prensani@13020 ` 44` ```lemma Graph1_aux [rule_format]: ``` prensani@13020 ` 45` ``` "\ Roots\Blacks M; \iBtoW(E!i,M)\ ``` prensani@13020 ` 46` ``` \ 1< length path \ (path!(length path - 1))\Roots \ ``` prensani@13020 ` 47` ``` (\ij. j < length E \ E!j=(path!(Suc i), path!i))) ``` prensani@13020 ` 48` ``` \ M!(path!0) = Black" ``` prensani@13020 ` 49` ```apply(induct_tac "path") ``` prensani@13020 ` 50` ``` apply force ``` prensani@13020 ` 51` ```apply clarify ``` prensani@13020 ` 52` ```apply simp ``` prensani@13020 ` 53` ```apply(case_tac "list") ``` prensani@13020 ` 54` ``` apply force ``` prensani@13020 ` 55` ```apply simp ``` berghofe@13601 ` 56` ```apply(rotate_tac -2) ``` prensani@13020 ` 57` ```apply(erule_tac x = "0" in all_dupE) ``` prensani@13020 ` 58` ```apply simp ``` prensani@13020 ` 59` ```apply clarify ``` prensani@13020 ` 60` ```apply(erule allE , erule (1) notE impE) ``` prensani@13020 ` 61` ```apply simp ``` prensani@13020 ` 62` ```apply(erule mp) ``` prensani@13020 ` 63` ```apply(case_tac "lista") ``` prensani@13020 ` 64` ``` apply force ``` prensani@13020 ` 65` ```apply simp ``` prensani@13020 ` 66` ```apply(erule mp) ``` prensani@13020 ` 67` ```apply clarify ``` prensani@13020 ` 68` ```apply(erule_tac x = "Suc i" in allE) ``` prensani@13020 ` 69` ```apply force ``` prensani@13020 ` 70` ```done ``` prensani@13020 ` 71` prensani@13020 ` 72` ```lemma Graph1: ``` prensani@13020 ` 73` ``` "\Roots\Blacks M; Proper_Edges(M, E); \iBtoW(E!i,M) \ ``` prensani@13020 ` 74` ``` \ Reach E\Blacks M" ``` prensani@13020 ` 75` ```apply (unfold Reach_def) ``` prensani@13020 ` 76` ```apply simp ``` prensani@13020 ` 77` ```apply clarify ``` prensani@13020 ` 78` ```apply(erule disjE) ``` prensani@13020 ` 79` ``` apply clarify ``` prensani@13020 ` 80` ``` apply(rule conjI) ``` prensani@13020 ` 81` ``` apply(subgoal_tac "0< length path - Suc 0") ``` prensani@13020 ` 82` ``` apply(erule allE , erule (1) notE impE) ``` prensani@13020 ` 83` ``` apply force ``` prensani@13020 ` 84` ``` apply simp ``` prensani@13020 ` 85` ``` apply(rule Graph1_aux) ``` prensani@13020 ` 86` ```apply auto ``` prensani@13020 ` 87` ```done ``` prensani@13020 ` 88` prensani@13022 ` 89` ```subsubsection{* Graph 2 *} ``` prensani@13020 ` 90` prensani@13020 ` 91` ```lemma Ex_first_occurrence [rule_format]: ``` prensani@13020 ` 92` ``` "P (n::nat) \ (\m. P m \ (\i. i \ P i))"; ``` prensani@13020 ` 93` ```apply(rule nat_less_induct) ``` prensani@13020 ` 94` ```apply clarify ``` prensani@13020 ` 95` ```apply(case_tac "\m. m \ P m") ``` prensani@13020 ` 96` ```apply auto ``` prensani@13020 ` 97` ```done ``` prensani@13020 ` 98` prensani@13020 ` 99` ```lemma Compl_lemma: "(n::nat)\l \ (\m. m\l \ n=l - m)" ``` prensani@13020 ` 100` ```apply(rule_tac x = "l - n" in exI) ``` prensani@13020 ` 101` ```apply arith ``` prensani@13020 ` 102` ```done ``` prensani@13020 ` 103` prensani@13020 ` 104` ```lemma Ex_last_occurrence: ``` prensani@13020 ` 105` ``` "\P (n::nat); n\l\ \ (\m. P (l - m) \ (\i. i \P (l - i)))" ``` prensani@13020 ` 106` ```apply(drule Compl_lemma) ``` prensani@13020 ` 107` ```apply clarify ``` prensani@13020 ` 108` ```apply(erule Ex_first_occurrence) ``` prensani@13020 ` 109` ```done ``` prensani@13020 ` 110` prensani@13020 ` 111` ```lemma Graph2: ``` prensani@13020 ` 112` ``` "\T \ Reach E; R \ T \ Reach (E[R:=(fst(E!R), T)])" ``` prensani@13020 ` 113` ```apply (unfold Reach_def) ``` prensani@13020 ` 114` ```apply clarify ``` prensani@13020 ` 115` ```apply simp ``` prensani@13020 ` 116` ```apply(case_tac "\zpath!z") ``` prensani@13020 ` 117` ``` apply(rule_tac x = "path" in exI) ``` prensani@13020 ` 118` ``` apply simp ``` prensani@13020 ` 119` ``` apply clarify ``` prensani@13020 ` 120` ``` apply(erule allE , erule (1) notE impE) ``` prensani@13020 ` 121` ``` apply clarify ``` prensani@13020 ` 122` ``` apply(rule_tac x = "j" in exI) ``` prensani@13020 ` 123` ``` apply(case_tac "j=R") ``` prensani@13020 ` 124` ``` apply(erule_tac x = "Suc i" in allE) ``` prensani@13020 ` 125` ``` apply simp ``` prensani@13020 ` 126` ``` apply (force simp add:nth_list_update) ``` prensani@13020 ` 127` ```apply simp ``` prensani@13020 ` 128` ```apply(erule exE) ``` prensani@13020 ` 129` ```apply(subgoal_tac "z \ length path - Suc 0") ``` prensani@13020 ` 130` ``` prefer 2 apply arith ``` prensani@13020 ` 131` ```apply(drule_tac P = "\m. m fst(E!R)=path!m" in Ex_last_occurrence) ``` prensani@13020 ` 132` ``` apply assumption ``` prensani@13020 ` 133` ```apply clarify ``` prensani@13020 ` 134` ```apply simp ``` prensani@13020 ` 135` ```apply(rule_tac x = "(path!0)#(drop (length path - Suc m) path)" in exI) ``` prensani@13020 ` 136` ```apply simp ``` prensani@13020 ` 137` ```apply(case_tac "length path - (length path - Suc m)") ``` prensani@13020 ` 138` ``` apply arith ``` prensani@13020 ` 139` ```apply simp ``` prensani@13020 ` 140` ```apply(subgoal_tac "(length path - Suc m) + nat \ length path") ``` prensani@13020 ` 141` ``` prefer 2 apply arith ``` prensani@13020 ` 142` ```apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0") ``` prensani@13020 ` 143` ``` prefer 2 apply arith ``` prensani@13020 ` 144` ```apply clarify ``` prensani@13020 ` 145` ```apply(case_tac "i") ``` prensani@13020 ` 146` ``` apply(force simp add: nth_list_update) ``` prensani@13020 ` 147` ```apply simp ``` prensani@13020 ` 148` ```apply(subgoal_tac "(length path - Suc m) + nata \ length path") ``` prensani@13020 ` 149` ``` prefer 2 apply arith ``` prensani@13020 ` 150` ```apply(subgoal_tac "(length path - Suc m) + (Suc nata) \ length path") ``` prensani@13020 ` 151` ``` prefer 2 apply arith ``` prensani@13020 ` 152` ```apply simp ``` prensani@13020 ` 153` ```apply(erule_tac x = "length path - Suc m + nata" in allE) ``` prensani@13020 ` 154` ```apply simp ``` prensani@13020 ` 155` ```apply clarify ``` prensani@13020 ` 156` ```apply(rule_tac x = "j" in exI) ``` prensani@13020 ` 157` ```apply(case_tac "R=j") ``` prensani@13020 ` 158` ``` prefer 2 apply force ``` prensani@13020 ` 159` ```apply simp ``` prensani@13020 ` 160` ```apply(drule_tac t = "path ! (length path - Suc m)" in sym) ``` prensani@13020 ` 161` ```apply simp ``` prensani@13020 ` 162` ```apply(case_tac " length path - Suc 0 < m") ``` prensani@13020 ` 163` ``` apply(subgoal_tac "(length path - Suc m)=0") ``` prensani@13020 ` 164` ``` prefer 2 apply arith ``` prensani@13020 ` 165` ``` apply(simp del: diff_is_0_eq) ``` prensani@13020 ` 166` ``` apply(subgoal_tac "Suc nata\nat") ``` prensani@13020 ` 167` ``` prefer 2 apply arith ``` prensani@13020 ` 168` ``` apply(drule_tac n = "Suc nata" in Compl_lemma) ``` prensani@13020 ` 169` ``` apply clarify ``` haftmann@31082 ` 170` ``` using [[linarith_split_limit = 0]] ``` prensani@13020 ` 171` ``` apply force ``` haftmann@31082 ` 172` ``` using [[linarith_split_limit = 9]] ``` prensani@13020 ` 173` ```apply(drule leI) ``` prensani@13020 ` 174` ```apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)") ``` prensani@13020 ` 175` ``` apply(erule_tac x = "m - (Suc nata)" in allE) ``` prensani@13020 ` 176` ``` apply(case_tac "m") ``` prensani@13020 ` 177` ``` apply simp ``` prensani@13020 ` 178` ``` apply simp ``` berghofe@13601 ` 179` ```apply simp ``` prensani@13020 ` 180` ```done ``` prensani@13020 ` 181` webertj@20432 ` 182` prensani@13022 ` 183` ```subsubsection{* Graph 3 *} ``` prensani@13020 ` 184` haftmann@32642 ` 185` ```declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp] ``` haftmann@32642 ` 186` prensani@13020 ` 187` ```lemma Graph3: ``` prensani@13020 ` 188` ``` "\ T\Reach E; R \ Reach(E[R:=(fst(E!R),T)]) \ Reach E" ``` prensani@13020 ` 189` ```apply (unfold Reach_def) ``` prensani@13020 ` 190` ```apply clarify ``` prensani@13020 ` 191` ```apply simp ``` prensani@13020 ` 192` ```apply(case_tac "\i(length path\m)") ``` prensani@13020 ` 202` ``` prefer 2 apply arith ``` nipkow@32442 ` 203` ``` apply(simp) ``` prensani@13020 ` 204` ``` apply(rule conjI) ``` prensani@13020 ` 205` ``` apply(subgoal_tac "\(m + length patha - 1 < m)") ``` prensani@13020 ` 206` ``` prefer 2 apply arith ``` nipkow@32442 ` 207` ``` apply(simp add: nth_append) ``` prensani@13020 ` 208` ``` apply(rule conjI) ``` prensani@13020 ` 209` ``` apply(case_tac "m") ``` prensani@13020 ` 210` ``` apply force ``` prensani@13020 ` 211` ``` apply(case_tac "path") ``` prensani@13020 ` 212` ``` apply force ``` prensani@13020 ` 213` ``` apply force ``` prensani@13020 ` 214` ``` apply clarify ``` prensani@13020 ` 215` ``` apply(case_tac "Suc i\m") ``` prensani@13020 ` 216` ``` apply(erule_tac x = "i" in allE) ``` prensani@13020 ` 217` ``` apply simp ``` prensani@13020 ` 218` ``` apply clarify ``` prensani@13020 ` 219` ``` apply(rule_tac x = "j" in exI) ``` prensani@13020 ` 220` ``` apply(case_tac "Suc i(length path\Suc m)" ) ``` prensani@13020 ` 247` ``` prefer 2 apply arith ``` nipkow@32442 ` 248` ``` apply clarsimp ``` prensani@13020 ` 249` ``` apply(erule_tac x = "i" in allE) ``` prensani@13020 ` 250` ``` apply simp ``` prensani@13020 ` 251` ``` apply clarify ``` prensani@13020 ` 252` ``` apply(case_tac "R=j") ``` prensani@13020 ` 253` ``` apply(force simp add: nth_list_update) ``` prensani@13020 ` 254` ``` apply(force simp add: nth_list_update) ``` prensani@13020 ` 255` ```--{* the changed edge is not part of the path *} ``` prensani@13020 ` 256` ```apply(rule_tac x = "path" in exI) ``` prensani@13020 ` 257` ```apply simp ``` prensani@13020 ` 258` ```apply clarify ``` prensani@13020 ` 259` ```apply(erule_tac x = "i" in allE) ``` prensani@13020 ` 260` ```apply clarify ``` prensani@13020 ` 261` ```apply(case_tac "R=j") ``` prensani@13020 ` 262` ``` apply(erule_tac x = "i" in allE) ``` prensani@13020 ` 263` ``` apply simp ``` prensani@13020 ` 264` ```apply(force simp add: nth_list_update) ``` prensani@13020 ` 265` ```done ``` prensani@13020 ` 266` prensani@13022 ` 267` ```subsubsection{* Graph 4 *} ``` prensani@13020 ` 268` prensani@13020 ` 269` ```lemma Graph4: ``` prensani@13020 ` 270` ``` "\T \ Reach E; Roots\Blacks M; I\length E; TiBtoW(E!i,M); RBlack\ \ ``` prensani@13020 ` 272` ``` (\r. I\r \ r BtoW(E[R:=(fst(E!R),T)]!r,M))" ``` prensani@13020 ` 273` ```apply (unfold Reach_def) ``` prensani@13020 ` 274` ```apply simp ``` prensani@13020 ` 275` ```apply(erule disjE) ``` prensani@13020 ` 276` ``` prefer 2 apply force ``` prensani@13020 ` 277` ```apply clarify ``` prensani@13020 ` 278` ```--{* there exist a black node in the path to T *} ``` prensani@13020 ` 279` ```apply(case_tac "\m T \ Reach E ; Roots \ Blacks M; \iBtoW(E!i,M); T Black\ ``` prensani@13020 ` 314` ``` \ (\r. R r BtoW(E[R:=(fst(E!R),T)]!r,M))" ``` prensani@13020 ` 315` ```apply (unfold Reach_def) ``` prensani@13020 ` 316` ```apply simp ``` prensani@13020 ` 317` ```apply(erule disjE) ``` prensani@13020 ` 318` ``` prefer 2 apply force ``` prensani@13020 ` 319` ```apply clarify ``` prensani@13020 ` 320` ```--{* there exist a black node in the path to T*} ``` prensani@13020 ` 321` ```apply(case_tac "\mR") ``` wenzelm@26316 ` 337` ``` apply(drule le_imp_less_or_eq [of _ R]) ``` prensani@13020 ` 338` ``` apply(erule disjE) ``` prensani@13020 ` 339` ``` apply(erule allE , erule (1) notE impE) ``` prensani@13020 ` 340` ``` apply force ``` prensani@13020 ` 341` ``` apply force ``` prensani@13020 ` 342` ``` apply(rule_tac x = "j" in exI) ``` prensani@13020 ` 343` ``` apply(force simp add: nth_list_update) ``` prensani@13020 ` 344` ```apply simp ``` prensani@13020 ` 345` ```apply(rotate_tac -1) ``` prensani@13020 ` 346` ```apply(erule_tac x = "length path - 1" in allE) ``` prensani@13020 ` 347` ```apply(case_tac "length path") ``` prensani@13020 ` 348` ``` apply force ``` prensani@13020 ` 349` ```apply force ``` prensani@13020 ` 350` ```done ``` prensani@13020 ` 351` prensani@13022 ` 352` ```subsubsection {* Other lemmas about graphs *} ``` prensani@13020 ` 353` prensani@13020 ` 354` ```lemma Graph6: ``` prensani@13020 ` 355` ``` "\Proper_Edges(M,E); R \ Proper_Edges(M,E[R:=(fst(E!R),T)])" ``` prensani@13020 ` 356` ```apply (unfold Proper_Edges_def) ``` prensani@13020 ` 357` ``` apply(force simp add: nth_list_update) ``` prensani@13020 ` 358` ```done ``` prensani@13020 ` 359` prensani@13020 ` 360` ```lemma Graph7: ``` prensani@13020 ` 361` ``` "\Proper_Edges(M,E)\ \ Proper_Edges(M[T:=a],E)" ``` prensani@13020 ` 362` ```apply (unfold Proper_Edges_def) ``` prensani@13020 ` 363` ```apply force ``` prensani@13020 ` 364` ```done ``` prensani@13020 ` 365` prensani@13020 ` 366` ```lemma Graph8: ``` prensani@13020 ` 367` ``` "\Proper_Roots(M)\ \ Proper_Roots(M[T:=a])" ``` prensani@13020 ` 368` ```apply (unfold Proper_Roots_def) ``` prensani@13020 ` 369` ```apply force ``` prensani@13020 ` 370` ```done ``` prensani@13020 ` 371` prensani@13020 ` 372` ```text{* Some specific lemmata for the verification of garbage collection algorithms. *} ``` prensani@13020 ` 373` prensani@13020 ` 374` ```lemma Graph9: "j Blacks M\Blacks (M[j := Black])" ``` prensani@13020 ` 375` ```apply (unfold Blacks_def) ``` prensani@13020 ` 376` ``` apply(force simp add: nth_list_update) ``` prensani@13020 ` 377` ```done ``` prensani@13020 ` 378` prensani@13020 ` 379` ```lemma Graph10 [rule_format (no_asm)]: "\i. M!i=a \M[i:=a]=M" ``` prensani@13020 ` 380` ```apply(induct_tac "M") ``` prensani@13020 ` 381` ```apply auto ``` prensani@13020 ` 382` ```apply(case_tac "i") ``` prensani@13020 ` 383` ```apply auto ``` prensani@13020 ` 384` ```done ``` prensani@13020 ` 385` prensani@13020 ` 386` ```lemma Graph11 [rule_format (no_asm)]: ``` prensani@13020 ` 387` ``` "\ M!j\Black;j \ Blacks M \ Blacks (M[j := Black])" ``` prensani@13020 ` 388` ```apply (unfold Blacks_def) ``` prensani@13020 ` 389` ```apply(rule psubsetI) ``` prensani@13020 ` 390` ``` apply(force simp add: nth_list_update) ``` prensani@13020 ` 391` ```apply safe ``` prensani@13020 ` 392` ```apply(erule_tac c = "j" in equalityCE) ``` prensani@13020 ` 393` ```apply auto ``` prensani@13020 ` 394` ```done ``` prensani@13020 ` 395` prensani@13020 ` 396` ```lemma Graph12: "\a\Blacks M;j \ a\Blacks (M[j := Black])" ``` prensani@13020 ` 397` ```apply (unfold Blacks_def) ``` prensani@13020 ` 398` ```apply(force simp add: nth_list_update) ``` prensani@13020 ` 399` ```done ``` prensani@13020 ` 400` prensani@13020 ` 401` ```lemma Graph13: "\a\ Blacks M;j \ a \ Blacks (M[j := Black])" ``` prensani@13020 ` 402` ```apply (unfold Blacks_def) ``` prensani@13020 ` 403` ```apply(erule psubset_subset_trans) ``` prensani@13020 ` 404` ```apply(force simp add: nth_list_update) ``` prensani@13020 ` 405` ```done ``` prensani@13020 ` 406` prensani@13020 ` 407` ```declare Graph_defs [simp del] ``` prensani@13020 ` 408` prensani@13020 ` 409` ```end ```