src/HOL/IOA/Solve.thy
author wenzelm
Tue Sep 06 19:03:39 2005 +0200 (2005-09-06)
changeset 17288 aa3833fb7bee
parent 4530 ac1821645636
child 19801 b2af2549efd1
permissions -rw-r--r--
converted to Isar theory format;
oheimb@4530
     1
(*  Title:      HOL/IOA/Solve.thy
mueller@3078
     2
    ID:         $Id$
mueller@3078
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@3078
     4
    Copyright   1994  TU Muenchen
mueller@3078
     5
*)
mueller@3078
     6
wenzelm@17288
     7
header {* Weak possibilities mapping (abstraction) *}
wenzelm@17288
     8
wenzelm@17288
     9
theory Solve
wenzelm@17288
    10
imports IOA
wenzelm@17288
    11
begin
mueller@3078
    12
mueller@3078
    13
constdefs
mueller@3078
    14
mueller@3078
    15
  is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
wenzelm@17288
    16
  "is_weak_pmap f C A ==
wenzelm@17288
    17
   (!s:starts_of(C). f(s):starts_of(A)) &
wenzelm@17288
    18
   (!s t a. reachable C s &
wenzelm@17288
    19
            (s,a,t):trans_of(C)
wenzelm@17288
    20
            --> (if a:externals(asig_of(C)) then
wenzelm@17288
    21
                   (f(s),a,f(t)):trans_of(A)
mueller@3078
    22
                 else f(s)=f(t)))"
mueller@3078
    23
wenzelm@17288
    24
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17288
    25
mueller@3078
    26
end