isabelle: src/HOLCF/IOA/meta_theory/RefCorrectness.thy@ff24ac6678dd (annotated)

3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	1	(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy
3275 3f53f2c876f4 changes for release 94-8 mueller parents: 3071 diff changeset	2	ID: $Id$
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	3	Author: Olaf Mueller
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	4	Copyright 1996 TU Muenchen
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	5
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	6	Correctness of Refinement Mappings in HOLCF/IOA
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	7	*)
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	8
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	9
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	10	RefCorrectness = RefMappings +
3433 2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	11
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	12	consts
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	13
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	14	corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) =>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	15	('a,'s1)execution => ('a,'s2)execution"
3433 2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	16	corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	17	-> ('s1 => ('a,'s2)pairs)"
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	18	is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool"
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	19
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	20	defs
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	21
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	22	corresp_ex_def
3433 2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	23	"corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))"
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	24
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	25
3433 2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	26	corresp_exC_def
2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	27	"corresp_exC A f == (fix`(LAM h ex. (%s. case ex of
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	28	nil => nil
3433 2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	29	\| x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	30	@@ ((h`xs) (snd pr)))
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	31	`x) )))"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	32
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	33	is_fair_ref_map_def
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	34	"is_fair_ref_map f C A ==
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	35	is_ref_map f C A &
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	36	(! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	37
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	38
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	39
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	40	rules
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	41	(* Axioms for fair trace inclusion proof support, not for the correctness proof
5976 44290b71a85f tuning to assimiliate it with PhD; mueller parents: 4559 diff changeset	42	of refinement mappings !
44290b71a85f tuning to assimiliate it with PhD; mueller parents: 4559 diff changeset	43	Note: Everything is superseded by LiveIOA.thy! *)
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	44
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	45	corresp_laststate
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	46	"Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	47
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	48	corresp_Finite
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	49	"Finite (snd (corresp_ex A f (s,ex))) = Finite ex"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	50
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	51	FromAtoC
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	52	"fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	53
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	54	FromCtoA
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	55	"inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	56
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	57
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	58	(* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	59	an index i from which on no W in ex. But W inf enabled, ie at least once after i
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	60	W is enabled. As W does not occur after i and W is enabling_persistent, W keeps
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	61	enabled until infinity, ie. indefinitely *)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	62	persistent
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	63	"[\|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W\|]
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	64	==> inf_often (%x. fst x :W) ex \| fin_often (%x. ~Enabled A W (snd x)) ex"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	65
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	66	infpostcond
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	67	"[\| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex\|]
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	68	==> inf_often (% x. set_was_enabled A W (snd x)) ex"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: 3433 diff changeset	69
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	70	end

author	nipkow
	Wed, 22 Nov 2000 13:16:55 +0100
changeset 10509	ff24ac6678dd
parent 5976	44290b71a85f
child 10835	f4745d77e620
permissions	-rw-r--r--