src/HOL/Modelcheck/EindhovenExample.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
mueller@6466
     1
(*  Title:      HOL/Modelcheck/EindhovenExample.thy
mueller@6466
     2
    ID:         $Id$
mueller@6466
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
mueller@6466
     4
    Copyright   1997  TU Muenchen
mueller@6466
     5
*)
mueller@6466
     6
wenzelm@17272
     7
theory EindhovenExample
wenzelm@17272
     8
imports EindhovenSyn CTL
wenzelm@17272
     9
begin
mueller@6466
    10
mueller@6466
    11
types
wenzelm@17272
    12
  state = "bool * bool * bool"
mueller@6466
    13
wenzelm@17272
    14
constdefs
wenzelm@17272
    15
  INIT :: "state pred"
wenzelm@17272
    16
  "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
mueller@6466
    17
wenzelm@17272
    18
  N :: "[state,state] => bool"
wenzelm@17272
    19
  "N == % (x1,x2,x3) (y1,y2,y3).
wenzelm@17272
    20
      (~x1 & ~x2 & ~x3 &   y1 & ~y2 & ~y3) |
wenzelm@17272
    21
      ( x1 & ~x2 & ~x3 &  ~y1 & ~y2 & ~y3) |
wenzelm@17272
    22
      ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)"
wenzelm@17272
    23
mueller@6466
    24
  reach:: "state pred"
wenzelm@17272
    25
  "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
mueller@6466
    26
wenzelm@17272
    27
lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)"
wenzelm@17272
    28
  by (simp add: INIT_def)
wenzelm@17272
    29
wenzelm@17272
    30
wenzelm@17272
    31
lemmas reach_rws = reach_def INIT_def N_def
mueller@6466
    32
wenzelm@17272
    33
lemma reach_ex: "reach (True, True, True)"
wenzelm@17272
    34
  apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *})
wenzelm@17272
    35
  txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *}
wenzelm@17272
    36
  pr (Eindhoven)
wenzelm@17272
    37
  txt {* actually invoke the model checker, try out after installing
wenzelm@17272
    38
    the model checker: see the README file *}
wenzelm@17272
    39
  apply (tactic {* mc_eindhoven_tac 1 *})
wenzelm@17272
    40
  done
mueller@6466
    41
mueller@6466
    42
end