--- a/src/HOL/IMP/AExp.thy Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/IMP/AExp.thy Fri Jan 12 14:08:53 2018 +0100
@@ -8,24 +8,24 @@
type_synonym val = int
type_synonym state = "vname \<Rightarrow> val"
-text_raw{*\snip{AExpaexpdef}{2}{1}{% *}
+text_raw\<open>\snip{AExpaexpdef}{2}{1}{%\<close>
datatype aexp = N int | V vname | Plus aexp aexp
-text_raw{*}%endsnip*}
+text_raw\<open>}%endsnip\<close>
-text_raw{*\snip{AExpavaldef}{1}{2}{% *}
+text_raw\<open>\snip{AExpavaldef}{1}{2}{%\<close>
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
-text_raw{*}%endsnip*}
+text_raw\<open>}%endsnip\<close>
value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
-text {* The same state more concisely: *}
+text \<open>The same state more concisely:\<close>
value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
-text {* A little syntax magic to write larger states compactly: *}
+text \<open>A little syntax magic to write larger states compactly:\<close>
definition null_state ("<>") where
"null_state \<equiv> \<lambda>x. 0"
@@ -35,28 +35,28 @@
"_State ms" == "_Update <> ms"
"_State (_updbinds b bs)" <= "_Update (_State b) bs"
-text {* \noindent
+text \<open>\noindent
We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
-*}
+\<close>
lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))"
by (rule refl)
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
-text {* In the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default:
-*}
+text \<open>In the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default:
+\<close>
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
-text{* Note that this @{text"<\<dots>>"} syntax works for any function space
-@{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} where @{text "\<tau>\<^sub>2"} has a @{text 0}. *}
+text\<open>Note that this @{text"<\<dots>>"} syntax works for any function space
+@{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} where @{text "\<tau>\<^sub>2"} has a @{text 0}.\<close>
subsection "Constant Folding"
-text{* Evaluate constant subsexpressions: *}
+text\<open>Evaluate constant subsexpressions:\<close>
-text_raw{*\snip{AExpasimpconstdef}{0}{2}{% *}
+text_raw\<open>\snip{AExpasimpconstdef}{0}{2}{%\<close>
fun asimp_const :: "aexp \<Rightarrow> aexp" where
"asimp_const (N n) = N n" |
"asimp_const (V x) = V x" |
@@ -64,7 +64,7 @@
(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*}
+text_raw\<open>}%endsnip\<close>
theorem aval_asimp_const:
"aval (asimp_const a) s = aval a s"
@@ -72,16 +72,16 @@
apply (auto split: aexp.split)
done
-text{* Now we also eliminate all occurrences 0 in additions. The standard
-method: optimized versions of the constructors: *}
+text\<open>Now we also eliminate all occurrences 0 in additions. The standard
+method: optimized versions of the constructors:\<close>
-text_raw{*\snip{AExpplusdef}{0}{2}{% *}
+text_raw\<open>\snip{AExpplusdef}{0}{2}{%\<close>
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
"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\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2"
-text_raw{*}%endsnip*}
+text_raw\<open>}%endsnip\<close>
lemma aval_plus[simp]:
"aval (plus a1 a2) s = aval a1 s + aval a2 s"
@@ -89,16 +89,16 @@
apply simp_all (* just for a change from auto *)
done
-text_raw{*\snip{AExpasimpdef}{2}{0}{% *}
+text_raw\<open>\snip{AExpasimpdef}{2}{0}{%\<close>
fun asimp :: "aexp \<Rightarrow> aexp" where
"asimp (N n) = N n" |
"asimp (V x) = V x" |
"asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)"
-text_raw{*}%endsnip*}
+text_raw\<open>}%endsnip\<close>
-text{* Note that in @{const asimp_const} the optimized constructor was
+text\<open>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. *}
+the code and the proofs.\<close>
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"