src/HOL/Modelcheck/MuckeExample1.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/MuckeExample1.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 MuckeExample1
wenzelm@17272
     8
imports MuckeSyn
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))"
wenzelm@17272
    17
  N    :: "[state,state] => bool"
wenzelm@17272
    18
  "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
wenzelm@17272
    19
                y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
wenzelm@17272
    20
            in (~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
  reach:: "state pred"
wenzelm@17272
    24
  "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
mueller@6466
    25
wenzelm@17272
    26
lemmas reach_rws = INIT_def N_def reach_def
wenzelm@17272
    27
wenzelm@17272
    28
lemma reach_ex1: "reach (True,True,True)"
wenzelm@17272
    29
  apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *})
wenzelm@17272
    30
  apply (tactic {* mc_mucke_tac [] 1 *})
wenzelm@17272
    31
  done
wenzelm@17272
    32
wenzelm@17272
    33
(*alternative*)
wenzelm@17272
    34
lemma reach_ex' "reach (True,True,True)"
wenzelm@17272
    35
  by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *})
mueller@6466
    36
mueller@6466
    37
end