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