isabelle: src/HOL/Modelcheck/CTL.thy@1f2d94b6a8ef (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	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 CTL
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	8	imports MuCalculus
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
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	12	'a trans = "('a * 'a) set"
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
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	15	CEX ::"['a trans,'a pred, 'a]=>bool"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	16	"CEX N f u == (? v. (f v & (u,v):N))"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	17	EG ::"['a trans,'a pred]=> 'a pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	18	"EG N f == nu (% Q. % u.(f u & CEX N Q u))"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	19
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 7295 diff changeset	20	ML {* use_legacy_bindings (the_context ()) *}
3882 6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	21
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	22	end

author	webertj
	Fri, 01 Jun 2007 23:21:40 +0200
changeset 23193	1f2d94b6a8ef
parent 17272	c63e5220ed77
child 24327	a207114007c6
permissions	-rw-r--r--