src/HOL/Hoare/SchorrWaite.thy
author wenzelm
Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898 89da4dcd1fa8
parent 81190 60fedd5b7c58
permissions -rw-r--r--
clarified colors, following d6a14ed060fb;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
     1
(*  Title:      HOL/Hoare/SchorrWaite.thy
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
     2
    Author:     Farhad Mehta
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
     3
    Copyright   2003 TUM
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
     4
*)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
     5
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 72806
diff changeset
     6
section \<open>Proof of the Schorr-Waite graph marking algorithm\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
     7
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 72806
diff changeset
     8
theory SchorrWaite
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 72806
diff changeset
     9
  imports HeapSyntax
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 72806
diff changeset
    10
begin
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    11
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 72806
diff changeset
    12
subsection \<open>Machinery for the Schorr-Waite proof\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    13
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    14
definition
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 67410
diff changeset
    15
  \<comment> \<open>Relations induced by a mapping\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    16
  rel :: "('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    17
  where "rel m = {(x,y). m x = Ref y}"
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    18
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    19
definition
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    20
  relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 44890
diff changeset
    21
  where "relS M = (\<Union>m \<in> M. rel m)"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    22
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    23
definition
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    24
  addrs :: "'a ref set \<Rightarrow> 'a set"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    25
  where "addrs P = {a. Ref a \<in> P}"
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    26
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    27
definition
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    28
  reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> 'a set"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    29
  where "reachable r P = (r\<^sup>* `` addrs P)"
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    30
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    31
lemmas rel_defs = relS_def rel_def
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    32
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
    33
text \<open>Rewrite rules for relations induced by a mapping\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    34
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    35
lemma self_reachable: "b \<in> B \<Longrightarrow> b \<in> R\<^sup>* `` B"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    36
apply blast
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    37
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    38
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    39
lemma oneStep_reachable: "b \<in> R``B \<Longrightarrow> b \<in> R\<^sup>* `` B"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    40
apply blast
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    41
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    42
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    43
lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
42154
478bdcea240a tuned proofs;
wenzelm
parents: 39302
diff changeset
    44
apply (clarsimp simp only:Image_iff)
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    45
apply (erule rtrancl_induct)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    46
 apply blast
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    47
apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    48
 apply (erule UnE)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    49
 apply (auto intro:rtrancl_into_rtrancl)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    50
apply blast
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    51
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    52
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    53
lemma still_reachable_eq: "\<lbrakk> A\<subseteq>Rb\<^sup>*``B; B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Ra-Rb. y \<in>(Rb\<^sup>*``B); \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Ra\<^sup>*``A =  Rb\<^sup>*``B "
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    54
apply (rule equalityI)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    55
 apply (erule still_reachable ,assumption)+
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    56
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    57
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    58
lemma reachable_null: "reachable mS {Null} = {}"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    59
apply (simp add: reachable_def addrs_def)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    60
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    61
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    62
lemma reachable_empty: "reachable mS {} = {}"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    63
apply (simp add: reachable_def addrs_def)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    64
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    65
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    66
lemma reachable_union: "(reachable mS aS \<union> reachable mS bS) = reachable mS (aS \<union> bS)"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    67
apply (simp add: reachable_def rel_defs addrs_def)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    68
apply blast
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    69
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    70
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    71
lemma reachable_union_sym: "reachable r (insert a aS) = (r\<^sup>* `` addrs {a}) \<union> reachable r aS"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    72
apply (simp add: reachable_def rel_defs addrs_def)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    73
apply blast
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    74
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    75
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    76
lemma rel_upd1: "(a,b) \<notin> rel (r(q:=t)) \<Longrightarrow> (a,b) \<in> rel r \<Longrightarrow> a=q"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    77
apply (rule classical)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    78
apply (simp add:rel_defs fun_upd_apply)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    79
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    80
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    81
lemma rel_upd2: "(a,b)  \<notin> rel r \<Longrightarrow> (a,b) \<in> rel (r(q:=t)) \<Longrightarrow> a=q"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    82
apply (rule classical)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    83
apply (simp add:rel_defs fun_upd_apply)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    84
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    85
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    86
definition
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 67410
diff changeset
    87
  \<comment> \<open>Restriction of a relation\<close>
81189
47a0dfee26ea more inner-syntax markup;
wenzelm
parents: 80914
diff changeset
    88
  restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set"
