isabelle: src/HOLCF/IOA/ABP/Correctness.thy@fc385ce6187d (annotated)

3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/ABP/Correctness.thy
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 5192 diff changeset	3	Author: Olaf M�ller
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* The main correctness proof: System_fin implements System *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
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 IOA Env Impl Impl_finite
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	consts
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	reduce :: "'a list => 'a list"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	abs :: 'c
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	system_ioa :: "('m action, bool * 'm impl_state)ioa"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	19
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20	primrec
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	reduce_Nil: "reduce [] = []"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	22	reduce_Cons: "reduce(x#xs) =
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	23	(case xs of
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	[] => [x]
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	25	\| y#ys => (if (x=y)
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	26	then reduce xs
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27	else (x#(reduce xs))))"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	29
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	defs
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	31
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	32	system_def:
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	"system_ioa == (env_ioa \|\| impl_ioa)"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	35	system_fin_def:
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36	"system_fin_ioa == (env_ioa \|\| impl_fin_ioa)"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	37
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	38	abs_def: "abs ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	39	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	40	(reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	42	axioms
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	43
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	44	sys_IOA: "IOA system_ioa"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	45	sys_fin_IOA: "IOA system_fin_ioa"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	46
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	47	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	48
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	49	end

author	aspinall
	Fri, 30 Sep 2005 18:18:34 +0200
changeset 17740	fc385ce6187d
parent 17244	0b2ff9541727
child 19689	a3a8594e19b4
permissions	-rw-r--r--