isabelle: src/HOL/Modelcheck/MuCalculus.thy@3489daf839d5 (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	Author: Olaf Mueller, Jan Philipps, Robert Sandner
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	3	Copyright 1997 TU Muenchen
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	4	*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	5
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	6	theory MuCalculus
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	7	imports Main
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	8	begin
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	9
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	10	types
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 3842 diff changeset	11	'a pred = "'a=>bool"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	12
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 24327 diff changeset	13	definition Charfun :: "'a set => 'a pred" where
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	14	"Charfun == (% A.% x. x:A)"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	15
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 24327 diff changeset	16	definition monoP :: "('a pred => 'a pred) => bool" where
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	17	"monoP f == mono(Collect o f o Charfun)"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	18
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 24327 diff changeset	19	definition mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10) where
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	20	"mu f == Charfun(lfp(Collect o f o Charfun))"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	21
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 24327 diff changeset	22	definition nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10) where
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	23	"nu f == Charfun(gfp(Collect o f o Charfun))"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	24
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	25	end

author	haftmann
	Mon, 12 Jul 2010 08:58:12 +0200
changeset 37764	3489daf839d5
parent 35416	d8d7d1b785af
permissions	-rw-r--r--