src/HOL/IMP/ACom.thy

 
 text_raw{*\snip{stripdef}{1}{1}{% *}
 fun strip :: "'a acom \<Rightarrow> com" where
 "strip (SKIP {P}) = com.SKIP" |
 "strip (x ::= e {P}) = x ::= e" |
-"strip (C\<^isub>1;;C\<^isub>2) = strip C\<^isub>1;; strip C\<^isub>2" |
-"strip (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {P}) =
-  IF b THEN strip C\<^isub>1 ELSE strip C\<^isub>2" |
+"strip (C\<^sub>1;;C\<^sub>2) = strip C\<^sub>1;; strip C\<^sub>2" |
+"strip (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {P}) =
+  IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2" |
 "strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C"
 text_raw{*}%endsnip*}
 
 text_raw{*\snip{asizedef}{1}{1}{% *}
 fun asize :: "com \<Rightarrow> nat" where
 "asize com.SKIP = 1" |
 "asize (x ::= e) = 1" |
-"asize (C\<^isub>1;;C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2" |
-"asize (IF b THEN C\<^isub>1 ELSE C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2 + 3" |
+"asize (C\<^sub>1;;C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2" |
+"asize (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2 + 3" |
 "asize (WHILE b DO C) = asize C + 3"
 text_raw{*}%endsnip*}
 
 text_raw{*\snip{annotatedef}{1}{1}{% *}
 definition shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
 "shift f n = (\<lambda>p. f(p+n))"
 
 fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
 "annotate f com.SKIP = SKIP {f 0}" |
 "annotate f (x ::= e) = x ::= e {f 0}" |
-"annotate f (c\<^isub>1;;c\<^isub>2) = annotate f c\<^isub>1;; annotate (shift f (asize c\<^isub>1)) c\<^isub>2" |
-"annotate f (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
-  IF b THEN {f 0} annotate (shift f 1) c\<^isub>1
-  ELSE {f(asize c\<^isub>1 + 1)} annotate (shift f (asize c\<^isub>1 + 2)) c\<^isub>2
-  {f(asize c\<^isub>1 + asize c\<^isub>2 + 2)}" |
+"annotate f (c\<^sub>1;;c\<^sub>2) = annotate f c\<^sub>1;; annotate (shift f (asize c\<^sub>1)) c\<^sub>2" |
+"annotate f (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
+  IF b THEN {f 0} annotate (shift f 1) c\<^sub>1
+  ELSE {f(asize c\<^sub>1 + 1)} annotate (shift f (asize c\<^sub>1 + 2)) c\<^sub>2
+  {f(asize c\<^sub>1 + asize c\<^sub>2 + 2)}" |
 "annotate f (WHILE b DO c) =
   {f 0} WHILE b DO {f 1} annotate (shift f 2) c {f(asize c + 2)}"
 text_raw{*}%endsnip*}
 
 text_raw{*\snip{annosdef}{1}{1}{% *}
 fun annos :: "'a acom \<Rightarrow> 'a list" where
 "annos (SKIP {P}) = [P]" |
 "annos (x ::= e {P}) = [P]" |
-"annos (C\<^isub>1;;C\<^isub>2) = annos C\<^isub>1 @ annos C\<^isub>2" |
-"annos (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) =
-  P\<^isub>1 # annos C\<^isub>1 @  P\<^isub>2 # annos C\<^isub>2 @ [Q]" |
+"annos (C\<^sub>1;;C\<^sub>2) = annos C\<^sub>1 @ annos C\<^sub>2" |
+"annos (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
+  P\<^sub>1 # annos C\<^sub>1 @  P\<^sub>2 # annos C\<^sub>2 @ [Q]" |
 "annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]"
 text_raw{*}%endsnip*}
 
 definition anno :: "'a acom \<Rightarrow> nat \<Rightarrow> 'a" where
 "anno C p = annos C ! p"

 
 text_raw{*\snip{mapacomdef}{1}{2}{% *}
 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
 "map_acom f (SKIP {P}) = SKIP {f P}" |
 "map_acom f (x ::= e {P}) = x ::= e {f P}" |
-"map_acom f (C\<^isub>1;;C\<^isub>2) = map_acom f C\<^isub>1;; map_acom f C\<^isub>2" |
-"map_acom f (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) =
-  IF b THEN {f P\<^isub>1} map_acom f C\<^isub>1 ELSE {f P\<^isub>2} map_acom f C\<^isub>2
+"map_acom f (C\<^sub>1;;C\<^sub>2) = map_acom f C\<^sub>1;; map_acom f C\<^sub>2" |
+"map_acom f (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
+  IF b THEN {f P\<^sub>1} map_acom f C\<^sub>1 ELSE {f P\<^sub>2} map_acom f C\<^sub>2
   {f Q}" |
 "map_acom f ({I} WHILE b DO {P} C {Q}) =
   {f I} WHILE b DO {f P} map_acom f C {f Q}"
 text_raw{*}%endsnip*}