author | berghofe |
Fri, 01 Jul 2005 13:54:12 +0200 | |
changeset 16633 | 208ebc9311f2 |
parent 7295 | fe09a0c5cebe |
permissions | -rw-r--r-- |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/Modelcheck/MuckeExample1.ML |
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 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
7 |
val reach_rws = [INIT_def,N_def,reach_def]; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
8 |
|
7295 | 9 |
Goal "reach (True,True,True)"; |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
10 |
by (simp_tac (Mucke_ss addsimps reach_rws) 1); |
7295 | 11 |
by (mc_mucke_tac [] 1); |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
12 |
qed "reach_ex_thm1"; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
13 |
|
7295 | 14 |
(*alternative*) |
15 |
Goal "reach (True,True,True)"; |
|
16 |
by (mc_mucke_tac reach_rws 1); |
|
17 |
qed "reach_ex_thm1'"; |