isabelle: src/HOL/Modelcheck/MuCalculus.thy@d5f39173444c (annotated)

3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	1	(* Title: HOL/Modelcheck/MuCalculus.thy
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	2	ID: $Id$
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	3	Author: Olaf Mueller, Jan Philipps, Robert Sandner
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	4	Copyright 1997 TU Muenchen
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	5	*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	6
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	7	theory MuCalculus
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	8	imports Main
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	9	begin
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	10
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	11	types
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 3842 diff changeset	12	'a pred = "'a=>bool"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	13
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	14	constdefs
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	15	Charfun :: "'a set => 'a pred"
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	16	"Charfun == (% A.% x. x:A)"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	17
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	18	monoP :: "('a pred => 'a pred) => bool"
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	19	"monoP f == mono(Collect o f o Charfun)"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	20
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	21	mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	22	"mu f == Charfun(lfp(Collect o f o Charfun))"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	23
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	24	nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	25	"nu f == Charfun(gfp(Collect o f o Charfun))"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	26
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	27	end

author	haftmann
	Mon, 29 Sep 2008 12:31:58 +0200
changeset 28401	d5f39173444c
parent 24327	a207114007c6
child 35416	d8d7d1b785af
permissions	-rw-r--r--