isabelle: src/HOL/Modelcheck/CTL.thy@6be7cf5086ab (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
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	7	CTL = MuCalculus +
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	8
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
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	13
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	14	consts
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	15
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	16	CEX ::"['a trans,'a pred, 'a]=>bool"
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	17	EG ::"['a trans,'a pred]=> 'a pred"
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	18
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	19
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	20
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	21	defs
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	22
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	23	CEX_def "CEX N f u == (? v. (f v & (u,v):N))"
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	24	EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	25
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	26
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	27
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	28
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	29
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	30
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	31	end

author	paulson
	Mon, 29 Sep 1997 11:46:33 +0200
changeset 3729	6be7cf5086ab
parent 3210	e80db1660614
child 3880	d93c62ec97a6
permissions	-rw-r--r--