author  nipkow 
Tue, 09 Jan 2001 15:36:30 +0100  
changeset 10835  f4745d77e620 
parent 4559  8e604d885b54 
child 12218  6597093b77e7 
permissions  rwrr 
3071  1 
(* Title: HOLCF/IOA/meta_theory/RefMappings.thy 
3275  2 
ID: $Id$ 
3071  3 
Author: Olaf Mueller 
4 
Copyright 1996 TU Muenchen 

5 

6 
Refinement Mappings in HOLCF/IOA 

7 
*) 

8 

9 
RefMappings = Traces + 

10 

11 
default term 

12 

13 
consts 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset

14 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

15 
move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" 
3071  16 
is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" 
17 
is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" 

18 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset

19 

3071  20 
defs 
21 

22 

23 
move_def 

24 
"move ioa ex s a t == 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

25 
(is_exec_frag ioa (s,ex) & Finite ex & 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

26 
laststate (s,ex)=t & 
10835  27 
mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))" 
3071  28 

29 
is_ref_map_def 

30 
"is_ref_map f C A == 

31 
(!s:starts_of(C). f(s):starts_of(A)) & 

32 
(!s t a. reachable C s & 

33 
s aC> t 

34 
> (? ex. move A ex (f s) a (f t)))" 

35 

36 
is_weak_ref_map_def 

37 
"is_weak_ref_map f C A == 

38 
(!s:starts_of(C). f(s):starts_of(A)) & 

39 
(!s t a. reachable C s & 

40 
s aC> t 

41 
> (if a:ext(C) 

42 
then (f s) aA> (f t) 

43 
else (f s)=(f t)))" 

44 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset

45 

3071  46 
end 