1(*  Title:      HOL/UNITY/Simple/Reach.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
6[this example took only four days!]
7*)
8
9theory Reach imports "../UNITY_Main" begin
10
11typedecl vertex
12
13type_synonym state = "vertex=>bool"
14
15consts
16  init ::  "vertex"
17
18  edges :: "(vertex*vertex) set"
19
20definition asgt :: "[vertex,vertex] => (state*state) set"
21  where "asgt u v = {(s,s'). s' = s(v:= s u | s v)}"
22
23definition Rprg :: "state program"
24  where "Rprg = mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
25
26definition reach_invariant :: "state set"
27  where "reach_invariant = {s. (\<forall>v. s v --> (init, v) \<in> edges\<^sup>*) & s init}"
28
29definition fixedpoint :: "state set"
30  where "fixedpoint = {s. \<forall>(u,v)\<in>edges. s u --> s v}"
31
32definition metric :: "state => nat"
33  where "metric s = card {v. ~ s v}"
34
35
36text\<open>*We assume that the set of vertices is finite\<close>
37axiomatization where
38  finite_graph:  "finite (UNIV :: vertex set)"
39  
40
41
42
43(*TO SIMPDATA.ML??  FOR CLASET??  *)
44lemma ifE [elim!]:
45    "[| if P then Q else R;     
46        [| P;   Q |] ==> S;     
47        [| ~ P; R |] ==> S |] ==> S"
48by (simp split: if_split_asm) 
49
50
51declare Rprg_def [THEN def_prg_Init, simp]
52
53declare asgt_def [THEN def_act_simp,simp]
54
55text\<open>All vertex sets are finite\<close>
56declare finite_subset [OF subset_UNIV finite_graph, iff]
57
58declare reach_invariant_def [THEN def_set_simp, simp]
59
60lemma reach_invariant: "Rprg \<in> Always reach_invariant"
61apply (rule AlwaysI, force) 
62apply (unfold Rprg_def, safety) 
63apply (blast intro: rtrancl_trans)
64done
65
66
67(*** Fixedpoint ***)
68
69(*If it reaches a fixedpoint, it has found a solution*)
70lemma fixedpoint_invariant_correct: 
71     "fixedpoint \<inter> reach_invariant = { %v. (init, v) \<in> edges\<^sup>* }"
72apply (unfold fixedpoint_def)
73apply (rule equalityI)
74apply (auto intro!: ext)
75apply (erule rtrancl_induct, auto)
76done
77
78lemma lemma1: 
79     "FP Rprg \<subseteq> fixedpoint"
80apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
81apply (auto simp add: stable_def constrains_def)
82apply (drule bspec, assumption)
83apply (simp add: Image_singleton image_iff)
84apply (drule fun_cong, auto)
85done
86
87lemma lemma2: 
88     "fixedpoint \<subseteq> FP Rprg"
89apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
90apply (auto intro!: ext simp add: stable_def constrains_def)
91done
92
93lemma FP_fixedpoint: "FP Rprg = fixedpoint"
94by (rule equalityI [OF lemma1 lemma2])
95
96
97(*If we haven't reached a fixedpoint then there is some edge for which u but
98  not v holds.  Progress will be proved via an ENSURES assertion that the
99  metric will decrease for each suitable edge.  A union over all edges proves
100  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
101  *)
102
103lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
104apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
105apply (rule subset_antisym)
106apply (auto simp add: Compl_FP UN_UN_flatten)
107 apply (rule fun_upd_idem, force)
108apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
109done
110
111lemma Diff_fixedpoint:
112     "A - fixedpoint = (\<Union>(u,v)\<in>edges. A \<inter> {s. s u & ~ s v})"
113by (simp add: Diff_eq Compl_fixedpoint, blast)
114
115
116(*** Progress ***)
117
118lemma Suc_metric: "~ s x ==> Suc (metric (s(x:=True))) = metric s"
119apply (unfold metric_def)
120apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}")
121 prefer 2 apply force
122apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
123done
124
125lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"
126by (erule Suc_metric [THEN subst], blast)
127
128lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s"
129  by (cases "s x --> s y") (auto intro: less_imp_le simp add: fun_upd_idem)
130
131lemma LeadsTo_Diff_fixedpoint:
132     "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
133apply (simp (no_asm) add: Diff_fixedpoint Rprg_def)
134apply (rule LeadsTo_UN, auto)
135apply (ensures_tac "asgt a b")
136 prefer 2 apply blast
137apply (simp (no_asm_use) add: linorder_not_less)
138apply (drule metric_le [THEN order_antisym]) 
139apply (auto elim: less_not_refl3 [THEN [2] rev_notE])
140done
141
142lemma LeadsTo_Un_fixedpoint:
143     "Rprg \<in> (metric-`{m}) LeadsTo (metric-`(lessThan m) \<union> fixedpoint)"
144apply (rule LeadsTo_Diff [OF LeadsTo_Diff_fixedpoint [THEN LeadsTo_weaken_R]
145                             subset_imp_LeadsTo], auto)
146done
147
148
149(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
150lemma LeadsTo_fixedpoint: "Rprg \<in> UNIV LeadsTo fixedpoint"
151apply (rule LessThan_induct, auto)
152apply (rule LeadsTo_Un_fixedpoint)
153done
154
155lemma LeadsTo_correct: "Rprg \<in> UNIV LeadsTo { %v. (init, v) \<in> edges\<^sup>* }"
156apply (subst fixedpoint_invariant_correct [symmetric])
157apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto)
158done
159
160end
161