--- a/src/HOL/IMP/Abs_Int0.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Jul 03 16:07:00 2013 +0200
@@ -148,7 +148,7 @@
text{* The interface for abstract values: *}
-locale Val_abs =
+locale Val_semilattice =
fixes \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
@@ -163,7 +163,7 @@
the name of the type parameter @{typ 'av} which would otherwise be renamed to
@{typ 'a}. *}
-locale Abs_Int_fun = Val_abs where \<gamma>=\<gamma>
+locale Abs_Int_fun = Val_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
--- a/src/HOL/IMP/Abs_Int1.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Jul 03 16:07:00 2013 +0200
@@ -8,7 +8,7 @@
text{* Abstract interpretation over type @{text st} instead of functions. *}
-context Gamma
+context Gamma_semilattice
begin
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
@@ -32,7 +32,7 @@
end
-locale Abs_Int = Gamma where \<gamma>=\<gamma>
+locale Abs_Int = Gamma_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
--- a/src/HOL/IMP/Abs_Int1_const.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Jul 03 16:07:00 2013 +0200
@@ -53,7 +53,7 @@
end
-interpretation Val_abs
+interpretation Val_semilattice
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
--- a/src/HOL/IMP/Abs_Int1_parity.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Jul 03 16:07:00 2013 +0200
@@ -102,7 +102,7 @@
text{* First we instantiate the abstract value interface and prove that the
functions on type @{typ parity} have all the necessary properties: *}
-interpretation Val_abs
+interpretation Val_semilattice
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof txt{* of the locale axioms *}
fix a b :: parity
--- a/src/HOL/IMP/Abs_Int2.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Wed Jul 03 16:07:00 2013 +0200
@@ -28,7 +28,7 @@
subclass (in bounded_lattice) semilattice_sup_top ..
-locale Val_abs1_gamma = Gamma where \<gamma> = \<gamma>
+locale Val_lattice_gamma = Gamma_semilattice where \<gamma> = \<gamma>
for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
assumes inter_gamma_subset_gamma_inf:
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
@@ -45,7 +45,7 @@
end
-locale Val_abs1 = Val_abs1_gamma where \<gamma> = \<gamma>
+locale Val_inv = Val_lattice_gamma where \<gamma> = \<gamma>
for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
and inv_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
@@ -57,7 +57,7 @@
i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> a\<^isub>1' \<and> i2 : \<gamma> a\<^isub>2'"
-locale Abs_Int1 = Val_abs1 where \<gamma> = \<gamma>
+locale Abs_Int_inv = Val_inv where \<gamma> = \<gamma>
for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
begin
@@ -184,7 +184,7 @@
subsubsection "Monotonicity"
-locale Abs_Int1_mono = Abs_Int1 +
+locale Abs_Int_inv_mono = Abs_Int_inv +
assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
and mono_inv_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
inv_plus' r a1 a2 \<le> inv_plus' r' b1 b2"
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Jul 03 16:07:00 2013 +0200
@@ -309,7 +309,7 @@
"\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
by(drule (1) add_mono) simp
-interpretation Val_abs
+interpretation Val_semilattice
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
proof
case goal1 thus ?case by transfer (simp add: le_iff_subset)
@@ -325,7 +325,7 @@
qed
-interpretation Val_abs1_gamma
+interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
defines aval_ivl is aval'
proof
@@ -334,7 +334,7 @@
case goal2 show ?case unfolding bot_ivl_def by transfer simp
qed
-interpretation Val_abs1
+interpretation Val_inv
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -357,7 +357,7 @@
done
qed
-interpretation Abs_Int1
+interpretation Abs_Int_inv
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -391,7 +391,7 @@
apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
-interpretation Abs_Int1_mono
+interpretation Abs_Int_inv_mono
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
--- a/src/HOL/IMP/Abs_Int3.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Jul 03 16:07:00 2013 +0200
@@ -13,7 +13,7 @@
class narrow =
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
-class WN = widen + narrow + order +
+class wn = widen + narrow + order +
assumes widen1: "x \<le> x \<nabla> y"
assumes widen2: "y \<le> x \<nabla> y"
assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
@@ -25,10 +25,10 @@
end
-lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{WN,top})"
+lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,top})"
by (metis eq_iff top_greatest widen2)
-instantiation ivl :: WN
+instantiation ivl :: wn
begin
definition "widen_rep p1 p2 =
@@ -53,7 +53,7 @@
end
-instantiation st :: ("{top,WN}")WN
+instantiation st :: ("{top,wn}")wn
begin
lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)"
@@ -80,7 +80,7 @@
end
-instantiation option :: (WN)WN
+instantiation option :: (wn)wn
begin
fun widen_option where
@@ -114,27 +114,7 @@
where
"map2_acom f C1 C2 = annotate (\<lambda>p. f (anno C1 p) (anno C2 p)) (strip C1)"
-(*
-text_raw{*\snip{maptwoacomdef}{2}{2}{% *}
-fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom"
-where
-"map2_acom f (SKIP {a\<^isub>1}) (SKIP {a\<^isub>2}) = (SKIP {f a\<^isub>1 a\<^isub>2})" |
-"map2_acom f (x ::= e {a\<^isub>1}) (x' ::= e' {a\<^isub>2}) = (x ::= e {f a\<^isub>1 a\<^isub>2})" |
-"map2_acom f (C\<^isub>1;C\<^isub>2) (D\<^isub>1;D\<^isub>2)
- = (map2_acom f C\<^isub>1 D\<^isub>1; map2_acom f C\<^isub>2 D\<^isub>2)" |
-"map2_acom f (IF b THEN {p\<^isub>1} C\<^isub>1 ELSE {p\<^isub>2} C\<^isub>2 {a\<^isub>1})
- (IF b' THEN {q\<^isub>1} D\<^isub>1 ELSE {q\<^isub>2} D\<^isub>2 {a\<^isub>2})
- = (IF b THEN {f p\<^isub>1 q\<^isub>1} map2_acom f C\<^isub>1 D\<^isub>1
- ELSE {f p\<^isub>2 q\<^isub>2} map2_acom f C\<^isub>2 D\<^isub>2 {f a\<^isub>1 a\<^isub>2})" |
-"map2_acom f ({a\<^isub>1} WHILE b DO {p} C {a\<^isub>2})
- ({a\<^isub>3} WHILE b' DO {q} D {a\<^isub>4})
- = ({f a\<^isub>1 a\<^isub>3} WHILE b DO {f p q} map2_acom f C D {f a\<^isub>2 a\<^isub>4})"
-text_raw{*}%endsnip*}
-*)(*
-lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
- annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
-by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2)
-*)
+
instantiation acom :: (widen)widen
begin
definition "widen_acom = map2_acom (op \<nabla>)"
@@ -160,10 +140,10 @@
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1"
by(simp add: narrow_acom_def)
-lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::WN acom)"
+lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::wn acom)"
by(simp add: narrow_acom_def narrow1 map2_acom_def less_eq_acom_def size_annos)
-lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::WN acom) \<le> C1"
+lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::wn acom) \<le> C1"
by(simp add: narrow_acom_def narrow2 map2_acom_def less_eq_acom_def size_annos)
@@ -205,7 +185,7 @@
qed
lemma iter_narrow_pfp:
-assumes mono: "!!x1 x2::_::WN acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
+assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p"
shows "P p \<and> f p \<le> p"
@@ -232,7 +212,7 @@
qed
lemma pfp_wn_pfp:
-assumes mono: "!!x1 x2::_::WN acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
+assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
and Pinv: "P x" "!!x. P x \<Longrightarrow> P(f x)"
"!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
"!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
@@ -253,8 +233,8 @@
(metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
-locale Abs_Int2 = Abs_Int1_mono where \<gamma>=\<gamma>
- for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set"
+locale Abs_Int_wn = Abs_Int_inv_mono where \<gamma>=\<gamma>
+ for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set"
begin
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
@@ -280,7 +260,7 @@
end
-interpretation Abs_Int2
+interpretation Abs_Int_wn
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -354,8 +334,8 @@
that not yet @{prop"y \<le> x"}. This complicates the termination proof for
widening. *}
-locale Measure_WN = Measure1 where m=m
- for m :: "'av::{top,WN} \<Rightarrow> nat" +
+locale Measure_wn = Measure1 where m=m
+ for m :: "'av::{top,wn} \<Rightarrow> nat" +
fixes n :: "'av \<Rightarrow> nat"
assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
@@ -380,7 +360,7 @@
shows "(\<Sum>x\<in>X. m (S1 x \<nabla> S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
proof-
have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S1 x \<nabla> S2 x)"
- by (metis m_anti_mono WN_class.widen1)
+ by (metis m_anti_mono wn_class.widen1)
have "x \<in> X" using assms(2,3)
by(auto simp add: Ball_def)
hence 2: "\<exists>x\<in>X. m(S1 x) > m(S1 x \<nabla> S2 x)"
@@ -488,7 +468,7 @@
lemma iter_widen_termination:
-fixes m :: "'a::WN acom \<Rightarrow> nat"
+fixes m :: "'a::wn acom \<Rightarrow> nat"
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
@@ -502,7 +482,7 @@
qed
lemma iter_narrow_termination:
-fixes n :: "'a::WN acom \<Rightarrow> nat"
+fixes n :: "'a::wn acom \<Rightarrow> nat"
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2"
@@ -521,8 +501,8 @@
by blast
qed
-locale Abs_Int2_measure = Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m
- for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
+locale Abs_Int_wn_measure = Abs_Int_wn where \<gamma>=\<gamma> + Measure_wn where m=m
+ for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
subsubsection "Termination: Intervals"
@@ -565,7 +545,7 @@
split: prod.splits if_splits extended.split)
-interpretation Abs_Int2_measure
+interpretation Abs_Int_wn_measure
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -614,7 +594,7 @@
text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.
It can already be lost after the first step: *}
-lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
+lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"
nitpick[card = 3, expect = genuine, show_consts]
(*
@@ -630,7 +610,7 @@
text{* Widening terminates but may converge more slowly than Kleene iteration.
In the following model, Kleene iteration goes from 0 to the least pfp
in one step but widening takes 2 steps to reach a strictly larger pfp: *}
-lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
+lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"
shows "f(x \<nabla> f x) \<le> x \<nabla> f x"
nitpick[card = 4, expect = genuine, show_consts]
--- a/src/HOL/IMP/Abs_State.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy Wed Jul 03 16:07:00 2013 +0200
@@ -128,7 +128,7 @@
lemma mono_fun: "S1 \<le> S2 \<Longrightarrow> fun S1 x \<le> fun S2 x"
by transfer (simp add: less_eq_st_rep_iff)
-locale Gamma = Val_abs where \<gamma>=\<gamma>
+locale Gamma_semilattice = Val_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin