# HG changeset patch
# User bulwahn
# Date 1278483923 -7200
# Node ID 2bf3a2cb5e58244297353d97c9b1e2edbb382726
# Parent  26e673df3fd0f398460b8f0b180e96daba4a58a1
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps

diff -r 26e673df3fd0 -r 2bf3a2cb5e58 src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Wed Jul 07 08:25:22 2010 +0200
+++ b/src/HOL/IMP/Expr.thy	Wed Jul 07 08:25:23 2010 +0200
@@ -85,46 +85,18 @@
 | "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
 | "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
 
-lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
-  by (rule,cases set: evala) auto
-
-lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
-  by (rule,cases set: evala) auto
-
-lemma   [simp]:
-  "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
-  by (rule,cases set: evala) auto
-
-lemma [simp]:
-  "(Op2 f a1 a2,sigma) -a-> i =
-  (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
-  by (rule,cases set: evala) auto
-
-lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
-  by (rule,cases set: evalb) auto
-
-lemma [simp]:
-  "((false,sigma) -b-> w) = (w=False)"
-  by (rule,cases set: evalb) auto
-
-lemma [simp]:
-  "((ROp f a0 a1,sigma) -b-> w) =
-  (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
-  by (rule,cases set: evalb) blast+
-
-lemma [simp]:
-  "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
-  by (rule,cases set: evalb) blast+
-
-lemma [simp]:
-  "((b0 andi b1,sigma) -b-> w) =
-  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
-  by (rule,cases set: evalb) blast+
-
-lemma [simp]:
-  "((b0 ori b1,sigma) -b-> w) =
-  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
-  by (rule,cases set: evalb) blast+
+inductive_simps
+  evala_simps [simp]:
+  "(N(n),s) -a-> n'" 
+  "(X(x),sigma) -a-> i"
+  "(Op1 f e,sigma) -a-> i"
+  "(Op2 f a1 a2,sigma) -a-> i"
+  "((true,sigma) -b-> w)"
+  "((false,sigma) -b-> w)"
+  "((ROp f a0 a1,sigma) -b-> w)"
+  "((noti(b),sigma) -b-> w)"
+  "((b0 andi b1,sigma) -b-> w)"
+  "((b0 ori b1,sigma) -b-> w)"
 
 
 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
diff -r 26e673df3fd0 -r 2bf3a2cb5e58 src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Wed Jul 07 08:25:22 2010 +0200
+++ b/src/HOL/IMP/Natural.thy	Wed Jul 07 08:25:23 2010 +0200
@@ -79,17 +79,10 @@
 text {* The next proofs are all trivial by rule inversion.
 *}
 
-lemma skip:
-  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
-  by auto
-
-lemma assign:
-  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
-  by auto
-
-lemma semi:
-  "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
-  by auto
+inductive_simps
+  skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
+  and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
+  and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
 
 lemma ifTrue:
   "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"