47a0dfee26ea more inner-syntax markup;
wenzelm
parents: 80914
diff changeset
    89
    (\<open>(\<open>notation=\<open>mixfix relation restriction\<close>\<close>_/ | _)\<close> [50, 51] 50)
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    90
  where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}"
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    91
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
    92
text \<open>Rewrite rules for the restriction of a relation\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    93
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    94
lemma restr_identity[simp]:
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    95
 " (\<forall>x. \<not> m x) \<Longrightarrow> (R |m) = R"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    96
by (auto simp add:restr_def)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    97
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    98
lemma restr_rtrancl[simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (R | m)\<^sup>* `` {l} = {l}"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
    99
by (auto simp add:restr_def elim:converse_rtranclE)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   100
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   101
lemma [simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (l,x) \<in> (R | m)\<^sup>* = (l=x)"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   102
by (auto simp add:restr_def elim:converse_rtranclE)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   103
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   104
lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   105
apply (auto simp:restr_def rel_def fun_upd_apply)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   106
apply (rename_tac a b)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   107
apply (case_tac "a=q")
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   108
 apply auto
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   109
done
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   110
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   111
lemma restr_un: "((r \<union> s)|m) = (r|m) \<union> (s|m)"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   112
  by (auto simp add:restr_def)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   113
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   114
lemma rel_upd3: "(a, b) \<notin> (r|(m(q := t))) \<Longrightarrow> (a,b) \<in> (r|m) \<Longrightarrow> a = q "
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   115
apply (rule classical)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   116
apply (simp add:restr_def fun_upd_apply)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   117
done
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   118
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
   119
definition
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 67410
diff changeset
   120
  \<comment> \<open>A short form for the stack mapping function for List\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   121
  S :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
   122
  where "S c l r = (\<lambda>x. if c x then r x else l x)"
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   123
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
   124
text \<open>Rewrite rules for Lists using S as their mapping\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   125
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   126
lemma [rule_format,simp]:
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   127
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   128
apply(induct_tac stack)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   129
 apply(simp add:fun_upd_apply S_def)+
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   130
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   131
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   132
lemma [rule_format,simp]:
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   133
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   134
apply(induct_tac stack)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   135
 apply(simp add:fun_upd_apply S_def)+
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   136
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   137
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   138
lemma [rule_format,simp]:
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   139
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   140
apply(induct_tac stack)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   141
 apply(simp add:fun_upd_apply S_def)+
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   142
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   143
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   144
lemma [rule_format,simp]:
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   145
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   146
apply(induct_tac stack)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   147
 apply(simp add:fun_upd_apply S_def)+
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   148
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   149
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 36866
diff changeset
   150
primrec
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 67410
diff changeset
   151
  \<comment> \<open>Recursive definition of what is means for a the graph/stack structure to be reconstructible\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   152
  stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow>  bool"
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 36866
diff changeset
   153
where
d98baa2cf589 modernized specifications;
wenzelm
parents: 36866
diff changeset
   154
  stkOk_nil:  "stkOk c l r iL iR t [] = True"
d98baa2cf589 modernized specifications;
wenzelm
parents: 36866
diff changeset
   155
| stkOk_cons:
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   156
    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and>
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 36866
diff changeset
   157
      iL p = (if c p then l p else t) \<and>
d98baa2cf589 modernized specifications;
wenzelm
parents: 36866
diff changeset
   158
      iR p = (if c p then t else r p))"
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   159
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
   160
text \<open>Rewrite rules for stkOk\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   161
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   162
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   163
  stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   164
apply (induct xs)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   165
 apply (auto simp:eq_sym_conv)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   166
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   167
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   168
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   169
 stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   170
apply (induct xs)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   171
 apply (auto simp:eq_sym_conv)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   172
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   173
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   174
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   175
 stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   176
apply (induct xs)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   177
 apply (auto simp:eq_sym_conv)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   178
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   179
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   180
lemma stkOk_r_rewrite [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   181
  stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   182
apply (induct xs)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   183
 apply (auto simp:eq_sym_conv)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   184
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   185
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   186
lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   187
 stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   188
apply (induct xs)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   189
 apply (auto simp:eq_sym_conv)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   190
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   191
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   192
lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   193
 stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   194
apply (induct xs)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   195
 apply (auto simp:eq_sym_conv)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   196
done
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   197
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   198
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 72806
diff changeset
   199
subsection \<open>The Schorr-Waite algorithm\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   200
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   201
theorem SchorrWaiteAlgorithm:
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   202
"VARS c m l r t p q root
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   203
 {R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l}
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   204
 t := root; p := Null;
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   205
 WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   206
 INV {\<exists>stack.
67410
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   207
          List (S c l r) p stack \<and>                                      \<comment> \<open>\<open>i1\<close>\<close>
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   208
          (\<forall>x \<in> set stack. m x) \<and>                                       \<comment> \<open>\<open>i2\<close>\<close>
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   209
          R = reachable (relS{l, r}) {t,p} \<and>                            \<comment> \<open>\<open>i3\<close>\<close>
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   210
          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                         \<comment> \<open>\<open>i4\<close>\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   211
                 x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
67410
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   212
          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         \<comment> \<open>\<open>i5\<close>\<close>
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   213
          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>             \<comment> \<open>\<open>i6\<close>\<close>
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   214
          (stkOk c l r iL iR t stack)                                   \<comment> \<open>\<open>i7\<close>\<close>}
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   215
 DO IF t = Null \<or> t^.m
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   216
      THEN IF p^.c
67410
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   217
               THEN q := t; t := p; p := p^.r; t^.r := q                \<comment> \<open>\<open>pop\<close>\<close>
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   218
               ELSE q := t; t := p^.r; p^.r := p^.l;                    \<comment> \<open>\<open>swing\<close>\<close>
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   219
                        p^.l := q; p^.c := True          FI
67410
64d928bacddd prefer formal comments;
wenzelm
parents: 62042
diff changeset
   220
      ELSE q := p; p := t; t := t^.l; p^.l := q;                        \<comment> \<open>\<open>push\<close>\<close>
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   221
               p^.m := True; p^.c := False            FI       OD
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   222
 {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
74503
403ce50e6a2a separated commands from annotations to be able to abstract about the latter only
nipkow
parents: 72990
diff changeset
   223
  (is "Valid
403ce50e6a2a separated commands from annotations to be able to abstract about the latter only
nipkow
parents: 72990
diff changeset
   224
         {(c, m, l, r, t, p, q, root). ?Pre c m l r root}
403ce50e6a2a separated commands from annotations to be able to abstract about the latter only
nipkow
parents: 72990
diff changeset
   225
         (Seq _ (Seq _ (While {(c, m, l, r, t, p, q, root). ?whileB m t p} _)))
403ce50e6a2a separated commands from annotations to be able to abstract about the latter only
nipkow
parents: 72990
diff changeset
   226
         (Aseq _ (Aseq _ (Awhile {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ _))) _")
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   227
proof (vcg)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   228
  {
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   229
    fix c m l r t p q root
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   230
    assume "?Pre c m l r root"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   231
    thus "?inv c m l r root Null"  by (auto simp add: reachable_def addrs_def)
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   232
  next
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   233
    fix c m l r t p q
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   234
    let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   235
    assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   236
    then obtain stack where inv: "?Inv stack" by blast
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   237
    from a have pNull: "p = Null" and tDisj: "t=Null \<or> (t\<noteq>Null \<and> t^.m )" by auto
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   238
    let "?I1 \<and> _ \<and> _ \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> _"  =  "?Inv stack"
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   239
    from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   240
    from pNull i1 have stackEmpty: "stack = []" by simp
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   241
    from tDisj i4 have RisMarked[rule_format]: "\<forall>x.  x \<in> R \<longrightarrow> m x"  by(auto simp: reachable_def addrs_def stackEmpty)
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   242
    from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL"  by(auto simp: stackEmpty fun_eq_iff intro:RisMarked)
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   243
  next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   244
    fix c m l r t p q root
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   245
    let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   246
    let "\<exists>stack. ?popInv stack"  =  "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   247
    let "\<exists>stack. ?swInv stack"  =
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   248
      "?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   249
    let "\<exists>stack. ?puInv stack"  =
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   250
      "?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   251
    let "?ifB1"  =  "(t = Null \<or> t^.m)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   252
    let "?ifB2"  =  "p^.c"
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   253
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   254
    assume "(\<exists>stack.?Inv stack) \<and> ?whileB m t p"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   255
    then obtain stack where inv: "?Inv stack" and whileB: "?whileB m t p" by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   256
    let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   257
    from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   258
                and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   259
    have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   260
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   261
    show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   262
                          (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   263
            (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   264
    proof -
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   265
      {
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   266
        assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   267
        from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   268
        then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   269
        with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   270
          by auto
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   271
        with i2 have m_addr_p: "p^.m" by auto
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   272
        have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   273
        from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   274
        let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   275
        have "?popInv stack_tl"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   276
        proof -
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   277
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   278
          \<comment> \<open>List property is maintained:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   279
          from i1 p_notin_stack_tl ifB2
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   280
          have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   281
            by(simp add: addr_p_eq stack_eq, simp add: S_def)
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   282
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   283
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   284
          \<comment> \<open>Everything on the stack is marked:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   285
          from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   286
          moreover
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   287
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   288
          \<comment> \<open>Everything is still reachable:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   289
          let "(R = reachable ?Ra ?A)" = "?I3"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   290
          let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   291
          let "?B" = "{p, p^.r}"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   292
          \<comment> \<open>Our goal is \<open>R = reachable ?Rb ?B\<close>.\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   293
          have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   294
          proof
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   295
            show "?L \<subseteq> ?R"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   296
            proof (rule still_reachable)
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   297
              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   298
                   intro:oneStep_reachable Image_iff[THEN iffD2])
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   299
              show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   300
                   (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   301
            qed
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   302
            show "?R \<subseteq> ?L"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   303
            proof (rule still_reachable)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   304
              show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   305
                by(fastforce simp:addrs_def rel_defs addr_p_eq
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   306
                    intro:oneStep_reachable Image_iff[THEN iffD2])
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   307
            next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   308
              show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   309
                by (clarsimp simp:relS_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   310
                   (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   311
            qed
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   312
          qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   313
          with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   314
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   315
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   316
          \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   317
          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A"  =  ?I4
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   318
          let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   319
          let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   320
          \<comment> \<open>Our goal is \<open>\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B\<close>.\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   321
          let ?T = "{t, p^.r}"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   322
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   323
          have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   324
          proof (rule still_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   325
            have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   326
              by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   327
            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   328
              by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   329
            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   330
              by (clarsimp simp:restr_def relS_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   331
                (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   332
          qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   333
          \<comment> \<open>We now bring a term from the right to the left of the subset relation.\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   334
          hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   335
            by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   336
          have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   337
          proof (rule allI, rule impI)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   338
            fix x
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   339
            assume a: "x \<in> R \<and> \<not> m x"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   340
            \<comment> \<open>First, a disjunction on \<^term>\<open>p^.r\<close> used later in the proof\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   341
            have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   342
              by auto
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   343
            \<comment> \<open>\<^term>\<open>x\<close> belongs to the left hand side of @{thm[source] subset}:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   344
            have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   345
            have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   346
            \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   347
            \<comment> \<open>which corresponds to our goal.\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   348
            from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   349
          qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   350
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   351
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   352
          \<comment> \<open>If it is marked, then it is reachable\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   353
          from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   354
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   355
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   356
          \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   357
          from i7 i6 ifB2
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   358
          have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   359
            by(auto simp: addr_p_eq stack_eq fun_upd_apply)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   360
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   361
          moreover
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   362
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   363
          \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   364
          from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   365
            by (clarsimp simp:stack_eq addr_p_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   366
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   367
          ultimately show "?popInv stack_tl" by simp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   368
        qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   369
        hence "\<exists>stack. ?popInv stack" ..
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   370
      }
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   371
      moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   372
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   373
      \<comment> \<open>Proofs of the Swing and Push arm follow.\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   374
      \<comment> \<open>Since they are in principle simmilar to the Pop arm proof,\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   375
      \<comment> \<open>we show fewer comments and use frequent pattern matching.\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   376
      {
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   377
        \<comment> \<open>Swing arm\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   378
        assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   379
        from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   380
        then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   381
        with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   382
        with i2 have m_addr_p: "p^.m" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   383
        from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   384
          by simp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   385
        let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   386
        have "?swInv stack"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   387
        proof -
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   388
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   389
          \<comment> \<open>List property is maintained:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   390
          from i1 p_notin_stack_tl nifB2
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   391
          have swI1: "?swI1"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   392
            by (simp add:addr_p_eq stack_eq, simp add:S_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   393
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   394
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   395
          \<comment> \<open>Everything on the stack is marked:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   396
          from i2
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   397
          have swI2: "?swI2" .
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   398
          moreover
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   399
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   400
          \<comment> \<open>Everything is still reachable:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   401
          let "R = reachable ?Ra ?A" = "?I3"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   402
          let "R = reachable ?Rb ?B" = "?swI3"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   403
          have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   404
          proof (rule still_reachable_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   405
            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   406
              by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   407
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   408
            show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   409
              by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   410
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   411
            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   412
              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   413
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   414
            show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   415
              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   416
          qed
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   417
          with i3
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   418
          have swI3: "?swI3" by (simp add:reachable_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   419
          moreover
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   420
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   421
          \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   422
          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   423
          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   424
          let ?T = "{t}"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   425
          have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   426
          proof (rule still_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   427
            have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   428
              by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   429
            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   430
              by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   431
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   432
            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   433
              by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   434
          qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   435
          then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   436
            by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   437
          have ?swI4
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   438
          proof (rule allI, rule impI)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   439
            fix x
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   440
            assume a: "x \<in> R \<and>\<not> m x"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   441
            with i4 addr_p_eq stack_eq  have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   442
              by (simp only:reachable_def, clarsimp)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   443
            with ifB1 a
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   444
            have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   445
              by (auto simp add:addrs_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   446
            from inc exc subset  show "x \<in> reachable ?Rb ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   447
              by (auto simp add:reachable_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   448
          qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   449
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   450
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   451
          \<comment> \<open>If it is marked, then it is reachable\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   452
          from i5
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   453
          have "?swI5" .
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   454
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   455
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   456
          \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   457
          from i6 stack_eq
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   458
          have "?swI6"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   459
            by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   460
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   461
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   462
          \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   463
          from stackDist i7 nifB2
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   464
          have "?swI7"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   465
            by (clarsimp simp:addr_p_eq stack_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   466
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   467
          ultimately show ?thesis by auto
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   468
        qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   469
        then have "\<exists>stack. ?swInv stack" by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   470
      }
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   471
      moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   472
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   473
      {
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   474
        \<comment> \<open>Push arm\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   475
        assume nifB1: "\<not>?ifB1"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   476
        from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   477
        then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   478
        with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   479
        from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   480
        with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   481
        let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   482
        have "?puInv new_stack"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   483
        proof -
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   484
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   485
          \<comment> \<open>List property is maintained:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   486
          from i1 t_notin_stack
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   487
          have puI1: "?puI1"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   488
            by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   489
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   490
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   491
          \<comment> \<open>Everything on the stack is marked:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   492
          from i2
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   493
          have puI2: "?puI2"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   494
            by (simp add:new_stack_eq fun_upd_apply)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   495
          moreover
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   496
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   497
          \<comment> \<open>Everything is still reachable:\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   498
          let "R = reachable ?Ra ?A" = "?I3"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   499
          let "R = reachable ?Rb ?B" = "?puI3"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   500
          have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   501
          proof (rule still_reachable_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   502
            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   503
              by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   504
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   505
            show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   506
              by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   507
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   508
            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   509
              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   510
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   511
            show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   512
              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   513
          qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   514
          with i3
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   515
          have puI3: "?puI3" by (simp add:reachable_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   516
          moreover
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   517
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   518
          \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   519
          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   520
          let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   521
          let ?T = "{t}"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   522
          have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   523
          proof (rule still_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   524
            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   525
              by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   526
          next
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   527
            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   528
              by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   529
                 (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   530
          qed
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   531
          then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   532
            by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   533
          have ?puI4
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   534
          proof (rule allI, rule impI)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   535
            fix x
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   536
            assume a: "x \<in> R \<and> \<not> ?new_m x"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   537
            have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   538
            with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   539
              by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   540
            have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   541
              using xDisj a n_m_addr_t
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   542
              by (clarsimp simp add:addrs_def addr_t_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   543
            from inc exc subset  show "x \<in> reachable ?Rb ?B"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   544
              by (auto simp add:reachable_def)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   545
          qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   546
          moreover
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   547
81190
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   548
          \<comment> \<open>If it is marked, then it is reachable\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   549
          from i5
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   550
          have "?puI5"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   551
            by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   552
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   553
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   554
          \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   555
          from i6
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   556
          have "?puI6"
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   557
            by (simp add:new_stack_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   558
          moreover
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   559
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   560
          \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   561
          from stackDist i6 t_notin_stack i7
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   562
          have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   563
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   564
          ultimately show ?thesis by auto
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   565
        qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   566
        then have "\<exists>stack. ?puInv stack" by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   567
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   568
      }
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   569
      ultimately show ?thesis by blast
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   570
    qed
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   571
  }
60fedd5b7c58 tuned whitespace;
wenzelm
parents: 81189
diff changeset
   572
qed
13820
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   573
87a8ab465b29 Proof of the Schorr-Waite graph marking algorithm.
mehta
parents:
diff changeset
   574
end