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