src/HOL/UNITY/Simple/Reach.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 14150 9a23e4eb5eb3
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
     1 (*  Title:      HOL/UNITY/Reach.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
     7 	[this example took only four days!]
     8 *)
     9 
    10 theory Reach = UNITY_Main:
    11 
    12 typedecl vertex
    13 
    14 types    state = "vertex=>bool"
    15 
    16 consts
    17   init ::  "vertex"
    18 
    19   edges :: "(vertex*vertex) set"
    20 
    21 constdefs
    22 
    23   asgt  :: "[vertex,vertex] => (state*state) set"
    24     "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
    25 
    26   Rprg :: "state program"
    27     "Rprg == mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
    28 
    29   reach_invariant :: "state set"
    30     "reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
    31 
    32   fixedpoint :: "state set"
    33     "fixedpoint == {s. \<forall>(u,v)\<in>edges. s u --> s v}"
    34 
    35   metric :: "state => nat"
    36     "metric s == card {v. ~ s v}"
    37 
    38 
    39 text{**We assume that the set of vertices is finite*}
    40 axioms 
    41   finite_graph:  "finite (UNIV :: vertex set)"
    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 \<in> 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 \<inter> reach_invariant = { %v. (init, v) \<in> 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 \<subseteq> fixedpoint"
    84 apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
    85 apply (auto simp add: stable_def constrains_def)
    86 apply (drule bspec, assumption)
    87 apply (simp add: Image_singleton image_iff)
    88 apply (drule fun_cong, auto)
    89 done
    90 
    91 lemma lemma2: 
    92      "fixedpoint \<subseteq> FP Rprg"
    93 apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
    94 apply (auto intro!: ext simp add: stable_def constrains_def)
    95 done
    96 
    97 lemma FP_fixedpoint: "FP Rprg = fixedpoint"
    98 by (rule equalityI [OF lemma1 lemma2])
    99 
   100 
   101 (*If we haven't reached a fixedpoint then there is some edge for which u but
   102   not v holds.  Progress will be proved via an ENSURES assertion that the
   103   metric will decrease for each suitable edge.  A union over all edges proves
   104   a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
   105   *)
   106 
   107 lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
   108 apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
   109 apply (auto simp add: Compl_FP UN_UN_flatten)
   110  apply (rule fun_upd_idem, force)
   111 apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
   112 done
   113 
   114 lemma Diff_fixedpoint:
   115      "A - fixedpoint = (\<Union>(u,v)\<in>edges. A \<inter> {s. s u & ~ s v})"
   116 by (simp add: Diff_eq Compl_fixedpoint, blast)
   117 
   118 
   119 (*** Progress ***)
   120 
   121 lemma Suc_metric: "~ s x ==> Suc (metric (s(x:=True))) = metric s"
   122 apply (unfold metric_def)
   123 apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}")
   124  prefer 2 apply force
   125 apply (simp add: card_Suc_Diff1)
   126 done
   127 
   128 lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"
   129 by (erule Suc_metric [THEN subst], blast)
   130 
   131 lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s"
   132 apply (case_tac "s x --> s y")
   133 apply (auto intro: less_imp_le simp add: fun_upd_idem)
   134 done
   135 
   136 lemma LeadsTo_Diff_fixedpoint:
   137      "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
   138 apply (simp (no_asm) add: Diff_fixedpoint Rprg_def)
   139 apply (rule LeadsTo_UN, auto)
   140 apply (ensures_tac "asgt a b")
   141  prefer 2 apply blast
   142 apply (simp (no_asm_use) add: not_less_iff_le)
   143 apply (drule metric_le [THEN order_antisym]) 
   144 apply (auto elim: less_not_refl3 [THEN [2] rev_notE])
   145 done
   146 
   147 lemma LeadsTo_Un_fixedpoint:
   148      "Rprg \<in> (metric-`{m}) LeadsTo (metric-`(lessThan m) \<union> fixedpoint)"
   149 apply (rule LeadsTo_Diff [OF LeadsTo_Diff_fixedpoint [THEN LeadsTo_weaken_R]
   150                              subset_imp_LeadsTo], auto)
   151 done
   152 
   153 
   154 (*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
   155 lemma LeadsTo_fixedpoint: "Rprg \<in> UNIV LeadsTo fixedpoint"
   156 apply (rule LessThan_induct, auto)
   157 apply (rule LeadsTo_Un_fixedpoint)
   158 done
   159 
   160 lemma LeadsTo_correct: "Rprg \<in> UNIV LeadsTo { %v. (init, v) \<in> edges^* }"
   161 apply (subst fixedpoint_invariant_correct [symmetric])
   162 apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto)
   163 done
   164 
   165 end