21 constdefs |
21 constdefs |
22 |
22 |
23 asgt :: "[vertex,vertex] => (state*state) set" |
23 asgt :: "[vertex,vertex] => (state*state) set" |
24 "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" |
24 "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" |
25 |
25 |
26 Rprg :: state program |
26 Rprg :: "state program" |
27 "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)" |
27 "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)" |
28 |
28 |
29 reach_invariant :: state set |
29 reach_invariant :: "state set" |
30 "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" |
30 "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" |
31 |
31 |
32 fixedpoint :: state set |
32 fixedpoint :: "state set" |
33 "fixedpoint == {s. ALL (u,v): edges. s u --> s v}" |
33 "fixedpoint == {s. ALL (u,v): edges. s u --> s v}" |
34 |
34 |
35 metric :: state => nat |
35 metric :: "state => nat" |
36 "metric s == card {v. ~ s v}" |
36 "metric s == card {v. ~ s v}" |
37 |
37 |
38 rules |
|
39 |
38 |
40 (*We assume that the set of vertices is finite*) |
39 text{**We assume that the set of vertices is finite*} |
41 finite_graph "finite (UNIV :: vertex set)" |
40 axioms |
|
41 finite_graph: "finite (UNIV :: vertex set)" |
42 |
42 |
|
43 |
|
44 |
|
45 |
|
46 (*TO SIMPDATA.ML?? FOR CLASET?? *) |
|
47 lemma ifE [elim!]: |
|
48 "[| if P then Q else R; |
|
49 [| P; Q |] ==> S; |
|
50 [| ~ P; R |] ==> S |] ==> S" |
|
51 by (simp split: split_if_asm) |
|
52 |
|
53 |
|
54 declare Rprg_def [THEN def_prg_Init, simp] |
|
55 |
|
56 declare asgt_def [THEN def_act_simp,simp] |
|
57 |
|
58 (*All vertex sets are finite*) |
|
59 declare finite_subset [OF subset_UNIV finite_graph, iff] |
|
60 |
|
61 declare reach_invariant_def [THEN def_set_simp, simp] |
|
62 |
|
63 lemma reach_invariant: "Rprg : Always reach_invariant" |
|
64 apply (rule AlwaysI, force) |
|
65 apply (unfold Rprg_def, constrains) |
|
66 apply (blast intro: rtrancl_trans) |
|
67 done |
|
68 |
|
69 |
|
70 (*** Fixedpoint ***) |
|
71 |
|
72 (*If it reaches a fixedpoint, it has found a solution*) |
|
73 lemma fixedpoint_invariant_correct: |
|
74 "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }" |
|
75 apply (unfold fixedpoint_def) |
|
76 apply (rule equalityI) |
|
77 apply (auto intro!: ext) |
|
78 prefer 2 apply (blast intro: rtrancl_trans) |
|
79 apply (erule rtrancl_induct, auto) |
|
80 done |
|
81 |
|
82 lemma lemma1: |
|
83 "FP Rprg <= fixedpoint" |
|
84 apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def, auto) |
|
85 apply (drule bspec, assumption) |
|
86 apply (simp add: Image_singleton image_iff) |
|
87 apply (drule fun_cong, auto) |
|
88 done |
|
89 |
|
90 lemma lemma2: |
|
91 "fixedpoint <= FP Rprg" |
|
92 apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def) |
|
93 apply (auto intro!: ext) |
|
94 done |
|
95 |
|
96 lemma FP_fixedpoint: "FP Rprg = fixedpoint" |
|
97 by (rule equalityI [OF lemma1 lemma2]) |
|
98 |
|
99 |
|
100 (*If we haven't reached a fixedpoint then there is some edge for which u but |
|
101 not v holds. Progress will be proved via an ENSURES assertion that the |
|
102 metric will decrease for each suitable edge. A union over all edges proves |
|
103 a LEADSTO assertion that the metric decreases if we are not at a fixedpoint. |
|
104 *) |
|
105 |
|
106 lemma Compl_fixedpoint: "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})" |
|
107 apply (simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def, auto) |
|
108 apply (rule fun_upd_idem, force) |
|
109 apply (force intro!: rev_bexI simp add: fun_upd_idem_iff) |
|
110 done |
|
111 |
|
112 lemma Diff_fixedpoint: |
|
113 "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})" |
|
114 apply (simp add: Diff_eq Compl_fixedpoint, blast) |
|
115 done |
|
116 |
|
117 |
|
118 (*** Progress ***) |
|
119 |
|
120 lemma Suc_metric: "~ s x ==> Suc (metric (s(x:=True))) = metric s" |
|
121 apply (unfold metric_def) |
|
122 apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}") |
|
123 prefer 2 apply force |
|
124 apply (simp add: card_Suc_Diff1) |
|
125 done |
|
126 |
|
127 lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s" |
|
128 by (erule Suc_metric [THEN subst], blast) |
|
129 |
|
130 lemma metric_le: "metric (s(y:=s x | s y)) <= metric s" |
|
131 apply (case_tac "s x --> s y") |
|
132 apply (auto intro: less_imp_le simp add: fun_upd_idem) |
|
133 done |
|
134 |
|
135 lemma LeadsTo_Diff_fixedpoint: |
|
136 "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))" |
|
137 apply (simp (no_asm) add: Diff_fixedpoint Rprg_def) |
|
138 apply (rule LeadsTo_UN, auto) |
|
139 apply (ensures_tac "asgt a b") |
|
140 prefer 2 apply blast |
|
141 apply (simp (no_asm_use) add: not_less_iff_le) |
|
142 apply (drule metric_le [THEN order_antisym]) |
|
143 apply (auto elim: less_not_refl3 [THEN [2] rev_notE]) |
|
144 done |
|
145 |
|
146 lemma LeadsTo_Un_fixedpoint: |
|
147 "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)" |
|
148 apply (rule LeadsTo_Diff [OF LeadsTo_Diff_fixedpoint [THEN LeadsTo_weaken_R] |
|
149 subset_imp_LeadsTo], auto) |
|
150 done |
|
151 |
|
152 |
|
153 (*Execution in any state leads to a fixedpoint (i.e. can terminate)*) |
|
154 lemma LeadsTo_fixedpoint: "Rprg : UNIV LeadsTo fixedpoint" |
|
155 apply (rule LessThan_induct, auto) |
|
156 apply (rule LeadsTo_Un_fixedpoint) |
|
157 done |
|
158 |
|
159 lemma LeadsTo_correct: "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }" |
|
160 apply (subst fixedpoint_invariant_correct [symmetric]) |
|
161 apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto) |
|
162 done |
|
163 |
43 end |
164 end |