src/HOL/Modelcheck/EindhovenExample.ML

Exported function unify_consts (workaround to avoid inconsistently
typed recursive constants in inductive and primrec definitions).

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

val reach_rws = [reach_def,INIT_def,N_def];


Goal "reach (True,True,True)";
by (simp_tac (Eindhoven_ss addsimps reach_rws) 1);

(*show the current proof state using the model checker syntax*)
setmp print_mode ["Eindhoven"] pr ();

(* actually invoke the model checker *)
(* try out after installing the model checker: see the README file *)

(* by (mc_eindhoven_tac 1); *)

(*qed "reach_ex_thm";*)



(* just to make a proof in this file :-) *)
Goalw [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)";
by (Simp_tac 1);
qed"init_state";