src/HOL/IOA/meta_theory/Solve.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1570 fd1b9c721ac7
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
     1 (*  Title:      HOL/IOA/meta_theory/Solve.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 
     6 Weak possibilities mapping (abstraction)
     7 *)
     8 
     9 Solve = IOA +
    10 
    11 constdefs
    12 
    13   is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
    14   "is_weak_pmap f C A ==                          
    15    (!s:starts_of(C). f(s):starts_of(A)) &        
    16    (!s t a. reachable C s &                      
    17             (s,a,t):trans_of(C)                  
    18             --> (if a:externals(asig_of(C)) then 
    19                    (f(s),a,f(t)):trans_of(A)     
    20                  else f(s)=f(t)))"
    21 
    22 end