src/HOL/Modelcheck/MuckeExample2.thy
author wenzelm
Tue Sep 06 16:24:53 2005 +0200 (2005-09-06)
changeset 17272 c63e5220ed77
parent 6466 2eba94dc5951
child 35416 d8d7d1b785af
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      HOL/Modelcheck/MuckeExample2.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 theory MuckeExample2
     8 imports MuckeSyn
     9 begin
    10 
    11 constdefs
    12   Init  :: "bool pred"
    13   "Init x == x"
    14   R     :: "[bool,bool] => bool"
    15   "R x y == (x & ~y) | (~x & y)"
    16   Reach :: "bool pred"
    17   "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
    18   Reach2:: "bool pred"
    19   "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
    20 
    21 lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
    22 
    23 lemma Reach: "Reach2 True"
    24   apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
    25   apply (tactic {* mc_mucke_tac [] 1 *})
    26   done
    27 
    28 (*alternative:*)
    29 lemma Reach': "Reach2 True"
    30   by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
    31 
    32 end