isabelle: src/HOL/Modelcheck/MuckeExample1.thy@de6285ebcc05 (annotated)

6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	1	(* Title: HOL/Modelcheck/MuckeExample1.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 MuckeExample1
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
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	11	types
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	12	state = "bool * bool * bool"
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	13
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	14	constdefs
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	15	INIT :: "state pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	16	"INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	17	N :: "[state,state] => bool"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	18	"N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	19	y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	20	in (~x1&~x2&~x3 & y1&~y2&~y3) \|
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	21	(x1&~x2&~x3 & ~y1&~y2&~y3) \|
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	22	(x1&~x2&~x3 & y1&y2&y3)"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	23	reach:: "state pred"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	24	"reach == mu (%Q x. INIT x \| (? y. Q y & N y x))"
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	25
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	26	lemmas reach_rws = INIT_def N_def reach_def
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	27
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	28	lemma reach_ex1: "reach (True,True,True)"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	29	apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	30	apply (tactic {* mc_mucke_tac [] 1 *})
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	31	done
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	32
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	33	(alternative)
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	34	lemma reach_ex' "reach (True,True,True)"
c63e5220ed77 converted to Isar theory format; wenzelm parents: 6466 diff changeset	35	by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *})
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	36
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	37	end

author	blanchet
	Fri, 23 Oct 2009 18:59:24 +0200
changeset 33197	de6285ebcc05
parent 17272	c63e5220ed77
child 35416	d8d7d1b785af
permissions	-rw-r--r--