Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Modelcheck/MuckeExample2.thy
author haftmann
Wed, 30 Jan 2008 10:57:44 +0100
changeset 26013 8764a1f1253b
parent 17272 c63e5220ed77
child 35416 d8d7d1b785af
permissions -rw-r--r--
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices

(*  Title:      HOL/Modelcheck/MuckeExample2.thy
    ID:         $Id$
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
    Copyright   1997  TU Muenchen
*)

theory MuckeExample2
imports MuckeSyn
begin

constdefs
  Init  :: "bool pred"
  "Init x == x"
  R     :: "[bool,bool] => bool"
  "R x y == (x & ~y) | (~x & y)"
  Reach :: "bool pred"
  "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
  Reach2:: "bool pred"
  "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"

lemmas Reach_rws = Init_def R_def Reach_def Reach2_def

lemma Reach: "Reach2 True"
  apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
  apply (tactic {* mc_mucke_tac [] 1 *})
  done

(*alternative:*)
lemma Reach': "Reach2 True"
  by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})

end
isabelle