isabelle: src/HOLCF/IOA/NTP/Correctness.thy@abf0f018b5ec (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/NTP/Correctness.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* The main correctness proof: Impl implements Spec *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Correctness
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Impl Spec
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	constdefs
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	hom :: "'m impl_state => 'm list"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
3898 f6bf42312e9e Simplified proof. nipkow parents: 3073 diff changeset	15	else tl(sq(sen s)))"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	17	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	18
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	end

author	wenzelm
	Sat, 14 Jan 2006 22:25:34 +0100
changeset 18688	abf0f018b5ec
parent 17244	0b2ff9541727
child 19739	c58ef2aa5430
permissions	-rw-r--r--