# HG changeset patch
# User nipkow
# Date 785790375 -3600
# Node ID 32b84b520cd30aa5e9e2a796b0bee0833b683a94
# Parent  fcf8024c920d1083e4cc199656752051a9fa3b36
Proved determinism.

diff -r fcf8024c920d -r 32b84b520cd3 IMP/Properties.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Properties.ML	Fri Nov 25 20:06:15 1994 +0100
@@ -0,0 +1,43 @@
+(*  Title: 	HOL/IMP/Properties.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow, TUM
+    Copyright   1994 TUM
+
+IMP is deterministic.
+*)
+
+(* evaluation of aexp is deterministic *)
+goal Com.thy "!m n. <a,s> -a-> m & <a,s> -a-> n --> m=n";
+by(res_inst_tac[("aexp","a")]Com.aexp.induct 1);
+by(REPEAT(fast_tac (HOL_cs addSIs evala.intrs addSEs evala_elim_cases) 1));
+val aexp_detD =
+  store_thm("aexp_detD", conjI RS (result() RS spec RS spec RS mp));
+
+(* evaluation of bexp is deterministic *)
+goal Com.thy "!v w. <b,s> -b-> v & <b,s> -b-> w --> v=w";
+by(res_inst_tac[("bexp","b")]Com.bexp.induct 1);
+by(REPEAT(fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases
+                           addDs [aexp_detD]) 1));
+val bexp_detD =
+  store_thm("bexp_detD", conjI RS (result() RS spec RS spec RS mp));
+
+
+val evalc_elim_cases = map (evalc.mk_cases com.simps)
+   ["<skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
+    "<ifc b then c1 else c2, s> -c-> t", "<while b do c,s> -c-> t"];
+
+(* evaluation of com is deterministic *)
+goal Com.thy "!!c. <c,s> -c-> t ==> !u. <c,s> -c-> u --> u=t";
+(* start with rule induction *)
+be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
+by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases addDs [aexp_detD]) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
+by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
+          atac, dtac bexp_detD, atac, etac False_neq_True]);
+by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
+          dtac bexp_detD, atac, etac (sym RS False_neq_True),
+          fast_tac HOL_cs]);
+result();
diff -r fcf8024c920d -r 32b84b520cd3 IMP/Properties.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Properties.thy	Fri Nov 25 20:06:15 1994 +0100
@@ -0,0 +1,1 @@
+Properties = "Com"
diff -r fcf8024c920d -r 32b84b520cd3 IMP/ROOT.ML
--- a/IMP/ROOT.ML	Fri Nov 25 16:24:18 1994 +0100
+++ b/IMP/ROOT.ML	Fri Nov 25 20:06:15 1994 +0100
@@ -17,4 +17,5 @@
 writeln"Root file for HOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
+time_use_thy "Properties";
 time_use_thy "Equiv";