diff --git a/thys/IMP2/automation/IMP2_Program_Analysis.thy b/thys/IMP2/automation/IMP2_Program_Analysis.thy
--- a/thys/IMP2/automation/IMP2_Program_Analysis.thy
+++ b/thys/IMP2/automation/IMP2_Program_Analysis.thy
@@ -1,346 +1,346 @@
 section \<open>Program Analysis\<close>
 theory IMP2_Program_Analysis
 imports "../basic/Annotated_Syntax" "../lib/Subgoal_Focus_Some" "../parser/Parser" IMP2_Basic_Decls
 begin
   subsection \<open>Analysis Simproc\<close>
 
   
   definition [simp]: "ANALYZE x \<equiv> x"
   (*lemma ANALYZE_cong[named_ss vcg_bb cong]: "ANALYZE x = ANALYZE x" by simp*)
   
   simproc_setup ANALYZE ("ANALYZE x") 
     = \<open>fn _ => fn ctxt => let
     
         val analysis_unfolds = 
           @{thm ANALYZE_def} 
           :: Named_Theorems.get ctxt @{named_theorems analysis_unfolds}
           @ Named_Theorems.get ctxt @{named_theorems vcg_annotation_defs}
     
         val unfold_conv = 
            map (Local_Defs.meta_rewrite_rule ctxt #> perhaps (try Drule.abs_def)) analysis_unfolds
         |> Raw_Simplifier.rewrite ctxt true
     
     in
       unfold_conv #> SOME
     end  
   \<close>
   declare [[simproc del: ANALYZE]]
 
   declaration \<open>fn _ => Named_Simpsets.map_ctxt @{named_simpset vcg_bb} (
     fn ctxt => ctxt addsimprocs [@{simproc ANALYZE}]
   )\<close>
 
   (* TODO: There's a more general concept here: 
     Activating specific simpsets depending on the context, or, in this case, a trigger constant.
     DUP with STRIP_ANNOT in VCG
   *)
 
   
   lemmas [analysis_unfolds] = Inline_def Params_def AssignIdx_retv_def ArrayCpy_retv_def
   
 
   subsection \<open>Modifies Sets\<close>
   
   definition modifies :: "vname set \<Rightarrow> state \<Rightarrow> state \<Rightarrow> bool" where
     "modifies vars s\<^sub>1 s\<^sub>2 = (\<forall>x. x\<notin>vars \<longrightarrow> s\<^sub>1 x = s\<^sub>2 x)"
   
   context notes[simp] = modifies_def begin
     lemma modifies_refl[intro!, simp]: "modifies vs a a" by simp
     lemma modifies_sym[sym]: "modifies vs a b \<Longrightarrow> modifies vs b a" by simp
     lemma modifies_trans'[trans]: "modifies vs\<^sub>1 a b \<Longrightarrow> modifies vs\<^sub>2 b c \<Longrightarrow> modifies (vs\<^sub>1\<union>vs\<^sub>2) a c" by simp
     lemma modifies_trans[trans]: "modifies vs a b \<Longrightarrow> modifies vs b c \<Longrightarrow> modifies vs a c" by simp
   
     (* Test for correct order of trans-rules *)
     notepad begin
       fix vs a b c
       assume "modifies vs a b"
       also assume "modifies vs b c"
       finally have "modifies vs a c" . (* This must be trivial. If you get vs\<union>vs, something went wrong! *)
     end
     
     
     lemma modifies_join: "\<lbrakk> modifies vs\<^sub>1 a b; modifies vs\<^sub>2 a b \<rbrakk> \<Longrightarrow> modifies (vs\<^sub>1\<inter>vs\<^sub>2) a b" by auto
     
     lemma modifies_mono: "\<lbrakk> vs\<^sub>1\<subseteq>vs\<^sub>2; modifies vs\<^sub>1 a b \<rbrakk> \<Longrightarrow> modifies vs\<^sub>2 a b" by auto
     
     lemma modifies_equals: "modifies vs s s' \<Longrightarrow> x\<notin>vs \<Longrightarrow> s x = s' x" by auto
     lemma modifies_upd: 
       "x\<in>vs \<Longrightarrow> modifies vs s (s'(x:=v)) \<longleftrightarrow> modifies vs s s'" 
       "x\<in>vs \<Longrightarrow> modifies vs (s(x:=v)) s' \<longleftrightarrow> modifies vs s s'" 
       by auto
       
     lemma modifies_split: "modifies vs (<l|g>) (<l'|g'>) 
       \<longleftrightarrow> modifies (Collect is_global \<union> vs) l l' \<and> modifies (Collect is_local \<union> vs) g g'"  
       apply (auto simp: combine_query) by (metis combine_query)
       
   end  
     
   definition "wp_mod \<pi> vs c Q s = wp \<pi> c (\<lambda>s'. modifies vs s' s \<and> Q s') s "
   definition "wlp_mod \<pi> vs c Q s = wlp \<pi> c (\<lambda>s'. modifies vs s' s \<and> Q s') s "
     
   subsubsection \<open>Simplification of Modifies Tags\<close>  
     
   ML \<open>
   
     val simp_modifies_tac = let
-      fun is_modifies _ ct = case Thm.term_of ct of _$(Const (@{const_name modifies},_)$_$_$_) => true | _ => false
-      fun dest_modifies (Const _ $ (Const (@{const_name modifies},_)$vs$s$d)) = (vs,s,d)
+      fun is_modifies _ ct = case Thm.term_of ct of _ $ \<^Const_>\<open>modifies for _ _ _\<close> => true | _ => false
+      fun dest_modifies (Const _ $ \<^Const_>\<open>modifies for vs s d\<close>) = (vs,s,d)
         | dest_modifies t = raise TERM("dest_modifies",[t])
         
         
     in
       Subgoal_Focus_Some.FOCUS_SOME_PREMS is_modifies (fn {context=ctxt, prems, concl, ...} => let
       
         val sts = map (#2 o dest_modifies o Thm.prop_of) prems |> Termtab.make_set
   
         fun collect_vars (a$b) = if Termtab.defined sts a then Termtab.insert_set b else collect_vars a o collect_vars b
           | collect_vars (Abs (_,_,t)) = collect_vars t
           | collect_vars _ = I
             
         val vars = 
           Termtab.empty
           |> collect_vars (Thm.term_of concl) o fold collect_vars (map Thm.prop_of prems)
           |> Termtab.keys 
           |> map (Thm.cterm_of ctxt)
   
         val ctxt_bb = Named_Simpsets.put @{named_simpset vcg_bb} ctxt  
         fun mk_mod_thm x thm = let
           val thm = @{thm modifies_equals} OF [thm]
           fun is_triv thm = case Thm.prop_of thm of @{prop "True"} => true | _ => false
           
           val thm = Drule.infer_instantiate' ctxt [SOME x] thm
             |> full_simplify ctxt_bb
         in
           if is_triv thm then NONE else SOME thm
         end
           
         val thms = map_product (mk_mod_thm) vars prems |> map_filter I 
         
         val ctxt = Simplifier.put_simpset HOL_basic_ss ctxt addsimps thms
         
       
       in HEADGOAL (asm_full_simp_tac ctxt) end)
     end
   \<close>
   
   method_setup i_vcg_modifies_simp = \<open>Scan.succeed (SIMPLE_METHOD' o simp_modifies_tac)\<close>
   
   
   subsubsection \<open>Syntactic Approximation of Modifies Set\<close>
 
   primrec lhsv' :: "com \<Rightarrow> vname set" where
     "lhsv' (x[_] ::= _) = {x}"
   | "lhsv' (x[] ::= _) = {x}"
   | "lhsv' (CLEAR x[]) = {x}"
   | "lhsv' (Assign_Locals l) = Collect is_local"
   | "lhsv' SKIP = {}"  
   | "lhsv' (c\<^sub>1;; c\<^sub>2) = lhsv' c\<^sub>1 \<union> lhsv' c\<^sub>2"
   | "lhsv' (IF _ THEN c\<^sub>1 ELSE c\<^sub>2) = lhsv' c\<^sub>1 \<union> lhsv' c\<^sub>2"
   | "lhsv' (WHILE _ DO c) = lhsv' c"
   | "lhsv' (SCOPE c) = Set.filter is_global (lhsv' c)"
   | "lhsv' (PCall p) = {}"
   | lhsv'_pscope_simp_orig[simp del]: 
     "lhsv' (PScope \<pi> c) = \<Union>(ran (map_option lhsv' o \<pi>)) \<union> lhsv' c"
   
   definition "lhsv\<pi> \<pi> \<equiv> (\<Union>c\<in>ran \<pi>. lhsv' c)"
   
   lemma lhsv'_pscope_simp[simp]: "lhsv' (PScope \<pi> c) = lhsv\<pi> \<pi> \<union> lhsv' c"
     by (auto simp: ran_def lhsv'_pscope_simp_orig lhsv\<pi>_def)
 
   lemma lhsv\<pi>_empty: "lhsv\<pi> Map.empty = {}" by (auto simp: lhsv\<pi>_def)
   lemma lhsv\<pi>_upd: "m p = None \<Longrightarrow> lhsv\<pi> (m(p\<mapsto>c)) = lhsv' c \<union> lhsv\<pi> m" 
     apply (auto simp: lhsv\<pi>_def ran_def)
     by (metis option.simps(3))
 
   lemmas lhsv\<pi>_maplet[simp] = lhsv\<pi>_empty lhsv\<pi>_upd
   
   notepad begin
     have "lhsv\<pi> [''foo'' \<mapsto> \<^imp>\<open>a=5\<close>, ''bar'' \<mapsto> \<^imp>\<open>c=7; b=5; rec foo()\<close>] = {''a'', ''b'', ''c''}"
       by (simp add: Params_def)
   end
 
   
   primrec lhsv :: "program \<Rightarrow> com \<Rightarrow> vname set" where
     "lhsv \<pi> (x[_] ::= _) = {x}"
   | "lhsv \<pi> (x[] ::= _) = {x}"
   | "lhsv \<pi> (CLEAR x[]) = {x}"
   | "lhsv \<pi> (Assign_Locals l) = Collect is_local"
   | "lhsv \<pi> SKIP = {}"  
   | "lhsv \<pi> (c\<^sub>1;; c\<^sub>2) = lhsv \<pi> c\<^sub>1 \<union> lhsv \<pi> c\<^sub>2"
   | "lhsv \<pi> (IF _ THEN c\<^sub>1 ELSE c\<^sub>2) = lhsv \<pi> c\<^sub>1 \<union> lhsv \<pi> c\<^sub>2"
   | "lhsv \<pi> (WHILE _ DO c) = lhsv \<pi> c"
   | "lhsv \<pi> (SCOPE c) = Set.filter is_global (lhsv \<pi> c)"
   | "lhsv \<pi> (PCall p) = lhsv\<pi> \<pi>"
   | "lhsv \<pi> (PScope \<pi>' c) = lhsv\<pi> \<pi>' \<union> lhsv' c"
   
   
   text \<open>Install special rule for procedure scope\<close>  
   lemmas [named_ss vcg_bb] = lhsv'.simps
   lemmas [named_ss vcg_bb del] = lhsv'_pscope_simp_orig 
   lemmas [named_ss vcg_bb] = lhsv'_pscope_simp
   
   lemmas [named_ss vcg_bb] = lhsv.simps
   lemmas [named_ss vcg_bb] = lhsv\<pi>_maplet
     
   lemmas [named_ss vcg_bb] = is_global.simps
   
   
           
     
   lemma modifies_lhsv'_gen:
     assumes "lhsv\<pi> \<pi> \<subseteq> vs"
     assumes "lhsv' c \<subseteq> vs"
     assumes "\<pi>: (c,s) \<Rightarrow> t"
     shows "modifies vs t s"
     using assms(3,1,2)
   proof (induction arbitrary: vs)
     case (Scope \<pi> c s s')
     from Scope.IH[where vs="vs \<union> Collect is_local"] Scope.prems 
     show ?case by (fastforce simp: modifies_def combine_states_def) 
   next
     case (PCall \<pi> p c s t)
     then show ?case by (auto simp: ran_def lhsv\<pi>_def)
   next
     case (PScope \<pi>' p c s t \<pi>)
     then show ?case by (simp add: SUP_le_iff ranI lhsv\<pi>_def)
   qed (auto simp: modifies_def combine_states_def)
 
   lemma modifies_lhsv\<pi>:
     assumes "\<pi>: (c, s) \<Rightarrow> t"
     assumes "\<pi> p = Some c"
     shows "modifies (lhsv\<pi> \<pi>) t s"
     apply (rule modifies_lhsv'_gen[OF _ _ assms(1)])
     using assms(2) by (auto simp: lhsv\<pi>_def ran_def)
 
   lemma lhsv_approx: "lhsv \<pi>' c \<subseteq> lhsv\<pi> \<pi>' \<union> lhsv' c" 
     apply (induction c arbitrary: \<pi>')
               apply auto
     apply (auto simp: lhsv\<pi>_def)
     done
   
               
 
   lemma modifies_lhsv:
     assumes "\<pi>: (c, s) \<Rightarrow> t"
     shows "modifies (lhsv \<pi> c) t s"
     using assms
     apply (induction)
                 apply (all \<open>(auto simp: modifies_def combine_states_def; fail)?\<close>)
      subgoal by (auto simp: modifies_lhsv\<pi>) []
     subgoal using lhsv_approx by (auto simp: modifies_def)
     done
     
     
       
   lemma wp_strengthen_modset: "wp \<pi> c Q s \<Longrightarrow> wp \<pi> c (\<lambda>s'. Q s' \<and> modifies (lhsv \<pi> c) s' s) s"
     unfolding wp_def 
     by (blast intro: modifies_lhsv)
   
   lemma wlp_strengthen_modset: "wlp \<pi> c Q s \<Longrightarrow> wlp \<pi> c (\<lambda>s'. Q s' \<and> modifies (lhsv \<pi> c) s' s) s"
     unfolding wlp_def 
     by (blast intro: modifies_lhsv)
 
   lemma wp_mod_lhsv_eq: "wp_mod \<pi> (lhsv \<pi> c) c Q s = wp \<pi> c Q s"
     unfolding wp_mod_def
     using modifies_lhsv wp_def by auto
   
   lemma wlp_mod_lhsv_eq: "wlp_mod \<pi> (lhsv \<pi> c) c Q s = wlp \<pi> c Q s"
     unfolding wlp_mod_def
     using modifies_lhsv wlp_def by auto
 
     
   subsubsection \<open>Hoare-Triple with Modifies-Set\<close>
   text \<open>We define a Hoare-Triple that contains a modifies declaration\<close>
   definition "HT_mods \<pi> mods P c Q \<equiv> HT \<pi> P c (\<lambda>s\<^sub>0 s. modifies mods s s\<^sub>0 \<and> Q s\<^sub>0 s)"
   definition "HT_partial_mods \<pi> mods P c Q \<equiv> HT_partial \<pi> P c (\<lambda>s\<^sub>0 s. Q s\<^sub>0 s \<and> modifies mods s s\<^sub>0)"
 
   lemma HT_mods_cong[named_ss vcg_bb cong]:
     assumes "vs = vs'"
     assumes "P=P'"
     assumes "c=c'"
     assumes "\<And>s\<^sub>0 s. modifies vs s s\<^sub>0 \<Longrightarrow> Q s\<^sub>0 s = Q' s\<^sub>0 s"
     shows "HT_mods \<pi> vs P c Q = HT_mods \<pi> vs' P' c' Q'"
     unfolding HT_mods_def HT_def using assms
     by (auto intro: wp_conseq)
     
   lemma HT_partial_mods_cong[named_ss vcg_bb cong]:
     assumes "vs = vs'"
     assumes "P=P'"
     assumes "c=c'"
     assumes "\<And>s\<^sub>0 s. modifies vs s s\<^sub>0 \<Longrightarrow> Q s\<^sub>0 s = Q' s\<^sub>0 s"
     shows "HT_partial_mods \<pi> vs P c Q = HT_partial_mods \<pi> vs' P' c' Q'"
     unfolding HT_partial_mods_def HT_partial_def using assms
     by (auto intro: wlp_conseq)
   
   lemma vcg_wp_conseq:
     assumes "HT_mods \<pi> mods P c Q"
     assumes "P s"
     assumes "\<And>s'. \<lbrakk>modifies mods s' s; Q s s'\<rbrakk> \<Longrightarrow> Q' s'"
     shows "wp \<pi> c Q' s"
     using assms unfolding HT_mods_def HT_def
     by (metis (no_types, lifting) wp_def)
     
   lemma vcg_wlp_conseq:
     assumes "HT_partial_mods \<pi> mods P c Q"
     assumes "P s"
     assumes "\<And>s'. \<lbrakk>modifies mods s' s; Q s s'\<rbrakk> \<Longrightarrow> Q' s'"
     shows "wlp \<pi> c Q' s"
     using assms unfolding HT_partial_mods_def HT_partial_def
     by (metis (no_types, lifting) wlp_def)
 
   text \<open>The last rule allows us to re-use a total correctness verification in a partial 
     correctness proof.\<close>  
   lemma vcg_wlp_wp_conseq:
     assumes "HT_mods \<pi> mods P c Q"
     assumes "P s"
     assumes "\<And>s'. \<lbrakk>modifies mods s' s; Q s s'\<rbrakk> \<Longrightarrow> Q' s'"
     shows "wlp \<pi> c Q' s"
     using assms vcg_wp_conseq wp_imp_wlp by auto
     
   (*
     TODO: Rules for combining proofs over the same program!
   *)
         
     
     
     
 subsection \<open>Free Variables of Expressions\<close> 
 
 text \<open>This function computes the set of variables that occur in an expression\<close>
 fun fv_aexp :: "aexp \<Rightarrow> vname set" where
   "fv_aexp (N _) = {}"
 | "fv_aexp (Vidx x i) = insert x (fv_aexp i)"
 | "fv_aexp (Unop f a) = fv_aexp a"
 | "fv_aexp (Binop f a b) = fv_aexp a \<union> fv_aexp b"
 
     
 declare fv_aexp.simps[named_ss vcg_bb]
 
 lemma aval_eq_on_fv: "(\<forall>x\<in>fv_aexp a. s x = s' x) \<Longrightarrow> aval a s = aval a s'"
   by (induction a) auto
     
 lemma aval_indep_non_fv: "x\<notin>fv_aexp a \<Longrightarrow> aval a (s(x:=y)) = aval a s"
   by (induction a) auto
 
 lemma redundant_array_assignment: "(x[] ::= a;; a[] ::= x) \<sim> (x[] ::= a)"
   apply rule
    apply (auto)
    apply (metis ArrayCpy fun_upd_def fun_upd_idem_iff)
   by (metis ArrayCpy Seq fun_upd_apply fun_upd_idem)
 
 lemma redundant_var_assignment: 
   assumes "x\<notin>fv_aexp i" "x\<notin>fv_aexp j"
   shows "(x[i] ::= Vidx a j;; a[j] ::= Vidx x i) \<sim> (x[i] ::= Vidx a j)"
   apply (rule)
   using assms[THEN aval_indep_non_fv]
    apply auto
   subgoal
     by (smt Assign' aval.simps(1) aval.simps(2) fun_upd_apply fun_upd_idem_iff)
   subgoal
     by (simp add: Assign' fun_upd_twist)
   subgoal
     by (smt Seq aval.simps(2) big_step.intros(2) fun_upd_def fun_upd_triv)
   done
 
     
 end
diff --git a/thys/IMP2/automation/IMP2_Specification.thy b/thys/IMP2/automation/IMP2_Specification.thy
--- a/thys/IMP2/automation/IMP2_Specification.thy
+++ b/thys/IMP2/automation/IMP2_Specification.thy
@@ -1,1118 +1,1117 @@
 section \<open>Specification Commands\<close>
 theory IMP2_Specification 
 imports IMP2_Basic_Simpset IMP2_Program_Analysis IMP2_Var_Postprocessor IMP2_Var_Abs
 keywords "ensures"
      and "returns" "variant" "relation"
      and "program_spec" :: thy_goal
      and "procedure_spec" :: thy_goal
      and "recursive_spec" :: thy_goal
 begin
 
   
 subsection \<open>Abstraction over Program Variables\<close>
 
 lemmas [named_ss vcg_bb cong] = refl[of "ANNOTATION _"]
 
 
 ML \<open> structure IMP_Annotations 
   = struct
     fun strip_annotations ctxt = 
       Local_Defs.unfold ctxt (Named_Theorems.get ctxt @{named_theorems vcg_annotation_defs})
     
     fun strip_annotations_term ctxt = 
       Thm.cterm_of ctxt #> Drule.mk_term #> 
       strip_annotations ctxt #>
       Drule.dest_term #> Thm.term_of
 
     fun mk_ANNOTATION t = let val T=fastype_of t in 
       Const (@{const_name ANNOTATION}, T --> T)$t end 
       
     fun dest_ANNOTATION (Const (@{const_name ANNOTATION}, _)$t) = t
       | dest_ANNOTATION t = raise TERM("dest_ANNOTATION", [t]);
       
     
     (* Provides a context for reading the term, and a postprocessing function *)
     type term_annot_reader = Proof.context * (term -> term)  
     fun gen_read_ta rd ((ctxt,post):term_annot_reader) src = rd ctxt src |> mk_BB_PROTECT |> post
     val read_ta_from_cartouche = gen_read_ta Term_Annot.read_term
 
     (* Annotations *)
     
     type cmd_annotation_readers = {
       rel_rd : term_annot_reader,
       variant_rd : term_annot_reader,
       invar_rd : term_annot_reader,
       com_post: term -> term
     }
     
           
     fun gen_interpret_annotations (annot_readers : cmd_annotation_readers) ctxt prog_t = let
     
       (* TODO/FIXME: Terms are read independently, which will cause too generic types to be inferred *)
 
       val read_invar = read_ta_from_cartouche (#invar_rd annot_readers)
       val read_variant = read_ta_from_cartouche (#variant_rd annot_readers)
       val read_rel = read_ta_from_cartouche (#rel_rd annot_readers)
           
       val mpt = map_types (map_type_tfree (K dummyT))
       
       fun interp_while_annot (t,@{syntax_const "_invariant_annotation"}) (R,V,I) = (R,V,read_invar t :: I)
         | interp_while_annot (t,@{syntax_const "_variant_annotation"})   (R,V,I) = (R,read_variant t :: V,I)
         | interp_while_annot (t,@{syntax_const "_relation_annotation"})  (R,V,I) = (read_rel t :: R,V,I)
         | interp_while_annot (_,ty) _ = error ("Unknown annotation type for while loop: " ^ ty)
       
       fun interp_while_annots annots = let
         val annots = HOLogic.strip_tuple annots
           |> map (apsnd (dest_Const #> fst) o Term_Annot.dest_annotated_term)
           
         val (Rs,Vs,Is) = fold interp_while_annot annots ([],[],[])
          
         val _ = length Rs > 1 andalso error "Multiple relation annotations to loop"
         val _ = length Vs > 1 andalso error "Multiple variant annotations to loop"
         val _ = length Is > 1 andalso error "Multiple invariants not yet supported. Combine them into one"
          
         local val m = map mk_ANNOTATION in
           val (Rs, Vs, Is) = (m Rs, m Vs, m Is)
         end
         
         
       in 
         case (Rs,Vs,Is) of
-          ([],[],[]) => mpt @{const While}
-        | ([],[],[I]) => mpt @{const WHILE_annotI} $ I
-        | ([],[V],[I]) => mpt @{const WHILE_annotVI} $ V $ I
-        | ([R],[V],[I]) => mpt @{const WHILE_annotRVI ('a)} $ R $ V $ I
+          ([],[],[]) => mpt \<^Const>\<open>While\<close>
+        | ([],[],[I]) => mpt \<^Const>\<open>WHILE_annotI for I\<close>
+        | ([],[V],[I]) => mpt \<^Const>\<open>WHILE_annotVI for V I\<close>
+        | ([R],[V],[I]) => mpt \<^Const>\<open>WHILE_annotRVI \<^typ>\<open>'a\<close> for R V I\<close>
         | _ => error "Illegal combination of annotations to while loop. The legal ones are: None, I, VI, RVI"
       
       end
       
       fun interp (Const (@{const_abbrev While_Annot},_)$annots) = interp_while_annots annots
         | interp (a$b) = interp a $ interp b
         | interp (Abs (x,T,t)) = Abs (x,T,interp t)
         | interp t = t
     
         
       val prog_t = interp prog_t
 
       (* All terms have been abstracted over vinfo, and over the variables of v0info. 
         Now, the whole term is valid wrt vinfo0/ctxt0, which contains declarations 
         of variables0 and state0
         *** TODO: Ideally, one would like to check teh term in a context that does not include 
               variables, but only state decl!
       *)      
       val prog_t = Syntax.check_term ctxt prog_t
       
             
       (* We now also abstract over state0, to make the program a function from state0 to an (annotated) command *)
       val res = (#com_post annot_readers) prog_t
 
       (*
       (* Alternatively, we strip the annotations from the program. This should also remove state0! *)
       val prog_t = strip_annotations_term ctxt prog_t
       *)
       
     in
       res
     end
 
 
     (*
       Make a reader according to a list of program variable abstractions.
       Each list item has the form (vars,sfx,full), where vars is a list of IMP variables,
       sfx is a suffix to be appended to the Isabelle variables, and full indicates whether the
       abstraction over the state should be done immediately, or delayed.
       
       The result is a reader, and a second term transformation to do the delayed abstractions.
     *)
     fun gen_mk_reader rds ctxt = let
       fun mk [] ctxt = ((ctxt, I), I)
         | mk ((vars,sfx,full)::rds) ctxt = let
             val vars = IMP_Parser.merge_variables vars
             val (vinfo,ctxt) = Program_Variables.declare_variables vars sfx ctxt
             val ((ctxt,pps1),pps2) = mk rds ctxt
                         
             val absv = Program_Variables.abstract_vars vinfo
             val abss = Program_Variables.abstract_state vinfo
             
             val (pps1,pps2) = if full then (absv #> pps1 #> abss,pps2) else (absv #> pps1, pps2 #> abss)
           in
             ((ctxt,pps1),pps2)
           end
           
     in
       mk rds ctxt
     end
 
     type rd_config = {
       add_vars  : IMP_Syntax.impvar list,           (* Additional variable declarations *)
       in_vars   : string list option,               (* Input variables: Default all vars *)
       out_vars  : string list option,               (* Output variables: Default all vars *)
       prog_vars : IMP_Syntax.impvar list            (* Variables in program *)
     }
     
         
     local  
       fun vars_dflt (cfg:rd_config) NONE = (#prog_vars cfg) @ (#add_vars cfg)
         | vars_dflt (cfg:rd_config) (SOME vs) = let
             val (gvs,lvs) = List.partition (IMP_Syntax.is_global) vs
             val _ = if gvs <> [] then 
               Pretty.block [Pretty.str "Ignoring global parameter/return variables: ",
                             Pretty.list "" "" (map (Pretty.str) gvs)]
               |> Pretty.string_of |> warning             
             else () 
         
           in
             (filter (fst #> member op= lvs) (#prog_vars cfg @ #add_vars cfg ))
           @ (filter (fst #> IMP_Syntax.is_global) (#add_vars cfg))  
           end
        
       fun cfg_in_vars cfg = vars_dflt cfg (#in_vars cfg)
       fun cfg_out_vars cfg = vars_dflt cfg (#out_vars cfg)
         
     in        
       (* Standard annotation readers *)
       
       
       fun mk_annot_readers (cfg:rd_config) ctxt = let
         val in_vars = cfg_in_vars cfg
         val prog_vars = (#prog_vars cfg) @ (#add_vars cfg)
         
         val (rel_rd,_) = gen_mk_reader [] ctxt
         val (annot_rd,post) = gen_mk_reader [(in_vars,"\<^sub>0",false),(prog_vars,"",true)] ctxt
       in 
         { 
           rel_rd = rel_rd,
           variant_rd = annot_rd,
           invar_rd = annot_rd,
           com_post = post
         }
       end
         
       fun mk_pre_reader cfg ctxt = gen_mk_reader [(cfg_in_vars cfg,"",true)] ctxt |> #1
         
       fun mk_post_reader cfg ctxt = let
         val in_vars = cfg_in_vars cfg
         val out_vars = cfg_out_vars cfg
       in
         gen_mk_reader [(in_vars,"\<^sub>0",true),(out_vars,"",true)] ctxt |> #1
       end  
   
       fun mk_variant_reader cfg ctxt = let
         val in_vars = cfg_in_vars cfg
       in
         gen_mk_reader [(in_vars,"",true)] ctxt |> #1
       end
 
       fun read_program cfg ctxt prog_t = 
         gen_interpret_annotations (mk_annot_readers cfg ctxt) ctxt prog_t
   
       
     end            
     
   end
 \<close>
 
 
 
 subsection \<open>Hoare Triple Syntax\<close>
   
 (* In-Term notation for Hoare Triples*)   
 syntax "_Htriple" :: "cartouche_position \<Rightarrow> cartouche_position \<Rightarrow> cartouche_position \<Rightarrow> logic" ("\<^htriple>_ _ _")
 syntax "_Htriple_Partial" :: "cartouche_position \<Rightarrow> cartouche_position \<Rightarrow> cartouche_position \<Rightarrow> logic" ("\<^htriple_partial>_ _ _")
 
 
 ML \<open> structure VCG_Htriple_Syntax 
   = struct
     
     fun mk_htriple' total env (pre,prog_t,post) = let    
       (* Assemble Hoare-triple *)
-      val HT_const = if total then @{const HT'} else @{const HT'_partial}
+      val HT_const = if total then \<^Const>\<open>HT'\<close> else \<^Const>\<open>HT'_partial\<close>
       val res = HT_const$ env $pre$prog_t$post
     in
       res
     end
     
     fun decon_cartouche_ast ((c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p) = (
       case Term_Position.decode_position p of 
         SOME (pos, _) => ((s,pos) (*, fn t => c$t$p*))
       | NONE => raise TERM ("cartouche with invalid pos",[c,p])  
     )
     | decon_cartouche_ast t = raise TERM ("decon_cartouche_ast",[t])  
         
     
     fun htriple_tr total ctxt [tpre, prog_t, tpost] = let
       open IMP_Annotations
     
       val (vars,prog_t) = decon_cartouche_ast prog_t |> IMP_Parser.parse_command_at ctxt
       
       val cfg = { add_vars = [], in_vars=NONE, out_vars=NONE, prog_vars=vars }
       
       val prog_t = read_program cfg ctxt prog_t
         
       val tpre = decon_cartouche_ast tpre 
         |> read_ta_from_cartouche (mk_pre_reader cfg ctxt)
         
       val tpost = decon_cartouche_ast tpost
         |> read_ta_from_cartouche (mk_post_reader cfg ctxt)
 
       val res = mk_htriple' total @{term "Map.empty :: program"} (tpre,prog_t,tpost)  
               
     in 
       IMP_Parser.mark_term res |> @{print}
     end
     | htriple_tr _ _ args = raise TERM ("htriple_tr", args)
       
     
   end
 \<close>
   
 parse_translation \<open>[
   (@{syntax_const "_Htriple"}, VCG_Htriple_Syntax.htriple_tr true),
   (@{syntax_const "_Htriple_Partial"}, VCG_Htriple_Syntax.htriple_tr false)
   ]
 \<close>
    
 term \<open>\<^htriple_partial> \<open>undefined x :: bool\<close> \<open>while (n\<noteq>0) @invariant \<open>x=1+undefined+n+foo\<close> n = n - 1; x=x+1\<close> \<open>True\<close>\<close> 
 
 term \<open>\<^htriple_partial> \<open>n\<ge>0+x+notex\<close> \<open>while (n\<noteq>0) n = n - 1; x=x+1\<close> \<open>n=0 \<and> x=1+x\<^sub>0\<close>\<close> 
 term \<open>\<^htriple> \<open>n\<ge>0+x+notex\<close> \<open>while (n\<noteq>0) n = n - 1; x=x+1\<close> \<open>n=0 \<and> x=1+x\<^sub>0\<close>\<close>
 
 
 subsection \<open>Postprocessing of Proved Specifications\<close>
 
 subsubsection \<open>Modified Sets\<close>
   
 lemma HT_to_mod: "HT \<pi> P c Q = HT_mods \<pi> (ANALYZE (lhsv \<pi> c)) P c Q"
   by (auto simp: HT_mods_def BB_PROTECT_def HT_def intro: wp_strengthen_modset wp_conseq)
 
 lemma HT_partial_to_mod: "HT_partial \<pi> P c Q = HT_partial_mods \<pi> (ANALYZE (lhsv \<pi> c)) P c Q"
   by (auto simp: HT_partial_mods_def BB_PROTECT_def HT_partial_def intro: wlp_strengthen_modset wlp_conseq)
 
 lemma mk_lhsv_thm:  
   assumes "c \<equiv> cmd"
   shows "lhsv \<pi> c = ANALYZE (lhsv \<pi> cmd)" "lhsv' c = ANALYZE (lhsv' cmd)"
   using assms by simp_all
   
   ML \<open> structure IMP2_Modified_Analysis 
     = struct
       fun dest_HT_mods (Const (@{const_name HT_mods},_)$pi$mods$P$c$Q) = (true,pi,mods,P,c,Q)
         | dest_HT_mods (Const (@{const_name HT_partial_mods},_)$pi$mods$P$c$Q) = (false,pi,mods,P,c,Q)
         | dest_HT_mods t = raise TERM("dest_HT_mods",[t])
           
 
       (* Valid modset must be set literal of string literals *)
       val is_valid_modset = can (HOLogic.dest_set #> map HOLogic.dest_string)
         
       (* Weaker criterion for valid modset  
       val is_valid_modset = not o exists_subterm (fn @{const lhsv} => true | _ => false)
       *)
       
                 
          
       (* HT \<rightarrow> HT_mods *) 
       fun mk_HT_mods ctxt thm = let
         (* Local_Defs.unfold will destroy names of bound variables here!?, so using simplify! *)
         fun simplified ctxt thms = simplify (Simplifier.clear_simpset ctxt addsimps thms)
       
         val ctxt = Named_Simpsets.put @{named_simpset vcg_bb} ctxt
       in
            thm
         |> simplified ctxt @{thms HT_to_mod HT_partial_to_mod}
         |> Simplifier.simplify ctxt
       end    
 
       
       (* c\<equiv>com \<rightarrow> [ lhsv c = \<dots>, lshv' c = \<dots> ] *)
       fun mk_lhsv_thms ctxt def_thm = let
         val ctxt = Named_Simpsets.put @{named_simpset vcg_bb} ctxt
       in
         map (fn thm => (def_thm RS thm) |> Simplifier.simplify ctxt) @{thms mk_lhsv_thm}
       end
       
     end
   \<close>
   
   
   
 subsubsection \<open>Parameter Passing\<close>  
 (* Forward assignment rule + renaming of assigned variable *)  
 lemma adjust_assign_after:
   assumes "HT \<pi> P c Q"
   shows "HT \<pi> P (c;;x[]::=y) (\<lambda>s\<^sub>0 s. \<exists>vx. Q s\<^sub>0 (s(x:=vx,y:=s x)))"  
   using assms unfolding HT_def
   apply (auto simp: wp_eq[abs_def])
   by (metis (mono_tags, lifting) fun_upd_triv wp_conseq)
 
 (* Standard backwards assignment rule *)
 lemma adjust_assign_before:
   assumes HT: "HT \<pi> P c Q"  
   shows "HT \<pi> (\<lambda>s. P (s(x:=s y)) ) (x[]::=y;; c) (\<lambda>s\<^sub>0 s. Q (s\<^sub>0(x:=s\<^sub>0 y)) s)"
   unfolding HT_def
   apply (clarsimp simp: wp_eq)  
   using HT_def assms by auto
     
   
 (* Forward + backward assignment rules, simultaneously for all local variables! *)
 lemma adjust_scope:
   assumes HT: "HT \<pi> P c Q"
   shows "HT \<pi> (\<lambda>s. P (<<>|s>)) (SCOPE c) (\<lambda>s\<^sub>0 s. \<exists>l. Q (<<>|s\<^sub>0>) (<l|s>))"
   unfolding HT_def
   apply (clarsimp simp: wp_eq)  
   by (smt HT_def assms combine_collapse combine_nest(1) wp_conseq)
 
   
 (* Forward assignment rule + renaming of assigned variable *)  
 lemma adjust_assign_after_partial:
   assumes "HT_partial \<pi> P c Q"
   shows "HT_partial \<pi> P (c;;x[]::=y) (\<lambda>s\<^sub>0 s. \<exists>vx. Q s\<^sub>0 (s(x:=vx,y:=s x)))"  
   using assms unfolding HT_partial_def
   apply (auto simp: wlp_eq[abs_def])
   by (metis (mono_tags, lifting) fun_upd_triv wlp_conseq)
 
 (* Standard backwards assignment rule *)
 lemma adjust_assign_before_partial:
   assumes HT: "HT_partial \<pi> P c Q"  
   shows "HT_partial \<pi> (\<lambda>s. P (s(x:=s y)) ) (x[]::=y;; c) (\<lambda>s\<^sub>0 s. Q (s\<^sub>0(x:=s\<^sub>0 y)) s)"
   unfolding HT_partial_def
   apply (clarsimp simp: wlp_eq)  
   using HT_partial_def assms by auto
     
   
 (* Forward + backward assignment rules, simultaneously for all local variables! *)
 lemma adjust_scope_partial:
   assumes HT: "HT_partial \<pi> P c Q"
   shows "HT_partial \<pi> (\<lambda>s. P (<<>|s>)) (SCOPE c) (\<lambda>s\<^sub>0 s. \<exists>l. Q (<<>|s\<^sub>0>) (<l|s>))"
   unfolding HT_partial_def
   apply (clarsimp simp: wlp_eq)  
   by (smt HT_partial_def assms combine_collapse combine_nest(1) wlp_conseq)
     
 
 definition "ADJUST_PRE_SCOPE P \<equiv> (\<lambda>s. P <<>|s>)"
 definition "ADJUST_PRE_PARAM l G P \<equiv> (\<lambda>s. P (s(l:=s G)))"
 definition "ADJUST_POST_SCOPE Q \<equiv> (\<lambda>s\<^sub>0 s. \<exists>l. Q (<<>|s\<^sub>0>) (<l|s>))"
 definition "ADJUST_POST_PARAM l G Q \<equiv> (\<lambda>s\<^sub>0 s. Q (s\<^sub>0(l:=s\<^sub>0 G)) s)"
 definition "ADJUST_POST_RETV G l Q \<equiv> (\<lambda>s\<^sub>0 s. \<exists>vx. Q s\<^sub>0 (s(G:=vx,l:=s G)))"
 
   
 lemma HT_strengthen_modset:  
   assumes "HT \<pi> P c Q"
   shows "HT \<pi> P c (\<lambda>s\<^sub>0 s. Q s\<^sub>0 s \<and> modifies (lhsv \<pi> c) s s\<^sub>0)"
   using assms unfolding HT_def by (auto intro: wp_strengthen_modset)
 
 lemma HT_partial_strengthen_modset:  
   assumes "HT_partial \<pi> P c Q"
   shows "HT_partial \<pi> P c (\<lambda>s\<^sub>0 s. Q s\<^sub>0 s \<and> modifies (lhsv \<pi> c) s s\<^sub>0)"
   using assms unfolding HT_partial_def by (auto intro: wlp_strengthen_modset)
       
     
 context
   notes [abs_def, simp] = VAR_def 
     ADJUST_PRE_SCOPE_def ADJUST_PRE_PARAM_def ADJUST_POST_SCOPE_def ADJUST_POST_PARAM_def ADJUST_POST_RETV_def
   notes [simp] = combine_query
 begin
 
   text \<open>A lot of straightforward lemmas, to transfer specification of function body to function specification\<close>
   
   lemma ADJUST_PRE_SCOPE_unfolds:
     "\<And>P. ADJUST_PRE_SCOPE (\<lambda>_. P) = (\<lambda>_. P)"
     "\<And>P. ADJUST_PRE_SCOPE (\<lambda>s. VAR v (\<lambda>x. P x s)) = VAR v (\<lambda>x. ADJUST_PRE_SCOPE (\<lambda>s. P x s))"
     
     "\<And>P. is_global x \<Longrightarrow> ADJUST_PRE_SCOPE (\<lambda>s. VAR (s x i) (\<lambda>x. P x s)) = (\<lambda>s. VAR (s x i) (\<lambda>x. ADJUST_PRE_SCOPE (\<lambda>s. P x s) s))"
     "\<And>P. is_global x \<Longrightarrow> ADJUST_PRE_SCOPE (\<lambda>s. VAR (s x) (\<lambda>x. P x s)) = (\<lambda>s. VAR (s x) (\<lambda>x. ADJUST_PRE_SCOPE (\<lambda>s. P x s) s))"
     by auto
   
   lemma ADJUST_PRE_PARAM_unfolds:  
     "\<And>P. ADJUST_PRE_PARAM l G (\<lambda>_. P) = (\<lambda>_. P)"
     "\<And>P. ADJUST_PRE_PARAM l G (\<lambda>s. VAR v (\<lambda>x. P x s)) = VAR v (\<lambda>x. ADJUST_PRE_PARAM l G (\<lambda>s. P x s))"
     
     
     "\<And>P. ADJUST_PRE_PARAM l G (\<lambda>s. VAR (s l i) (\<lambda>x. P x s)) = (\<lambda>s. VAR (s G i) (\<lambda>x. ADJUST_PRE_PARAM l G (\<lambda>s. P x s) s))"
     "\<And>P. ADJUST_PRE_PARAM l G (\<lambda>s. VAR (s l) (\<lambda>x. P x s)) = (\<lambda>s. VAR (s G) (\<lambda>x. ADJUST_PRE_PARAM l G (\<lambda>s. P x s) s))"
     
     "\<And>P. x\<noteq>l \<Longrightarrow> ADJUST_PRE_PARAM l G (\<lambda>s. VAR (s x i) (\<lambda>x. P x s)) = (\<lambda>s. VAR (s x i) (\<lambda>x. ADJUST_PRE_PARAM l G (\<lambda>s. P x s) s))"
     "\<And>P. x\<noteq>l \<Longrightarrow> ADJUST_PRE_PARAM l G (\<lambda>s. VAR (s x) (\<lambda>x. P x s)) = (\<lambda>s. VAR (s x) (\<lambda>x. ADJUST_PRE_PARAM l G (\<lambda>s. P x s) s))"
     by auto
     
   lemma ADJUST_POST_SCOPE_unfolds:
     "\<And>P. ADJUST_POST_SCOPE (\<lambda>_ _. P) = (\<lambda>_ _. P)"
     
     "\<And>P. is_global x \<Longrightarrow> ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x i) (\<lambda>x. ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. is_global x \<Longrightarrow> ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x) (\<lambda>x. ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     
     "\<And>P. is_global x \<Longrightarrow> ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. VAR (s x i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s x i) (\<lambda>x. ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. is_global x \<Longrightarrow> ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. VAR (s x) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s x) (\<lambda>x. ADJUST_POST_SCOPE (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     by auto
   
   lemma ADJUST_POST_PARAM_unfolds: 
     "\<And>P. ADJUST_POST_PARAM l G (\<lambda>_ _. P) = (\<lambda>_ _. P)" 
     
     "\<And>P. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 l i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 G i) (\<lambda>x. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 l) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 G) (\<lambda>x. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
   
     "\<And>P. x\<noteq>l \<Longrightarrow> ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x i) (\<lambda>x. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. x\<noteq>l \<Longrightarrow> ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x) (\<lambda>x. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     
     "\<And>P. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. VAR (s x i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s x i) (\<lambda>x. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. VAR (s x) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s x) (\<lambda>x. ADJUST_POST_PARAM l G (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     by auto
         
   lemma ADJUST_POST_RETV_unfolds:
     "\<And>P. ADJUST_POST_RETV G l (\<lambda>_ _. P) = (\<lambda>_ _. P)"
     
     "\<And>P. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x i) (\<lambda>x. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s\<^sub>0 x) (\<lambda>x. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
   
     "\<And>P. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. VAR (s l i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s G i) (\<lambda>x. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. VAR (s l) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s G) (\<lambda>x. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
       
     "\<And>P. \<lbrakk>x\<noteq>G; x\<noteq>l\<rbrakk> \<Longrightarrow> ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. VAR (s x i) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s x i) (\<lambda>x. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     "\<And>P. \<lbrakk>x\<noteq>G; x\<noteq>l\<rbrakk> \<Longrightarrow> ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. VAR (s x) (\<lambda>x. P x s\<^sub>0 s)) = (\<lambda>s\<^sub>0 s. VAR (s x) (\<lambda>x. ADJUST_POST_RETV G l (\<lambda>s\<^sub>0 s. P x s\<^sub>0 s) s\<^sub>0 s))"
     by auto
   
   lemmas ADJUST_unfolds = ADJUST_PRE_SCOPE_unfolds ADJUST_PRE_PARAM_unfolds 
     ADJUST_POST_SCOPE_unfolds ADJUST_POST_PARAM_unfolds ADJUST_POST_RETV_unfolds
       
   (* TODO: Clean up these proofs! *)  
   lemma HT_mods_adjust_scope: 
     assumes "HT_mods \<pi> vs P c Q"
     shows "HT_mods \<pi> (Set.filter is_global vs) (ADJUST_PRE_SCOPE P) (SCOPE c) (ADJUST_POST_SCOPE Q)"
     using assms unfolding HT_mods_def 
     apply (drule_tac adjust_scope)
     apply simp
     apply (drule_tac HT_strengthen_modset)
     apply (erule HT_conseq)
      apply simp
     apply (clarsimp simp: modifies_split)
     apply (drule (1) modifies_join)
     apply (auto elim: modifies_mono[rotated])
     done
     
   lemma HT_mods_adjust_param: 
     assumes "HT_mods \<pi> vs P c Q"
     shows "HT_mods \<pi> (insert l vs) (ADJUST_PRE_PARAM l G P) (l[]::=G;; c) (ADJUST_POST_PARAM l G Q)"
     using assms unfolding HT_mods_def 
     apply (drule_tac adjust_assign_before[of \<pi> P c _ l G])
     apply (erule HT_conseq)
      apply simp
     apply (auto simp: modifies_def)
     done
     
   lemma HT_mods_adjust_retv:
     assumes "HT_mods \<pi> vs P c Q"
     shows "HT_mods \<pi> (insert G vs) P (c;; G[]::=l) (ADJUST_POST_RETV G l Q)"
     using assms unfolding HT_mods_def
     apply simp
     apply (unfold HT_def; clarsimp simp: wp_eq)
     apply (drule spec, erule (1) impE)
     apply (erule wp_conseq)
     apply (auto simp add: wp_eq modifies_def)
     by (metis fun_upd_triv)
 
   lemma HT_partial_mods_adjust_scope: 
     assumes "HT_partial_mods \<pi> vs P c Q"
     shows "HT_partial_mods \<pi> (Set.filter is_global vs) (ADJUST_PRE_SCOPE P) (SCOPE c) (ADJUST_POST_SCOPE Q)"
     using assms unfolding HT_partial_mods_def 
     apply (drule_tac adjust_scope_partial)
     apply (drule_tac HT_partial_strengthen_modset)
     apply (erule HT_partial_conseq)
      apply simp
     apply (clarsimp simp: modifies_split)
     apply (drule (1) modifies_join)
     apply (auto elim: modifies_mono[rotated])
     done
     
   lemma HT_partial_mods_adjust_param: 
     assumes "HT_partial_mods \<pi> vs P c Q"
     shows "HT_partial_mods \<pi> (insert l vs) (ADJUST_PRE_PARAM l G P) (l[]::=G;; c) (ADJUST_POST_PARAM l G Q)"
     using assms unfolding HT_partial_mods_def 
     apply (drule_tac adjust_assign_before_partial[of \<pi> P c _ l G])
     apply (erule HT_partial_conseq)
      apply simp
     apply (auto simp: modifies_def)
     done
     
   lemma HT_partial_mods_adjust_retv:
     assumes "HT_partial_mods \<pi> vs P c Q"
     shows "HT_partial_mods \<pi> (insert G vs) P (c;; G[]::=l) (ADJUST_POST_RETV G l Q)"
     using assms unfolding HT_partial_mods_def
     apply simp
     apply (unfold HT_partial_def; clarsimp simp: wlp_eq)
     apply (drule spec, erule (1) impE)
     apply (erule wlp_conseq)
     apply (auto simp add: wlp_eq modifies_def)
     by (metis fun_upd_triv)
     
         
 end
 
 lemma HT_generalize_penv:
   assumes "HT_mods Map.empty mods P c Q"
   shows "HT_mods \<pi> mods P c Q"
   using assms unfolding HT_mods_def HT_def wp_def
   apply auto 
   using big_step_mono_prog map_le_empty by blast
 
   
 ML \<open>structure IMP2_Parameters 
   = struct
     fun adjust_retv_rl ctxt G l thm = let
       val G = HOLogic.mk_string G |> Thm.cterm_of ctxt
       val l = HOLogic.mk_string l |> Thm.cterm_of ctxt
       
       val rs_thms = @{thms HT_mods_adjust_retv HT_partial_mods_adjust_retv}
         |> map (Drule.infer_instantiate' ctxt [NONE, NONE, NONE, NONE, NONE, SOME G, SOME l])
     in thm RS_fst rs_thms end
   
     fun adjust_param_rl ctxt G l thm = let
       val G = HOLogic.mk_string G |> Thm.cterm_of ctxt
       val l = HOLogic.mk_string l |> Thm.cterm_of ctxt
       
       val rs_thms = @{thms HT_mods_adjust_param HT_partial_mods_adjust_param}
         |> map (Drule.infer_instantiate' ctxt [NONE, NONE, NONE, NONE, NONE, SOME l, SOME G])
     in thm RS_fst rs_thms end
     
     fun adjust_scope_rl (_:Proof.context) thm = thm RS_fst @{thms HT_mods_adjust_scope HT_partial_mods_adjust_scope}
       
     
     fun adjust_proc_rl imp_params imp_retvs ctxt thm = let
       val params = IMP_Syntax.zip_with_param_names imp_params
       val retvs = IMP_Syntax.zip_with_ret_names imp_retvs
       
       val ctxt = Named_Simpsets.put @{named_simpset vcg_bb} ctxt
       val ctxt = ctxt addsimps @{thms ADJUST_unfolds}
   
       val thm = thm
         |> fold_rev (uncurry (adjust_retv_rl ctxt)) retvs
         |> fold_rev (uncurry (adjust_param_rl ctxt)) params
         |> adjust_scope_rl ctxt
         |> Simplifier.simplify ctxt
     
     in
       thm
     end
   
   end
 \<close>
   
   
   
 subsubsection \<open>Recursion\<close>
 lemma HT_mods_fold_call:
   assumes "\<pi> p = Some c"
   assumes "HT_mods \<pi> mods P c Q"
   shows "HT_mods \<pi> mods P (PCall p) Q"
   using assms 
   unfolding HT_mods_def HT_def
   by (auto simp: wp_eq wp_pcall_eq)
 
     
 lemma localize_HT_mods: 
   assumes "HT_mods \<pi> mods P (PCall p) Q"
   shows "HT_mods \<pi>' mods P (PScope \<pi> (PCall p)) Q"
   using assms unfolding HT_mods_def HT_def wp_def
   by (simp add: localize_recursion)
 
 lemmas localize_HT_mods' = localize_HT_mods[where \<pi>'="Map.empty"]
   
 
 definition "PROVE_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 \<Theta> \<equiv> \<forall>P c Q. (f\<^sub>0,(P,c,Q))\<in>\<Theta> \<and> P s\<^sub>0 \<longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0"
 
 lemma PROVE_\<Theta>I[vcg_preprocess_rules]:
   "PROVE_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 {}" 
   "\<lbrakk>\<lbrakk>RENAMING f\<^sub>0 f; BB_PROTECT (P s\<^sub>0)\<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0; PROVE_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 \<Theta>\<rbrakk> \<Longrightarrow> PROVE_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 (insert (f,(P,c,Q)) \<Theta>)" 
   unfolding PROVE_\<Theta>_def BB_PROTECT_def RENAMING_def
   by auto 
 
   
 definition "JOIN_VARS f g P \<equiv> P f g"  
 lemma JOIN_VARS: 
   "\<And>v f g P. JOIN_VARS (VAR v (\<lambda>x. f x)) g P = VAR v (\<lambda>x. JOIN_VARS (f x) g P)"
   "\<And>v f g P. JOIN_VARS f (VAR v (\<lambda>x. g x)) P = VAR v (\<lambda>x. JOIN_VARS f (g x) P)"
   "\<And>f g P. JOIN_VARS (BB_PROTECT f) (BB_PROTECT g) P = P f g"
   by (auto simp: JOIN_VARS_def BB_PROTECT_def VAR_def)
   
 ML \<open>
   fun join_vars_rl ctxt thm0 = let 
     val thm = Local_Defs.unfold ctxt @{thms JOIN_VARS} thm0
     
     val t = Thm.prop_of thm
     val cns = Term.add_const_names t []
     val _ = member op= cns @{const_name JOIN_VARS} andalso raise THM("join_vars_rl: not joined",~1,[thm0,thm])
   in
     thm
   end
 \<close>  
   
   
 definition "ASSUME_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 R \<Theta> \<equiv> HT'set_r (\<lambda>f' s'. ((f' s'),(f\<^sub>0 s\<^sub>0))\<in>R ) \<pi> \<Theta>"
   
 lemmas ASSUME_\<Theta>E1 = thin_rl[of "ASSUME_\<Theta> _ _ _ _ {}"]
 
 lemma ASSUME_\<Theta>E2:
   assumes "ASSUME_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 R (insert (f,(P,c,Q)) \<Theta>)"
   obtains "HT' \<pi> (\<lambda>s. JOIN_VARS (f s) (P s) (\<lambda>v P. BB_PROTECT ((v,(f\<^sub>0 s\<^sub>0))\<in>R \<and> P))) c Q" "ASSUME_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 R \<Theta>"
   using assms unfolding ASSUME_\<Theta>_def HT'set_r_def JOIN_VARS_def BB_PROTECT_def by auto
   
 lemmas ASSUME_\<Theta>E = ASSUME_\<Theta>E1 ASSUME_\<Theta>E2
 
 lemma vcg_HT'setI:    
   assumes "wf R"
   assumes RL: "\<And>f\<^sub>0 s\<^sub>0. \<lbrakk> ASSUME_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 R \<Theta> \<rbrakk> \<Longrightarrow> PROVE_\<Theta> \<pi> f\<^sub>0 s\<^sub>0 \<Theta>"
   shows "HT'set \<pi> \<Theta>"
   using assms HT'setI[of R \<pi> \<Theta>] 
   unfolding ASSUME_\<Theta>_def PROVE_\<Theta>_def HT'set_def 
   by auto
 
   
 subsubsection \<open>Consistency Check\<close>  
 
 ML \<open>structure Spec_Consistency_Check 
   = struct
       fun check_ht_mods thm = let
         val (_,_,mods,P,_,Q) = Thm.concl_of thm 
           |> HOLogic.dest_Trueprop |> IMP2_Modified_Analysis.dest_HT_mods
       
         fun fail msg = raise THM ("Consistency check: "^msg,~1,[thm])
         
         (* Check that modset is OK *)  
         val _ = IMP2_Modified_Analysis.is_valid_modset mods orelse fail "invalid modset"
         
         (* Check for relicts in pre/postcondition *)
         val bad_consts = [
           @{const_name ADJUST_PRE_PARAM}, 
           @{const_name ADJUST_PRE_SCOPE}, 
           @{const_name ADJUST_POST_PARAM}, 
           @{const_name ADJUST_POST_RETV}, 
           @{const_name ADJUST_POST_SCOPE}
           ]
 
         fun is_bad_const (n,_) = member op= bad_consts n
           
         val _ = exists_Const is_bad_const P andalso fail "VCG relict in precondition"
         val _ = exists_Const is_bad_const Q andalso fail "VCG relict in precondition"
       in
         ()
       end
   
   end
 \<close>
   
 (* Summarizes postprocessors for specifications *)
 ML \<open>structure Spec_Postprocessing 
   = struct
     (*
       Strip annotations
     *)
     fun cnv_HT'_to_HT ctxt = 
          IMP_Annotations.strip_annotations ctxt
       #> Local_Defs.unfold ctxt @{thms HT'_unfolds}
     
     (*
       Modifies Analysis
     *)
     val cnv_HT_to_HTmod = IMP2_Modified_Analysis.mk_HT_mods
       
     (*
       Make procedure frame
     *)
     val cnv_body_to_proc = IMP2_Parameters.adjust_proc_rl
     
     (*
       Generalize over procedure environment
     *)
     fun cnv_HTmod_generalize_penv thm = thm RS_fst @{thms HT_generalize_penv asm_rl}
   
     (*
       Define command as constant
     *)
     fun define_HTmod_const binding thm lthy = let
       (* Extract Command *)
       val (_,_,_,_,cmd,_) = Thm.concl_of thm |> HOLogic.dest_Trueprop |> IMP2_Modified_Analysis.dest_HT_mods
 
       (* Define *)
       val lhs = Free (Binding.name_of binding, fastype_of cmd)
       val eqn = Logic.mk_equals (lhs,cmd)
       val ((lhs,(_,def_thm)),lthy) = Specification.definition (SOME (binding,NONE,Mixfix.NoSyn)) [] [] ((Binding.empty,[]),eqn) lthy
       
       (* Fold definition in theorem *)
       val thm = Local_Defs.fold lthy [def_thm] thm
       
       (* Sanity check: Has definition actually been folded? *)
       val _ = exists_subterm (curry op = lhs) (Thm.prop_of thm)
         orelse raise THM("spec_program_cmd: Failed to fold command definition",~1,[thm])
       
     in
       ((binding,def_thm,thm), lthy)
     end 
     
     (*
       Declare defined command and specification to VCG
     *)
     fun declare_defined_spec (binding,def_thm,thm) lthy = let
       (* Sanity check: Various consistency checks *)  
       val _ = Spec_Consistency_Check.check_ht_mods thm
 
       val note = snd oo Local_Theory.note
 
       (* Note specification theorem, register as [vcg_rule] *)
       val spec_thm_name = Binding.suffix_name "_spec" binding
       val lthy = note ((spec_thm_name,@{attributes [vcg_specs]}),[thm]) lthy 
                 
       (* Create lhsv-theorems, register as vcg_bb simp-rule *)
       val lhsv_thms = IMP2_Modified_Analysis.mk_lhsv_thms lthy def_thm
       val lhsv_thm_name = Binding.suffix_name "_lhsv" binding
       val lthy = note ((lhsv_thm_name,@{attributes [named_ss vcg_bb]}),lhsv_thms) lthy
     in
       lthy
     end
 
     fun define_declare binding thm = 
         define_HTmod_const binding thm 
       #> uncurry declare_defined_spec
         
 
   end
 \<close>
 
 subsection \<open>Program Specification Commands\<close>
 
 ML \<open>structure Simple_Program_Specification 
   = struct
     fun simple_spec_program_cmd binding partial add_vars params pre_src post_src cmd_src lthy = let
       val total = not partial
       
       open IMP_Annotations
       
       val (prog_vars,prog_t) = IMP_Parser.parse_command_at lthy cmd_src
       
       val cfg = case params of 
         NONE => { add_vars = add_vars, in_vars=NONE, out_vars=NONE, prog_vars=prog_vars }
       | SOME (pvs,rvs) => { add_vars = add_vars, in_vars=SOME pvs, out_vars=SOME rvs, prog_vars=prog_vars }
       
       val prog_t = read_program cfg lthy prog_t
       
       val pre = gen_read_ta Syntax.read_term (mk_pre_reader cfg lthy) pre_src
       val post = gen_read_ta Syntax.read_term (mk_post_reader cfg lthy) post_src
       
       val goal = VCG_Htriple_Syntax.mk_htriple' total @{term "Map.empty::program"} (pre,prog_t,post)
       
       val goal = HOLogic.mk_Trueprop goal
 
       fun after_qed thmss lthy = let
       
         val param_post = case params of 
           NONE => K I 
         | SOME (pvs,rvs) => Spec_Postprocessing.cnv_body_to_proc pvs rvs
       
         val thm = flat thmss 
           |> the_single
           |> Spec_Postprocessing.cnv_HT'_to_HT lthy
           |> Spec_Postprocessing.cnv_HT_to_HTmod lthy
           |> param_post lthy
           |> Spec_Postprocessing.cnv_HTmod_generalize_penv
 
         val lthy = Spec_Postprocessing.define_declare binding thm lthy
       in
         lthy
       end
     
     in Proof.theorem NONE after_qed [[(goal,[])]] lthy end
 
   end
 \<close>
 
 
 ML \<open>structure Recursive_Program_Specification 
   = struct
       type proc_spec_src = {    
         binding:  binding,                   (* name *)
         params: string list,                 (* parameters *)
         retvs: string list,                  (* return variables *)
         addvars: IMP_Syntax.impvar list,     (* additional variables *)
         pre_src: string,                     (* precondition src *)
         post_src: string,                    (* postcondition src *)
         variant_src: string,                 (* variant src *)
         cmd_src: string * Position.T         (* body src *)
       }
   
       type proc_spec = {    
         binding:  binding,                   (* name *)
         params: string list,                 (* parameters *)
         retvs: string list,                  (* return variables *)
         addvars: IMP_Syntax.impvar list,     (* additional variables *)
         pre: term,                           (* precondition src *)
         post: term,                          (* postcondition src *)
         variant: term,                       (* variant src *)
         cmd: term                            (* body src *)
       }
       
           
       fun check_spec ctxt (spec_src : proc_spec_src) = let
         open IMP_Annotations
       
         val (prog_vars,prog_t) = IMP_Parser.parse_command_at ctxt (#cmd_src spec_src)
         val cfg = { 
           add_vars = #addvars spec_src, 
           in_vars=SOME (#params spec_src), 
           out_vars=SOME (#retvs spec_src), 
           prog_vars=prog_vars }
         
         val prog_t = read_program cfg ctxt prog_t
         
         val pre = gen_read_ta Syntax.read_term (mk_pre_reader cfg ctxt) (#pre_src spec_src)
         val post = gen_read_ta Syntax.read_term (mk_post_reader cfg ctxt) (#post_src spec_src)
         val variant = gen_read_ta Syntax.read_term (mk_variant_reader cfg ctxt) (#variant_src spec_src)
         
       in
         ({
           binding = (#binding spec_src),
           params=(#params spec_src),
           retvs=(#retvs spec_src),
           addvars=(#addvars spec_src),
           pre=pre,
           post=post,
           variant=variant,
           cmd=prog_t
         })
       end
   
   
       fun adjust_thm params retvs ctxt = let
         open Spec_Postprocessing
       in
         I
         #> cnv_HT'_to_HT ctxt
         #> cnv_HT_to_HTmod ctxt
         #> cnv_body_to_proc params retvs ctxt
       end
       
       fun gen_spec_program_cmd rel_src spec_srcs lthy = let
       
         val ctxt = lthy
       
         fun trace msg = tracing msg
       
         val _ = trace "(* Check Specification *)"
       
         val rel = the_default @{term \<open>measure nat\<close>} (Option.map (Syntax.read_term ctxt) rel_src)
         val relT = fastype_of rel |> HOLogic.dest_setT |> HOLogic.dest_prodT |> fst
       
         val specs = map (check_spec ctxt) spec_srcs
   
         val _ = trace "(* Create dummy procedure environment *)"
         (*val ctxt0 = ctxt*)
         val (pe_var,ctxt) = yield_singleton Proof_Context.add_fixes (@{binding \<pi>},SOME @{typ program},Mixfix.NoSyn) ctxt
         val pe_var = Free (pe_var,@{typ program})
         
         val _ = trace "(* Define initial goal *)"
         fun mk_theta_entry {variant, pre, cmd, post, ...} = HOLogic.mk_tuple [variant, HOLogic.mk_tuple [pre,cmd,post]]
         
         val thetaT = @{typ "'a \<Theta>elem_t"} |> typ_subst_atomic [(@{typ 'a},relT)]
         val theta = map mk_theta_entry specs |> HOLogic.mk_set thetaT
         
-        val HT'setC = @{const HT'set ('a)} |> subst_atomic_types [(@{typ 'a},relT)]
-        val goal = HT'setC $ pe_var $ theta
+        val goal = \<^Const>\<open>HT'set relT\<close> $ pe_var $ theta
           |> HOLogic.mk_Trueprop
         
         val _ = trace "(* Start proof *)"
         val st = Thm.cterm_of ctxt goal |> Goal.init  
           
         val _ = trace "(* Apply recursion rule, and solve wf-precondition *)"
         val crel = Thm.cterm_of ctxt rel
         val sr_rl = Drule.infer_instantiate' ctxt [SOME crel] @{thm vcg_HT'setI}
   
         val st = Det_Goal_Refine.apply1 "" (resolve_tac ctxt [sr_rl]) st
         val st = Det_Goal_Refine.apply1 "Failed to solve wf-goal" 
           (SOLVED' (force_tac ctxt ORELSE' SELECT_GOAL (print_tac ctxt ""))) st
   
         val _ = trace "(* Explode theta-assumptions *)"
         val st = Det_Goal_Refine.apply1 "" (REPEAT_ALL_NEW (ematch_tac ctxt @{thms ASSUME_\<Theta>E})) st
       
         (* At this point, we have: \<And>f\<^sub>0 s\<^sub>0. \<lbrakk> HT' \<pi> \<dots>; HT' \<pi> \<dots>; \<dots> \<rbrakk> \<Longrightarrow> PROVE_\<Theta> \<pi> \<dots> *)
         
         val _ = trace "(* Join VARs in preconditions *)"
         val st = Det_Goal_Refine.apply1 "" (Thm_Mapping.map_all_prems_tac join_vars_rl ctxt) st
         
         val _ = trace "(* Wrap premises *)"
         fun wrap_thm_rl {params,retvs,...} ctxt thm = adjust_thm params retvs ctxt thm
         val wrap_thm_rls = map wrap_thm_rl specs 
         val st = Det_Goal_Refine.apply1 "" (Thm_Mapping.map_prems_tac wrap_thm_rls ctxt) st
         
         val _ = trace "(* Read wrapped commands to define procedure environment *)"
         val cmds = Logic.prems_of_goal (Thm.prop_of st) 1
           |> map (
                HOLogic.dest_Trueprop 
             #> IMP2_Modified_Analysis.dest_HT_mods
             #> #5
           )
           
         val _ = trace "(* Define procedure environment *)"
         fun proc_name_t_of {binding, ...} = HOLogic.mk_string (Binding.name_of binding)
           
         val penv_pairs = specs ~~ cmds
           |> map (apfst proc_name_t_of)
         
         val penv = HOLOption.mk_map_list @{typ pname} @{typ com} penv_pairs
                   
         val eqn = Logic.mk_equals (pe_var,penv) |> Thm.cterm_of ctxt
         val (pe_def,ctxt) = yield_singleton (Assumption.add_assms Local_Defs.def_export) eqn ctxt
   
         
         val _ = trace "(* Add theorem for lhsv\<pi> \<pi> *)"
         val lhsv_pi_thm = (@{lemma \<open>\<And>\<pi> \<pi>r. \<pi>\<equiv>\<pi>r \<Longrightarrow> lhsv\<pi> \<pi> = ANALYZE (lhsv\<pi> \<pi>r)\<close> by auto} OF [pe_def])
           |> vcg_bb_simplify [] ctxt
           
         val ctxt = Context.proof_map (Named_Simpsets.add_simp @{named_simpset vcg_bb} lhsv_pi_thm) ctxt
   
         val _ = trace "(* Finish modifies-analysis in HT' assumptions *)"
         fun finish_mdf ctxt thm = 
           (@{lemma \<open>\<And>\<pi> vs P c Q. HT_mods \<pi> vs P c Q \<Longrightarrow> HT_mods \<pi> (ANALYZE vs) P c Q\<close> by auto} OF [thm])
           |> vcg_bb_simplify [] ctxt
           
         val st = Det_Goal_Refine.apply1 "" (Thm_Mapping.map_all_prems_tac finish_mdf ctxt) st
         
         val _ = trace "(* Wrap assumptions into calls *)"
         (** First, show unfold theorems *)
         fun mk_unfold_thm (pname,com) = Goal.prove ctxt [] [] 
           (HOLogic.mk_eq (pe_var$pname,HOLOption.mk_Some com) |> HOLogic.mk_Trueprop)
           (fn {context=ctxt, ...} => ALLGOALS (vcg_bb_simp_tac [pe_def] ctxt))
         
         val unfold_thms = map mk_unfold_thm penv_pairs
                 
         val wrap_call_rls = map (fn ufthm => fn _ => fn htthm => @{thm HT_mods_fold_call} OF [ufthm,htthm]) unfold_thms
         val st = Det_Goal_Refine.apply1 "" (Thm_Mapping.map_prems_tac wrap_call_rls ctxt) st
   
         val _ = trace "(* Focus on goal *)"
         val st_before_focus = st val ctxt_before_focus = ctxt
         val (focus as {context = ctxt, prems, ...},st) = Subgoal.focus ctxt 1 NONE st
         
         val _ = trace "(* Note ht-premises *)"
         val (_,ctxt) = Proof_Context.note_thms "" 
             ((Binding.name "rec_rules",[Named_Theorems.add @{named_theorems vcg_specs}]), 
               [(prems,[])]) ctxt
         
         val _ = trace "(* Prepare user proof *)"
         val termss = Thm.prems_of st |> map (fn t => (t,[]))
         
         (* --- user proof is logically here --- *)
         
         fun after_qed thmss goal_ctxt' = let
           val thms = flat thmss |> Proof_Context.export goal_ctxt' ctxt
           val _ = trace "(* Solve subgoals of st *)"
           val st = fold (fn thm => fn st => Thm.implies_elim st thm) thms st (* TODO: Use resolve_tac here? *)
            
           val st = singleton (Proof_Context.export ctxt (#context focus)) st
           
           val _ = trace "(* retrofit over focus, and finish goal *)"
           val st = Subgoal.retrofit (#context focus) ctxt_before_focus (#params focus) (#asms focus) 1 st st_before_focus 
             |> Det_Goal_Refine.seq_first ""
           val ctxt = ctxt_before_focus  
             
           val thm = Goal.finish ctxt st |> Goal.norm_result ctxt
           
           val _ = trace "(* Explode HT'set goal into single HTs *)"
           fun explode_HT'set thm = (case try (fn thm => thm RS @{thm HT'setD(1)}) thm of
             NONE => []
           | SOME thm' => thm' :: explode_HT'set (thm RS @{thm HT'setD(2)}))
   
           val thms = explode_HT'set thm
                   
           val _ = trace "(* Adjust theorems *)"
           
           val thms = thms
             |> Thm_Mapping.map_thms ctxt wrap_thm_rls
             |> Thm_Mapping.map_thms ctxt wrap_call_rls
           
           val thms = map (fn thm => thm RS @{thm localize_HT_mods}) thms  
   
           val _ = trace "(* Define constants *)"
           
           val ctxt = fold 
             (fn ({binding,...},thm) => Spec_Postprocessing.define_declare binding thm) 
             (specs ~~ thms) ctxt
             
         in
           ctxt
         end      
   
       in Proof.theorem NONE after_qed [termss] ctxt end
   end
 \<close>
 
 
 ML \<open> structure Program_Specification_Parser 
   = struct
     val parse_param_decls = Args.parens (Parse.enum "," Parse.name)
     
     val parse_var_decl = Parse.name -- Scan.optional (\<^keyword>\<open>[\<close>--\<^keyword>\<open>]\<close> >> K IMP_Syntax.ARRAY) IMP_Syntax.VAL
     val parse_var_decls = Scan.optional (\<^keyword>\<open>for\<close> |-- Scan.repeat parse_var_decl) []
   
     val parse_returns_clause = Scan.optional (
       \<^keyword>\<open>returns\<close> |-- (Args.parens (Parse.enum "," Parse.name) || Parse.name >> single)
     ) []
     
     val parse_proc_spec = (
           Parse.binding 
        -- parse_param_decls
        -- parse_returns_clause
       --| \<^keyword>\<open>assumes\<close> -- Parse.term 
       --| \<^keyword>\<open>ensures\<close> -- Parse.term 
       --| \<^keyword>\<open>variant\<close> -- Parse.term 
        -- parse_var_decls
       --| \<^keyword>\<open>defines\<close> -- (Parse.position (Parse.cartouche>>cartouche)) 
       ) >> (fn (((((((binding,params),retvs),pre_src),post_src),variant_src),addvars),cmd_src) => 
         {
           binding = binding, 
           params=params, 
           retvs=retvs, 
           pre_src=pre_src, 
           post_src=post_src, 
           variant_src=variant_src,
           addvars=addvars,
           cmd_src=cmd_src} : Recursive_Program_Specification.proc_spec_src
       )
     
     
   end
 \<close>
 
 
   ML \<open>
     let
       open Simple_Program_Specification Recursive_Program_Specification Program_Specification_Parser
     in
       
       Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>program_spec\<close> "Define IMP program and prove specification"
         ((Args.mode "partial" -- Parse.binding 
           --| \<^keyword>\<open>assumes\<close> -- Parse.term 
           --| \<^keyword>\<open>ensures\<close> -- Parse.term 
            -- parse_var_decls
           --| \<^keyword>\<open>defines\<close> -- (Parse.position (Parse.cartouche>>cartouche)) 
           ) >> (fn (((((partial,bnd),pre_src),post_src),addvars),cmd_src) => 
                   simple_spec_program_cmd bnd partial addvars NONE pre_src post_src cmd_src));
     
     
     Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>procedure_spec\<close> "Define IMP procedure and prove specification"
       ((Args.mode "partial" -- Parse.binding 
          -- parse_param_decls
          -- parse_returns_clause
         --| \<^keyword>\<open>assumes\<close> -- Parse.term 
         --| \<^keyword>\<open>ensures\<close> -- Parse.term 
          -- parse_var_decls
         --| \<^keyword>\<open>defines\<close> -- (Parse.position (Parse.cartouche>>cartouche)) 
         ) >>
         
           (fn (((((((partial,bnd),params),retvs),pre_src),post_src),addvars),cmd_src) => 
                 simple_spec_program_cmd bnd partial addvars (SOME (params,retvs)) pre_src post_src cmd_src
              )
          );
           
       Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>recursive_spec\<close> "Define IMP procedure and prove specification"
         (    Scan.option (\<^keyword>\<open>relation\<close> |-- Parse.term)
           -- Parse.and_list1 parse_proc_spec 
           >> (fn (rel,specs) => gen_spec_program_cmd rel specs))
         
     end
   \<close>
 
 end
diff --git a/thys/IMP2/automation/IMP2_Var_Postprocessor.thy b/thys/IMP2/automation/IMP2_Var_Postprocessor.thy
--- a/thys/IMP2/automation/IMP2_Var_Postprocessor.thy
+++ b/thys/IMP2/automation/IMP2_Var_Postprocessor.thy
@@ -1,168 +1,168 @@
 section \<open>Program Variables to Isabelle Variables\<close>
 theory IMP2_Var_Postprocessor
 imports "../basic/Semantics" "../parser/Parser" "../lib/Subgoal_Focus_Some"
 begin
   definition RENAMING :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     where "RENAMING s d \<equiv> s = d"
     
   lemma RENAMINGD: "RENAMING s d \<Longrightarrow> s = d" unfolding RENAMING_def by auto
   lemma RENAMINGI:
     assumes "\<And>d. RENAMING s d \<Longrightarrow> P"
     shows "P" using assms
     unfolding RENAMING_def by simp
     
   ML \<open>
     structure Renaming = struct
       fun RENAMING_rl ctxt (s,d) = let
         (* FIXME: Rough approximation to hit \<And>d. \<dots> *)
         fun rn (Abs ("d",T,t)) = Abs (d,T,t)
           | rn (a$b) = rn a $ rn b
           | rn t = t
     
         val s = Thm.cterm_of ctxt s
           
         val thm = @{thm RENAMINGI}
           |> Drule.infer_instantiate' ctxt [SOME s]
         
         val t = thm  |> Thm.prop_of |> rn
         val thm' = Thm.renamed_prop t thm
       in thm' end
   
       
       fun apply_renamings_tac ctxt = let
         fun is_renaming (Const (@{const_name RENAMING},_)$_$_) = true | is_renaming _ = false
       in 
         Subgoal_Focus_Some.FOCUS_SOME_PREMS (fn _ => Thm.term_of #> HOLogic.dest_Trueprop #> is_renaming)
           (fn {context=ctxt, prems, ...} => let 
             val thms = map (fn t => @{thm RENAMINGD} OF [t]) prems
           in 
             Local_Defs.unfold_tac ctxt thms end) ctxt
       
       end
       
       
       fun remove_renamings_tac ctxt = let 
         (* TODO: Unsafe. Should check that source does not occur elsewhere in goal! *)
       in
         SELECT_GOAL (
           REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms thin_rl[of "RENAMING _ _"]})
             THEN Local_Defs.unfold_tac ctxt @{thms triv_forall_equality}
           ))
       end
       
       
     end
   \<close>  
 
   method_setup i_vcg_apply_renamings_tac = \<open>Scan.succeed (SIMPLE_METHOD' o Renaming.apply_renamings_tac)\<close>
   method_setup i_vcg_remove_renamings_tac = \<open>Scan.succeed (SIMPLE_METHOD' o Renaming.remove_renamings_tac)\<close>
       
 
   definition NAMING_HINT :: "state \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool" where "NAMING_HINT s x n \<equiv> True"  
     
           
   ML \<open>
     (*
       Postprocess VCs to convert states applied to variable names to actual logical variables.
     *)
     structure VC_Postprocessor = struct
     
       (* Guess suffix from name, e.g. "a\<^sub>3" \<mapsto> "\<^sub>3" *)  
       val guess_suffix = let
         val sfxs = ["'","\<^sub>","\<^sup>","\<^bsub>","\<^bsup>"]
       in  
         Symbol.explode #> chop_prefix (not o member op = sfxs) #> snd #> implode
       end
     
       fun guess_renaming param_rename_tab ((s,x),(kind,vname)) = let
 
         fun name_of (Free (n,_)) = n
           | name_of _ = "v"
             
         val sname = the_default (name_of s) (Termtab.lookup param_rename_tab s)
       
         val sfx = guess_suffix sname
         val src = case kind of
           IMP_Syntax.ARRAY => s$x | IMP_Syntax.VAL => s$x$ @{term "0::int"}
       
         val dst = suffix sfx vname
       in
         (src,dst)
       end
       
       
       structure Candtab = Table(type key = term*term val ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord)
       
       fun add_state_candidates ((s as Free (_,@{typ state})) $ x) = (
         case try HOLogic.dest_string x of
           SOME vname => apfst (Candtab.update ((s,x),(IMP_Syntax.ARRAY,vname)))
         | NONE => apsnd (insert op= s) #> add_state_candidates x  
       )
       | add_state_candidates ((s as Free (_,@{typ state})) $ x $ @{term "0::int"}) = (
         case try HOLogic.dest_string x of
           SOME vname => apfst (Candtab.default ((s,x),(IMP_Syntax.VAL,vname)))
         | NONE => apsnd (insert op= s) #> add_state_candidates x  
       )
       | add_state_candidates (s as Free (_,@{typ state})) = apsnd (insert op= s)
       | add_state_candidates (a$b) = add_state_candidates a #> add_state_candidates b
       | add_state_candidates (Abs (_,_,t)) = add_state_candidates t
       | add_state_candidates _ = I
       
       fun hint_renaming hint_tab (rn as (sx,(kind,_))) = case Candtab.lookup hint_tab sx of
         NONE => rn
       | SOME vname' => (sx,(kind,vname'))
       
       fun compute_renamings param_rename_tab hint_tab (good,bad) = 
         subtract (fn (bs, ((s,_),_)) => bs=s) bad (Candtab.dest good)
       |> map (hint_renaming hint_tab)  
       |> map (guess_renaming param_rename_tab)
       
       (* Naming hints go to hint-tab in #1, other premises go to list in #2 *)
-      fun add_naming_hint (@{const Trueprop}$(@{const NAMING_HINT}$s$x$n)) = (case try HOLogic.dest_string n of
+      fun add_naming_hint \<^Const>\<open>Trueprop for \<^Const>\<open>NAMING_HINT for s x n\<close>\<close> =
+        (case try HOLogic.dest_string n of
           SOME n => apfst (Candtab.update ((s,x),n))
-        | NONE => (warning "NAMING_HINT with non-string constant ignored"; I)
-        )
+        | NONE => (warning "NAMING_HINT with non-string constant ignored"; I))
       | add_naming_hint t = apsnd (cons t)
       
       
       val insert_vbind_tac = Subgoal.FOCUS_PREMS (fn {context=ctxt, concl, params, prems, ...} => let
           val conclt = Thm.term_of concl
           
           val param_rename_tab = params |> map (apsnd (Thm.term_of) #> swap) |> Termtab.make 
           
           val (hint_tab,prem_ts) = 
             fold (add_naming_hint o Thm.prop_of) prems (Candtab.empty,[]) 
           
           (* val _ = @{print} (hint_tab,prem_ts)  *)
             
           val renamings = 
               add_state_candidates conclt (Candtab.empty,[]) 
             |> fold (add_state_candidates) prem_ts
             |> compute_renamings param_rename_tab hint_tab
             
           val tacs = map (resolve_tac ctxt o single o Renaming.RENAMING_rl ctxt) renamings
         in
           EVERY1 tacs
         end
         )
       
       fun remove_tac ctxt = let 
         (* TODO: Unsafe. Should check that source does not occur elsewhere in goal! *)
       in
         SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms thin_rl[of "NAMING_HINT _ _ _"]})))
         THEN' Renaming.remove_renamings_tac ctxt
       end
         
         
       fun postprocess_vc_tac ctxt =
         insert_vbind_tac ctxt
         THEN' Renaming.apply_renamings_tac ctxt
         THEN' remove_tac ctxt
   
     end
   \<close>  
   
   method_setup i_vcg_insert_vbind_tac = \<open>Scan.succeed (SIMPLE_METHOD' o VC_Postprocessor.insert_vbind_tac)\<close>
   method_setup i_vcg_postprocess_vars = \<open>Scan.succeed (SIMPLE_METHOD' o VC_Postprocessor.postprocess_vc_tac)\<close>
 
 end
diff --git a/thys/IMP2/lib/IMP2_Utils.thy b/thys/IMP2/lib/IMP2_Utils.thy
--- a/thys/IMP2/lib/IMP2_Utils.thy
+++ b/thys/IMP2/lib/IMP2_Utils.thy
@@ -1,145 +1,143 @@
 theory IMP2_Utils
 imports Main
 begin
 
   ML \<open>
     (*
       Explicit refinement of goal state, deterministic and with error messages.
       
       TODO:
         Add functions to extract subgoals, prove them externally, and then discharge them.
           This is currently done by hand in recursive_spec command   
         
     *)
     structure Det_Goal_Refine : sig
       (* Apply tactic *)
       val apply: string -> tactic -> thm -> thm
       
       (* Apply tactic to first goal *)
       val apply1: string -> (int -> tactic) -> thm -> thm
       
       (* Apply tactic on goal obtained from theorem *)
       val apply_on_thm: string -> tactic -> thm -> thm
       
       (* Extract first element from seq, error message if empty *)
       val seq_first: string -> 'a Seq.seq -> 'a
     end = struct
       fun seq_first msg seq = case Seq.pull seq of 
         NONE => error (if msg="" then "Empty result sequence" else msg) 
       | SOME (x,_) => x
       
       fun apply msg (tac:tactic) = tac #> seq_first msg
       fun apply1 msg tac = apply msg (HEADGOAL tac)
     
       fun apply_on_thm msg tac thm = Goal.protect (Thm.nprems_of thm) thm |> apply msg tac |> Goal.conclude
     end
   
   
   
   \<close>
 
   ML \<open>
     (*
       ML-level interface to option datatype. 
       
       I would have expected this in HOLogic, but it isn't there!
     *)
     structure HOLOption : sig
       val mk_None: typ -> term
       val mk_Some: term -> term
-      val mk_optionT: typ -> typ
       
       val mk_fun_upd: term * term -> term -> term
       
       val mk_map_empty: typ -> typ -> term
       val mk_map_sng: term * term -> term
       val mk_map_upd: term * term -> term -> term
       val mk_map_list: typ -> typ -> (term * term) list -> term
     end = struct
       fun mk_fun_upd (x,y) f = let
         val xT = fastype_of x
         val yT = fastype_of y
       in
         Const (@{const_name Fun.fun_upd}, (xT-->yT) --> xT --> yT --> (xT --> yT))$f$x$y
       end
     
-      fun mk_optionT T = Type(@{type_name option},[T])
-      fun mk_Some x = Const (@{const_name Option.Some},fastype_of x --> mk_optionT (fastype_of x))$x
-      fun mk_None T = Const (@{const_name Option.None}, mk_optionT T)
+      fun mk_Some x = \<^Const>\<open>Some \<open>fastype_of x\<close> for x\<close>
+      fun mk_None T = \<^Const>\<open>None T\<close>
       
       fun mk_map_upd (k,v) m = mk_fun_upd (k,mk_Some v) m
       fun mk_map_empty K V = Abs ("uu_",K,mk_None V)
     
       fun mk_map_list K V kvs = fold mk_map_upd kvs (mk_map_empty K V)
       
       fun mk_map_sng (k,v) = mk_map_upd (k,v) (mk_map_empty (fastype_of k) (fastype_of v))
     end
   
   \<close>
 
   ML \<open>
     (*
       Application of rules (thm -> thm) to premises of subgoals
     *)
     structure Thm_Mapping : sig
       val thin_fst_prem_tac: Proof.context -> int -> tactic
       val thin_fst_prems_tac: int -> Proof.context -> int -> tactic
     
       type rule = Proof.context -> thm -> thm
       
       (* Map first premises with respective rules *)
       val map_prems_tac: rule list -> Proof.context -> int -> tactic
       (* Map all premises with rule *)
       val map_all_prems_tac: rule -> Proof.context -> int -> tactic
       
       (* Apply ith rule to ith thm *)
       val map_thms: Proof.context -> rule list -> thm list -> thm list
     end = struct
 
       type rule = Proof.context -> thm -> thm
         
       fun thin_fst_prem_tac ctxt i = DETERM (eresolve_tac ctxt [Drule.thin_rl] i)
       
       fun thin_fst_prems_tac 0 _ _ = all_tac
         | thin_fst_prems_tac n ctxt i = thin_fst_prem_tac ctxt i THEN thin_fst_prems_tac (n-1) ctxt i
       
       fun map_prems_tac fs ctxt = SUBGOAL (fn (t,i) => let
         val nprems = length (Logic.strip_assums_hyp t)
       in (
           Subgoal.FOCUS_PREMS (fn {context=ctxt, prems, ...} => HEADGOAL (
             Method.insert_tac ctxt (map (fn (f,prem) => f ctxt prem) (fs~~take (length fs) prems))
           )) ctxt
           THEN' thin_fst_prems_tac (length fs) ctxt
           THEN' rotate_tac (nprems - length fs)
         ) i
       end)
     
       fun map_all_prems_tac f ctxt = SUBGOAL (fn (t,i) => let
         val n = length (Logic.strip_assums_hyp t)
       in map_prems_tac (replicate n f) ctxt i end)
        
       fun map_thms ctxt rls thms = rls ~~ thms
         |> map (fn (rl,thm) => rl ctxt thm)
   
   
     end
   \<close>
   
   
   ML \<open>
     infix 0 RS_fst
 
     (* Resolve with first matching rule
     
       Common idiom: thm RS_fst [\<dots>,asm_rl] to keep original thm if no other rule matches
      *)  
     fun _ RS_fst [] = error "RS_fst"
       | thma RS_fst (thm::thms) = case try (op RS) (thma,thm) of
           SOME thm => thm
         | NONE => thma RS_fst thms  
   
   \<close>
 
 
 
 end
diff --git a/thys/IMP2/parser/Parser.thy b/thys/IMP2/parser/Parser.thy
--- a/thys/IMP2/parser/Parser.thy
+++ b/thys/IMP2/parser/Parser.thy
@@ -1,690 +1,690 @@
 section \<open>Parser\<close>
 theory Parser
 imports "../basic/Syntax"
 begin
 
 subsection \<open>Tagging\<close>
   text \<open>We define a few tag constants.
     They are inserted by the parser, and tag certain situations, 
     like parameter passing or inlined commands.
    \<close>
     
   definition Inline :: "com \<Rightarrow> com" where "Inline c = c"  
   
   definition Params :: "com \<Rightarrow> com" where "Params c \<equiv> c"
 
   text \<open>Assignment commands to assign the return value. 
     The VCG will add a renaming, such that the assigned variable name rather
     the \<open>G_ret\<close> will be used for the VCs\<close>
   definition "AssignIdx_retv x i rv \<equiv> AssignIdx x i (V rv)"      
   definition "ArrayCpy_retv x rv \<equiv> ArrayCpy x rv"      
     
   abbreviation "Assign_retv x rv \<equiv> AssignIdx_retv x (N 0) rv"
 
 subsection \<open>Parser for IMP Programs\<close>
 
   text \<open>The parser also understands annotated programs.
     However, the basic parser will leave the annotations uninterpreted,
     and it's up to the client of the parser to interpret them.
   \<close>
 
   
   abbreviation (input) While_Annot :: "'a \<Rightarrow> bexp \<Rightarrow> com \<Rightarrow> com" 
     where "While_Annot I \<equiv> While"
 
   (* Note: Still a very early prototype *)
 
   abbreviation (input) VARIABLEI :: "string \<Rightarrow> string" where "VARIABLEI x \<equiv> x" (* Used to mark integer variables *)
   abbreviation (input) VARIABLEA :: "string \<Rightarrow> string" where "VARIABLEA x \<equiv> x" (* Used to mark array variables *)
   
   syntax "_annotated_term" :: "logic \<Rightarrow> _ \<Rightarrow> _ \<Rightarrow> logic" (* Annotated term: term string pos *)
   
   
   ML \<open>
     structure Term_Annot : sig
       (* Annotate terms *)
       val annotate_term: term -> string * Position.T -> term
       val dest_annotated_term: term -> (string * Position.T) * term
       
       (* Annotation = annotated dummy term *)
       val annotation: string * Position.T -> term
       val dest_annotation: term -> term
 
       (* Checking for annotations in Term *)
       val is_annotated_term: term -> bool
       val has_annotations: term -> bool
 
       (* Removing annotations *)
       val strip_annotations: term -> term
       (* Replaces annotated terms by dummy term *)
       val strip_annotated_terms: term -> term
             
       (* Parsing *)
       (* Parse cartouche (independent of term annotations)*)
       val parse_cartouche: (string * Position.T) parser
       (* Parse cartouche into annotation *)
       val parse_annotation: term parser
       (* Parse cartouche into annotation of syntax constant (used to get typed annotations) *)
       val parse_annotate: string -> term parser
       
       (* Read term from cartouche and position *)
       val read_term: Proof.context -> string * Position.T -> term
       
       (* Read annotation part of annotated term as term *)
       val read_annotation_as_term: Proof.context -> term -> term * term
     end = struct
       fun annotate_term t (str,pos) = let
         val pos = Free (Term_Position.encode pos,dummyT)
         val str = Free (str,dummyT)
         val c = Const (@{syntax_const "_annotated_term"}, dummyT --> dummyT --> dummyT --> dummyT)
       in
         c$t$str$pos
       end
 
       fun dest_annotated_term (Const (@{syntax_const "_annotated_term"},_)$t$Free (str,_)$Free (pos,_)) = let
             val pos = case Term_Position.decode pos of 
               SOME pos => pos | NONE => raise TERM ("dest_term_annot: invalid pos",[t])
           in ((str,pos),t) end
         | dest_annotated_term t = raise TERM("dest_annot",[t])      
         
       val is_annotated_term = can dest_annotated_term
       val has_annotations = Term.exists_subterm is_annotated_term
 
       val annotation = annotate_term Term.dummy
       val dest_annotation = dest_annotated_term #> #2
       
       val parse_cartouche = Parse.position Parse.cartouche >> apfst cartouche
 
       val parse_annotation = parse_cartouche >> annotation
       
       fun parse_annotate n = parse_cartouche >> annotate_term (Const (n,dummyT))
       
       fun read_term_tk ctxt tk = Args.term (Context.Proof ctxt, [tk]) |> #1
       
       fun read_term ctxt spos = let
         val tk = Symbol_Pos.explode spos |> Token.read_cartouche
       in
         read_term_tk ctxt tk
       end  
       
       fun read_annotation_as_term ctxt = dest_annotated_term #>> read_term ctxt 
       
       
       (* Strip one level of term annotations. *)
       fun strip_annotations (Const (@{syntax_const "_annotated_term"},_)$t$_$_) = t
         | strip_annotations (a$b) = strip_annotations a $ strip_annotations b
         | strip_annotations (Abs (x,T,t)) = Abs (x,T,strip_annotations t)
         | strip_annotations t = t
 
         
       fun strip_annotated_terms (Const (@{syntax_const "_annotated_term"},_)$_$_$_) = Term.dummy
         | strip_annotated_terms (a$b) = strip_annotated_terms a $ strip_annotated_terms b
         | strip_annotated_terms (Abs (x,T,t)) = Abs (x,T,strip_annotated_terms t)
         | strip_annotated_terms t = t
               
     end    
   \<close>
    
   
   ML \<open>
     structure IMP_Syntax = struct
     
       fun antf t = (
         exists_type is_TFree t andalso raise TERM("This won't support polymorphism in commands!",[t]);
         t)
 
       val mk_varname = HOLogic.mk_string 
 
       (*fun mk_aexp_V x = antf(@{term V})$x
       fun mk_aexp_Vidx x i = @{const Vidx}$x$i
       val mk_aexp_V' = mk_aexp_V o mk_var
       *)
 
-      fun mk_aexp_const i = @{const N} $ HOLogic.mk_number @{typ int} i
+      fun mk_aexp_const i = \<^Const>\<open>N\<close> $ HOLogic.mk_number @{typ int} i
                         
             
       fun mk_var_i x = Const (@{const_abbrev VARIABLEI}, dummyT) $ mk_varname x
       fun mk_var_a x = Const (@{const_abbrev VARIABLEA}, dummyT) $ mk_varname x
 
 
       (* Caution: This must match the Isabelle function is_global! *)
       fun is_global "" = true
         | is_global s = nth_string s 0 = "G"
 
       val is_local = not o is_global              
       
       (* Expressions *)
 
       datatype rval = RV_AEXP of term | RV_VAR of string
       fun rv_t (RV_AEXP t) = t
-        | rv_t (RV_VAR x) = @{const Vidx} $ mk_var_i x $ mk_aexp_const 0
+        | rv_t (RV_VAR x) = \<^Const>\<open>Vidx\<close> $ mk_var_i x $ mk_aexp_const 0
 
       val rv_var = RV_VAR
-      fun rv_var_idx x i = RV_AEXP (@{const Vidx} $ mk_var_a x $ rv_t i)
+      fun rv_var_idx x i = RV_AEXP (\<^Const>\<open>Vidx\<close> $ mk_var_a x $ rv_t i)
       
       
       (*fun rv_int t = RV_AEXP (@{const N} $ (rv_t t))*)
       val rv_int' = RV_AEXP o mk_aexp_const
 
       fun rv_unop f t = RV_AEXP (f $ rv_t t)
       fun rv_binop f a b = RV_AEXP (f $ rv_t a $ rv_t b)
       
-      fun rv_BC t = RV_AEXP (@{const Bc}$t)
-      fun rv_BC' true = rv_BC @{const True}
-        | rv_BC' false = rv_BC @{const False}
+      fun rv_BC t = RV_AEXP \<^Const>\<open>Bc for t\<close>
+      fun rv_BC' true = rv_BC \<^Const>\<open>True\<close>
+        | rv_BC' false = rv_BC \<^Const>\<open>False\<close>
 
-      fun rv_not t = RV_AEXP (@{const Not} $ rv_t t)
+      fun rv_not t = RV_AEXP \<^Const>\<open>Not for \<open>rv_t t\<close>\<close>
                       
       (* TODO: Add other constructors here *)
       
       (* TODO: Interface for variable tagging mk_var_xxx is not clear! *)
       
       (* Commands*)
-      val mk_Skip = @{const SKIP}
+      val mk_Skip = \<^Const>\<open>SKIP\<close>
       fun mk_Assign x t = antf(@{term Assign})$x$t
-      fun mk_AssignIdx x i t = @{const AssignIdx}$x$i$t
-      fun mk_ArrayCpy d s = @{const ArrayCpy}$d$s
-      fun mk_ArrayInit d = @{const ArrayClear}$d
-      fun mk_Scope c = @{const Scope}$c
-      fun mk_Seq c1 c2 = @{const Seq}$c1$c2
+      fun mk_AssignIdx x i t = @{Const AssignIdx}$x$i$t
+      fun mk_ArrayCpy d s = \<^Const>\<open>ArrayCpy for d s\<close>
+      fun mk_ArrayInit d = \<^Const>\<open>ArrayClear for d\<close>
+      fun mk_Scope c = \<^Const>\<open>Scope for c\<close>
+      fun mk_Seq c1 c2 = \<^Const>\<open>Seq for c1 c2\<close>
 
-      fun mk_Inline t = @{const Inline}$t
-      fun mk_Params t = @{const Params}$t
+      fun mk_Inline t = \<^Const>\<open>Inline for t\<close>
+      fun mk_Params t = \<^Const>\<open>Params for t\<close>
         
       val While_Annot_c = Const (@{const_abbrev While_Annot}, dummyT --> @{typ "bexp \<Rightarrow> com \<Rightarrow> com"})
         
-      fun mk_If b t e = @{const If} $ rv_t b $ t $ e
+      fun mk_If b t e = \<^Const>\<open>If for \<open>rv_t b\<close> t e\<close>
       fun mk_While_annot annots b c = While_Annot_c $ annots $ rv_t b $ c
 
-      fun mk_pcall name = @{const PCall} $ (HOLogic.mk_string name)
+      fun mk_pcall name = \<^Const>\<open>PCall for \<open>HOLogic.mk_string name\<close>\<close>
       
               
       
       (* Derived Constructs *)
 
       datatype varkind = VAL | ARRAY
       type impvar = string * varkind      
       
       datatype lval = LV_IDX of string * term | LV_VAR of string
 
       fun lv_idx x rv = LV_IDX (x, rv_t rv)
       
                     
       fun mk_lr_assign (LV_IDX (x,i)) rv = mk_AssignIdx (mk_var_a x) i (rv_t rv)  
         | mk_lr_assign (LV_VAR x) (RV_AEXP e) = mk_Assign (mk_var_i x) e
         | mk_lr_assign (LV_VAR x) (RV_VAR v) = mk_ArrayCpy (mk_var_i x) (mk_var_i v)
         
       fun list_Seq [] = mk_Skip
         | list_Seq [c] = c
         | list_Seq (c::cs) = mk_Seq c (list_Seq cs)
 
         
-      fun mk_AssignIdx_retv x i y = @{const AssignIdx_retv}$x$i$y
-      fun mk_ArrayCpy_retv d s = @{const ArrayCpy_retv}$d$s
+      fun mk_AssignIdx_retv x i y = \<^Const>\<open>AssignIdx_retv for x i y\<close>
+      fun mk_ArrayCpy_retv d s = \<^Const>\<open>ArrayCpy_retv for d s\<close>
       fun mk_Assign_retv x t = antf(@{term Assign_retv})$x$t
       
 
       fun mk_assign_from_retv (LV_IDX (x,i)) y = mk_AssignIdx_retv (mk_var_a x) i (mk_var_i y)
         | mk_assign_from_retv (LV_VAR x) y = mk_ArrayCpy_retv (mk_var_i x) (mk_var_i y)
       
               
         
       fun param_varnames n = map (fn i => "G_par_"^Int.toString i) (1 upto n)
       fun zip_with_param_names xs = (param_varnames (length xs)) ~~ xs
       fun zip_with_param_lvs xs = map LV_VAR (param_varnames (length xs)) ~~ xs
       fun zip_with_param_rvs xs = map RV_VAR (param_varnames (length xs)) ~~ xs
 
       fun ret_varnames n = map (fn i => "G_ret_"^Int.toString i) (1 upto n)
       fun zip_with_ret_names xs = (ret_varnames (length xs)) ~~ xs
       fun zip_with_ret_lvs xs = map LV_VAR (ret_varnames (length xs)) ~~ xs
       fun zip_with_ret_rvs xs = map RV_VAR (ret_varnames (length xs)) ~~ xs
 
       fun mk_params ress name_t args = let
         val param_assigns = zip_with_param_lvs args
           |> map (uncurry mk_lr_assign)
       
         val res_assigns = zip_with_ret_names ress
           |> map (fn (rv,res) => mk_assign_from_retv res rv)  
           
         val res = param_assigns @ [mk_Params name_t] @ res_assigns  
           |> list_Seq
           
       in
         res
       end
 
       
     end  
   
   \<close>
   
     
    
   (* Syntax constants to discriminate annotation types *)
   syntax
     "_invariant_annotation" :: "_"
     "_variant_annotation" :: "_"
     "_relation_annotation" :: "_"
   
   
   ML \<open>
     structure IMP_Parser = struct
     
       fun scan_if_then_else scan1 scan2 scan3 xs = let
         val r = SOME (Scan.catch scan1 xs) handle Fail _ => NONE
       in
         case r of 
           NONE => scan3 xs
         | SOME (a,xs) => scan2 a xs
       end
       
     
       infixr 0 |||
       infix 5 ---
   
       fun (g,p) ||| e = scan_if_then_else g p e
           
       fun lastg (g,p) = g :|-- p
     
     
       datatype op_kind = Binop | Unop
       
       (*
       val int_c = @{const N}
       val bool_c = @{const Bc}
       val var_c = @{const V}
       *)
       
       
       type op_decl = op_kind * (string * term)
 
       fun name_eq_op_decl ((k,(a,_)), ((k',(b,_)))) = k=k' andalso a=b
       
       fun is_binop ((Binop,_):op_decl) = true | is_binop _ = false
       fun is_unop ((Unop,_):op_decl) = true | is_unop _ = false
       
       structure Opr_Data = Generic_Data (
         type T = op_decl list Inttab.table
         val empty = Inttab.empty
         val merge = Inttab.merge_list name_eq_op_decl
         val extend = I
       )
   
       fun tab_add_unop (p,n,f) = Inttab.insert_list name_eq_op_decl (p,(Unop,(n,f)))
       fun tab_add_binop (p,n,f) = Inttab.insert_list name_eq_op_decl (p,(Binop,(n,f)))
       
       val add_unop = Opr_Data.map o tab_add_unop
       val add_binop = Opr_Data.map o tab_add_binop
 
       val parse_varname = (Parse.short_ident || Parse.term_var) 
             
       
       local
         fun parse_level parse_opr op_decls = let
         
           open IMP_Syntax
         
           val binops = filter is_binop op_decls |> 
             map (fn (_,(k,c)) => Parse.$$$ k >> (K c))
           
           val unops = filter is_unop op_decls |>
             map (fn (_,(k,c)) => Parse.$$$ k >> (K c))
           
           val bopg = Parse.group (fn () => "Binary operator") (Scan.first binops) 
           val uopg = Parse.group (fn () => "Unary operator") (Scan.first unops) 
             
           
           fun mk_right a ([]) = a
             | mk_right a (((f,b)::fxs)) = mk_right (rv_binop f a b) fxs
           
           val parse_bop = (parse_opr, fn a => Scan.repeat (bopg -- parse_opr) >> mk_right a)
           val parse_unop = (uopg, fn f => parse_opr >> (fn x => rv_unop f x))
           
           val parse = (parse_bop ||| lastg parse_unop)
         in
           parse
         end
         
         fun parse_levels lvls = let
           open IMP_Syntax
         
           val parse_int = Parse.nat >> rv_int'
           val parse_var = parse_varname >> rv_var
           
           val pbc = Parse.keyword_markup (true,Markup.keyword3)
           
           val parse_bool = 
                pbc "true" >> (K (rv_BC' true))
             || pbc "false" >> (K (rv_BC' false))
         
           fun parse [] xs = (parse_int || parse_varidx || parse_var || parse_bool || (Parse.$$$ "(" |-- parse lvls --| Parse.$$$ ")")) xs
             | parse (lv::lvs) xs = (parse_level (parse lvs) lv) xs
           and parse_varidx xs = ((parse_varname -- Args.bracks (parse lvls)) 
             >> (fn (n,i) => rv_var_idx n i)) xs
             
         in
           parse lvls
         end
         
       in      
         val parse_exp_tab = Inttab.dest #> map snd #> parse_levels
         
         val parse_exp = Context.Proof #> Opr_Data.get #> parse_exp_tab
       end  
 
       (* TODO/FIXME: Going through the Args.term parser feels like a hack *)
       fun read_term_pos ctxt spos = Args.term (Context.Proof ctxt, [Token.make_string spos]) |> fst
       
       fun parse_proc_name ctxt = 
         Parse.$$$ "rec" |-- Parse.name >> IMP_Syntax.mk_pcall
         || Parse.name >> Syntax.read_term ctxt
         (*|| Parse.position Parse.name >> (read_term_pos ctxt)*)
       
       fun parse_args ctxt = Args.parens (Parse.enum "," (parse_exp ctxt))
 
       fun parse_lhs ctxt = 
          parse_varname -- Args.bracks (parse_exp ctxt) >> uncurry IMP_Syntax.lv_idx
       || parse_varname >> IMP_Syntax.LV_VAR     
 
       fun parse_multiret_lhs ctxt = 
         Args.parens (Parse.enum "," (parse_lhs ctxt))  
       
       fun parse_rhs_call ctxt = parse_proc_name ctxt -- parse_args ctxt
         
 
       fun g_parse_call_assign ctxt = 
         (parse_lhs ctxt --| Parse.$$$ "=", fn lhs => (parse_rhs_call ctxt >> (fn (f,args) => IMP_Syntax.mk_params [lhs] f args)
                            || (parse_exp ctxt >> (fn rhs => IMP_Syntax.mk_lr_assign lhs rhs))))
         
       fun g_parse_multiret_call ctxt = (
         (parse_multiret_lhs ctxt --| Parse.$$$ "=", fn ress => parse_rhs_call ctxt 
                                       >> (fn (f,args) => IMP_Syntax.mk_params ress f args)))
                                       
       fun g_parse_void_call ctxt = (parse_rhs_call ctxt, 
             fn (f,args) => Scan.succeed (IMP_Syntax.mk_params [] f args))
                           
       val fixed_keywords = ["(",")","{","}","true","false","[]","[","]",
         "if","else","while","scope","skip","=",";",",",
         "call", "sreturn", "inline","clear","rec",
         "@invariant", "@variant", "@relation",
         "__term"]
       
       fun parse_command ctxt = let
         val pkw = Parse.keyword_markup (true,Markup.keyword1)
         val pcm = Parse.keyword_markup (true,Markup.keyword2)
       
       
         val g_parse_skip = (pcm "skip", fn _ => Scan.succeed @{term SKIP})
         
         fun g_parse_block p = (Parse.$$$ "{", fn _ => p --| Parse.$$$ "}")
 
         val g_parse_clear = (pcm "clear", fn _ => parse_varname --| Parse.$$$ "[]" 
               >> (IMP_Syntax.mk_ArrayInit o IMP_Syntax.mk_var_a))
         
         
         val parse_invar_annotation = (pkw "@invariant", fn _ => Term_Annot.parse_annotate @{syntax_const "_invariant_annotation"})
         val parse_var_annotation = (pkw "@variant", fn _ => Term_Annot.parse_annotate @{syntax_const "_variant_annotation"})
         val parse_rel_annotation = (pkw "@relation", fn _ => Term_Annot.parse_annotate @{syntax_const "_relation_annotation"})
 
         val parse_while_annots = Scan.repeat (parse_invar_annotation ||| parse_var_annotation ||| lastg parse_rel_annotation)
               >> HOLogic.mk_tuple
         
         
         fun parse_atomic_com xs = 
           (
                 g_parse_call_assign ctxt
             ||| g_parse_multiret_call ctxt
             ||| g_parse_void_call ctxt
             ||| g_parse_skip 
             ||| g_parse_clear
             ||| lastg (g_parse_block parse_com)
           ) xs
         
         and parse_com1 xs = (
             (pkw "if", fn _ => pkw "(" |-- parse_exp ctxt --| pkw ")" -- parse_com1 
               -- scan_if_then_else (pkw "else") (K parse_com1) (Scan.succeed IMP_Syntax.mk_Skip) 
                 >> (fn ((b,t),e) => IMP_Syntax.mk_If b t e))
          ||| (pkw "while", fn _ => pkw "(" |-- parse_exp ctxt --| pkw ")" -- parse_while_annots -- parse_com1
                 >> (fn ((b,annots),c) => IMP_Syntax.mk_While_annot annots b c))
          ||| (pkw "scope", fn _ => parse_com1 >> IMP_Syntax.mk_Scope)
          ||| (pkw "__term", fn _ => Term_Annot.parse_cartouche >> Term_Annot.read_term ctxt)
          ||| (pkw "inline", fn _ => Parse.position Parse.name >> (IMP_Syntax.mk_Inline o read_term_pos ctxt))
          ||| parse_atomic_com
         
         ) xs
         and parse_com xs = (
            parse_com1 -- (Scan.unless (Parse.$$$ ";") (Scan.succeed NONE) || Parse.$$$ ";" |-- parse_com >> SOME )
            >> (fn (s,SOME t) => IMP_Syntax.mk_Seq s t | (s,NONE) => s)
         
         ) xs
       
       in parse_com end 
       
       fun parse_all ctxt p src = let
         val src = map Token.init_assignable src
         val (res,_) = Scan.catch (Scan.finite Token.stopper (p --| Scan.ahead Parse.eof)) src
         
         val rp = map Token.reports_of_value src |> flat
         val _ = Context_Position.reports ctxt rp
         
         (* val src = map Token.closure src |> @{print} *)
       in
         res
       end
       
       val keywords_of_tab : op_decl list Inttab.table -> string list 
         = Inttab.dest_list #> map (snd#>snd#>fst)
       
       fun keywords ctxt = let 
         val kws = ctxt |> Context.Proof |> Opr_Data.get |> keywords_of_tab 
         val kws = (kws @ fixed_keywords)
           |> Symtab.make_set |> Symtab.keys
           |> map (fn x => ((x,Position.none),Keyword.no_spec))
       in
         Keyword.add_keywords kws Keyword.empty_keywords
       end
         
       fun parse_pos_text p ctxt (pos,text) = 
           Token.explode (keywords ctxt) pos text 
         |> filter Token.is_proper  
         |> parse_all ctxt (p ctxt)
         
       fun parse_sympos p ctxt xs = let
         val kws = keywords ctxt
         val tks = Token.tokenize kws {strict=true} xs
         val rp = map (Token.reports kws) tks |> flat  (* TODO: More detailed report AFTER parsing! *)
         val _ = Context_Position.reports_text ctxt rp
       in
           tks 
         |> filter Token.is_proper  
         |> parse_all ctxt (p ctxt)
       end
 
       fun variables_of t = let
         fun add (Const (@{const_abbrev VARIABLEI},_)$x) = (Symtab.default (HOLogic.dest_string x,IMP_Syntax.VAL))
           | add (Const (@{const_abbrev VARIABLEA},_)$x) = (Symtab.update (HOLogic.dest_string x,IMP_Syntax.ARRAY))
           | add (a$b) = add a #> add b
           | add (Abs (_,_,t)) = add t
           | add _ = I
       
       in
         add t Symtab.empty |> Symtab.dest
       end
 
       fun merge_variables vars = let
         fun add (x,IMP_Syntax.VAL) = Symtab.default (x,IMP_Syntax.VAL) 
           | add (x,IMP_Syntax.ARRAY) = Symtab.update (x,IMP_Syntax.ARRAY)
       in
         fold add vars Symtab.empty |> Symtab.dest
       end
       
       
       
       fun parse_command_at ctxt spos = let
         val syms = spos |> Symbol_Pos.explode |> Symbol_Pos.cartouche_content
         val res = parse_sympos parse_command ctxt syms
         val vars = variables_of res
       in
         (vars,res)
       end
     
       (* From Makarius: Protect a term such that it "survives" the subsequent translation phase *)
       fun mark_term (Const (c, T)) = Const (Lexicon.mark_const c, T)
         | mark_term (Free (x, T)) = Const (Lexicon.mark_fixed x, T)
         | mark_term (t $ u) = mark_term t $ mark_term u
         | mark_term (Abs (x, T, b)) = Abs (x, T, mark_term b)
         | mark_term a = a;
       
       
       fun cartouche_tr ctxt args = let  
         fun err () = raise TERM ("imp",args)
       
         fun parse spos = let 
           val (_,t) = parse_command_at ctxt spos 
           val t = if Term_Annot.has_annotations t then (warning "Stripped annotations from program"; Term_Annot.strip_annotated_terms t) else t
           val t = Syntax.check_term ctxt t
             |> mark_term
         in  
           t
         end
         
       in 
         (case args of
           [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
             (case Term_Position.decode_position p of
               SOME (pos, _) => c $ parse (s,pos) $ p
             | NONE => err ())
         | _ => err ())
       end
                 
     end
   \<close>
 
   
   
   syntax "_Imp" :: "cartouche_position \<Rightarrow> logic" ("\<^imp>_")
 
   parse_translation \<open>
     [(@{syntax_const "_Imp"}, IMP_Parser.cartouche_tr)]
   \<close>
 
   term \<open>\<^imp>\<open>skip\<close>\<close>
   
   
   
     
   declaration \<open>K ( I
   #> IMP_Parser.add_unop (31,"-",@{term "Unop uminus"})  
   #> IMP_Parser.add_binop (25,"*",@{term "Binop (*)"})
   #> IMP_Parser.add_binop (25,"/",@{term "Binop (div)"})
   #> IMP_Parser.add_binop (25,"mod",@{term "Binop (mod)"})
   #> IMP_Parser.add_binop (21,"+",@{term "Binop (+)"})
   #> IMP_Parser.add_binop (21,"-",@{term "Binop (-)"})
   #> IMP_Parser.add_binop (11,"<",@{term "Cmpop (<)"})
   #> IMP_Parser.add_binop (11,"\<le>",@{term "Cmpop (\<le>)"})
   #> IMP_Parser.add_binop (11,">",@{term "Cmpop (>)"})
   #> IMP_Parser.add_binop (11,"\<ge>",@{term "Cmpop (\<ge>)"})
   #> IMP_Parser.add_binop (11,"==",@{term "Cmpop (=)"})
   #> IMP_Parser.add_binop (11,"\<noteq>",@{term "Cmpop (\<noteq>)"})
   #> IMP_Parser.add_unop (7,"\<not>",@{term "Not"})
   #> IMP_Parser.add_binop (5,"\<and>",@{term "BBinop (\<and>)"})
   #> IMP_Parser.add_binop (3,"\<or>",@{term "BBinop (\<or>)"})
     )\<close>
 
 subsection \<open>Examples\<close>
     
 experiment
 begin
 
   definition \<open>p1 \<equiv> \<^imp>\<open> x = 42 \<close>\<close>
 
   ML_val \<open>Syntax.read_term @{context} "p1"\<close>
   
   term p1
   
   
   term \<open>\<^imp>\<open>
     x=y;                      \<comment> \<open>Variable assignment / array copy\<close>
     a[i] = x;                 \<comment> \<open>Assign array index\<close>
     clear a[];                \<comment> \<open>Array initialization\<close>
     
     
     a = b[i];                 \<comment> \<open>Array indexing\<close>
     b = a[1] + x*a[a[i]+1];   
         
     
     p1();                     \<comment> \<open>Function call, ignore return value\<close>
     
     p1(x,b+1,y[a]);           \<comment> \<open>Function call with parameters\<close>
     
     a[i]=p1();                \<comment> \<open>Return value assigned to \<open>a[i]\<close>\<close>  
     a=p1();                   \<comment> \<open>Returns array (also works for value)\<close>
     
     (a,b,c) = p1(a,b);        \<comment> \<open>Multiple return values\<close>
     
     
     \<comment> \<open>Special syntax for recursive calls. TODO: Get rid of this? \<close>
     rec p();
     rec p(a,b);
     a = rec p(a,b);
     (a,b,c) = rec p(a,b);
     
     skip
   \<close>\<close>
   
   
   term  \<open> \<^imp>\<open>
     a = 1;
     if (true) a=a;
     if (false) skip else {skip; skip};
     while (n > 0) 
       @invariant \<open>not interpreted here\<close>
       @variant \<open>not interpreted here\<close>
       @relation \<open>not interpreted here\<close>
     {
       a = a + a;
       
       __term \<open>SKIP;; p1\<close>;
       
       inline p1;
       
       y = p1();
       scope {
         n=0
       };
       
       n = n - 1
     }
   \<close>\<close>  
    
 end  
 
 term "\<^imp>\<open>
     a=1;
     while (n>0) {
       a=a+a;
       n=n-1
     }
   \<close>"
 
 subsubsection \<open>Parameter Passing\<close>  
 
 experiment
 begin
   text \<open>The parser generates parameter and return value passing code, using the global
     variables \<open>G_par_i\<close> and \<open>G_ret_i\<close>. 
 
     To illustrate this, we first define an example procedure. Its signature would be
       \<open>(int,int) f (int p1, int p2)\<close>
     
   \<close>
   definition "f \<equiv> \<^imp>\<open>scope { p1 = G_par_1; p2 = G_par_2; G_ret_1=x1+x2; G_ret_2=x1-x2 }\<close>"
 
   text \<open>The parser generates the corresponding caller-side code for the invocation of 
     this procedure:\<close>
   term \<open>\<^imp>\<open>(x1,x2) = f(a,b+1)\<close>\<close>
 
 
 end
 
 end