src/HOL/Modelcheck/MuckeExample2.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/MuckeExample2.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
```
```     4     Copyright   1997  TU Muenchen
```
```     5 *)
```
```     6
```
```     7 theory MuckeExample2
```
```     8 imports MuckeSyn
```
```     9 begin
```
```    10
```
```    11 constdefs
```
```    12   Init  :: "bool pred"
```
```    13   "Init x == x"
```
```    14   R     :: "[bool,bool] => bool"
```
```    15   "R x y == (x & ~y) | (~x & y)"
```
```    16   Reach :: "bool pred"
```
```    17   "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
```
```    18   Reach2:: "bool pred"
```
```    19   "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
```
```    20
```
```    21 lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
```
```    22
```
```    23 lemma Reach: "Reach2 True"
```
```    24   apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
```
```    25   apply (tactic {* mc_mucke_tac [] 1 *})
```
```    26   done
```
```    27
```
```    28 (*alternative:*)
```
```    29 lemma Reach': "Reach2 True"
```
```    30   by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
```
```    31
```
```    32 end
```