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