isabelle: src/HOLCF/IOA/ex/TrivEx2.thy@6edb84c661dd (annotated)

6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/TrivEx.thy
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 6470 diff changeset	3	Author: Olaf M�ller
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	4
12218 6597093b77e7 GPLed; wenzelm parents: 6470 diff changeset	5	Trivial Abstraction Example with fairness.
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	6	*)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	7
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	8	TrivEx2 = Abstraction + IOA +
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	9
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	10	datatype action = INC
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	11
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	12	consts
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	13
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	14	C_asig :: "action signature"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	15	C_trans :: (action, nat)transition set
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	16	C_ioa :: (action, nat)ioa
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	17	C_live_ioa :: (action, nat)live_ioa
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	18
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	19	A_asig :: "action signature"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	20	A_trans :: (action, bool)transition set
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	21	A_ioa :: (action, bool)ioa
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	22	A_live_ioa :: (action, bool)live_ioa
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	23
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	24	h_abs :: "nat => bool"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	25
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	26	defs
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	27
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	28	C_asig_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	29	"C_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	30
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	31	C_trans_def "C_trans ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	32	{tr. let s = fst(tr);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	33	t = snd(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	34	in case fst(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	35	of
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	36	INC => t = Suc(s)}"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	37
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	38	C_ioa_def "C_ioa ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	39	(C_asig, {0}, C_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	40
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	41	C_live_ioa_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	42	"C_live_ioa == (C_ioa, WF C_ioa {INC})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	43
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	44	A_asig_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	45	"A_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	46
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	47	A_trans_def "A_trans ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	48	{tr. let s = fst(tr);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	49	t = snd(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	50	in case fst(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	51	of
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	52	INC => t = True}"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	53
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	54	A_ioa_def "A_ioa ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	55	(A_asig, {False}, A_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	56
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	57	A_live_ioa_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	58	"A_live_ioa == (A_ioa, WF A_ioa {INC})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	59
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	60
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	61
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	62	h_abs_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	63	"h_abs n == n~=0"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	64
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	65	rules
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	66
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	67	MC_result
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	68	"validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	69
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	70	end

author	quigley
	Fri, 02 Sep 2005 21:29:55 +0200
changeset 17236	6edb84c661dd
parent 14981	e73f8140af78
child 17244	0b2ff9541727
permissions	-rw-r--r--