src/HOL/IMP/AExp.thy
changeset 45246 4fbeabee6487
parent 45238 ed2bb3b58cc4
child 45255 ffc06165d272
--- a/src/HOL/IMP/AExp.thy	Fri Oct 21 17:39:07 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Sat Oct 22 20:17:50 2011 +0200
@@ -52,13 +52,15 @@
 
 text{* Evaluate constant subsexpressions: *}
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpconstdef}{% *}
 fun asimp_const :: "aexp \<Rightarrow> aexp" where
 "asimp_const (N n) = N n" |
 "asimp_const (V x) = V x" |
-"asimp_const (Plus a1 a2) =
-  (case (asimp_const a1, asimp_const a2) of
-    (N n1, N n2) \<Rightarrow> N(n1+n2) |
-    (a1',a2') \<Rightarrow> Plus a1' a2')"
+"asimp_const (Plus a\<^isub>1 a\<^isub>2) =
+  (case (asimp_const a\<^isub>1, asimp_const a\<^isub>2) of
+    (N n\<^isub>1, N n\<^isub>2) \<Rightarrow> N(n\<^isub>1+n\<^isub>2) |
+    (b\<^isub>1,b\<^isub>2) \<Rightarrow> Plus b\<^isub>1 b\<^isub>2)"
+text_raw{*}\end{isaverbatimwrite}*}
 
 theorem aval_asimp_const:
   "aval (asimp_const a) s = aval a s"
@@ -69,11 +71,13 @@
 text{* Now we also eliminate all occurrences 0 in additions. The standard
 method: optimized versions of the constructors: *}
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpplusdef}{% *}
 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
-"plus (N i1) (N i2) = N(i1+i2)" |
+"plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)" |
 "plus (N i) a = (if i=0 then a else Plus (N i) a)" |
 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
-"plus a1 a2 = Plus a1 a2"
+"plus a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2"
+text_raw{*}\end{isaverbatimwrite}*}
 
 lemma aval_plus[simp]:
   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
@@ -81,10 +85,12 @@
 apply simp_all (* just for a change from auto *)
 done
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpdef}{% *}
 fun asimp :: "aexp \<Rightarrow> aexp" where
 "asimp (N n) = N n" |
 "asimp (V x) = V x" |
-"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
+"asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)"
+text_raw{*}\end{isaverbatimwrite}*}
 
 text{* Note that in @{const asimp_const} the optimized constructor was
 inlined. Making it a separate function @{const plus} improves modularity of