src/HOL/Modelcheck/CTL.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17272 c63e5220ed77
child 24327 a207114007c6
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
mueller@3210
     1
(*  Title:      HOL/Modelcheck/CTL.thy
mueller@3210
     2
    ID:         $Id$
mueller@3210
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
mueller@3210
     4
    Copyright   1997  TU Muenchen
mueller@3210
     5
*)
mueller@3210
     6
wenzelm@17272
     7
theory CTL
wenzelm@17272
     8
imports MuCalculus
wenzelm@17272
     9
begin
mueller@3210
    10
mueller@3210
    11
types
mueller@3210
    12
  'a trans  = "('a * 'a) set"
mueller@3210
    13
wenzelm@17272
    14
constdefs
wenzelm@17272
    15
  CEX ::"['a trans,'a pred, 'a]=>bool"
wenzelm@17272
    16
  "CEX N f u == (? v. (f v & (u,v):N))"
wenzelm@17272
    17
  EG ::"['a trans,'a pred]=> 'a pred"
wenzelm@17272
    18
  "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
mueller@3210
    19
wenzelm@17272
    20
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@3882
    21
mueller@3210
    22
end