isabelle: src/HOL/Modelcheck/CTL.thy@70b2651af635 (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	consts
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 3882 diff changeset	14	CEX ::"['a trans,'a pred, 'a]=>bool"
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 3882 diff changeset	15	EG ::"['a trans,'a pred]=> 'a pred"
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	16
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	17	defs
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 3882 diff changeset	18	CEX_def "CEX N f u == (? v. (f v & (u,v):N))"
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 3882 diff changeset	19	EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
3882 6d7df9b98537 revert to 1.1; wenzelm parents: 3880 diff changeset	20
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	21	end

author	paulson
	Wed, 16 Jan 2002 17:53:22 +0100
changeset 12777	70b2651af635
parent 7295	fe09a0c5cebe
child 17272	c63e5220ed77
permissions	-rw-r--r--