src/HOL/UNITY/Traces.thy
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5648 fe887910e32e
child 6012 1894bfc4aee9
permissions -rw-r--r--
Drule.rev_triv_goal;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     1
(*  Title:      HOL/UNITY/Traces
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     2
    ID:         $Id$
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     4
    Copyright   1998  University of Cambridge
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     5
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     6
Inductive definitions of
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     7
  * traces: the possible execution traces
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     8
  * reachable: the set of reachable states
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
     9
*)
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    10
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    11
Traces = LessThan +
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    13
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    15
  (*Initial states and program => (final state, reversed trace to it)...
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    16
    Arguments MUST be curried in an inductive definition*)
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    17
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    18
inductive "traces Init Acts"  
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    19
  intrs 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
         (*Initial trace is empty*)
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    21
    Init  "s: Init ==> (s,[]) : traces Init Acts"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    23
    Acts  "[| act: Acts;  (s,evs) : traces Init Acts;  (s,s'): act |]
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 4837
diff changeset
    24
	   ==> (s', s#evs) : traces Init Acts"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    25
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    26
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    27
typedef (Program)
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5596
diff changeset
    28
  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5313
diff changeset
    29
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5313
diff changeset
    30
constdefs
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    31
    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5596
diff changeset
    32
    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    33
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    34
    Init :: "'a program => 'a set"
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5608
diff changeset
    35
    "Init F == fst (Rep_Program F)"
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    36
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5313
diff changeset
    37
    Acts :: "'a program => ('a * 'a)set set"
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5608
diff changeset
    38
    "Acts F == snd (Rep_Program F)"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    39
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    40
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    41
consts reachable :: "'a program => 'a set"
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    42
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5608
diff changeset
    43
inductive "reachable F"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    44
  intrs 
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5608
diff changeset
    45
    Init  "s: Init F ==> s : reachable F"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    46
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5608
diff changeset
    47
    Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
3ac11c4af76a tidying and renaming
paulson
parents: 5608
diff changeset
    48
	   ==> s' : reachable F"
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    49
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    50
end