src/HOL/HoareParallel/Graph.thy
author wenzelm
Wed, 01 Aug 2007 16:55:37 +0200
changeset 24110 4ab3084e311c
parent 24078 04b28c723d43
child 24742 73b8b42a36b6
permissions -rw-r--r--
tuned config options: eliminated separate attribute "option";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     3
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     4
\section {Formalization of the Memory} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     5
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13601
diff changeset
     6
theory Graph imports Main begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     7
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     8
datatype node = Black | White
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     9
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    10
types 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
  nodes = "node list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
  edge  = "nat \<times> nat"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
  edges = "edge list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    15
consts Roots :: "nat set"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
constdefs
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
  Proper_Roots :: "nodes \<Rightarrow> bool"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
  "Proper_Roots M \<equiv> Roots\<noteq>{} \<and> Roots \<subseteq> {i. i<length M}"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    21
  Proper_Edges :: "(nodes \<times> edges) \<Rightarrow> bool"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
  "Proper_Edges \<equiv> (\<lambda>(M,E). \<forall>i<length E. fst(E!i)<length M \<and> snd(E!i)<length M)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    23
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    24
  BtoW :: "(edge \<times> nodes) \<Rightarrow> bool"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    25
  "BtoW \<equiv> (\<lambda>(e,M). (M!fst e)=Black \<and> (M!snd e)\<noteq>Black)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    26
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    27
  Blacks :: "nodes \<Rightarrow> nat set"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    28
  "Blacks M \<equiv> {i. i<length M \<and> M!i=Black}"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    29
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    30
  Reach :: "edges \<Rightarrow> nat set"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    31
  "Reach E \<equiv> {x. (\<exists>path. 1<length path \<and> path!(length path - 1)\<in>Roots \<and> x=path!0
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    32
              \<and> (\<forall>i<length path - 1. (\<exists>j<length E. E!j=(path!(i+1), path!i))))
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    33
	      \<or> x\<in>Roots}"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    34
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
text{* Reach: the set of reachable nodes is the set of Roots together with the
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    36
nodes reachable from some Root by a path represented by a list of
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    37
  nodes (at least two since we traverse at least one edge), where two
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    38
consecutive nodes correspond to an edge in E. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    39
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    40
subsection {* Proofs about Graphs *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    41
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    42
lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    43
declare Graph_defs [simp]
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    44
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
    45
subsubsection{* Graph 1 *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    46
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    47
lemma Graph1_aux [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    48
  "\<lbrakk> Roots\<subseteq>Blacks M; \<forall>i<length E. \<not>BtoW(E!i,M)\<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    49
  \<Longrightarrow> 1< length path \<longrightarrow> (path!(length path - 1))\<in>Roots \<longrightarrow>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    50
  (\<forall>i<length path - 1. (\<exists>j. j < length E \<and> E!j=(path!(Suc i), path!i))) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    51
  \<longrightarrow> M!(path!0) = Black"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    52
apply(induct_tac "path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    53
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    54
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    55
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    56
apply(case_tac "list")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    57
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    58
apply simp
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13022
diff changeset
    59
apply(rotate_tac -2)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    60
apply(erule_tac x = "0" in all_dupE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    61
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    62
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    63
apply(erule allE , erule (1) notE impE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    64
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    65
apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    66
apply(case_tac "lista")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    67
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    68
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    69
apply(erule mp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    70
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    71
apply(erule_tac x = "Suc i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    72
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    73
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    74
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    75
lemma Graph1: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    76
  "\<lbrakk>Roots\<subseteq>Blacks M; Proper_Edges(M, E); \<forall>i<length E. \<not>BtoW(E!i,M) \<rbrakk> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    77
  \<Longrightarrow> Reach E\<subseteq>Blacks M"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    78
apply (unfold Reach_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    79
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    80
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    81
apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    82
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    83
 apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    84
  apply(subgoal_tac "0< length path - Suc 0")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    85
   apply(erule allE , erule (1) notE impE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    86
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    87
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    88
 apply(rule Graph1_aux)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    89
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    90
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    91
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
    92
subsubsection{* Graph 2 *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    93
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    94
lemma Ex_first_occurrence [rule_format]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    95
  "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))";
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    96
apply(rule nat_less_induct)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    97
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    98
apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    99
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   100
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   101
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   102
lemma Compl_lemma: "(n::nat)\<le>l \<Longrightarrow> (\<exists>m. m\<le>l \<and> n=l - m)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   103
apply(rule_tac x = "l - n" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   104
apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   105
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   106
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   107
lemma Ex_last_occurrence: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   108
  "\<lbrakk>P (n::nat); n\<le>l\<rbrakk> \<Longrightarrow> (\<exists>m. P (l - m) \<and> (\<forall>i. i<m \<longrightarrow> \<not>P (l - i)))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   109
apply(drule Compl_lemma)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   110
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   111
apply(erule Ex_first_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   112
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   113
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   114
lemma Graph2: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   115
  "\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   116
apply (unfold Reach_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   117
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   118
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   119
apply(case_tac "\<forall>z<length path. fst(E!R)\<noteq>path!z")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   120
 apply(rule_tac x = "path" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   121
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   122
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   123
 apply(erule allE , erule (1) notE impE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   124
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   125
 apply(rule_tac x = "j" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   126
 apply(case_tac "j=R")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   127
  apply(erule_tac x = "Suc i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   128
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   129
 apply (force simp add:nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   130
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   131
apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   132
apply(subgoal_tac "z \<le> length path - Suc 0")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   133
 prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   134
apply(drule_tac P = "\<lambda>m. m<length path \<and> fst(E!R)=path!m" in Ex_last_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   135
 apply assumption
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   136
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   137
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   138
apply(rule_tac x = "(path!0)#(drop (length path - Suc m) path)" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   139
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   140
apply(case_tac "length path - (length path - Suc m)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   141
 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   142
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   143
apply(subgoal_tac "(length path - Suc m) + nat \<le> length path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   144
 prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   145
apply(drule nth_drop)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   146
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   147
apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   148
 prefer 2 apply arith 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   149
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   150
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   151
apply(case_tac "i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   152
 apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   153
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   154
apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   155
 prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   156
apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   157
 prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   158
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   159
apply(erule_tac x = "length path - Suc m + nata" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   160
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   161
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   162
apply(rule_tac x = "j" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   163
apply(case_tac "R=j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   164
 prefer 2 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   165
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   166
apply(drule_tac t = "path ! (length path - Suc m)" in sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   167
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   168
apply(case_tac " length path - Suc 0 < m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   169
 apply(subgoal_tac "(length path - Suc m)=0")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   170
  prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   171
 apply(simp del: diff_is_0_eq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   172
 apply(subgoal_tac "Suc nata\<le>nat")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   173
 prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   174
 apply(drule_tac n = "Suc nata" in Compl_lemma)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   175
 apply clarify
24110
4ab3084e311c tuned config options: eliminated separate attribute "option";
wenzelm
parents: 24078
diff changeset
   176
 using [[fast_arith_split_limit = 0]]
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   177
 apply force
24110
4ab3084e311c tuned config options: eliminated separate attribute "option";
wenzelm
parents: 24078
diff changeset
   178
 using [[fast_arith_split_limit = 9]]
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   179
apply(drule leI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   180
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   181
 apply(erule_tac x = "m - (Suc nata)" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   182
 apply(case_tac "m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   183
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   184
 apply simp
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13022
diff changeset
   185
apply simp
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   186
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   187
20432
07ec57376051 lin_arith_prover: splitting reverted because of performance loss
webertj
parents: 20279
diff changeset
   188
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
   189
subsubsection{* Graph 3 *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   190
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   191
lemma Graph3: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   192
  "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   193
apply (unfold Reach_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   194
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   195
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   196
apply(case_tac "\<exists>i<length path - 1. (fst(E!R),T)=(path!(Suc i),path!i)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   197
--{* the changed edge is part of the path *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   198
 apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   199
 apply(drule_tac P = "\<lambda>i. i<length path - 1 \<and> (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   200
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   201
 apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   202
--{* T is NOT a root *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   203
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   204
  apply(rule_tac x = "(take m path)@patha" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   205
  apply(subgoal_tac "\<not>(length path\<le>m)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   206
   prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   207
  apply(simp add: min_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   208
  apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   209
   apply(subgoal_tac "\<not>(m + length patha - 1 < m)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   210
    prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   211
   apply(simp add: nth_append min_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   212
  apply(rule conjI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   213
   apply(case_tac "m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   214
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   215
   apply(case_tac "path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   216
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   217
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   218
  apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   219
  apply(case_tac "Suc i\<le>m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   220
   apply(erule_tac x = "i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   221
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   222
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   223
   apply(rule_tac x = "j" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   224
   apply(case_tac "Suc i<m")
22230
bdec4a82f385 a few additions and deletions
nipkow
parents: 20432
diff changeset
   225
    apply(simp add: nth_append)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   226
    apply(case_tac "R=j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   227
     apply(simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   228
     apply(case_tac "i=m")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   229
      apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   230
     apply(erule_tac x = "i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   231
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   232
    apply(force simp add: nth_list_update)
22230
bdec4a82f385 a few additions and deletions
nipkow
parents: 20432
diff changeset
   233
   apply(simp add: nth_append)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   234
   apply(subgoal_tac "i=m - 1")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   235
    prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   236
   apply(case_tac "R=j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   237
    apply(erule_tac x = "m - 1" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   238
    apply(simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   239
   apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   240
  apply(simp add: nth_append min_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   241
  apply(rotate_tac -4)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   242
  apply(erule_tac x = "i - m" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   243
  apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   244
    prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   245
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   246
--{* T is a root *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   247
 apply(case_tac "m=0")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   248
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   249
 apply(rule_tac x = "take (Suc m) path" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   250
 apply(subgoal_tac "\<not>(length path\<le>Suc m)" )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   251
  prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   252
 apply(simp add: min_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   253
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   254
 apply(erule_tac x = "i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   255
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   256
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   257
 apply(case_tac "R=j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   258
  apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   259
 apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   260
--{* the changed edge is not part of the path *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   261
apply(rule_tac x = "path" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   262
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   263
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   264
apply(erule_tac x = "i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   265
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   266
apply(case_tac "R=j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   267
 apply(erule_tac x = "i" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   268
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   269
apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   270
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   271
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
   272
subsubsection{* Graph 4 *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   273
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   274
lemma Graph4: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   275
  "\<lbrakk>T \<in> Reach E; Roots\<subseteq>Blacks M; I\<le>length E; T<length M; R<length E; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   276
  \<forall>i<I. \<not>BtoW(E!i,M); R<I; M!fst(E!R)=Black; M!T\<noteq>Black\<rbrakk> \<Longrightarrow> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   277
  (\<exists>r. I\<le>r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   278
apply (unfold Reach_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   279
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   280
apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   281
 prefer 2 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   282
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   283
--{* there exist a black node in the path to T *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   284
apply(case_tac "\<exists>m<length path. M!(path!m)=Black")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   285
 apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   286
 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   287
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   288
 apply(case_tac "ma")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   289
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   290
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   291
 apply(case_tac "length path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   292
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   293
 apply simp
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13022
diff changeset
   294
 apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   295
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   296
 apply clarify
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13022
diff changeset
   297
 apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   298
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   299
 apply(case_tac "j<I")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   300
  apply(erule_tac x = "j" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   301
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   302
 apply(rule_tac x = "j" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   303
 apply(force  simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   304
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   305
apply(rotate_tac -1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   306
apply(erule_tac x = "length path - 1" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   307
apply(case_tac "length path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   308
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   309
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   310
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   311
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
   312
subsubsection {* Graph 5 *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   313
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   314
lemma Graph5: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   315
  "\<lbrakk> T \<in> Reach E ; Roots \<subseteq> Blacks M; \<forall>i<R. \<not>BtoW(E!i,M); T<length M; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   316
    R<length E; M!fst(E!R)=Black; M!snd(E!R)=Black; M!T \<noteq> Black\<rbrakk> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   317
   \<Longrightarrow> (\<exists>r. R<r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   318
apply (unfold Reach_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   319
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   320
apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   321
 prefer 2 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   322
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   323
--{* there exist a black node in the path to T*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   324
apply(case_tac "\<exists>m<length path. M!(path!m)=Black")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   325
 apply(erule exE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   326
 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   327
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   328
 apply(case_tac "ma")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   329
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   330
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   331
 apply(case_tac "length path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   332
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   333
 apply simp
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13022
diff changeset
   334
 apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   335
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   336
 apply clarify
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13022
diff changeset
   337
 apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   338
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   339
 apply(case_tac "j\<le>R")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   340
  apply(drule le_imp_less_or_eq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   341
  apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   342
   apply(erule allE , erule (1) notE impE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   343
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   344
  apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   345
 apply(rule_tac x = "j" in exI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   346
 apply(force  simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   347
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   348
apply(rotate_tac -1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   349
apply(erule_tac x = "length path - 1" in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   350
apply(case_tac "length path")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   351
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   352
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   353
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   354
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
   355
subsubsection {* Other lemmas about graphs *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   356
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   357
lemma Graph6: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   358
 "\<lbrakk>Proper_Edges(M,E); R<length E ; T<length M\<rbrakk> \<Longrightarrow> Proper_Edges(M,E[R:=(fst(E!R),T)])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   359
apply (unfold Proper_Edges_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   360
 apply(force  simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   361
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   362
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   363
lemma Graph7: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   364
 "\<lbrakk>Proper_Edges(M,E)\<rbrakk> \<Longrightarrow> Proper_Edges(M[T:=a],E)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   365
apply (unfold Proper_Edges_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   366
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   367
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   368
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   369
lemma Graph8: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   370
 "\<lbrakk>Proper_Roots(M)\<rbrakk> \<Longrightarrow> Proper_Roots(M[T:=a])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   371
apply (unfold Proper_Roots_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   372
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   373
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   374
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   375
text{* Some specific lemmata for the verification of garbage collection algorithms. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   376
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   377
lemma Graph9: "j<length M \<Longrightarrow> Blacks M\<subseteq>Blacks (M[j := Black])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   378
apply (unfold Blacks_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   379
 apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   380
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   381
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   382
lemma Graph10 [rule_format (no_asm)]: "\<forall>i. M!i=a \<longrightarrow>M[i:=a]=M"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   383
apply(induct_tac "M")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   384
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   385
apply(case_tac "i")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   386
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   387
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   388
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   389
lemma Graph11 [rule_format (no_asm)]: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   390
  "\<lbrakk> M!j\<noteq>Black;j<length M\<rbrakk> \<Longrightarrow> Blacks M \<subset> Blacks (M[j := Black])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   391
apply (unfold Blacks_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   392
apply(rule psubsetI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   393
 apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   394
apply safe
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   395
apply(erule_tac c = "j" in equalityCE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   396
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   397
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   398
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   399
lemma Graph12: "\<lbrakk>a\<subseteq>Blacks M;j<length M\<rbrakk> \<Longrightarrow> a\<subseteq>Blacks (M[j := Black])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   400
apply (unfold Blacks_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   401
apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   402
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   403
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   404
lemma Graph13: "\<lbrakk>a\<subset> Blacks M;j<length M\<rbrakk> \<Longrightarrow> a \<subset> Blacks (M[j := Black])"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   405
apply (unfold Blacks_def)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   406
apply(erule psubset_subset_trans)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   407
apply(force simp add: nth_list_update)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   408
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   409
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   410
declare Graph_defs [simp del]
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   411
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   412
end