IOA/meta_theory/Solve.thy
author clasohm
Wed, 02 Nov 1994 11:50:09 +0100
changeset 156 fd1be45b64bf
child 168 44ff2275d44f
permissions -rw-r--r--
added IOA to isabelle/HOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
156
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     1
(* Methods of proof for IOA. *)
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     2
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     3
Solve = IOA +
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     4
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     5
consts
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     6
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     7
  is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     8
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     9
rules
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    10
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    11
is_weak_pmap_def
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    12
  "is_weak_pmap(f,C,A) ==                           \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    13
\   (!s:starts_of(C). f(s):starts_of(A)) &        \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    14
\   (!s t a. reachable(C,s) &                       \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    15
\            <s,a,t>:trans_of(C)                    \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    16
\            --> if(a:externals(asig_of(C)),        \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    17
\                   <f(s),a,f(t)>:trans_of(A),      \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    18
\                   f(s)=f(t)))"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    19
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    20
end