--- a/src/HOL/IMP/Abs_Int1.thy Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Apr 17 21:11:01 2013 +0200
@@ -4,6 +4,20 @@
imports Abs_State
begin
+(* FIXME mv *)
+instantiation acom :: (type) vars
+begin
+
+definition "vars_acom = vars o strip"
+
+instance ..
+
+end
+
+lemma finite_Cvars: "finite(vars(C::'a acom))"
+by(simp add: vars_acom_def)
+
+
lemma le_iff_le_annos_zip: "C1 \<le> C2 \<longleftrightarrow>
(\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<le> a2) \<and> strip C1 = strip C2"
by(induct C1 C2 rule: less_eq_acom.induct) (auto simp: size_annos_same2)
@@ -12,28 +26,10 @@
strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
-
-lemma mono_fun_L[simp]: "F \<in> L X \<Longrightarrow> F \<le> G \<Longrightarrow> x : X \<Longrightarrow> fun F x \<le> fun G x"
-by(simp add: mono_fun L_st_def)
-
-lemma bot_in_L[simp]: "bot c \<in> L(vars c)"
-by(simp add: L_acom_def bot_def)
-
-lemma L_acom_simps[simp]: "SKIP {P} \<in> L X \<longleftrightarrow> P \<in> L X"
- "(x ::= e {P}) \<in> L X \<longleftrightarrow> x : X \<and> vars e \<subseteq> X \<and> P \<in> L X"
- "(C1;C2) \<in> L X \<longleftrightarrow> C1 \<in> L X \<and> C2 \<in> L X"
- "(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) \<in> L X \<longleftrightarrow>
- vars b \<subseteq> X \<and> C1 \<in> L X \<and> C2 \<in> L X \<and> P1 \<in> L X \<and> P2 \<in> L X \<and> Q \<in> L X"
- "({I} WHILE b DO {P} C {Q}) \<in> L X \<longleftrightarrow>
- I \<in> L X \<and> vars b \<subseteq> X \<and> P \<in> L X \<and> C \<in> L X \<and> Q \<in> L X"
-by(auto simp add: L_acom_def)
-
-lemma post_in_annos: "post C : set(annos C)"
+(* FIXME mv *)
+lemma post_in_annos: "post C \<in> set(annos C)"
by(induction C) auto
-lemma post_in_L[simp]: "C \<in> L X \<Longrightarrow> post C \<in> L X"
-by(simp add: L_acom_def post_in_annos)
-
subsection "Computable Abstract Interpretation"
@@ -47,15 +43,15 @@
"aval' (V x) S = fun S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> vars a \<subseteq> dom S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
+lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
by (induction a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def)
lemma gamma_Step_subcomm: fixes C1 C2 :: "'a::semilattice_sup acom"
- assumes "!!x e S. x : X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> S \<in> L X \<Longrightarrow> f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)"
- "!!b S. S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
- shows "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
+ assumes "!!x e S. f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)"
+ "!!b S. g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
+ shows "Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
proof(induction C arbitrary: S)
-qed (auto simp: assms intro!: mono_gamma_o post_in_L sup_ge1 sup_ge2)
+qed (auto simp: assms intro!: mono_gamma_o sup_ge1 sup_ge2)
lemma in_gamma_update: "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
by(simp add: \<gamma>_st_def)
@@ -63,16 +59,6 @@
end
-lemma Step_in_L: fixes C :: "'a::semilatticeL acom"
-assumes "!!x e S. \<lbrakk>S \<in> L X; x \<in> X; vars e \<subseteq> X\<rbrakk> \<Longrightarrow> f x e S \<in> L X"
- "!!b S. S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> g b S \<in> L X"
-shows"\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> Step f g S C \<in> L X"
-proof(induction C arbitrary: S)
- case Assign thus ?case
- by(auto simp: L_st_def assms split: option.splits)
-qed (auto simp: assms)
-
-
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}. *}
@@ -85,7 +71,7 @@
(\<lambda>b S. S)"
definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' (Top(vars c))) (bot c)"
+"AI c = pfp (step' \<top>) (bot c)"
lemma strip_step'[simp]: "strip(step' S C) = strip C"
@@ -94,32 +80,23 @@
text{* Soundness: *}
-lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
+lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
- (auto simp: L_st_def intro!: aval'_sound in_gamma_update split: option.splits)
-
-lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
-unfolding step'_def
-by(rule Step_in_L)(auto simp: L_st_def step'_def split: option.splits)
+ (auto simp: intro!: aval'_sound in_gamma_update split: option.splits)
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
- assume 1: "pfp (step' (Top(vars c))) (bot c) = Some C"
- have "C \<in> L(vars c)"
- by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
- (erule step'_in_L[OF _ Top_in_L])
- have pfp': "step' (Top(vars c)) C \<le> C" by(rule pfp_pfp[OF 1])
- have 2: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+ assume 1: "pfp (step' \<top>) (bot c) = Some C"
+ have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
+ have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C" --"transfer the pfp'"
proof(rule order_trans)
- show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (Top(vars c)) C)"
- by(rule step_step'[OF `C \<in> L(vars c)` Top_in_L])
- show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
- by(rule mono_gamma_c[OF pfp'])
+ show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
+ show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
qed
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
- have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
- by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
+ have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
+ by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -128,49 +105,34 @@
subsubsection "Monotonicity"
-lemma le_sup_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow>
- x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
+lemma le_sup_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> (z::_::semilattice_sup)"
by (metis sup_ge1 sup_ge2 order_trans)
-theorem mono2_Step: fixes C1 :: "'a::semilatticeL acom"
- assumes "!!x e S1 S2. \<lbrakk>S1 \<in> L X; S2 \<in> L X; x \<in> X; vars e \<subseteq> X; S1 \<le> S2\<rbrakk> \<Longrightarrow> f x e S1 \<le> f x e S2"
- "!!b S1 S2. S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
- shows "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
- S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
+theorem mono2_Step: fixes C1 :: "'a::semilattice acom"
+ assumes "!!x e S1 S2. S1 \<le> S2 \<Longrightarrow> f x e S1 \<le> f x e S2"
+ "!!b S1 S2. S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
+ shows "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
by(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
- (auto simp: mono_post assms le_sup_disj le_sup_disj[OF post_in_L post_in_L])
+ (auto simp: mono_post assms le_sup_disj)
locale Abs_Int_mono = Abs_Int +
assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
begin
-lemma mono_aval':
- "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<le> aval' e S2"
-by(induction e) (auto simp: less_eq_st_def mono_plus' L_st_def)
+lemma mono_aval': "S1 \<le> S2 \<Longrightarrow> aval' e S1 \<le> aval' e S2"
+by(induction e) (auto simp: mono_plus' mono_fun)
-theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
- S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+theorem mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
unfolding step'_def
by(rule mono2_Step) (auto simp: mono_aval' split: option.split)
-lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
- C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'"
-by (metis Top_in_L mono_step' order_refl)
+lemma mono_step'_top: "C \<le> C' \<Longrightarrow> step' \<top> C \<le> step' \<top> C'"
+by (metis mono_step' order_refl)
-lemma pfp_bot_least:
-assumes "\<forall>x\<in>L(vars c)\<inter>{C. strip C = c}.\<forall>y\<in>L(vars c)\<inter>{C. strip C = c}.
- x \<le> y \<longrightarrow> f x \<le> f y"
-and "\<forall>C. C \<in> L(vars c)\<inter>{C. strip C = c} \<longrightarrow> f C \<in> L(vars c)\<inter>{C. strip C = c}"
-and "f C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
+lemma AI_least_pfp: assumes "AI c = Some C" "step' \<top> C' \<le> C'" "strip C' = c"
shows "C \<le> C'"
-by(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
- (simp_all add: assms(4,5) bot_least)
-
-lemma AI_least_pfp: assumes "AI c = Some C"
-and "step' (Top(vars c)) C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)"
-shows "C \<le> C'"
-by(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
+by(rule pfp_bot_least[OF _ _ assms(2,3) assms(1)[unfolded AI_def]])
(simp_all add: mono_step'_top)
end
@@ -196,44 +158,112 @@
locale Measure1 =
-fixes m :: "'av::order \<Rightarrow> nat"
+fixes m :: "'av::{order,top} \<Rightarrow> nat"
fixes h :: "nat"
assumes h: "m x \<le> h"
begin
-definition m_s :: "'av st \<Rightarrow> nat" ("m\<^isub>s") where
-"m_s S = (\<Sum> x \<in> dom S. m(fun S x))"
+definition m_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("m\<^isub>s") where
+"m_s X S = (\<Sum> x \<in> X. m(fun S x))"
+
+lemma m_s_h: "finite X \<Longrightarrow> m_s X S \<le> h * card X"
+by(simp add: m_s_def) (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
-lemma m_s_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_s x \<le> h * card X"
-by(simp add: L_st_def m_s_def)
- (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
+definition m_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
+"m_o X opt = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s X S)"
-definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
-"m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_s S)"
-
-lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)"
-by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h)
+lemma m_o_h: "finite X \<Longrightarrow> m_o X opt \<le> (h*card X + 1)"
+by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
-"m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
+"m_c C = (\<Sum>i<size(annos C). m_o (vars C) (annos C ! i))"
-lemma m_c_h: assumes "C \<in> L(vars(strip C))"
-shows "m_c C \<le> size(annos C) * (h * card(vars(strip C)) + 1)"
+text{* Upper complexity bound: *}
+lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
- let ?X = "vars(strip C)" let ?n = "card ?X" let ?a = "size(annos C)"
- { fix i assume "i < ?a"
- hence "annos C ! i \<in> L ?X" using assms by(simp add: L_acom_def)
- note m_o_h[OF this finite_cvars]
- } note 1 = this
- have "m_c C = (\<Sum>i<?a. m_o ?n (annos C ! i))" by(simp add: m_c_def)
+ let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
+ have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))" by(simp add: m_c_def)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
- apply(rule setsum_mono) using 1 by simp
+ apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
finally show ?thesis .
qed
end
+text{* The predicates @{text "top_on X a"} that follow describe that @{text a} is some object
+that maps all variables in @{text X} to @{term \<top>}.
+This is an important invariant for the termination proof where we argue that only
+the finitely many variables in the program change. That the others do not change
+follows because they remain @{term \<top>}. *}
+
+class top_on =
+fixes top_on :: "vname set \<Rightarrow> 'a \<Rightarrow> bool"
+
+instantiation st :: (top)top_on
+begin
+
+fun top_on_st :: "vname set \<Rightarrow> 'a st \<Rightarrow> bool" where
+"top_on_st X F = (\<forall>x\<in>X. fun F x = \<top>)"
+
+instance ..
+
+end
+
+instantiation option :: (top_on)top_on
+begin
+
+fun top_on_option :: "vname set \<Rightarrow> 'a option \<Rightarrow> bool" where
+"top_on_option X (Some F) = top_on X F" |
+"top_on_option X None = True"
+
+instance ..
+
+end
+
+instantiation acom :: (top_on)top_on
+begin
+
+definition top_on_acom :: "vname set \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on X a)"
+
+instance ..
+
+end
+
+lemma top_on_top: "top_on X (\<top>::_ st option)"
+by(auto simp: top_option_def fun_top)
+
+lemma top_on_bot: "top_on X (bot c)"
+by(auto simp add: top_on_acom_def bot_def)
+
+lemma top_on_post: "top_on X C \<Longrightarrow> top_on X (post C)"
+by(simp add: top_on_acom_def post_in_annos)
+
+lemma top_on_acom_simps:
+ "top_on X (SKIP {Q}) = top_on X Q"
+ "top_on X (x ::= e {Q}) = top_on X Q"
+ "top_on X (C1;C2) = (top_on X C1 \<and> top_on X C2)"
+ "top_on X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+ (top_on X P1 \<and> top_on X C1 \<and> top_on X P2 \<and> top_on X C2 \<and> top_on X Q)"
+ "top_on X ({I} WHILE b DO {P} C {Q}) =
+ (top_on X I \<and> top_on X C \<and> top_on X P \<and> top_on X Q)"
+by(auto simp add: top_on_acom_def)
+
+lemma top_on_sup:
+ "top_on X o1 \<Longrightarrow> top_on X o2 \<Longrightarrow> top_on X (o1 \<squnion> o2 :: _ st option)"
+apply(induction o1 o2 rule: sup_option.induct)
+apply(auto)
+by transfer simp
+
+lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
+assumes "!!x e S. \<lbrakk>top_on X S; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on X (f x e S)"
+ "!!b S. top_on X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on X (g b S)"
+shows "\<lbrakk> vars C \<subseteq> -X; top_on X S; top_on X C \<rbrakk> \<Longrightarrow> top_on X (Step f g S C)"
+proof(induction C arbitrary: S)
+qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
+
+
locale Measure = Measure1 +
assumes m2: "x < y \<Longrightarrow> m x > m y"
begin
@@ -241,62 +271,79 @@
lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
by(auto simp: le_less m2)
-lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 > m_s S2"
-proof(auto simp add: less_st_def less_eq_st_def m_s_def)
- assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
- hence 1: "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
- fix x assume "x \<in> dom S2" "\<not> fun S2 x \<le> fun S1 x"
- hence 2: "\<exists>x\<in>dom S2. m(fun S1 x) > m(fun S2 x)" by (metis 0 m2 less_le_not_le)
- from setsum_strict_mono_ex1[OF `finite(dom S2)` 1 2]
- show "(\<Sum>x\<in>dom S2. m (fun S2 x)) < (\<Sum>x\<in>dom S2. m (fun S1 x))" .
+lemma m_s2_rep: assumes "finite(X)" and "S1 = S2 on -X" and "\<forall>x. S1 x \<le> S2 x" and "S1 \<noteq> S2"
+shows "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
+proof-
+ from assms(3) have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S2 x)" by (simp add: m1)
+ from assms(2,3,4) have "EX x:X. S1 x < S2 x"
+ by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
+ hence 2: "\<exists>x\<in>X. m(S1 x) > m(S2 x)" by (metis m2)
+ from setsum_strict_mono_ex1[OF `finite X` 1 2]
+ show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
qed
-lemma m_o2: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
- o1 < o2 \<Longrightarrow> m_o (card X) o1 > m_o (card X) o2"
+lemma m_s2: "finite(X) \<Longrightarrow> fun S1 = fun S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s X S1 > m_s X S2"
+apply(auto simp add: less_st_def m_s_def)
+apply (transfer fixing: m)
+apply(simp add: less_eq_st_rep_iff eq_st_def m_s2_rep)
+done
+
+lemma m_o2: "finite X \<Longrightarrow> top_on (-X) o1 \<Longrightarrow> top_on (-X) o2 \<Longrightarrow>
+ o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
proof(induction o1 o2 rule: less_eq_option.induct)
- case 1 thus ?case by (auto simp: m_o_def L_st_def m_s2 less_option_def)
+ case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
next
case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h)
next
case 3 thus ?case by (auto simp: less_option_def)
qed
-lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
- o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
+lemma m_o1: "finite X \<Longrightarrow> top_on (-X) o1 \<Longrightarrow> top_on (-X) o2 \<Longrightarrow>
+ o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
by(auto simp: le_less m_o2)
-lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow>
+
+lemma m_c2: "top_on (-vars C1) C1 \<Longrightarrow> top_on (-vars C2) C2 \<Longrightarrow>
C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
-proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] less_acom_def L_acom_def)
+proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
let ?X = "vars(strip C2)"
- let ?n = "card ?X"
- assume V1: "\<forall>a\<in>set(annos C1). a \<in> L ?X"
- and V2: "\<forall>a\<in>set(annos C2). a \<in> L ?X"
- and strip_eq: "strip C1 = strip C2"
- and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
- hence 1: "\<forall>i<size(annos C2). m_o ?n (annos C1 ! i) \<ge> m_o ?n (annos C2 ! i)"
- by (auto simp: all_set_conv_all_nth)
- (metis finite_cvars m_o1 size_annos_same2)
- fix i assume "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
- hence "m_o ?n (annos C1 ! i) > m_o ?n (annos C2 ! i)" (is "?P i")
- by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0 less_option_def)
+ assume top: "top_on (- vars(strip C2)) C1" "top_on (- vars(strip C2)) C2"
+ and strip_eq: "strip C1 = strip C2"
+ and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
+ hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
+ apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
+ by (metis finite_cvars m_o1 size_annos_same2)
+ fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
+ have topo1: "top_on (- ?X) (annos C1 ! i)"
+ using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
+ have topo2: "top_on (- ?X) (annos C2 ! i)"
+ using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
+ from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
+ by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
- show "(\<Sum>i<size(annos C2). m_o ?n (annos C2 ! i))
- < (\<Sum>i<size(annos C2). m_o ?n (annos C1 ! i))"
+ show "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
+ < (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
qed
end
+
locale Abs_Int_measure =
Abs_Int_mono where \<gamma>=\<gamma> + Measure where m=m
for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
begin
+lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on X C \<rbrakk> \<Longrightarrow> top_on X (step' \<top> C)"
+unfolding step'_def
+by(rule top_on_Step)
+ (auto simp add: top_option_def fun_top split: option.splits)
+
lemma AI_Some_measure: "\<exists>C. AI c = Some C"
unfolding AI_def
-apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> C \<in> L(vars c)" and m="m_c"])
-apply(simp_all add: m_c2 mono_step'_top bot_least)
+apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on (- vars C) C" and m="m_c"])
+apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
+apply(auto simp add: top_on_step' vars_acom_def)
done
end
--- a/src/HOL/IMP/Abs_Int1_const.thy Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Apr 17 21:11:01 2013 +0200
@@ -80,7 +80,7 @@
subsubsection "Tests"
-definition "steps c i = (step_const(Top(vars c)) ^^ i) (bot c)"
+definition "steps c i = (step_const \<top> ^^ i) (bot c)"
value "show_acom (steps test1_const 0)"
value "show_acom (steps test1_const 1)"
--- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Apr 17 21:11:01 2013 +0200
@@ -141,7 +141,7 @@
''x'' ::= N 1;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
-definition "steps c i = (step_parity(Top(vars c)) ^^ i) (bot c)"
+definition "steps c i = ((step_parity \<top>) ^^ i) (bot c)"
value "show_acom (steps test2_parity 0)"
value "show_acom (steps test2_parity 1)"
--- a/src/HOL/IMP/Abs_Int2.thy Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Wed Apr 17 21:11:01 2013 +0200
@@ -26,10 +26,10 @@
subsection "Backward Analysis of Expressions"
-class lattice = semilattice + semilattice_inf + bot
+subclass (in bounded_lattice) semilattice ..
locale Val_abs1_gamma =
- Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set" +
+ Gamma 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)"
and gamma_bot[simp]: "\<gamma> \<bottom> = {}"
@@ -47,7 +47,7 @@
locale Val_abs1 =
Val_abs1_gamma where \<gamma> = \<gamma>
- for \<gamma> :: "'av::lattice \<Rightarrow> val set" +
+ for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
@@ -59,19 +59,19 @@
locale Abs_Int1 =
- Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set"
+ Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
begin
lemma in_gamma_sup_UpI:
- "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
-by (metis (hide_lams, no_types) semilatticeL_class.sup_ge1 semilatticeL_class.sup_ge2 mono_gamma_o subsetD)
+ "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
+by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
"aval'' e None = \<bottom>" |
"aval'' e (Some sa) = aval' e sa"
-lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> S \<in> L X \<Longrightarrow> vars a \<subseteq> X \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
-by(simp add: L_option_def L_st_def aval'_sound split: option.splits)
+lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
+by(cases S)(auto simp add: aval'_sound split: option.splits)
subsubsection "Backward analysis"
@@ -104,12 +104,7 @@
(let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
in afilter e1 a1 (afilter e2 a2 S))"
-lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
-by(induction e arbitrary: a S)
- (auto simp: Let_def L_st_def split: option.splits prod.split)
-
-lemma afilter_sound: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
- s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
+lemma afilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
proof(induction e arbitrary: a S)
case N thus ?case by simp (metis test_num')
next
@@ -117,33 +112,29 @@
obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>s S'" using `s : \<gamma>\<^isub>o S`
by(auto simp: in_gamma_option_iff)
moreover hence "s x : \<gamma> (fun S' x)"
- using V(1,2) by(simp add: \<gamma>_st_def L_st_def)
+ using V(1,2) by(simp add: \<gamma>_st_def)
moreover have "s x : \<gamma> a" using V by simp
- ultimately show ?case using V(3)
+ ultimately show ?case
by(simp add: Let_def \<gamma>_st_def)
(metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
next
case (Plus e1 e2) thus ?case
- using filter_plus'[OF _ aval''_sound[OF Plus.prems(3)] aval''_sound[OF Plus.prems(3)]]
- by (auto simp: afilter_in_L split: prod.split)
+ using filter_plus'[OF _ aval''_sound aval''_sound]
+ by (auto split: prod.split)
qed
-lemma bfilter_in_L: "S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> bfilter b bv S \<in> L X"
-by(induction b arbitrary: bv S)(auto simp: afilter_in_L split: prod.split)
-
-lemma bfilter_sound: "S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
- s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)"
+lemma bfilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)"
proof(induction b arbitrary: S bv)
case Bc thus ?case by simp
next
case (Not b) thus ?case by simp
next
case (And b1 b2) thus ?case
- by simp (metis And(1) And(2) bfilter_in_L in_gamma_sup_UpI)
+ by simp (metis And(1) And(2) in_gamma_sup_UpI)
next
case (Less e1 e2) thus ?case
by(auto split: prod.split)
- (metis (lifting) afilter_in_L afilter_sound aval''_sound filter_less')
+ (metis (lifting) afilter_sound aval''_sound filter_less')
qed
definition "step' = Step
@@ -151,40 +142,41 @@
(\<lambda>b S. bfilter b True S)"
definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' \<top>\<^bsub>vars c\<^esub>) (bot c)"
+"AI c = pfp (step' \<top>) (bot c)"
lemma strip_step'[simp]: "strip(step' S c) = strip c"
by(simp add: step'_def)
+lemma top_on_afilter: "\<lbrakk> top_on X S; vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on X (afilter e a S)"
+by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)
+
+lemma top_on_bfilter: "\<lbrakk>top_on X S; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on X (bfilter b r S)"
+by(induction b arbitrary: r S) (auto simp: top_on_afilter top_on_sup split: prod.split)
+
+lemma top_on_step': "top_on (- vars C) C \<Longrightarrow> top_on (- vars C) (step' \<top> C)"
+unfolding step'_def
+by(rule top_on_Step)
+ (auto simp add: top_on_top top_on_bfilter split: option.split)
subsubsection "Soundness"
-lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
+lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
- (auto simp: L_st_def intro!: aval'_sound bfilter_sound in_gamma_update split: option.splits)
-
-lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
-unfolding step'_def
-by(rule Step_in_L)(auto simp: bfilter_in_L L_st_def step'_def split: option.splits)
+ (auto simp: intro!: aval'_sound bfilter_sound in_gamma_update split: option.splits)
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
- assume 1: "pfp (step' (Top(vars c))) (bot c) = Some C"
- have "C \<in> L(vars c)"
- by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
- (erule step'_in_L[OF _ Top_in_L])
- have pfp': "step' (Top(vars c)) C \<le> C" by(rule pfp_pfp[OF 1])
- have 2: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+ assume 1: "pfp (step' \<top>) (bot c) = Some C"
+ have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
+ have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C" --"transfer the pfp'"
proof(rule order_trans)
- show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (Top(vars c)) C)"
- by(rule step_step'[OF `C \<in> L(vars c)` Top_in_L])
- show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
- by(rule mono_gamma_c[OF pfp'])
+ show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
+ show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
qed
- have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
- have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
- by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
+ have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
+ have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
+ by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -202,46 +194,42 @@
begin
lemma mono_aval':
- "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<le> aval' e S2"
-by(induction e) (auto simp: less_eq_st_def mono_plus' L_st_def)
+ "S1 \<le> S2 \<Longrightarrow> aval' e S1 \<le> aval' e S2"
+by(induction e) (auto simp: mono_plus' mono_fun)
lemma mono_aval'':
- "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
+ "S1 \<le> S2 \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
apply(cases S1)
apply simp
apply(cases S2)
apply simp
by (simp add: mono_aval')
-lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
- r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
+lemma mono_afilter: "r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
apply(induction e arbitrary: r1 r2 S1 S2)
apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
apply (metis mono_gamma subsetD)
- apply (metis inf_mono le_bot mono_fun_L)
- apply (metis inf_mono mono_fun_L mono_update)
-apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
+ apply (metis le_bot inf_mono le_st_iff)
+ apply (metis inf_mono mono_update le_st_iff)
+apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv)
done
-lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
- S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
+lemma mono_bfilter: "S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
apply(induction b arbitrary: bv S1 S2)
apply(simp)
apply(simp)
apply simp
- apply(metis sup_least order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2] bfilter_in_L)
+ apply(metis order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2])
apply (simp split: prod.splits)
-apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
+apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv)
done
-theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
- S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+theorem mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
unfolding step'_def
by(rule mono2_Step) (auto simp: mono_aval' mono_bfilter split: option.split)
-lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
- C1 \<le> C2 \<Longrightarrow> step' (Top X) C1 \<le> step' (Top X) C2"
-by (metis Top_in_L mono_step' order_refl)
+lemma mono_step'_top: "C1 \<le> C2 \<Longrightarrow> step' \<top> C1 \<le> step' \<top> C2"
+by (metis mono_step' order_refl)
end
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Apr 17 21:11:01 2013 +0200
@@ -139,7 +139,7 @@
lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)"
by(simp add: not_less)
-instantiation ivl :: lattice
+instantiation ivl :: bounded_lattice
begin
definition inf_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
@@ -392,7 +392,7 @@
value "show_acom_opt (AI_ivl test4_const)"
value "show_acom_opt (AI_ivl test6_const)"
-definition "steps c i = (step_ivl(Top(vars c)) ^^ i) (bot c)"
+definition "steps c i = (step_ivl \<top> ^^ i) (bot c)"
value "show_acom_opt (AI_ivl test2_ivl)"
value "show_acom (steps test2_ivl 0)"
--- a/src/HOL/IMP/Abs_Int3.thy Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Apr 17 21:11:01 2013 +0200
@@ -4,58 +4,6 @@
imports Abs_Int2_ivl
begin
-subsubsection "Welltypedness"
-
-class Lc =
-fixes Lc :: "com \<Rightarrow> 'a set"
-
-instantiation st :: (type)Lc
-begin
-
-definition Lc_st :: "com \<Rightarrow> 'a st set" where
-"Lc_st c = L (vars c)"
-
-instance ..
-
-end
-
-instantiation acom :: (Lc)Lc
-begin
-
-definition Lc_acom :: "com \<Rightarrow> 'a acom set" where
-"Lc c = {C. strip C = c \<and> (\<forall>a\<in>set(annos C). a \<in> Lc c)}"
-
-instance ..
-
-end
-
-instantiation option :: (Lc)Lc
-begin
-
-definition Lc_option :: "com \<Rightarrow> 'a option set" where
-"Lc c = {None} \<union> Some ` Lc c"
-
-lemma Lc_option_simps[simp]: "None \<in> Lc c" "(Some x \<in> Lc c) = (x \<in> Lc c)"
-by(auto simp: Lc_option_def)
-
-instance ..
-
-end
-
-lemma Lc_option_iff_wt[simp]: fixes a :: "_ st option"
-shows "(a \<in> Lc c) = (a \<in> L (vars c))"
-by(auto simp add: L_option_def Lc_st_def split: option.splits)
-
-
-context Abs_Int1
-begin
-
-lemma step'_in_Lc: "C \<in> Lc c \<Longrightarrow> S \<in> Lc c \<Longrightarrow> step' S C \<in> Lc c"
-apply(auto simp add: Lc_acom_def)
-by(metis step'_in_L[simplified L_acom_def mem_Collect_eq] order_refl)
-
-end
-
subsection "Widening and Narrowing"
@@ -70,15 +18,15 @@
assumes widen2: "y \<le> x \<nabla> y"
assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
+begin
-class WN_Lc = widen + narrow + order + Lc +
-assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<le> x \<nabla> y"
-assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<le> x \<nabla> y"
-assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
-assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
-assumes Lc_widen[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<nabla> y \<in> Lc c"
-assumes Lc_narrow[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<triangle> y \<in> Lc c"
+lemma narrowid[simp]: "x \<triangle> x = x"
+by (metis eq_iff narrow1 narrow2)
+end
+
+lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{WN,top})"
+by (metis eq_iff top_greatest widen2)
instantiation ivl :: WN
begin
@@ -101,38 +49,38 @@
instance
proof
-qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset \<gamma>_rep_def subset_eq is_empty_rep_def empty_rep_def split: if_splits extended.splits)+
+qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset \<gamma>_rep_def subset_eq is_empty_rep_def empty_rep_def eq_ivl_def split: if_splits extended.splits)+
end
-
-instantiation st :: (WN)WN_Lc
+instantiation st :: ("{top,WN}")WN
begin
-definition "widen_st F1 F2 = St (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
+lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)"
+by(auto simp: eq_st_def)
-definition "narrow_st F1 F2 = St (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
+lift_definition narrow_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<triangle>)"
+by(auto simp: eq_st_def)
instance
proof
- case goal1 thus ?case by(simp add: widen_st_def less_eq_st_def WN_class.widen1)
+ case goal1 thus ?case
+ by transfer (simp add: less_eq_st_rep_iff widen1)
next
case goal2 thus ?case
- by(simp add: widen_st_def less_eq_st_def WN_class.widen2 Lc_st_def L_st_def)
-next
- case goal3 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow1)
+ by transfer (simp add: less_eq_st_rep_iff widen2)
next
- case goal4 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow2)
+ case goal3 thus ?case
+ by transfer (simp add: less_eq_st_rep_iff narrow1)
next
- case goal5 thus ?case by(auto simp: widen_st_def Lc_st_def L_st_def)
-next
- case goal6 thus ?case by(auto simp: narrow_st_def Lc_st_def L_st_def)
+ case goal4 thus ?case
+ by transfer (simp add: less_eq_st_rep_iff narrow2)
qed
end
-instantiation option :: (WN_Lc)WN_Lc
+instantiation option :: (WN)WN
begin
fun widen_option where
@@ -158,12 +106,6 @@
next
case goal4 thus ?case
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
-next
- case goal5 thus ?case
- by(induction x y rule: widen_option.induct)(auto simp: Lc_st_def)
-next
- case goal6 thus ?case
- by(induction x y rule: narrow_option.induct)(auto simp: Lc_st_def)
qed
end
@@ -178,6 +120,9 @@
"map2_acom f ({a1} WHILE b DO {p} C {a2}) ({a3} WHILE b' DO {p'} C' {a4}) =
({f a1 a3} WHILE b DO {f p p'} map2_acom f C C' {f a2 a4})"
+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
@@ -191,21 +136,6 @@
instance ..
end
-instantiation acom :: (WN_Lc)WN_Lc
-begin
-
-lemma widen_acom1: fixes C1 :: "'a acom" shows
- "\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk>
- \<Longrightarrow> C1 \<le> C1 \<nabla> C2"
-by(induct C1 C2 rule: less_eq_acom.induct)
- (auto simp: widen_acom_def widen1 Lc_acom_def)
-
-lemma widen_acom2: fixes C1 :: "'a acom" shows
- "\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk>
- \<Longrightarrow> C2 \<le> C1 \<nabla> C2"
-by(induct C1 C2 rule: less_eq_acom.induct)
- (auto simp: widen_acom_def widen2 Lc_acom_def)
-
lemma strip_map2_acom[simp]:
"strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1"
by(induct f C1 C2 rule: map2_acom.induct) simp_all
@@ -218,53 +148,11 @@
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1"
by(simp add: narrow_acom_def)
-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)
-
-instance
-proof
- case goal1 thus ?case by(auto simp: Lc_acom_def widen_acom1)
-next
- case goal2 thus ?case by(auto simp: Lc_acom_def widen_acom2)
-next
- case goal3 thus ?case
- by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1)
-next
- case goal4 thus ?case
- by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2)
-next
- case goal5 thus ?case
- by(auto simp: Lc_acom_def widen_acom_def split_conv elim!: in_set_zipE)
-next
- case goal6 thus ?case
- by(auto simp: Lc_acom_def narrow_acom_def split_conv elim!: in_set_zipE)
-qed
+lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::WN acom)"
+by(induct C1 C2 rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1)
-end
-
-lemma widen_o_in_L[simp]: fixes x1 x2 :: "_ st option"
-shows "x1 \<in> L X \<Longrightarrow> x2 \<in> L X \<Longrightarrow> x1 \<nabla> x2 \<in> L X"
-by(induction x1 x2 rule: widen_option.induct)
- (simp_all add: widen_st_def L_st_def)
-
-lemma narrow_o_in_L[simp]: fixes x1 x2 :: "_ st option"
-shows "x1 \<in> L X \<Longrightarrow> x2 \<in> L X \<Longrightarrow> x1 \<triangle> x2 \<in> L X"
-by(induction x1 x2 rule: narrow_option.induct)
- (simp_all add: narrow_st_def L_st_def)
-
-lemma widen_c_in_L: fixes C1 C2 :: "_ st option acom"
-shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<nabla> C2 \<in> L X"
-by(induction C1 C2 rule: less_eq_acom.induct)
- (auto simp: widen_acom_def)
-
-lemma narrow_c_in_L: fixes C1 C2 :: "_ st option acom"
-shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<triangle> C2 \<in> L X"
-by(induction C1 C2 rule: less_eq_acom.induct)
- (auto simp: narrow_acom_def)
-
-lemma bot_in_Lc[simp]: "bot c \<in> Lc c"
-by(simp add: Lc_acom_def bot_def)
+lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::WN acom) \<le> C1"
+by(induct C1 C2 rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2)
subsubsection "Post-fixed point computation"
@@ -305,7 +193,7 @@
qed
lemma iter_narrow_pfp:
-assumes mono: "!!x1 x2::_::WN_Lc. 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"
@@ -318,10 +206,10 @@
have "?Q ?p'"
proof auto
show "P ?p'" by (blast intro: P Pinv)
- have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)` P narrow2[OF 1]])
- also have "\<dots> \<le> ?p'" by(rule narrow1[OF 1])
+ have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)` P narrow2_acom[OF 1]])
+ also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1])
finally show "f ?p' \<le> ?p'" .
- have "?p' \<le> p" by (rule narrow2[OF 1])
+ have "?p' \<le> p" by (rule narrow2_acom[OF 1])
also have "p \<le> p0" by(rule 2)
finally show "?p' \<le> p0" .
qed
@@ -332,7 +220,7 @@
qed
lemma pfp_wn_pfp:
-assumes mono: "!!x1 x2::_::WN_Lc. 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)"
@@ -354,28 +242,27 @@
locale Abs_Int2 = Abs_Int1_mono
-where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set"
+where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set"
begin
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
-"AI_wn c = pfp_wn (step' (Top(vars c))) (bot c)"
+"AI_wn c = pfp_wn (step' \<top>) (bot c)"
lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_wn_def)
- assume 1: "pfp_wn (step' (Top(vars c))) (bot c) = Some C"
- have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<le> C"
- by(rule pfp_wn_pfp[where x="bot c"])
- (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
- have pfp: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+ assume 1: "pfp_wn (step' \<top>) (bot c) = Some C"
+ have 2: "strip C = c \<and> step' \<top> C \<le> C"
+ by(rule pfp_wn_pfp[where x="bot c"]) (simp_all add: 1 mono_step'_top)
+ have pfp: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
proof(rule order_trans)
- show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (Top(vars c)) C)"
- by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] Top_in_L])
+ show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)"
+ by(rule step_step')
show "... \<le> \<gamma>\<^isub>c C"
by(rule mono_gamma_c[OF conjunct2[OF 2]])
qed
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
- have "lfp c (step (\<gamma>\<^isub>o (Top(vars c)))) \<le> \<gamma>\<^isub>c C"
- by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 pfp])
+ have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
+ by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 pfp])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -392,9 +279,9 @@
subsubsection "Tests"
definition "step_up_ivl n =
- ((\<lambda>C. C \<nabla> step_ivl (Top(vars(strip C))) C)^^n)"
+ ((\<lambda>C. C \<nabla> step_ivl \<top> C)^^n)"
definition "step_down_ivl n =
- ((\<lambda>C. C \<triangle> step_ivl (Top(vars(strip C))) C)^^n)"
+ ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)"
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
the loop took to execute. In contrast, @{const AI_ivl'} converges in a
@@ -424,13 +311,31 @@
subsubsection "Generic Termination Proof"
+lemma top_on_opt_widen: "top_on X o1 \<Longrightarrow> top_on X o2 \<Longrightarrow> top_on X (o1 \<nabla> o2 :: _ st option)"
+apply(induct o1 o2 rule: widen_option.induct)
+apply (auto)
+by transfer simp
+
+lemma top_on_opt_narrow: "top_on X o1 \<Longrightarrow> top_on X o2 \<Longrightarrow> top_on X (o1 \<triangle> o2 :: _ st option)"
+apply(induct o1 o2 rule: narrow_option.induct)
+apply (auto)
+by transfer simp
+
+lemma top_on_acom_widen:
+ "\<lbrakk>top_on X C1; strip C1 = strip C2; top_on X C2\<rbrakk> \<Longrightarrow> top_on X (C1 \<nabla> C2 :: _ st option acom)"
+by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE)
+
+lemma top_on_acom_narrow:
+ "\<lbrakk>top_on X C1; strip C1 = strip C2; top_on X C2\<rbrakk> \<Longrightarrow> top_on X (C1 \<triangle> C2 :: _ st option acom)"
+by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE)
+
text{* The assumptions for widening and narrowing differ because during
narrowing we have the invariant @{prop"y \<le> x"} (where @{text y} is the next
iterate), but during widening there is no such invariant, there we only have
that not yet @{prop"y \<le> x"}. This complicates the termination proof for
widening. *}
-locale Measure_WN = Measure1 where m=m for m :: "'av::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"
@@ -438,129 +343,132 @@
begin
-lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
-proof(auto simp add: less_eq_st_def m_s_def)
- assume "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
- hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m_anti_mono)
- thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
- by (metis setsum_mono)
+lemma m_s_anti_mono_rep: assumes "\<forall>x. S1 x \<le> S2 x"
+shows "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))"
+proof-
+ from assms have "\<forall>x. m(S1 x) \<ge> m(S2 x)" by (metis m_anti_mono)
+ thus "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" by (metis setsum_mono)
qed
-lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
- ~ S2 \<le> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
-proof(auto simp add: less_eq_st_def m_s_def L_st_def widen_st_def)
- assume "finite(dom S1)"
- have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
+lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s X S1 \<ge> m_s X S2"
+unfolding m_s_def
+apply (transfer fixing: m)
+apply(simp add: less_eq_st_rep_iff eq_st_def m_s_anti_mono_rep)
+done
+
+lemma m_s_widen_rep: assumes "finite X" "S1 = S2 on -X" "\<not> S2 x \<le> S1 x"
+ 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)
- fix x assume "x \<in> dom S1" "\<not> fun S2 x \<le> fun S1 x"
- hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
- using m_widen by blast
- from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2]
- show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
+ 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)"
+ using assms(3) m_widen by blast
+ from setsum_strict_mono_ex1[OF `finite X` 1 2]
+ show ?thesis .
qed
-lemma m_o_anti_mono: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
- o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
+lemma m_s_widen: "finite X \<Longrightarrow> fun S1 = fun S2 on -X ==>
+ ~ S2 \<le> S1 \<Longrightarrow> m_s X (S1 \<nabla> S2) < m_s X S1"
+apply(auto simp add: less_st_def m_s_def)
+apply (transfer fixing: m)
+apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep)
+done
+
+lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on (-X) o1 \<Longrightarrow> top_on (-X) o2 \<Longrightarrow>
+ o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
proof(induction o1 o2 rule: less_eq_option.induct)
case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
next
case 2 thus ?case
- by(simp add: L_option_def m_o_def le_SucI m_s_h split: option.splits)
+ by(simp add: m_o_def le_SucI m_s_h split: option.splits)
next
case 3 thus ?case by simp
qed
-lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
- m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1"
-by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
+lemma m_o_widen: "\<lbrakk> finite X; top_on (-X) S1; top_on (-X) S2; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
+ m_o X (S1 \<nabla> S2) < m_o X S1"
+by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
lemma m_c_widen:
- "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
-apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
+ "strip C1 = strip C2 \<Longrightarrow> top_on (-vars C1) C1 \<Longrightarrow> top_on (-vars C2) C2
+ \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
+apply(auto simp: m_c_def widen_acom_def)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)
apply(rule setsum_strict_mono_ex1)
- apply simp
- apply (clarsimp)
- apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
-apply(auto simp: le_iff_le_annos listrel_iff_nth)
+ apply(auto simp add: m_o_anti_mono vars_acom_def top_on_acom_def top_on_opt_widen widen1 le_iff_le_annos listrel_iff_nth)
apply(rule_tac x=i in bexI)
- prefer 2 apply simp
-apply(rule m_o_widen)
- apply (simp add: finite_cvars)+
+ apply (auto simp: vars_acom_def m_o_widen top_on_acom_def)
done
-definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where
-"n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))"
+definition n_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("n\<^isub>s") where
+"n\<^isub>s X S = (\<Sum>x\<in>X. n(fun S x))"
-lemma less_stD:
- "(S1 < S2) \<Longrightarrow> (S1 \<le> S2 \<and> (\<exists>x\<in>dom S1. fun S1 x < fun S2 x))"
-by (metis less_eq_st_def less_le_not_le)
-
-lemma n_s_narrow:
-assumes "finite(dom S1)" and "S2 \<le> S1" "S1 \<triangle> S2 < S1"
-shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1"
+lemma n_s_narrow_rep:
+assumes "finite X" "S1 = S2 on -X" "\<forall>x. S2 x \<le> S1 x" "\<forall>x. S1 x \<triangle> S2 x \<le> S1 x"
+ "S1 x \<noteq> S1 x \<triangle> S2 x"
+shows "(\<Sum>x\<in>X. n (S1 x \<triangle> S2 x)) < (\<Sum>x\<in>X. n (S1 x))"
proof-
- from `S2\<le>S1`
- have dom[simp]: "dom S1 = dom S2" and "\<forall>x\<in>dom S1. fun S2 x \<le> fun S1 x"
- by(simp_all add: less_eq_st_def)
- { fix x assume "x \<in> dom S1"
- hence "n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
- using less_stD[OF `S1 \<triangle> S2 < S1`] `S2 \<le> S1` dom
- apply(auto simp: less_eq_st_def narrow_st_def)
- by (metis less_le n_narrow not_less)
- } note 1 = this
- have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)"
- using less_stD[OF `S1 \<triangle> S2 < S1`] `S2 \<le> S1`
- by(auto simp: less_eq_st_def narrow_st_def intro: n_narrow)
- have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
- apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
- moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
- ultimately show ?thesis by(simp add: n_s_def)
+ have 1: "\<forall>x. n(S1 x \<triangle> S2 x) \<le> n(S1 x)"
+ by (metis assms(3) assms(4) eq_iff less_le_not_le n_narrow)
+ have "x \<in> X" by (metis Compl_iff assms(2) assms(5) narrowid)
+ hence 2: "\<exists>x\<in>X. n(S1 x \<triangle> S2 x) < n(S1 x)"
+ by (metis assms(3-5) eq_iff less_le_not_le n_narrow)
+ show ?thesis
+ apply(rule setsum_strict_mono_ex1[OF `finite X`]) using 1 2 by blast+
qed
+lemma n_s_narrow: "finite X \<Longrightarrow> fun S1 = fun S2 on -X \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1
+ \<Longrightarrow> n\<^isub>s X (S1 \<triangle> S2) < n\<^isub>s X S1"
+apply(auto simp add: less_st_def n_s_def)
+apply (transfer fixing: n)
+apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep)
+done
-definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
-"n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
+definition n_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("n\<^isub>o") where
+"n\<^isub>o X opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s X S + 1)"
lemma n_o_narrow:
- "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
- \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
+ "top_on (-X) S1 \<Longrightarrow> top_on (-X) S2 \<Longrightarrow> finite X
+ \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o X (S1 \<triangle> S2) < n\<^isub>o X S1"
apply(induction S1 S2 rule: narrow_option.induct)
-apply(auto simp: n_o_def L_st_def n_s_narrow)
+apply(auto simp: n_o_def n_s_narrow)
done
definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^isub>c") where
-"n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))"
+"n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (vars C) (as!i))"
lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
(\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
-lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow>
- C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
-apply(auto simp: n_c_def Let_def Lc_acom_def narrow_acom_def)
+lemma n_c_narrow: "strip C1 = strip C2
+ \<Longrightarrow> top_on (- vars C1) C1 \<Longrightarrow> top_on (- vars C2) C2
+ \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
+apply(auto simp: n_c_def Let_def narrow_acom_def)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)
apply(simp add: less_annos_iff le_iff_le_annos)
apply(rule setsum_strict_mono_ex1)
-apply auto
+apply (auto simp: vars_acom_def top_on_acom_def)
apply (metis n_o_narrow nth_mem finite_cvars less_imp_le le_less order_refl)
apply(rule_tac x=i in bexI)
prefer 2 apply simp
-apply(rule n_o_narrow[where X = "vars(strip C1)"])
-apply (simp_all add: finite_cvars)
+apply(rule n_o_narrow[where X = "vars(strip C2)"])
+apply (simp_all)
done
end
lemma iter_widen_termination:
-fixes m :: "'a::WN_Lc \<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"
@@ -574,7 +482,7 @@
qed
lemma iter_narrow_termination:
-fixes n :: "'a::WN_Lc \<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"
@@ -587,7 +495,7 @@
fix C assume 1: "P C \<and> f C \<le> C" and 2: "C \<triangle> f C < C"
hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C"
- by (metis narrow1 narrow2 1 mono order_trans)
+ by (metis narrow1_acom narrow2_acom 1 mono order_trans)
moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f)
ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<le> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C"
by blast
@@ -595,7 +503,7 @@
locale Abs_Int2_measure =
Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m
- for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
+ for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
subsubsection "Termination: Intervals"
@@ -654,26 +562,19 @@
-- "note that the first assms is unnecessary for intervals"
qed
-
lemma iter_winden_step_ivl_termination:
- "\<exists>C. iter_widen (step_ivl (Top(vars c))) (bot c) = Some C"
-apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
-apply (simp_all add: step'_in_Lc m_c_widen)
+ "\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C"
+apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on (- vars C) C"])
+apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def]
+ vars_acom_def top_on_acom_widen)
done
lemma iter_narrow_step_ivl_termination:
- "C0 \<in> Lc c \<Longrightarrow> step_ivl (Top(vars c)) C0 \<le> C0 \<Longrightarrow>
- \<exists>C. iter_narrow (step_ivl (Top(vars c))) C0 = Some C"
-apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
-apply (simp add: step'_in_Lc)
-apply (simp)
-apply(rule mono_step'_top)
-apply(simp add: Lc_acom_def L_acom_def)
-apply(simp add: Lc_acom_def L_acom_def)
-apply assumption
-apply(erule (3) n_c_narrow)
-apply assumption
-apply assumption
+ "top_on (- vars C0) C0 \<Longrightarrow> step_ivl \<top> C0 \<le> C0 \<Longrightarrow>
+ \<exists>C. iter_narrow (step_ivl \<top>) C0 = Some C"
+apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. strip C0 = strip C \<and> top_on (-vars C) C"])
+apply(auto simp: top_on_step'[simplified comp_def vars_acom_def]
+ mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow)
done
theorem AI_ivl'_termination:
@@ -681,8 +582,10 @@
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
split: option.split)
apply(rule iter_narrow_step_ivl_termination)
-apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>vars c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>vars c\<^esub>" and c=c, simplified])
-apply(erule iter_widen_pfp)
+apply(rule conjunct2)
+apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on (- vars C) C"])
+apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def]
+ iter_widen_pfp top_on_bot vars_acom_def)
done
(*unused_thms Abs_Int_init - *)
--- a/src/HOL/IMP/Abs_State.thy Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy Wed Apr 17 21:11:01 2013 +0200
@@ -4,133 +4,56 @@
imports Abs_Int0
begin
-subsubsection "Set-based lattices"
-
-
-class L =
-fixes L :: "vname set \<Rightarrow> 'a set"
-
-
-instantiation acom :: (L)L
-begin
+type_synonym 'a st_rep = "(vname * 'a) list"
-definition L_acom where
-"L X = {C. vars(strip C) \<subseteq> X \<and> (\<forall>a \<in> set(annos C). a \<in> L X)}"
-
-instance ..
-
-end
-
-
-instantiation option :: (L)L
-begin
-
-definition L_option where
-"L X = {opt. case opt of None \<Rightarrow> True | Some x \<Rightarrow> x \<in> L X}"
+definition fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
+"fun_rep ps = (\<lambda>x. case map_of ps x of Some a \<Rightarrow> a | None \<Rightarrow> \<top>)"
-lemma L_option_simps[simp]: "None \<in> L X" "(Some x \<in> L X) = (x \<in> L X)"
-by(simp_all add: L_option_def)
-
-instance ..
-
-end
+definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
+"eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
-class semilatticeL = order + sup + L +
-fixes Top :: "vname set \<Rightarrow> 'a"
-assumes sup_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<le> x \<squnion> y"
-and sup_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<le> x \<squnion> y"
-and sup_least[simp]: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
-and Top[simp]: "x \<in> L X \<Longrightarrow> x \<le> Top X"
-and Top_in_L[simp]: "Top X \<in> L X"
-and sup_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
-
-notation (input) Top ("\<top>\<^bsub>_\<^esub>")
-notation (latex output) Top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
-
-instantiation option :: (semilatticeL)semilatticeL
-begin
-
-definition Top_option where "Top c = Some(Top c)"
+quotient_type 'a st = "('a::top) st_rep" / eq_st
+by (metis eq_st_def equivpI reflpI sympI transpI)
-instance proof
- case goal1 thus ?case by(cases x, simp, cases y, simp_all)
-next
- case goal2 thus ?case by(cases y, simp, cases x, simp_all)
-next
- case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
-next
- case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
-next
- case goal5 thus ?case by(simp add: Top_option_def)
-next
- case goal6 thus ?case by(simp add: L_option_def split: option.splits)
-qed
+lemma st_cons[simp]: "fun_rep ((x,y) # ps) = (fun_rep ps) (x := y)"
+by(auto simp: fun_rep_def fun_eq_iff split: option.splits if_splits)
-end
-
-
-subsection "Abstract State with Computable Ordering"
-
-hide_type st --"to avoid long names"
-
-text{* A concrete type of state with computable @{text"\<le>"}: *}
-
-fun st :: "(vname \<Rightarrow> 'a) * vname set \<Rightarrow> bool" where
-"st (f,X) = (\<forall>x. x \<notin> X \<longrightarrow> f x = undefined)"
+lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st" is "\<lambda>ps x a. (x,a)#ps"
+by(auto simp: eq_st_def)
-typedef 'a st = "{p :: (vname \<Rightarrow> 'a) * vname set. st p}"
-proof
- show "(\<lambda>x. undefined,{}) \<in> {p. st p}" by simp
-qed
-
-setup_lifting type_definition_st
-
-lift_definition St :: "(vname \<Rightarrow> 'a) \<Rightarrow> vname set \<Rightarrow> 'a st" is
- "\<lambda>f X. (\<lambda>x. if x \<in> X then f x else undefined, X)"
-by(simp)
-
-lift_definition update :: "'a st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st" is
- "\<lambda>(f,X) x a. (f(x := a), insert x X)"
-by(auto)
+lift_definition "fun" :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
+by(simp add: eq_st_def)
-lift_definition "fun" :: "'a st \<Rightarrow> vname \<Rightarrow> 'a" is fst ..
-
-lift_definition dom :: "'a st \<Rightarrow> vname set" is snd ..
-
-lemma dom_St[simp]: "dom(St f X) = X"
-by(simp add: St.rep_eq dom.rep_eq)
+definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
+"show_st X S = (\<lambda>x. (x, fun S x)) ` X"
-lemma fun_St[simp]: "fun(St f X) = (\<lambda>x. if x \<in> X then f x else undefined)"
-by(simp add: St.rep_eq fun.rep_eq)
-
-definition show_st :: "'a st \<Rightarrow> (vname * 'a)set" where
-"show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
-
-definition "show_acom = map_acom (Option.map show_st)"
+definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
definition "show_acom_opt = Option.map show_acom"
lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
by transfer auto
-lemma dom_update[simp]: "dom (update S x y) = insert x (dom S)"
-by transfer auto
+definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
+"\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
-definition \<gamma>_st :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
-"\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom F. f x \<in> \<gamma>(fun F x)}"
+instantiation st :: ("{order,top}") order
+begin
-lemma ext_st: "dom F = dom G \<Longrightarrow> \<forall>x \<in> dom G. fun F x = fun G x \<Longrightarrow> F=G"
-apply(induct F rule:Abs_st_induct)
-apply(induct G rule:Abs_st_induct)
-apply (auto simp:Abs_st_inject fun_def dom_def Abs_st_inverse simp del: st.simps)
-apply(rule ext)
-apply auto
+definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
+"less_eq_st_rep ps1 ps2 =
+ ((\<forall>x \<in> set(map fst ps1) \<union> set(map fst ps2). fun_rep ps1 x \<le> fun_rep ps2 x))"
+
+lemma less_eq_st_rep_iff: "less_eq_st_rep r1 r2 = (\<forall>x. fun_rep r1 x \<le> fun_rep r2 x)"
+apply(auto simp: less_eq_st_rep_def fun_rep_def split: option.split)
+apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
+apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
done
-instantiation st :: (order) order
-begin
+corollary less_eq_st_rep_iff_fun: "less_eq_st_rep r1 r2 = (fun_rep r1 \<le> fun_rep r2)"
+by (metis less_eq_st_rep_iff le_fun_def)
-definition less_eq_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
-"F \<le> (G::'a st) = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<le> fun G x))"
+lift_definition less_eq_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" is less_eq_st_rep
+by(auto simp add: eq_st_def less_eq_st_rep_iff)
definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
@@ -138,61 +61,64 @@
proof
case goal1 show ?case by(rule less_st_def)
next
- case goal2 show ?case by(auto simp: less_eq_st_def)
+ case goal2 show ?case by transfer (auto simp: less_eq_st_rep_def)
next
- case goal3 thus ?case by(fastforce simp: less_eq_st_def)
+ case goal3 thus ?case
+ by transfer (metis less_eq_st_rep_iff order_trans)
next
- case goal4 thus ?case by (metis less_eq_st_def antisym ext_st)
+ case goal4 thus ?case
+ by transfer (metis less_eq_st_rep_iff eq_st_def fun_eq_iff antisym)
qed
end
-instantiation st :: (sup) sup
+lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
+by transfer (rule less_eq_st_rep_iff)
+
+fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
+"map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
+"map2_st_rep f ((x,y)#ps1) ps2 =
+ (let y2 = (case map_of ps2 x of Some y2 \<Rightarrow> y2 | None \<Rightarrow> \<top>)
+ in (x,f y y2) # map2_st_rep f ps1 ps2)"
+
+lemma fun_rep_map2_rep[simp]:
+ "f \<top> \<top> = \<top> \<Longrightarrow> fun_rep (map2_st_rep f ps1 ps2) = (\<lambda>x. f (fun_rep ps1 x) (fun_rep ps2 x))"
+apply(induction f ps1 ps2 rule: map2_st_rep.induct)
+apply(simp add: fun_rep_def map_of_map fun_eq_iff split: option.split)
+apply(fastforce simp: fun_rep_def fun_eq_iff split:option.splits)
+done
+
+instantiation st :: (semilattice) semilattice
begin
-definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
-"F \<squnion> (G::'a st) = St (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
+lift_definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<squnion>)"
+by (simp add: eq_st_def)
-instance ..
-
-end
+lift_definition top_st :: "'a st" is "[]"
+by(simp add: eq_st_def)
-instantiation st :: (type) L
-begin
-
-definition L_st :: "vname set \<Rightarrow> 'a st set" where
-"L(X::vname set) = {F. dom F = X}"
-
-instance ..
+instance
+proof
+ case goal1 show ?case by transfer (simp add:less_eq_st_rep_iff)
+next
+ case goal2 show ?case by transfer (simp add:less_eq_st_rep_iff)
+next
+ case goal3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
+next
+ case goal4 show ?case by transfer (simp add:less_eq_st_rep_iff fun_rep_def)
+qed
end
-instantiation st :: (semilattice) semilatticeL
-begin
-
-definition Top_st :: "vname set \<Rightarrow> 'a st" where "Top(X) = St (\<lambda>x. \<top>) X"
-
-instance
-proof qed(auto simp add: less_eq_st_def sup_st_def Top_st_def L_st_def)
-
-end
-
-
-text{* Trick to make code generator happy. *}
-lemma [code]: "L = (L :: _ \<Rightarrow> _ st set)"
-by(rule refl)
-(* L is not used in the code but is part of a type class that is used.
- Hence the code generator wants to build a dictionary with L in it.
- But L is not executable. This looping defn makes it look as if it were. *)
-
-
-lemma mono_fun: "F \<le> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<le> fun G x"
-by(auto simp: less_eq_st_def)
+lemma fun_top: "fun \<top> = (\<lambda>x. \<top>)"
+by transfer (simp add: fun_rep_def)
lemma mono_update[simp]:
"a1 \<le> a2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> update S1 x a1 \<le> update S2 x a2"
-by(auto simp add: less_eq_st_def)
+by transfer (auto simp add: less_eq_st_rep_def)
+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> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
begin
@@ -206,15 +132,14 @@
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
-lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (Top X) = UNIV"
-by(auto simp: Top_st_def \<gamma>_st_def)
+lemma gamma_s_top[simp]: "\<gamma>\<^isub>s \<top> = UNIV"
+by(auto simp: \<gamma>_st_def fun_top)
-lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (Top X) = UNIV"
-by (simp add: Top_option_def)
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o \<top> = UNIV"
+by (simp add: top_option_def)
lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
-apply(simp add:\<gamma>_st_def subset_iff less_eq_st_def split: if_splits)
-by (metis mono_gamma subsetD)
+by(simp add:\<gamma>_st_def le_st_iff subset_iff) (metis mono_gamma subsetD)
lemma mono_gamma_o:
"S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"