isabelle: src/HOL/Modelcheck/MuckeExample2.thy@35815ce9218a (annotated)

6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	1	(* Title: HOL/Modelcheck/MuckeExample2.thy
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	2	ID: $Id$
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	3	Author: Olaf Mueller, Jan Philipps, Robert Sandner
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	4	Copyright 1997 TU Muenchen
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	5	*)
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	6
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	7	theory MuckeExample2
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	8	imports MuckeSyn
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	9	begin
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	10
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 17272 diff changeset	11	definition Init :: "bool pred" where
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	12	"Init x == x"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	13	R :: "[bool,bool] => bool"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	14	"R x y == (x & ~y) \| (~x & y)"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	15	Reach :: "bool pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	16	"Reach == mu (%Q x. Init x \| (? y. Q y & R y x))"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	17	Reach2:: "bool pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	18	"Reach2 == mu (%Q x. Reach x \| (? y. Q y & R y x))"
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	19
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	20	lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	21
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	22	lemma Reach: "Reach2 True"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	23	apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	24	apply (tactic {* mc_mucke_tac [] 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	25	done
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	26
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	27	(alternative:)
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	28	lemma Reach': "Reach2 True"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	29	by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	30
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	31	end

author	wenzelm
	Mon, 21 Jun 2010 11:24:19 +0200
changeset 37380	35815ce9218a
parent 35416	d8d7d1b785af
permissions	-rw-r--r--