IOA/example/Correctness.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
Correctness = Solve + Impl + Spec + "Lemmas" +
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     2
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     3
consts
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     4
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     5
hom :: "'m impl_state => 'm list"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     6
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     7
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     8
rules
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     9
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    10
hom_def 
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    11
"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)),  \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    12
\                          sq(sen(s)),                   \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    13
\                          ttl(sq(sen(s))))"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    14
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    15
end