isabelle: src/HOLCF/IOA/Storage/Correctness.thy@6597093b77e7 (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
6597093b77e7 GPLed; wenzelm parents: 6008 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	5
12218 6597093b77e7 GPLed; wenzelm parents: 6008 diff changeset	6	Correctness Proof.
6008 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
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	9	Correctness = SimCorrectness + Spec + Impl +
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	10
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	11	default term
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	12
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	13	consts
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	14
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	15	sim_relation :: "((nat * bool) * (nat set * bool)) set"
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	16
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	17	defs
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	18
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	19	sim_relation_def
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	20	"sim_relation == {qua. let c = fst qua; a = snd qua ;
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	21	k = fst c; b = snd c;
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	22	used = fst a; c = snd a
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	23	in
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	24	(! l:used. l < k) & b=c }"
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	25
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	26	end

author	wenzelm
	Thu, 15 Nov 2001 23:25:46 +0100
changeset 12218	6597093b77e7
parent 6008	d0e9b1619468
child 12338	de0f4a63baa5
permissions	-rw-r--r--