src/HOL/IMP/Expr.thy
changeset 37736 2bf3a2cb5e58
parent 27362 a6dc1769fdda
child 41589 bbd861837ebc
     1.1 --- a/src/HOL/IMP/Expr.thy	Wed Jul 07 08:25:22 2010 +0200
     1.2 +++ b/src/HOL/IMP/Expr.thy	Wed Jul 07 08:25:23 2010 +0200
     1.3 @@ -85,46 +85,18 @@
     1.4  | "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
     1.5  | "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
     1.6  
     1.7 -lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
     1.8 -  by (rule,cases set: evala) auto
     1.9 -
    1.10 -lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
    1.11 -  by (rule,cases set: evala) auto
    1.12 -
    1.13 -lemma   [simp]:
    1.14 -  "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
    1.15 -  by (rule,cases set: evala) auto
    1.16 -
    1.17 -lemma [simp]:
    1.18 -  "(Op2 f a1 a2,sigma) -a-> i =
    1.19 -  (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
    1.20 -  by (rule,cases set: evala) auto
    1.21 -
    1.22 -lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
    1.23 -  by (rule,cases set: evalb) auto
    1.24 -
    1.25 -lemma [simp]:
    1.26 -  "((false,sigma) -b-> w) = (w=False)"
    1.27 -  by (rule,cases set: evalb) auto
    1.28 -
    1.29 -lemma [simp]:
    1.30 -  "((ROp f a0 a1,sigma) -b-> w) =
    1.31 -  (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
    1.32 -  by (rule,cases set: evalb) blast+
    1.33 -
    1.34 -lemma [simp]:
    1.35 -  "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
    1.36 -  by (rule,cases set: evalb) blast+
    1.37 -
    1.38 -lemma [simp]:
    1.39 -  "((b0 andi b1,sigma) -b-> w) =
    1.40 -  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
    1.41 -  by (rule,cases set: evalb) blast+
    1.42 -
    1.43 -lemma [simp]:
    1.44 -  "((b0 ori b1,sigma) -b-> w) =
    1.45 -  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
    1.46 -  by (rule,cases set: evalb) blast+
    1.47 +inductive_simps
    1.48 +  evala_simps [simp]:
    1.49 +  "(N(n),s) -a-> n'" 
    1.50 +  "(X(x),sigma) -a-> i"
    1.51 +  "(Op1 f e,sigma) -a-> i"
    1.52 +  "(Op2 f a1 a2,sigma) -a-> i"
    1.53 +  "((true,sigma) -b-> w)"
    1.54 +  "((false,sigma) -b-> w)"
    1.55 +  "((ROp f a0 a1,sigma) -b-> w)"
    1.56 +  "((noti(b),sigma) -b-> w)"
    1.57 +  "((b0 andi b1,sigma) -b-> w)"
    1.58 +  "((b0 ori b1,sigma) -b-> w)"
    1.59  
    1.60  
    1.61  lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"