isabelle: src/HOLCF/IOA/Storage/Correctness.thy@fb65eda72fc7 (annotated)

6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	1	(* Title: HOL/IOA/example/Correctness.thy
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 6008 diff changeset	3	Author: Olaf M�ller
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	4
12218 6597093b77e7 GPLed; wenzelm parents: 6008 diff changeset	5	Correctness Proof.
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	6	*)
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	7
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	8	Correctness = SimCorrectness + Spec + Impl +
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	9
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 12218 diff changeset	10	default type
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	11
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	12	consts
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	13
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	14	sim_relation :: "((nat * bool) * (nat set * bool)) set"
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	15
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	16	defs
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	17
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	18	sim_relation_def
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	19	"sim_relation == {qua. let c = fst qua; a = snd qua ;
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	20	k = fst c; b = snd c;
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	21	used = fst a; c = snd a
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	22	in
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	23	(! l:used. l < k) & b=c }"
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	24
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	25	end

author	wenzelm
	Sun, 28 Aug 2005 16:04:44 +0200
changeset 17160	fb65eda72fc7
parent 14981	e73f8140af78
child 17244	0b2ff9541727
permissions	-rw-r--r--