# HG changeset patch
# User nipkow
# Date 778860959 -7200
# Node ID bca8203b0e91f82e6a1402d48ef197c9f2867a10
# Parent  0a43cf4589987b85f99096a8aae14eaf681f6ad1
Converted rules to primrecs

diff -r 0a43cf458998 -r bca8203b0e91 IMP/Denotation.thy
--- a/IMP/Denotation.thy	Tue Sep 06 13:24:29 1994 +0200
+++ b/IMP/Denotation.thy	Tue Sep 06 16:15:59 1994 +0200
@@ -14,34 +14,34 @@
   C     :: "com => (state*state)set"
   Gamma :: "[bexp,com,(state*state)set] => (state*state)set"
 
-rules
-  A_nat_def	"A(N(n)) == (%s. n)"
-  A_loc_def	"A(X(x)) == (%s. s(x))" 
-  A_op1_def	"A(Op1(f,a)) == (%s. f(A(a,s)))"
-  A_op2_def	"A(Op2(f,a0,a1)) == (%s. f(A(a0,s),A(a1,s)))"
+primrec A aexp
+  A_nat_def	"A(N(n)) = (%s. n)"
+  A_loc_def	"A(X(x)) = (%s. s(x))" 
+  A_op1_def	"A(Op1(f,a)) = (%s. f(A(a,s)))"
+  A_op2_def	"A(Op2(f,a0,a1)) = (%s. f(A(a0,s),A(a1,s)))"
 
-
-  B_true_def	"B(true) == (%s. True)"
-  B_false_def	"B(false) == (%s. False)"
-  B_op_def	"B(ROp(f,a0,a1)) == (%s. f(A(a0,s),A(a1,s)))" 
+primrec B bexp
+  B_true_def	"B(true) = (%s. True)"
+  B_false_def	"B(false) = (%s. False)"
+  B_op_def	"B(ROp(f,a0,a1)) = (%s. f(A(a0,s),A(a1,s)))" 
 
 
-  B_not_def	"B(noti(b)) == (%s. ~B(b,s))"
-  B_and_def	"B(b0 andi b1) == (%s. B(b0,s) & B(b1,s))"
-  B_or_def	"B(b0 ori b1) == (%s. B(b0,s) | B(b1,s))"
+  B_not_def	"B(noti(b)) = (%s. ~B(b,s))"
+  B_and_def	"B(b0 andi b1) = (%s. B(b0,s) & B(b1,s))"
+  B_or_def	"B(b0 ori b1) = (%s. B(b0,s) | B(b1,s))"
 
-  C_skip_def	"C(skip) == id"
-  C_assign_def	"C(x := a) == {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
-
-  C_comp_def	"C(c0 ; c1) == C(c1) O C(c0)"
-  C_if_def	"C(ifc b then c0 else c1) ==   \
-\		   {io. io:C(c0) & B(b,fst(io))} Un \
-\	           {io. io:C(c1) & ~B(b,fst(io))}"
-
+defs
   Gamma_def	"Gamma(b,c) ==   \
 \		   (%phi.{io. io : (phi O C(c)) & B(b,fst(io))} Un \
 \	                 {io. io : id & ~B(b,fst(io))})"
 
-  C_while_def	"C(while b do c) == lfp(Gamma(b,c))"
+primrec C com
+  C_skip_def	"C(skip) = id"
+  C_assign_def	"C(x := a) = {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
+  C_comp_def	"C(c0 ; c1) = C(c1) O C(c0)"
+  C_if_def	"C(ifc b then c0 else c1) =   \
+\		   {io. io:C(c0) & B(b,fst(io))} Un \
+\	           {io. io:C(c1) & ~B(b,fst(io))}"
+  C_while_def	"C(while b do c) = lfp(Gamma(b,c))"
 
 end
diff -r 0a43cf458998 -r bca8203b0e91 IMP/Equiv.ML
--- a/IMP/Equiv.ML	Tue Sep 06 13:24:29 1994 +0200
+++ b/IMP/Equiv.ML	Tue Sep 06 16:15:59 1994 +0200
@@ -7,7 +7,7 @@
 goal Equiv.thy "(<a,s> -a-> n) = (A(a,s) = n)";
 by (res_inst_tac [("x","n")] spec 1);                     (* quantify n *)
 by (aexp.induct_tac "a" 1);                		  (* struct. ind. *)
-by (rewrite_goals_tac A_rewrite_rules);			  (* rewr. Den.   *)
+by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
                              addSEs aexp_elim_cases)));
 val aexp_iff = result();
@@ -19,7 +19,8 @@
 goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)";
 by (res_inst_tac [("x","w")] spec 1);			(* quantify w *)
 by (bexp.induct_tac "b" 1);		                (* struct. ind. *)
-by (rewrite_goals_tac B_rewrite_rules);			(* rewr. Den.   *)
+by(rewrite_goals_tac B_simps);
+  (* simplification with HOL_ss too agressive: (True=x) == True *)
 by (safe_tac (HOL_cs addSIs (aexp2::evalb.intrs)
                      addSDs [aexp1] addSEs bexp_elim_cases)
     THEN ALLGOALS(best_tac HOL_cs));
@@ -38,8 +39,8 @@
 
 (* start with rule induction *)
 be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
-
-by (rewrite_tac (Gamma_def::C_rewrite_rules));
+by (rewrite_tac (Gamma_def::C_simps));
+  (* simplification with HOL_ss again too agressive *)
 (* skip *)
 by (fast_tac comp_cs 1);
 (* assign *)
@@ -62,7 +63,7 @@
 
 goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
 by (com.induct_tac "c" 1);
-by (rewrite_tac C_rewrite_rules);
+by (rewrite_tac C_simps);
 by (safe_tac com_cs);
 by (ALLGOALS (asm_full_simp_tac prod_ss));