src/HOL/UNITY/Traces.thy
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5253 82a5ca6290aa
child 5584 aad639e56d4e
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     1 (*  Title:      HOL/UNITY/Traces
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Inductive definitions of
     7   * traces: the possible execution traces
     8   * reachable: the set of reachable states
     9 *)
    10 
    11 Traces = UNITY +
    12 
    13 consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
    14 
    15   (*Initial states and program => (final state, reversed trace to it)...
    16     Arguments MUST be curried in an inductive definition*)
    17 
    18 inductive "traces Init Acts"  
    19   intrs 
    20          (*Initial trace is empty*)
    21     Init  "s: Init ==> (s,[]) : traces Init Acts"
    22 
    23     Acts  "[| act: Acts;  (s,evs) : traces Init Acts;  (s,s'): act |]
    24 	   ==> (s', s#evs) : traces Init Acts"
    25 
    26 
    27 record 'a program =
    28   Init :: 'a set
    29   Acts :: "('a * 'a)set set"
    30 
    31 
    32 consts reachable :: "'a program => 'a set"
    33 
    34 inductive "reachable prg"
    35   intrs 
    36     Init  "s: Init prg ==> s : reachable prg"
    37 
    38     Acts  "[| act: Acts prg;  s : reachable prg;  (s,s'): act |]
    39 	   ==> s' : reachable prg"
    40 
    41 end