src/HOL/IOA/Solve.thy
author mueller
Wed, 30 Apr 1997 11:56:17 +0200
changeset 3078 984866a8f905
child 4530 ac1821645636
permissions -rw-r--r--
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     1
(*  Title:      HOL/IOA/meta_theory/Solve.thy
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     2
    ID:         $Id$
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     4
    Copyright   1994  TU Muenchen
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     5
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     6
Weak possibilities mapping (abstraction)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     7
*)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     8
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     9
Solve = IOA +
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    10
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    11
constdefs
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    12
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    13
  is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    14
  "is_weak_pmap f C A ==                          
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    15
   (!s:starts_of(C). f(s):starts_of(A)) &        
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    16
   (!s t a. reachable C s &                      
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    17
            (s,a,t):trans_of(C)                  
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    18
            --> (if a:externals(asig_of(C)) then 
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    19
                   (f(s),a,f(t)):trans_of(A)     
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    20
                 else f(s)=f(t)))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    21
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    22
end