Old_HOL: IOA/example/Correctness.thy@44ff2275d44f (annotated)

168 44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	1	(* Title: HOL/IOA/example/Correctness.thy
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	2	ID: $Id$
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	3	Author: Tobias Nipkow & Konrad Slind
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	4	Copyright 1994 TU Muenchen
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	5
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	6	The main correctness proof: Impl implements Spec
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	7	*)
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	8
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	9	Correctness = Solve + Impl + Spec +
156 fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	10
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	11	consts
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	12
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	13	hom :: "'m impl_state => 'm list"
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	14
168 44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	15	defs
156 fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	16
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	17	hom_def
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	18	"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	19	\ sq(sen(s)), \
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	20	\ ttl(sq(sen(s))))"
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	21
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	22	end

author	nipkow
	Wed, 09 Nov 1994 19:51:09 +0100
changeset 168	44ff2275d44f
parent 156	fd1be45b64bf
child 249	492493334e0f
permissions	-rw-r--r--