src/HOL/Modelcheck/CTL.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 7295 fe09a0c5cebe
child 17272 c63e5220ed77
permissions -rw-r--r--
Constant "If" is now local
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
mueller@3210
     7
CTL = MuCalculus + 
mueller@3210
     8
mueller@3210
     9
mueller@3210
    10
types
mueller@3210
    11
  'a trans  = "('a * 'a) set"
mueller@3210
    12
mueller@3210
    13
consts
wenzelm@7295
    14
  CEX   ::"['a trans,'a pred, 'a]=>bool"
wenzelm@7295
    15
  EG    ::"['a trans,'a pred]=> 'a pred"
mueller@3210
    16
mueller@3210
    17
defs
wenzelm@7295
    18
  CEX_def  "CEX N f u == (? v. (f v & (u,v):N))"
wenzelm@7295
    19
  EG_def   "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
wenzelm@3882
    20
mueller@3210
    21
end