tuned

--- a/src/HOL/IMP/AExp.thy	Sun Oct 23 17:37:21 2011 +1100
+++ b/src/HOL/IMP/AExp.thy	Sun Oct 23 14:03:37 2011 +0200
@@ -8,12 +8,16 @@
 type_synonym val = int
 type_synonym state = "vname \<Rightarrow> val"
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpaexpdef}{% *}
 datatype aexp = N int | V vname | Plus aexp aexp
+text_raw{*}\end{isaverbatimwrite}*}
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpavaldef}{% *}
 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
 "aval (N n) s = n" |
 "aval (V x) s = s x" |
 "aval (Plus a1 a2) s = aval a1 s + aval a2 s"
+text_raw{*}\end{isaverbatimwrite}*}
 
 
 value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
@@ -48,7 +52,7 @@
 @{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}
 
 
-subsection "Optimization"
+subsection "Constant Folding"
 
 text{* Evaluate constant subsexpressions: *}
 

--- a/src/HOL/IMP/BExp.thy	Sun Oct 23 17:37:21 2011 +1100
+++ b/src/HOL/IMP/BExp.thy	Sun Oct 23 14:03:37 2011 +0200
@@ -2,60 +2,81 @@
 
 subsection "Boolean Expressions"
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbexpdef}{% *}
 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+text_raw{*}\end{isaverbatimwrite}*}
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbvaldef}{% *}
 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
 "bval (Bc v) s = v" |
 "bval (Not b) s = (\<not> bval b s)" |
-"bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
-"bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
+"bval (And b\<^isub>1 b\<^isub>2) s = (bval b\<^isub>1 s \<and> bval b\<^isub>2 s)" |
+"bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
+text_raw{*}\end{isaverbatimwrite}*}
 
 value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
             <''x'' := 3, ''y'' := 1>"
 
 
-subsection "Optimization"
+text{* To improve automation: *}
 
-text{* Optimized constructors: *}
+lemma bval_And_if[simp]:
+  "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)"
+by(simp)
+
+declare bval.simps(3)[simp del]  --"remove the original eqn"
+
 
+subsection "Constant Folding"
+
+text{* Optimizing constructors: *}
+
+text_raw{*\begin{isaverbatimwrite}\newcommand{\BExplessdef}{% *}
 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
-"less (N n1) (N n2) = Bc(n1 < n2)" |
-"less a1 a2 = Less a1 a2"
+"less (N n\<^isub>1) (N n\<^isub>2) = Bc(n\<^isub>1 < n\<^isub>2)" |
+"less a\<^isub>1 a\<^isub>2 = Less a\<^isub>1 a\<^isub>2"
+text_raw{*}\end{isaverbatimwrite}*}
 
 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
 apply(induction a1 a2 rule: less.induct)
 apply simp_all
 done
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpanddef}{% *}
 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
 "and (Bc True) b = b" |
 "and b (Bc True) = b" |
 "and (Bc False) b = Bc False" |
 "and b (Bc False) = Bc False" |
-"and b1 b2 = And b1 b2"
+"and b\<^isub>1 b\<^isub>2 = And b\<^isub>1 b\<^isub>2"
+text_raw{*}\end{isaverbatimwrite}*}
 
 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
 apply(induction b1 b2 rule: and.induct)
 apply simp_all
 done
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpnotdef}{% *}
 fun not :: "bexp \<Rightarrow> bexp" where
 "not (Bc True) = Bc False" |
 "not (Bc False) = Bc True" |
 "not b = Not b"
+text_raw{*}\end{isaverbatimwrite}*}
 
-lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
+lemma bval_not[simp]: "bval (not b) s = (\<not> bval b s)"
 apply(induction b rule: not.induct)
 apply simp_all
 done
 
 text{* Now the overall optimizer: *}
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbsimpdef}{% *}
 fun bsimp :: "bexp \<Rightarrow> bexp" where
-"bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
-"bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
+"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)" |
+"bsimp (And b\<^isub>1 b\<^isub>2) = and (bsimp b\<^isub>1) (bsimp b\<^isub>2)" |
 "bsimp (Not b) = not(bsimp b)" |
 "bsimp (Bc v) = Bc v"
+text_raw{*}\end{isaverbatimwrite}*}
 
 value "bsimp (And (Less (N 0) (N 1)) b)"