src/HOL/IMP/AExp.thy

 
 text_raw{*\snip{AExpavaldef}{1}{2}{% *}
 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
 "aval (N n) s = n" |
 "aval (V x) s = s x" |
-"aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
+"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
 text_raw{*}%endsnip*}
 
 
 value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
 

 text {* In  the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default:
 *}
 value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
 
 text{* Note that this @{text"<\<dots>>"} syntax works for any function space
-@{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}
+@{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} where @{text "\<tau>\<^sub>2"} has a @{text 0}. *}
 
 
 subsection "Constant Folding"
 
 text{* Evaluate constant subsexpressions: *}
 
 text_raw{*\snip{AExpasimpconstdef}{0}{2}{% *}
 fun asimp_const :: "aexp \<Rightarrow> aexp" where
 "asimp_const (N n) = N n" |
 "asimp_const (V x) = V x" |
-"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)"
+"asimp_const (Plus a\<^sub>1 a\<^sub>2) =
+  (case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of
+    (N n\<^sub>1, N n\<^sub>2) \<Rightarrow> N(n\<^sub>1+n\<^sub>2) |
+    (b\<^sub>1,b\<^sub>2) \<Rightarrow> Plus b\<^sub>1 b\<^sub>2)"
 text_raw{*}%endsnip*}
 
 theorem aval_asimp_const:
   "aval (asimp_const a) s = aval a s"
 apply(induction a)

 text{* Now we also eliminate all occurrences 0 in additions. The standard
 method: optimized versions of the constructors: *}
 
 text_raw{*\snip{AExpplusdef}{0}{2}{% *}
 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
-"plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)" |
+"plus (N i\<^sub>1) (N i\<^sub>2) = N(i\<^sub>1+i\<^sub>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 a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2"
+"plus a\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2"
 text_raw{*}%endsnip*}
 
 lemma aval_plus[simp]:
   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
 apply(induction a1 a2 rule: plus.induct)

 
 text_raw{*\snip{AExpasimpdef}{2}{0}{% *}
 fun asimp :: "aexp \<Rightarrow> aexp" where
 "asimp (N n) = N n" |
 "asimp (V x) = V x" |
-"asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)"
+"asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)"
 text_raw{*}%endsnip*}
 
 text{* Note that in @{const asimp_const} the optimized constructor was
 inlined. Making it a separate function @{const plus} improves modularity of
 the code and the proofs. *}