src/HOL/Modelcheck/MuckeExample1.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
     1 (*  Title:      HOL/Modelcheck/MuckeExample1.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 MuckeExample1 = MuckeSyn + 
     8 
     9 
    10 
    11 types
    12     state = "bool * bool * bool"
    13 
    14 consts
    15 
    16   INIT :: "state pred"
    17   N    :: "[state,state] => bool"
    18   reach:: "state pred"
    19 
    20 defs
    21   
    22   INIT_def "INIT x ==  ~(fst x)&~(fst (snd x))&~(snd (snd x))"
    23 
    24   N_def   "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));   
    25 	                  y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y)) 
    26                      in (~x1&~x2&~x3 & y1&~y2&~y3) |   
    27 	                (x1&~x2&~x3 & ~y1&~y2&~y3) |   
    28 	                (x1&~x2&~x3 & y1&y2&y3)    "
    29   
    30   reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
    31   
    32 
    33 end
    34