src/HOL/IMP/Natural.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1973 8c94c9a5be10
child 4089 96fba19bcbe2
permissions -rw-r--r--
Dep. on Provers/nat_transitive
nipkow@1700
     1
(*  Title:      HOL/IMP/Natural.ML
nipkow@1700
     2
    ID:         $Id$
nipkow@1700
     3
    Author:     Tobias Nipkow & Larry Paulson, TUM
nipkow@1700
     4
    Copyright   1996 TUM
nipkow@1700
     5
*)
nipkow@1700
     6
nipkow@1700
     7
open Natural;
nipkow@1700
     8
nipkow@1973
     9
AddIs evalc.intrs;
nipkow@1973
    10
nipkow@1700
    11
val evalc_elim_cases = map (evalc.mk_cases com.simps)
nipkow@1700
    12
   ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
nipkow@1700
    13
    "<IF b THEN c1 ELSE c2, s> -c-> t"];
nipkow@1700
    14
nipkow@1700
    15
val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
nipkow@1700
    16
nipkow@1973
    17
AddSEs evalc_elim_cases;
nipkow@1700
    18
nipkow@1700
    19
(* evaluation of com is deterministic *)
paulson@1730
    20
goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
paulson@1730
    21
by (etac evalc.induct 1);
paulson@1958
    22
by (thin_tac "<?c,s2> -c-> s1" 7);
nipkow@1973
    23
by (ALLGOALS (deepen_tac (!claset addEs [evalc_WHILE_case]) 4));
nipkow@1700
    24
qed_spec_mp "com_det";