src/HOL/Modelcheck/MuckeExample1.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 17272 c63e5220ed77 child 35416 d8d7d1b785af permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
```     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 theory MuckeExample1
```
```     8 imports MuckeSyn
```
```     9 begin
```
```    10
```
```    11 types
```
```    12   state = "bool * bool * bool"
```
```    13
```
```    14 constdefs
```
```    15   INIT :: "state pred"
```
```    16   "INIT x ==  ~(fst x)&~(fst (snd x))&~(snd (snd x))"
```
```    17   N    :: "[state,state] => bool"
```
```    18   "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
```
```    19                 y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
```
```    20             in (~x1&~x2&~x3 & y1&~y2&~y3) |
```
```    21                (x1&~x2&~x3 & ~y1&~y2&~y3) |
```
```    22                (x1&~x2&~x3 & y1&y2&y3)"
```
```    23   reach:: "state pred"
```
```    24   "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
```
```    25
```
```    26 lemmas reach_rws = INIT_def N_def reach_def
```
```    27
```
```    28 lemma reach_ex1: "reach (True,True,True)"
```
```    29   apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *})
```
```    30   apply (tactic {* mc_mucke_tac [] 1 *})
```
```    31   done
```
```    32
```
```    33 (*alternative*)
```
```    34 lemma reach_ex' "reach (True,True,True)"
```
```    35   by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *})
```
```    36
```
```    37 end
```