isabelle: src/HOLCF/IOA/Storage/Correctness.thy@aa27c10a040e (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	*)
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* Correctness Proof *}
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	7
17244 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 SimCorrectness Spec Impl
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	11
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	defaultsort type
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	13
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	constdefs
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15	sim_relation :: "((nat * bool) * (nat set * bool)) set"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	16	"sim_relation == {qua. let c = fst qua; a = snd qua ;
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	17	k = fst c; b = snd c;
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	18	used = fst a; c = snd a
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	19	in
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	20	(! l:used. l < k) & b=c }"
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	21
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	22	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	23
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	end

author	paulson
	Wed, 14 Dec 2005 16:13:09 +0100
changeset 18404	aa27c10a040e
parent 17244	0b2ff9541727
child 19740	6b38551d0798
permissions	-rw-r--r--