isabelle: src/HOLCF/IOA/ex/TrivEx.thy@ae5bb6001afb (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	*)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* Trivial Abstraction Example *}
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 TrivEx
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Abstraction
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
6470 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	datatype action = INC
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	consts
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	15
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	16	C_asig :: "action signature"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	17	C_trans :: "(action, nat)transition set"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	18	C_ioa :: "(action, nat)ioa"
6470 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"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	A_trans :: "(action, bool)transition set"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	22	A_ioa :: "(action, bool)ioa"
6470 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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	28	C_asig_def:
6470 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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	31	C_trans_def: "C_trans ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	32	{tr. let s = fst(tr);
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	33	t = snd(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	34	in case fst(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	35	of
6470 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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	38	C_ioa_def: "C_ioa ==
6470 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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	41	A_asig_def:
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	42	"A_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	43
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	44	A_trans_def: "A_trans ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	45	{tr. let s = fst(tr);
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	46	t = snd(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	47	in case fst(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	48	of
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	49	INC => t = True}"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	50
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	51	A_ioa_def: "A_ioa ==
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	52	(A_asig, {False}, A_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	53
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	54	h_abs_def:
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	55	"h_abs n == n~=0"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	56
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	57	axioms
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	58
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	59	MC_result:
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	60	"validIOA A_ioa (<>[] <%(b,a,c). b>)"
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	61
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	62	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	63
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	64	end

author	paulson
	Tue, 20 Sep 2005 18:43:39 +0200
changeset 17525	ae5bb6001afb
parent 17244	0b2ff9541727
child 19740	6b38551d0798
permissions	-rw-r--r--