isabelle: src/HOLCF/IOA/Storage/Correctness.thy@c7df55158574 (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$
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	3	Author: Olaf Mueller
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	4	Copyright 1997 TU Muenchen
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	5
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	6	Correctness Proof
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
	Fri, 05 Oct 2001 21:49:59 +0200
changeset 11699	c7df55158574
parent 6008	d0e9b1619468
child 12218	6597093b77e7
permissions	-rw-r--r--