src/HOL/IMP/Abs_Int0.thy

 functions. *}
 
 context Val_abs
 begin
 
-fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
+fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
 "aval' (N n) S = num' n" |
 "aval' (V x) S = lookup S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
 lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
 by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def lookup_def)
 
 end
 
-locale Abs_Int = Val_abs
+text{* The for-clause (here and elsewhere) only serves the purpose of fixing
+the name of the type parameter @{typ 'av} which would otherwise be renamed to
+@{typ 'a}. *}
+
+locale Abs_Int = Val_abs \<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
 begin
 
-fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
+fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" where
 "step' S (SKIP {P}) = (SKIP {S})" |
 "step' S (x ::= e {P}) =
   x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
 "step' S (c1; c2) = step' S c1; step' (post c1) c2" |
 "step' S (IF b THEN c1 ELSE c2 {P}) =
   (let c1' = step' S c1; c2' = step' S c2
    in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
 "step' S ({Inv} WHILE b DO c {P}) =
    {S \<squnion> post c} WHILE b DO step' Inv c {Inv}"
 
-definition AI :: "com \<Rightarrow> 'a st option acom option" where
+definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI = lpfp\<^isub>c (step' \<top>)"
 
 
 lemma strip_step'[simp]: "strip(step' S c) = strip c"
 by(induct c arbitrary: S) (simp_all add: Let_def)