src/HOL/Modelcheck/MuckeExample1.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/MuckeExample1.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
MuckeExample1 = MuckeSyn + 
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     8
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
     9
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    10
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    11
types
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    12
    state = "bool * bool * bool"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    13
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    14
consts
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    15
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    16
  INIT :: "state pred"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    17
  N    :: "[state,state] => bool"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    18
  reach:: "state pred"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    19
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    20
defs
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    21
  
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    22
  INIT_def "INIT x ==  ~(fst x)&~(fst (snd x))&~(snd (snd x))"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    23
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    24
  N_def   "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));   
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    25
	                  y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y)) 
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    26
                     in (~x1&~x2&~x3 & y1&~y2&~y3) |   
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    27
	                (x1&~x2&~x3 & ~y1&~y2&~y3) |   
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    28
	                (x1&~x2&~x3 & y1&y2&y3)    "
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    29
  
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    30
  reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    31
  
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    32
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    33
end
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff changeset
    34