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

author	wenzelm
	Thu, 15 Nov 2001 23:25:46 +0100
changeset 12218	6597093b77e7
parent 6470	f3015fd68d66
child 14981	e73f8140af78
permissions	-rw-r--r--