src/HOLCF/IOA/meta_theory/RefMappings.thy
author mueller
Wed, 21 May 1997 15:08:52 +0200
changeset 3275 3f53f2c876f4
parent 3071 981258186b71
child 3433 2de17c994071
permissions -rw-r--r--
changes for release 94-8
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     2
    ID:         $Id$
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     3
    Author:     Olaf Mueller
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     6
Refinement Mappings in HOLCF/IOA
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
*)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     8
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     9
RefMappings = Traces  +
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    10
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    11
default term
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    12
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    13
consts
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    14
  laststate    ::"('a,'s)execution => 's"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    15
  move         ::"[('a,'s)ioa,('a,'s)execution,'s,'a,'s] => bool"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    16
  is_ref_map   ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    17
  is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    18
 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    19
defs
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    20
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    21
laststate_def
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    22
  "laststate ex == case Last`(snd ex) of
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    23
                      Undef  => fst ex
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    24
                    | Def at => snd at"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    25
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    26
(* FIX: see paper, move should be defined on pairs, not on execs, then fst ex=s can
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    27
   be omitted *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    28
move_def
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    29
  "move ioa ex s a t ==    
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    30
    (is_execution_fragment ioa ex &  Finite (snd ex) & 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    31
     fst ex=s & laststate ex=t  &     
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    32
     mk_trace ioa`(snd ex) = (if a:ext(ioa) then a>>nil else nil))"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    33
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    34
is_ref_map_def
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    35
  "is_ref_map f C A ==                          
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    36
   (!s:starts_of(C). f(s):starts_of(A)) &        
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    37
   (!s t a. reachable C s &                      
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    38
            s -a--C-> t                 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    39
            --> (? ex. move A ex (f s) a (f t)))"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    40
 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    41
is_weak_ref_map_def
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    42
  "is_weak_ref_map f C A ==                          
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    43
   (!s:starts_of(C). f(s):starts_of(A)) &        
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    44
   (!s t a. reachable C s &                      
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    45
            s -a--C-> t     
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    46
            --> (if a:ext(C) 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    47
                 then (f s) -a--A-> (f t)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    48
                 else (f s)=(f t)))" 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    49
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    50
end