author | paulson |
Wed, 22 Dec 1999 17:16:23 +0100 | |
changeset 8072 | 5b95377d7538 |
parent 8055 | bb15396278fb |
child 8122 | b43ad07660b9 |
permissions | -rw-r--r-- |
8044 | 1 |
(* Title: HOL/UNITY/ELT |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
leadsTo strengthened with a specification of the allowable sets transient parts |
|
7 |
*) |
|
8 |
||
9 |
ELT = Project + |
|
10 |
||
11 |
consts |
|
12 |
||
13 |
(*LEADS-TO constant for the inductive definition*) |
|
14 |
elt :: "['a set set, 'a program] => ('a set * 'a set) set" |
|
15 |
||
16 |
||
17 |
inductive "elt CC F" |
|
18 |
intrs |
|
19 |
||
8072
5b95377d7538
removing the "{} : CC" requirement for leadsTo[CC]
paulson
parents:
8055
diff
changeset
|
20 |
Basis "[| F : A ensures B; A-B : (insert {} CC) |] ==> (A,B) : elt CC F" |
8044 | 21 |
|
22 |
Trans "[| (A,B) : elt CC F; (B,C) : elt CC F |] ==> (A,C) : elt CC F" |
|
23 |
||
24 |
Union "{(A,B) | A. A: S} : Pow (elt CC F) ==> (Union S, B) : elt CC F" |
|
25 |
||
26 |
monos Pow_mono |
|
27 |
||
28 |
||
29 |
constdefs |
|
30 |
||
31 |
(*the set of all sets determined by f alone*) |
|
32 |
givenBy :: "['a => 'b] => 'a set set" |
|
33 |
"givenBy f == range (%B. f-`` B)" |
|
34 |
||
35 |
(*visible version of the LEADS-TO relation*) |
|
36 |
leadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
|
37 |
("(3_/ leadsTo[_]/ _)" [80,0,80] 80) |
|
38 |
"leadsETo A CC B == {F. (A,B) : elt CC F}" |
|
39 |
||
40 |
LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
|
41 |
("(3_/ LeadsTo[_]/ _)" [80,0,80] 80) |
|
42 |
"LeadsETo A CC B == |
|
43 |
{F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) `` CC] B}" |
|
44 |
||
45 |
end |