isabelle: src/HOLCF/IOA/ex/TrivEx.thy@a901bafe4578 (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$
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	3	Author: Olaf Mueller
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	4	Copyright 1995 TU Muenchen
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	5
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	6	Trivial Abstraction Example
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	TrivEx = Abstraction +
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
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
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	23	h_abs :: "nat => bool"
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	defs
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	C_asig_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	28	"C_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	29
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	30	C_trans_def "C_trans ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	31	{tr. let s = fst(tr);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	32	t = snd(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	33	in case fst(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	34	of
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	35	INC => t = Suc(s)}"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	36
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	37	C_ioa_def "C_ioa ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	38	(C_asig, {0}, C_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	39
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	40	A_asig_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	41	"A_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	42
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	43	A_trans_def "A_trans ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	44	{tr. let s = fst(tr);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	45	t = snd(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	46	in case fst(snd(tr))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	47	of
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	48	INC => t = True}"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	49
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	50	A_ioa_def "A_ioa ==
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	51	(A_asig, {False}, A_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	52
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	53	h_abs_def
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	54	"h_abs n == n~=0"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	55
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	56	rules
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	MC_result
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	59	"validIOA A_ioa (<>[] <%(b,a,c). b>)"
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	end

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 6470	f3015fd68d66
child 12218	6597093b77e7
permissions	-rw-r--r--