isabelle: src/HOL/Modelcheck/CTL.thy@c1b6cc29496b (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
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	20	end

author	haftmann
	Fri, 23 Oct 2009 17:12:47 +0200
changeset 33085	c1b6cc29496b
parent 24327	a207114007c6
child 35416	d8d7d1b785af
permissions	-rw-r--r--