Old_HOL: IOA/example/Correctness.thy@f04b33ce250f (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
249 492493334e0f removed \...\ inside strings clasohm parents: 168 diff changeset	18	"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)),
492493334e0f removed \...\ inside strings clasohm parents: 168 diff changeset	19	sq(sen(s)),
492493334e0f removed \...\ inside strings clasohm parents: 168 diff changeset	20	ttl(sq(sen(s))))"
156 fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	21
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	22	end

author	clasohm
	Tue, 24 Oct 1995 14:59:17 +0100
changeset 251	f04b33ce250f
parent 249	492493334e0f
permissions	-rw-r--r--