src/HOL/IOA/meta_theory/Solve.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1570 fd1b9c721ac7
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@966
     1
(*  Title:      HOL/IOA/meta_theory/Solve.thy
clasohm@966
     2
    ID:         $Id$
clasohm@966
     3
    Author:     Tobias Nipkow & Konrad Slind
clasohm@966
     4
    Copyright   1994  TU Muenchen
clasohm@966
     5
clasohm@966
     6
Weak possibilities mapping (abstraction)
clasohm@966
     7
*)
clasohm@966
     8
clasohm@966
     9
Solve = IOA +
clasohm@966
    10
clasohm@1570
    11
constdefs
clasohm@966
    12
clasohm@966
    13
  is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
clasohm@1151
    14
  "is_weak_pmap f C A ==                          
clasohm@1151
    15
   (!s:starts_of(C). f(s):starts_of(A)) &        
clasohm@1151
    16
   (!s t a. reachable C s &                      
clasohm@1151
    17
            (s,a,t):trans_of(C)                  
clasohm@1151
    18
            --> (if a:externals(asig_of(C)) then 
clasohm@1151
    19
                   (f(s),a,f(t)):trans_of(A)     
clasohm@1151
    20
                 else f(s)=f(t)))"
clasohm@966
    21
clasohm@966
    22
end