isabelle: src/HOLCF/IOA/NTP/Correctness.thy@f08ea8e964d8 (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
12218 6597093b77e7 GPLed; wenzelm parents: 4816 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
12218 6597093b77e7 GPLed; wenzelm parents: 4816 diff changeset	6	The main correctness proof: Impl implements Spec.
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8
4816 64f075872f69 simplification of explicit theory usage and merges oheimb parents: 3898 diff changeset	9	Correctness = Impl + Spec +
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	constdefs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	hom :: 'm impl_state => 'm list
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: 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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	end

author	streckem
	Tue, 30 Mar 2004 19:33:57 +0200
changeset 14499	f08ea8e964d8
parent 12218	6597093b77e7
child 14981	e73f8140af78
permissions	-rw-r--r--