src/HOL/Modelcheck/EindhovenExample.thy
 author haftmann Mon Mar 01 13:40:23 2010 +0100 (2010-03-01) changeset 35416 d8d7d1b785af parent 17272 c63e5220ed77 permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
```     1 (*  Title:      HOL/Modelcheck/EindhovenExample.thy
```
```     2     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
```
```     3     Copyright   1997  TU Muenchen
```
```     4 *)
```
```     5
```
```     6 theory EindhovenExample
```
```     7 imports EindhovenSyn CTL
```
```     8 begin
```
```     9
```
```    10 types
```
```    11   state = "bool * bool * bool"
```
```    12
```
```    13 definition INIT :: "state pred" where
```
```    14   "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
```
```    15
```
```    16 definition N :: "[state,state] => bool" where
```
```    17   "N == % (x1,x2,x3) (y1,y2,y3).
```
```    18       (~x1 & ~x2 & ~x3 &   y1 & ~y2 & ~y3) |
```
```    19       ( x1 & ~x2 & ~x3 &  ~y1 & ~y2 & ~y3) |
```
```    20       ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)"
```
```    21
```
```    22 definition reach:: "state pred" where
```
```    23   "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
```
```    24
```
```    25 lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)"
```
```    26   by (simp add: INIT_def)
```
```    27
```
```    28
```
```    29 lemmas reach_rws = reach_def INIT_def N_def
```
```    30
```
```    31 lemma reach_ex: "reach (True, True, True)"
```
```    32   apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *})
```
```    33   txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *}
```
```    34   pr (Eindhoven)
```
```    35   txt {* actually invoke the model checker, try out after installing
```
```    36     the model checker: see the README file *}
```
```    37   apply (tactic {* mc_eindhoven_tac 1 *})
```
```    38   done
```
```    39
```
```    40 end
```