src/HOL/Modelcheck/EindhovenExample.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17272 c63e5220ed77 child 35416 d8d7d1b785af permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     1 (*  Title:      HOL/Modelcheck/EindhovenExample.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
```
```     4     Copyright   1997  TU Muenchen
```
```     5 *)
```
```     6
```
```     7 theory EindhovenExample
```
```     8 imports EindhovenSyn CTL
```
```     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
```
```    18   N :: "[state,state] => bool"
```
```    19   "N == % (x1,x2,x3) (y1,y2,y3).
```
```    20       (~x1 & ~x2 & ~x3 &   y1 & ~y2 & ~y3) |
```
```    21       ( x1 & ~x2 & ~x3 &  ~y1 & ~y2 & ~y3) |
```
```    22       ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)"
```
```    23
```
```    24   reach:: "state pred"
```
```    25   "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
```
```    26
```
```    27 lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)"
```
```    28   by (simp add: INIT_def)
```
```    29
```
```    30
```
```    31 lemmas reach_rws = reach_def INIT_def N_def
```
```    32
```
```    33 lemma reach_ex: "reach (True, True, True)"
```
```    34   apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *})
```
```    35   txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *}
```
```    36   pr (Eindhoven)
```
```    37   txt {* actually invoke the model checker, try out after installing
```
```    38     the model checker: see the README file *}
```
```    39   apply (tactic {* mc_eindhoven_tac 1 *})
```
```    40   done
```
```    41
```
```    42 end
```