src/HOL/IMP/Natural.ML
author paulson
Thu, 05 Sep 1996 18:42:48 +0200
changeset 1958 6f20ecbd87cb
parent 1730 1c7f793fc374
child 1973 8c94c9a5be10
permissions -rw-r--r--
Now uses thin_tac

(*  Title:      HOL/IMP/Natural.ML
    ID:         $Id$
    Author:     Tobias Nipkow & Larry Paulson, TUM
    Copyright   1996 TUM
*)

open Natural;

val evalc_elim_cases = map (evalc.mk_cases com.simps)
   ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
    "<IF b THEN c1 ELSE c2, s> -c-> t"];

val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";

val evalc_cs = set_cs addSEs evalc_elim_cases
                      addEs  [evalc_WHILE_case];

(* evaluation of com is deterministic *)
goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
by (etac evalc.induct 1);
by (thin_tac "<?c,s2> -c-> s1" 7);
by (ALLGOALS (deepen_tac evalc_cs 4));
qed_spec_mp "com_det";