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