isabelle: src/HOL/Modelcheck/CTL.thy@61dd8c145da7 (annotated)

3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	1	(* Title: HOL/Modelcheck/CTL.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 CTL
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	7	imports MuCalculus
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
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	11	'a trans = "('a * 'a) set"
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 CEX :: "['a trans,'a pred, 'a]=>bool" where
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	14	"CEX N f u == (? v. (f v & (u,v):N))"
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 24327 diff changeset	15
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 24327 diff changeset	16	definition EG ::"['a trans,'a pred]=> 'a pred" where
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	17	"EG N f == nu (% Q. % u.(f u & CEX N Q u))"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	18
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	19	end

author	haftmann
	Fri, 11 Jun 2010 17:14:02 +0200
changeset 37407	61dd8c145da7
parent 35416	d8d7d1b785af
permissions	-rw-r--r--