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
paulson@5111
     1
(*  Title:      HOL/UNITY/Traces
paulson@5111
     2
    ID:         $Id$
paulson@5111
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5111
     4
    Copyright   1998  University of Cambridge
paulson@5111
     5
paulson@5111
     6
Inductive definitions of
paulson@5111
     7
  * traces: the possible execution traces
paulson@5111
     8
  * reachable: the set of reachable states
paulson@5111
     9
*)
paulson@5111
    10
paulson@4776
    11
Traces = UNITY +
paulson@4776
    12
paulson@5111
    13
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
paulson@4776
    14
paulson@5111
    15
  (*Initial states and program => (final state, reversed trace to it)...
paulson@5111
    16
    Arguments MUST be curried in an inductive definition*)
paulson@5111
    17
paulson@5111
    18
inductive "traces Init Acts"  
paulson@4776
    19
  intrs 
paulson@4776
    20
         (*Initial trace is empty*)
paulson@5111
    21
    Init  "s: Init ==> (s,[]) : traces Init Acts"
paulson@4776
    22
paulson@5111
    23
    Acts  "[| act: Acts;  (s,evs) : traces Init Acts;  (s,s'): act |]
paulson@5111
    24
	   ==> (s', s#evs) : traces Init Acts"
paulson@4776
    25
paulson@4776
    26
paulson@5253
    27
record 'a program =
paulson@5253
    28
  Init :: 'a set
paulson@5253
    29
  Acts :: "('a * 'a)set set"
paulson@5253
    30
paulson@5253
    31
paulson@5253
    32
consts reachable :: "'a program => 'a set"
paulson@5253
    33
paulson@5253
    34
inductive "reachable prg"
paulson@5253
    35
  intrs 
paulson@5253
    36
    Init  "s: Init prg ==> s : reachable prg"
paulson@5253
    37
paulson@5253
    38
    Acts  "[| act: Acts prg;  s : reachable prg;  (s,s'): act |]
paulson@5253
    39
	   ==> s' : reachable prg"
paulson@5253
    40
paulson@4776
    41
end