src/HOL/Modelcheck/MuckeExample2.thy
author wenzelm
Thu, 30 Nov 2000 20:04:16 +0100
changeset 10548 e8c774c12105
parent 6466 2eba94dc5951
child 17272 c63e5220ed77
permissions -rw-r--r--
'consumes' att;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6466
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/Modelcheck/MuckeExample2.thy
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     2
    ID:         $Id$
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     4
    Copyright   1997  TU Muenchen
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     5
*)
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     6
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     7
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     8
MuckeExample2 = MuckeSyn +
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     9
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    10
consts
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    11
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    12
  Init  :: "bool pred"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    13
  R	:: "[bool,bool] => bool"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    14
  Reach	:: "bool pred"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    15
  Reach2:: "bool pred"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    16
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    17
defs
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    18
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    19
  Init_def " Init x == x"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    20
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    21
  R_def "R x y == (x & ~y) | (~x & y)"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    22
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    23
  Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    24
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    25
  Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    26
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    27
end