src/HOLCF/IOA/meta_theory/RefMappings.thy
author wenzelm
Fri Sep 02 17:23:59 2005 +0200 (2005-09-02)
changeset 17233 41eee2e7b465
parent 14981 e73f8140af78
child 19741 f65265d71426
permissions -rw-r--r--
converted specifications to Isar theories;
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
mueller@3275
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@3071
     4
*)
mueller@3071
     5
wenzelm@17233
     6
header {* Refinement Mappings in HOLCF/IOA *}
mueller@3071
     7
wenzelm@17233
     8
theory RefMappings
wenzelm@17233
     9
imports Traces
wenzelm@17233
    10
begin
wenzelm@17233
    11
wenzelm@17233
    12
defaultsort type
mueller@3071
    13
mueller@3071
    14
consts
mueller@3433
    15
  move         ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool"
mueller@3071
    16
  is_ref_map   ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@3071
    17
  is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
wenzelm@17233
    18
mueller@4559
    19
mueller@3071
    20
defs
mueller@3071
    21
wenzelm@17233
    22
move_def:
wenzelm@17233
    23
  "move ioa ex s a t ==
wenzelm@17233
    24
    (is_exec_frag ioa (s,ex) &  Finite ex &
wenzelm@17233
    25
     laststate (s,ex)=t  &
nipkow@10835
    26
     mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
mueller@3071
    27
wenzelm@17233
    28
is_ref_map_def:
wenzelm@17233
    29
  "is_ref_map f C A ==
wenzelm@17233
    30
   (!s:starts_of(C). f(s):starts_of(A)) &
wenzelm@17233
    31
   (!s t a. reachable C s &
wenzelm@17233
    32
            s -a--C-> t
mueller@3071
    33
            --> (? ex. move A ex (f s) a (f t)))"
wenzelm@17233
    34
wenzelm@17233
    35
is_weak_ref_map_def:
wenzelm@17233
    36
  "is_weak_ref_map f C A ==
wenzelm@17233
    37
   (!s:starts_of(C). f(s):starts_of(A)) &
wenzelm@17233
    38
   (!s t a. reachable C s &
wenzelm@17233
    39
            s -a--C-> t
wenzelm@17233
    40
            --> (if a:ext(C)
mueller@3071
    41
                 then (f s) -a--A-> (f t)
wenzelm@17233
    42
                 else (f s)=(f t)))"
mueller@3071
    43
wenzelm@17233
    44
ML {* use_legacy_bindings (the_context ()) *}
mueller@4559
    45
mueller@3071
    46
end