src/HOL/Modelcheck/MuckeExample2.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
mueller@6466
     1
(*  Title:      HOL/Modelcheck/MuckeExample2.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 MuckeExample2
wenzelm@17272
     8
imports MuckeSyn
wenzelm@17272
     9
begin
mueller@6466
    10
wenzelm@17272
    11
constdefs
wenzelm@17272
    12
  Init  :: "bool pred"
wenzelm@17272
    13
  "Init x == x"
wenzelm@17272
    14
  R     :: "[bool,bool] => bool"
wenzelm@17272
    15
  "R x y == (x & ~y) | (~x & y)"
wenzelm@17272
    16
  Reach :: "bool pred"
wenzelm@17272
    17
  "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
wenzelm@17272
    18
  Reach2:: "bool pred"
wenzelm@17272
    19
  "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
mueller@6466
    20
wenzelm@17272
    21
lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
mueller@6466
    22
wenzelm@17272
    23
lemma Reach: "Reach2 True"
wenzelm@17272
    24
  apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
wenzelm@17272
    25
  apply (tactic {* mc_mucke_tac [] 1 *})
wenzelm@17272
    26
  done
mueller@6466
    27
wenzelm@17272
    28
(*alternative:*)
wenzelm@17272
    29
lemma Reach': "Reach2 True"
wenzelm@17272
    30
  by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
wenzelm@17272
    31
wenzelm@17272
    32
end