IMP/Denotation.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Denotation.ML	Fri Jan 19 12:49:36 1996 +0100
@@ -0,0 +1,24 @@
+(*  Title: 	HOL/IMP/Denotation.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+open Denotation;
+
+(**** Rewrite Rules for A,B,C ****)
+
+val A_simps =
+     [A_nat,A_loc,A_op1,A_op2];
+
+val B_simps = map (fn t => t RS eq_reflection)
+     [B_true,B_false,B_op,B_not,B_and,B_or]
+
+val C_simps = map (fn t => t RS eq_reflection)
+  [C_skip,C_assign,C_comp,C_if,C_while]; 
+
+(**** mono (Gamma(b,c)) ****)
+
+qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
+	"mono(Gamma(b,c))"
+     (fn _ => [(best_tac comp_cs 1)]);