src/HOL/IOA/Solve.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 4530 ac1821645636
child 17288 aa3833fb7bee
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/IOA/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