# HG changeset patch
# User nipkow
# Date 1325350430 -3600
# Node ID 81ebd0cdb3003ed8d1fc275e72084ff5fc7db111
# Parent  9bc924006136032514bf2299aa171083c90e092a
tuned types

diff -r 9bc924006136 -r 81ebd0cdb300 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sat Dec 31 17:53:50 2011 +0100
@@ -12,7 +12,7 @@
 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)"
@@ -22,10 +22,14 @@
 
 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))}" |
@@ -36,7 +40,7 @@
 "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>)"
 
 
diff -r 9bc924006136 -r 81ebd0cdb300 src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Sat Dec 31 17:53:50 2011 +0100
@@ -52,7 +52,8 @@
 end
 
 
-interpretation Val_abs \<gamma>_cval Const plus_cval
+interpretation Val_abs
+where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
 defines aval'_const is aval'
 proof
   case goal1 thus ?case
@@ -66,7 +67,8 @@
     by(auto simp: plus_cval_cases split: cval.split)
 qed
 
-interpretation Abs_Int \<gamma>_cval Const plus_cval
+interpretation Abs_Int
+where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
 defines AI_const is AI
 and step_const is step'
 proof qed
@@ -74,7 +76,8 @@
 
 text{* Monotonicity: *}
 
-interpretation Abs_Int_mono \<gamma>_cval Const plus_cval
+interpretation Abs_Int_mono
+where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
 proof
   case goal1 thus ?case
     by(auto simp: plus_cval_cases split: cval.split)
diff -r 9bc924006136 -r 81ebd0cdb300 src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Sat Dec 31 17:53:50 2011 +0100
@@ -234,26 +234,26 @@
 text{* The interface for abstract values: *}
 
 locale Val_abs =
-fixes \<gamma> :: "'a::SL_top \<Rightarrow> val set"
+fixes \<gamma> :: "'av::SL_top \<Rightarrow> val set"
   assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
   and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
-fixes num' :: "val \<Rightarrow> 'a"
-and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+fixes num' :: "val \<Rightarrow> 'av"
+and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
   assumes gamma_num': "n : \<gamma>(num' n)"
   and gamma_plus':
  "n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
 
-type_synonym 'a st = "(vname \<Rightarrow> 'a)"
+type_synonym 'av st = "(vname \<Rightarrow> 'av)"
 
-locale Abs_Int_Fun = Val_abs
+locale Abs_Int_Fun = Val_abs \<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
 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 = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
+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}) =
@@ -264,7 +264,7 @@
 "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>)"
 
 
@@ -272,13 +272,13 @@
 by(induct c arbitrary: S) (simp_all add: Let_def)
 
 
-abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
 where "\<gamma>\<^isub>f == \<gamma>_fun \<gamma>"
 
-abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
 where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
 
-abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
 lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
diff -r 9bc924006136 -r 81ebd0cdb300 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Sat Dec 31 17:53:50 2011 +0100
@@ -38,8 +38,7 @@
 end
 
 locale Val_abs1_gamma =
-  Val_abs \<gamma> num' plus'
-  for \<gamma> :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
+  Val_abs where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
 assumes inter_gamma_subset_gamma_meet:
   "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
 and gamma_Bot[simp]: "\<gamma> \<bottom> = {}"
@@ -54,22 +53,25 @@
 end
 
 
-locale Val_abs1 = Val_abs1_gamma +
-fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+locale Val_abs1 =
+ Val_abs1_gamma where \<gamma> = \<gamma>
+ for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
+fixes filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
+and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
 assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
   n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
 and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
   n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
 
 
-locale Abs_Int1 = Val_abs1
+locale Abs_Int1 =
+  Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set"
 begin
 
 lemma in_gamma_join_UpI: "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
 by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp)
 
-fun aval'' :: "aexp \<Rightarrow> 'a st option \<Rightarrow> 'a" where
+fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
 "aval'' e None = \<bottom>" |
 "aval'' e (Some sa) = aval' e sa"
 
@@ -78,7 +80,7 @@
 
 subsubsection "Backward analysis"
 
-fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st option \<Rightarrow> 'a st option" where
+fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
 "afilter (N n) a S = (if n : \<gamma> a then S else None)" |
 "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
   let a' = lookup S x \<sqinter> a in
@@ -97,7 +99,7 @@
 making the analysis less precise. *}
 
 
-fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st option \<Rightarrow> 'a st option" where
+fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
 "bfilter (Bc v) res S = (if v=res then S else None)" |
 "bfilter (Not b) res S = bfilter b (\<not> res) S" |
 "bfilter (And b1 b2) res S =
@@ -139,7 +141,7 @@
 qed
 
 
-fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
+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}) =
@@ -153,7 +155,7 @@
    WHILE b DO step' (bfilter b True Inv) c
    {bfilter b False 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"
diff -r 9bc924006136 -r 81ebd0cdb300 src/HOL/IMP/Abs_Int1_ivl.thy
--- a/src/HOL/IMP/Abs_Int1_ivl.thy	Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Sat Dec 31 17:53:50 2011 +0100
@@ -170,7 +170,8 @@
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
-interpretation Val_abs \<gamma>_ivl num_ivl plus_ivl
+interpretation Val_abs
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 defines aval_ivl is aval'
 proof
   case goal1 thus ?case
@@ -184,7 +185,8 @@
     by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
 qed
 
-interpretation Val_abs1_gamma \<gamma>_ivl num_ivl plus_ivl
+interpretation Val_abs1_gamma
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 proof
   case goal1 thus ?case
     by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -201,8 +203,9 @@
 done
 
 
-interpretation
-  Val_abs1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Val_abs1
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
   case goal1 thus ?case
     by(auto simp add: filter_plus_ivl_def)
@@ -213,8 +216,9 @@
       auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
-interpretation
-  Abs_Int1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Abs_Int1
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
 and step_ivl is step'
@@ -225,8 +229,9 @@
 
 text{* Monotonicity: *}
 
-interpretation
-  Abs_Int1_mono \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Abs_Int1_mono
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
   case goal1 thus ?case
     by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
diff -r 9bc924006136 -r 81ebd0cdb300 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Sat Dec 31 17:53:50 2011 +0100
@@ -180,10 +180,11 @@
 apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
 by (metis (no_types) strip_lpfpc strip_map2_acom strip_while)
 
-locale Abs_Int2 = Abs_Int1_mono \<gamma> for \<gamma> :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
+locale Abs_Int2 = Abs_Int1_mono
+where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"
 begin
 
-definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
+definition AI_WN :: "com \<Rightarrow> 'av st option acom option" where
 "AI_WN = pfp_WN (step' \<top>)"
 
 lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
@@ -206,8 +207,9 @@
 
 end
 
-interpretation
-  Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl \<gamma>_ivl
+interpretation Abs_Int2
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 defines AI_ivl' is AI_WN
 proof qed
 
diff -r 9bc924006136 -r 81ebd0cdb300 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Sat Dec 31 17:53:50 2011 +0100
@@ -61,13 +61,13 @@
 context Val_abs
 begin
 
-abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
 where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>"
 
-abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
 where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
 
-abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
 lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"