isabelle: src/HOL/Modelcheck/CTL.thy@97601cf26262 (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
3882 6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	23	CEX_def "CEX N f u == (? v. (f v & (u,v):N))"
6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	24	EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	25
6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	26
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	27
3882 6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	28
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	29
3882 6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	30
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	31	end

author	paulson
	Thu, 20 Nov 1997 11:03:26 +0100
changeset 4242	97601cf26262
parent 3882	6d7df9b98537
child 7295	fe09a0c5cebe
permissions	-rw-r--r--