src/HOL/IOA/Solve.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 4530 ac1821645636
child 17288 aa3833fb7bee
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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
Weak possibilities mapping (abstraction)
mueller@3078
     7
*)
mueller@3078
     8
mueller@3078
     9
Solve = IOA +
mueller@3078
    10
mueller@3078
    11
constdefs
mueller@3078
    12
mueller@3078
    13
  is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
mueller@3078
    14
  "is_weak_pmap f C A ==                          
mueller@3078
    15
   (!s:starts_of(C). f(s):starts_of(A)) &        
mueller@3078
    16
   (!s t a. reachable C s &                      
mueller@3078
    17
            (s,a,t):trans_of(C)                  
mueller@3078
    18
            --> (if a:externals(asig_of(C)) then 
mueller@3078
    19
                   (f(s),a,f(t)):trans_of(A)     
mueller@3078
    20
                 else f(s)=f(t)))"
mueller@3078
    21
mueller@3078
    22
end