src/HOL/UNITY/Reach.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 4896 4727272f3db6
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/UNITY/Reach.thy
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
paulson@4776
     7
*)
paulson@4776
     8
paulson@4776
     9
Reach = Update + FP + Traces + SubstAx +
paulson@4776
    10
paulson@4776
    11
types   vertex
paulson@4776
    12
        state = "vertex=>bool"
paulson@4776
    13
paulson@4776
    14
arities vertex :: term
paulson@4776
    15
paulson@4776
    16
consts
paulson@4776
    17
  init ::  "vertex"
paulson@4776
    18
paulson@4776
    19
  edges :: "(vertex*vertex) set"
paulson@4776
    20
paulson@4776
    21
constdefs
paulson@4776
    22
paulson@4776
    23
  asgt  :: "[vertex,vertex] => (state*state) set"
paulson@4776
    24
    "asgt u v == {(s,s'). s' = s[v|-> s u | s v]}"
paulson@4776
    25
paulson@4776
    26
  racts :: "(state*state) set set"
paulson@4776
    27
    "racts == insert id (UN (u,v): edges. {asgt u v})"
paulson@4776
    28
paulson@4776
    29
  rinit :: "state set"
paulson@4776
    30
    "rinit == {%v. v=init}"
paulson@4776
    31
paulson@4776
    32
  invariant :: state set
paulson@4776
    33
    "invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
paulson@4776
    34
paulson@4776
    35
  fixedpoint :: state set
paulson@4776
    36
    "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
paulson@4776
    37
paulson@4776
    38
  metric :: state => nat
paulson@4776
    39
    "metric == (%s. card {v. ~ s v})"
paulson@4776
    40
paulson@4776
    41
rules
paulson@4776
    42
paulson@4776
    43
  (*We assume that the set of vertices is finite*)
paulson@4776
    44
  finite_graph "finite (UNIV :: vertex set)"
paulson@4776
    45
  
paulson@4776
    46
end