isabelle: src/HOL/Modelcheck/MuckeExample2.thy@c1b6cc29496b (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
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	11	constdefs
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	12	Init :: "bool pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	13	"Init x == x"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	14	R :: "[bool,bool] => bool"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	15	"R x y == (x & ~y) \| (~x & y)"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	16	Reach :: "bool pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	17	"Reach == mu (%Q x. Init x \| (? y. Q y & R y x))"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	18	Reach2:: "bool pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	19	"Reach2 == mu (%Q x. Reach x \| (? y. Q y & R y x))"
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	20
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	21	lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	22
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	23	lemma Reach: "Reach2 True"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	24	apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	25	apply (tactic {* mc_mucke_tac [] 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	26	done
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	27
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	28	(alternative:)
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	29	lemma Reach': "Reach2 True"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	30	by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	31
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	32	end

author	haftmann
	Fri, 23 Oct 2009 17:12:47 +0200
changeset 33085	c1b6cc29496b
parent 17272	c63e5220ed77
child 35416	d8d7d1b785af
permissions	-rw-r--r--