src/HOL/Modelcheck/MuckeExample2.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 6466 2eba94dc5951
child 17272 c63e5220ed77
permissions -rw-r--r--
Constant "If" is now local
mueller@6466
     1
(*  Title:      HOL/Modelcheck/MuckeExample2.thy
mueller@6466
     2
    ID:         $Id$
mueller@6466
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
mueller@6466
     4
    Copyright   1997  TU Muenchen
mueller@6466
     5
*)
mueller@6466
     6
mueller@6466
     7
mueller@6466
     8
MuckeExample2 = MuckeSyn +
mueller@6466
     9
mueller@6466
    10
consts
mueller@6466
    11
mueller@6466
    12
  Init  :: "bool pred"
mueller@6466
    13
  R	:: "[bool,bool] => bool"
mueller@6466
    14
  Reach	:: "bool pred"
mueller@6466
    15
  Reach2:: "bool pred"
mueller@6466
    16
mueller@6466
    17
defs
mueller@6466
    18
mueller@6466
    19
  Init_def " Init x == x"
mueller@6466
    20
mueller@6466
    21
  R_def "R x y == (x & ~y) | (~x & y)"
mueller@6466
    22
mueller@6466
    23
  Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
mueller@6466
    24
mueller@6466
    25
  Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
mueller@6466
    26
mueller@6466
    27
end