major redesign: order instead of preorder, new definition of intervals as quotients
--- a/src/HOL/IMP/Abs_Int0.thy Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Mar 06 16:10:56 2013 +0100
@@ -6,52 +6,26 @@
subsection "Orderings"
-class preord =
-fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
-assumes le_refl[simp]: "x \<sqsubseteq> x"
-and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-begin
-
-definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
-
-declare le_trans[trans]
+notation
+ Orderings.bot ("\<bottom>") and
+ Orderings.top ("\<top>")
-end
+declare order_trans[trans]
-text{* Note: no antisymmetry. Allows implementations where some abstract
-element is implemented by two different values @{prop "x \<noteq> y"}
-such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
-needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
-*}
-
-class join = preord +
+class join = order +
fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
-class semilattice = join +
-fixes Top :: "'a" ("\<top>")
-assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
-and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
-and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<sqsubseteq> \<top>"
+class semilattice = join + top +
+assumes join_ge1 [simp]: "x \<le> x \<squnion> y"
+and join_ge2 [simp]: "y \<le> x \<squnion> y"
+and join_least: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
begin
-lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-by (metis join_ge1 join_ge2 join_least le_trans)
-
-lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
-by (metis join_ge1 join_ge2 le_trans)
-
-end
+lemma join_le_iff[simp]: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
+by (metis join_ge1 join_ge2 join_least order_trans)
-instantiation "fun" :: (type, preord) preord
-begin
-
-definition "f \<sqsubseteq> g = (\<forall>x. f x \<sqsubseteq> g x)"
-
-instance
-proof
- case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
-qed (simp_all add: le_fun_def)
+lemma le_join_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
+by (metis join_ge1 join_ge2 order_trans)
end
@@ -60,81 +34,41 @@
begin
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
-definition "\<top> = (\<lambda>x. \<top>)"
lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
by (simp add: join_fun_def)
instance
proof
-qed (simp_all add: le_fun_def Top_fun_def)
+qed (simp_all add: le_fun_def)
end
-instantiation acom :: (preord) preord
+instantiation option :: (order)order
begin
-fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
-"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
-"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
-"le_acom (C1;C2) (D1;D2) = (C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)" |
-"le_acom (IF b THEN {p1} C1 ELSE {p2} C2 {S}) (IF b' THEN {q1} D1 ELSE {q2} D2 {S'}) =
- (b=b' \<and> p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" |
-"le_acom ({I} WHILE b DO {p} C {P}) ({I'} WHILE b' DO {p'} C' {P'}) =
- (b=b' \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')" |
-"le_acom _ _ = False"
-
-lemma [simp]: "SKIP {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = SKIP {S'} \<and> S \<sqsubseteq> S')"
-by (cases C) auto
-
-lemma [simp]: "x ::= e {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = x ::= e {S'} \<and> S \<sqsubseteq> S')"
-by (cases C) auto
-
-lemma [simp]: "C1;C2 \<sqsubseteq> C \<longleftrightarrow> (\<exists>D1 D2. C = D1;D2 \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)"
-by (cases C) auto
-
-lemma [simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<sqsubseteq> C \<longleftrightarrow>
- (\<exists>q1 q2 D1 D2 S'. C = IF b THEN {q1} D1 ELSE {q2} D2 {S'} \<and>
- p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')"
-by (cases C) auto
+fun less_eq_option where
+"Some x \<le> Some y = (x \<le> y)" |
+"None \<le> y = True" |
+"Some _ \<le> None = False"
-lemma [simp]: "{I} WHILE b DO {p} C {P} \<sqsubseteq> W \<longleftrightarrow>
- (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')"
-by (cases W) auto
+definition less_option where "x < (y::'a option) = (x \<le> y \<and> \<not> y \<le> x)"
-instance
-proof
- case goal1 thus ?case by (induct x) auto
-next
- case goal2 thus ?case
- apply(induct x y arbitrary: z rule: le_acom.induct)
- apply (auto intro: le_trans)
- done
-qed
-
-end
-
-
-instantiation option :: (preord)preord
-begin
-
-fun le_option where
-"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" |
-"None \<sqsubseteq> y = True" |
-"Some _ \<sqsubseteq> None = False"
-
-lemma [simp]: "(x \<sqsubseteq> None) = (x = None)"
+lemma [simp]: "(x \<le> None) = (x = None)"
by (cases x) simp_all
-lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y \<and> x \<sqsubseteq> y)"
+lemma [simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
by (cases u) auto
instance proof
- case goal1 show ?case by(cases x, simp_all)
+ case goal1 show ?case by(rule less_option_def)
+next
+ case goal2 show ?case by(cases x, simp_all)
next
- case goal2 thus ?case
- by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
+ case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, auto)
+next
+ case goal4 thus ?case by(cases y, simp, cases x, auto)
qed
end
@@ -157,25 +91,21 @@
instantiation option :: (semilattice)semilattice
begin
-definition "\<top> = Some \<top>"
+definition top_option where "\<top> = Some \<top>"
instance proof
- case goal1 thus ?case by(cases x, simp, cases y, simp_all)
+ case goal1 show ?case by(cases a, simp_all add: top_option_def)
next
- case goal2 thus ?case by(cases y, simp, cases x, simp_all)
+ case goal2 thus ?case by(cases x, simp, cases y, simp_all)
next
- case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+ case goal3 thus ?case by(cases y, simp, cases x, simp_all)
next
- case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
+ case goal4 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
qed
end
-class bot = preord +
-fixes bot :: "'a" ("\<bottom>")
-assumes bot[simp]: "\<bottom> \<sqsubseteq> x"
-
-instantiation option :: (preord)bot
+instantiation option :: (order)bot
begin
definition bot_option :: "'a option" where
@@ -192,7 +122,7 @@
definition bot :: "com \<Rightarrow> 'a option acom" where
"bot c = anno None c"
-lemma bot_least: "strip C = c \<Longrightarrow> bot c \<sqsubseteq> C"
+lemma bot_least: "strip C = c \<Longrightarrow> bot c \<le> C"
by(induct C arbitrary: c)(auto simp: bot_def)
lemma strip_bot[simp]: "strip(bot c) = c"
@@ -201,20 +131,21 @@
subsubsection "Post-fixed point iteration"
-definition pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
-"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f"
+definition pfp :: "(('a::order) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
+"pfp f = while_option (\<lambda>x. \<not> f x \<le> x) f"
-lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x"
+lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<le> x"
using while_option_stop[OF assms[simplified pfp_def]] by simp
lemma while_least:
-assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L"
-and "\<forall>x \<in> L. b \<sqsubseteq> x" and "b \<in> L" and "f q \<sqsubseteq> q" and "q \<in> L"
+fixes q :: "'a::order"
+assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<le> y \<longrightarrow> f x \<le> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L"
+and "\<forall>x \<in> L. b \<le> x" and "b \<in> L" and "f q \<le> q" and "q \<in> L"
and "while_option P f b = Some p"
-shows "p \<sqsubseteq> q"
+shows "p \<le> q"
using while_option_rule[OF _ assms(7)[unfolded pfp_def],
- where P = "%x. x \<in> L \<and> x \<sqsubseteq> q"]
-by (metis assms(1-6) le_trans)
+ where P = "%x. x \<in> L \<and> x \<le> q"]
+by (metis assms(1-6) order_trans)
lemma pfp_inv:
"pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
@@ -238,7 +169,7 @@
locale Val_abs =
fixes \<gamma> :: "'av::semilattice \<Rightarrow> val set"
- assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
+ assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'av"
and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
@@ -284,21 +215,21 @@
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 = UNIV"
-by(simp add: Top_fun_def \<gamma>_fun_def)
+lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s \<top> = UNIV"
+by(simp add: top_fun_def \<gamma>_fun_def)
-lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = 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: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
+lemma mono_gamma_s: "f1 \<le> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
lemma mono_gamma_o:
- "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
+ "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
+by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
-lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
+lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
+by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
text{* Soundness: *}
@@ -326,7 +257,7 @@
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>) (bot c) = Some C"
- have pfp': "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+ 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>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
@@ -343,21 +274,21 @@
subsubsection "Monotonicity"
-lemma mono_post: "C1 \<sqsubseteq> C2 \<Longrightarrow> post C1 \<sqsubseteq> post C2"
-by(induction C1 C2 rule: le_acom.induct) (auto)
+lemma mono_post: "C1 \<le> C2 \<Longrightarrow> post C1 \<le> post C2"
+by(induction C1 C2 rule: less_eq_acom.induct) (auto)
locale Abs_Int_Fun_mono = Abs_Int_Fun +
-assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
begin
-lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+lemma mono_aval': "S \<le> S' \<Longrightarrow> aval' e S \<le> aval' e S'"
by(induction e)(auto simp: le_fun_def mono_plus')
-lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
+lemma mono_update: "a \<le> a' \<Longrightarrow> S \<le> S' \<Longrightarrow> S(x := a) \<le> S'(x := a')"
by(simp add: le_fun_def)
-lemma mono_step': "S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
split: option.split)
done
--- a/src/HOL/IMP/Abs_Int1.thy Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Mar 06 16:10:56 2013 +0100
@@ -4,16 +4,16 @@
imports Abs_State
begin
-lemma le_iff_le_annos_zip: "C1 \<sqsubseteq> C2 \<longleftrightarrow>
- (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<sqsubseteq> a2) \<and> strip C1 = strip C2"
-by(induct C1 C2 rule: le_acom.induct) (auto simp: size_annos_same2)
+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)
-lemma le_iff_le_annos: "C1 \<sqsubseteq> C2 \<longleftrightarrow>
- strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<sqsubseteq> annos C2 ! i)"
+lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
+ 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 \<sqsubseteq> G \<Longrightarrow> x : X \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
+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)"
@@ -71,7 +71,7 @@
{S \<squnion> post C} WHILE b DO {I} step' P C {I}"
definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' (top(vars c))) (bot c)"
+"AI c = pfp (step' (Top(vars c))) (bot c)"
lemma strip_step'[simp]: "strip(step' S C) = strip C"
@@ -94,7 +94,7 @@
case Seq thus ?case by auto
next
case (If b p1 C1 p2 C2 P)
- hence "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
+ hence "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
by(simp, metis post_in_L join_ge1 join_ge2)
thus ?case using If by (auto simp: mono_gamma_o)
next
@@ -105,26 +105,26 @@
"\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> (step' S C) \<in> L X"
proof(induction C arbitrary: S)
case Assign thus ?case
- by(auto simp: L_st_def update_def split: option.splits)
+ by(auto simp: L_st_def split: option.splits)
qed auto
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"
+ 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 \<sqsubseteq> 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"
+ (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"
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"
+ 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'])
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 "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])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -134,41 +134,41 @@
subsubsection "Monotonicity"
lemma le_join_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow>
- x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
-by (metis join_ge1 join_ge2 preord_class.le_trans)
+ x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
+by (metis join_ge1 join_ge2 order_trans)
locale Abs_Int_mono = Abs_Int +
-assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
begin
lemma mono_aval':
- "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
-by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
+ "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)
theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
- S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+ S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
apply (auto simp: Let_def mono_aval' mono_post
le_join_disj le_join_disj[OF post_in_L post_in_L]
split: option.split)
done
lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
- C \<sqsubseteq> C' \<Longrightarrow> step' (top X) C \<sqsubseteq> step' (top X) C'"
-by (metis top_in_L mono_step' preord_class.le_refl)
+ C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'"
+by (metis Top_in_L 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 \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
+ 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' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
-shows "C \<sqsubseteq> C'"
+and "f C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
+shows "C \<le> C'"
apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
by (simp_all add: assms(4,5) bot_least)
lemma AI_least_pfp: assumes "AI c = Some C"
-and "step' (top(vars c)) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
-shows "C \<sqsubseteq> C'"
+and "step' (Top(vars c)) C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)"
+shows "C \<le> C'"
apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
by (simp_all add: mono_step'_top)
@@ -177,30 +177,27 @@
subsubsection "Termination"
-abbreviation sqless (infix "\<sqsubset>" 50) where
-"x \<sqsubset> y == x \<sqsubseteq> y \<and> \<not> y \<sqsubseteq> x"
-
lemma pfp_termination:
-fixes x0 :: "'a::preord" and m :: "'a \<Rightarrow> nat"
-assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> m x > m y"
-and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<sqsubseteq> f x0"
+fixes x0 :: "'a::order" and m :: "'a \<Rightarrow> nat"
+assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x < y \<Longrightarrow> m x > m y"
+and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<le> f x0"
shows "\<exists>x. pfp f x0 = Some x"
-proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<sqsubseteq> f x"])
- show "wf {(y,x). ((I x \<and> x \<sqsubseteq> f x) \<and> \<not> f x \<sqsubseteq> x) \<and> y = f x}"
+proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<le> f x"])
+ show "wf {(y,x). ((I x \<and> x \<le> f x) \<and> \<not> f x \<le> x) \<and> y = f x}"
by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
next
- show "I x0 \<and> x0 \<sqsubseteq> f x0" using `I x0` `x0 \<sqsubseteq> f x0` by blast
+ show "I x0 \<and> x0 \<le> f x0" using `I x0` `x0 \<le> f x0` by blast
next
- fix x assume "I x \<and> x \<sqsubseteq> f x" thus "I(f x) \<and> f x \<sqsubseteq> f(f x)"
+ fix x assume "I x \<and> x \<le> f x" thus "I(f x) \<and> f x \<le> f(f x)"
by (blast intro: I mono)
qed
locale Measure1 =
-fixes m :: "'av::preord \<Rightarrow> nat"
+fixes m :: "'av::order \<Rightarrow> nat"
fixes h :: "nat"
-assumes m1: "x \<sqsubseteq> y \<Longrightarrow> m x \<ge> m y"
+assumes m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
assumes h: "m x \<le> h"
begin
@@ -211,9 +208,9 @@
by(simp add: L_st_def m_s_def)
(metis nat_mult_commute of_nat_id setsum_bounded[OF h])
-lemma m_s1: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
-proof(auto simp add: le_st_def m_s_def)
- assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
+lemma m_s1: "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 m1)
thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
by (metis setsum_mono)
@@ -226,8 +223,8 @@
by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h)
lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
- o1 \<sqsubseteq> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
-proof(induction o1 o2 rule: le_option.induct)
+ o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
+proof(induction o1 o2 rule: less_eq_option.induct)
case 1 thus ?case by (simp add: m_o_def)(metis m_s1)
next
case 2 thus ?case
@@ -257,46 +254,45 @@
end
locale Measure = Measure1 +
-assumes m2: "x \<sqsubset> y \<Longrightarrow> m x > m y"
+assumes m2: "x < y \<Longrightarrow> m x > m y"
begin
-lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 \<sqsubset> S2 \<Longrightarrow> m_s S1 > m_s S2"
-proof(auto simp add: le_st_def m_s_def)
- assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
+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 \<sqsubseteq> fun S1 x"
- hence 2: "\<exists>x\<in>dom S2. m(fun S1 x) > m(fun S2 x)" using 0 m2 by blast
+ 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))" .
qed
lemma m_o2: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
- o1 \<sqsubset> o2 \<Longrightarrow> m_o (card X) o1 > m_o (card X) o2"
-proof(induction o1 o2 rule: le_option.induct)
- case 1 thus ?case by (simp add: m_o_def L_st_def m_s2)
+ o1 < o2 \<Longrightarrow> m_o (card X) o1 > m_o (card 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)
next
- case 2 thus ?case
- by(auto simp add: m_o_def le_imp_less_Suc m_s_h)
+ 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 simp
+ case 3 thus ?case by (auto simp: less_option_def)
qed
-
+find_theorems "(_<_) = _"
lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow>
- C1 \<sqsubset> 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] L_acom_def)
+ 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)
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 \<sqsubseteq> annos C2 ! i"
+ 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 \<sqsubseteq> annos C1 ! i"
+ 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)
+ by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0 less_option_def)
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))"
@@ -312,8 +308,7 @@
lemma AI_Some_measure: "\<exists>C. AI c = Some C"
unfolding AI_def
-apply(rule pfp_termination[where I = "%C. strip C = c \<and> C \<in> L(vars c)"
- and m="m_c"])
+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)
done
--- a/src/HOL/IMP/Abs_Int1_const.thy Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Mar 06 16:10:56 2013 +0100
@@ -23,10 +23,12 @@
instantiation const :: semilattice
begin
-fun le_const where
-"_ \<sqsubseteq> Any = True" |
-"Const n \<sqsubseteq> Const m = (n=m)" |
-"Any \<sqsubseteq> Const _ = False"
+fun less_eq_const where
+"_ \<le> Any = True" |
+"Const n \<le> Const m = (n=m)" |
+"Any \<le> Const _ = False"
+
+definition "a < (b::const) = (a \<le> b & ~ b \<le> a)"
fun join_const where
"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
@@ -36,17 +38,21 @@
instance
proof
- case goal1 thus ?case by (cases x) simp_all
+ case goal1 thus ?case by (rule less_const_def)
+next
+ case goal2 show ?case by (cases x) simp_all
next
- case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
+ case goal3 thus ?case by(cases z, cases y, cases x, simp_all)
next
- case goal3 thus ?case by(cases x, cases y, simp_all)
+ case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
next
- case goal4 thus ?case by(cases y, cases x, simp_all)
+ case goal6 thus ?case by(cases x, cases y, simp_all)
+next
+ case goal7 thus ?case by(cases y, cases x, simp_all)
next
- case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
+ case goal8 thus ?case by(cases z, cases y, cases x, simp_all)
next
- case goal6 thus ?case by(simp add: Top_const_def)
+ case goal5 thus ?case by(simp add: top_const_def)
qed
end
@@ -58,7 +64,7 @@
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
next
- case goal2 show ?case by(simp add: Top_const_def)
+ case goal2 show ?case by(simp add: top_const_def)
next
case goal3 show ?case by simp
next
@@ -74,7 +80,7 @@
subsubsection "Tests"
-definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)"
+definition "steps c i = (step_const(Top(vars c)) ^^ i) (bot c)"
value "show_acom (steps test1_const 0)"
value "show_acom (steps test1_const 1)"
@@ -139,7 +145,7 @@
next
case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
next
- case goal3 thus ?case by(auto simp: m_const_def split: const.splits)
+ case goal3 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
qed
thm AI_Some_measure
--- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Mar 06 16:10:56 2013 +0100
@@ -1,3 +1,5 @@
+(* Author: Tobias Nipkow *)
+
theory Abs_Int1_parity
imports Abs_Int1
begin
@@ -6,29 +8,41 @@
datatype parity = Even | Odd | Either
-text{* Instantiation of class @{class preord} with type @{typ parity}: *}
+text{* Instantiation of class @{class order} with type @{typ parity}: *}
-instantiation parity :: preord
+instantiation parity :: order
begin
-text{* First the definition of the interface function @{text"\<sqsubseteq>"}. Note that
-the header of the definition must refer to the ascii name @{const le} of the
-constants as @{text le_parity} and the definition is named @{text
-le_parity_def}. Inside the definition the symbolic names can be used. *}
+text{* First the definition of the interface function @{text"\<le>"}. Note that
+the header of the definition must refer to the ascii name @{const less_eq} of the
+constants as @{text less_eq_parity} and the definition is named @{text
+less_eq_parity_def}. Inside the definition the symbolic names can be used. *}
+
+definition less_eq_parity where
+"x \<le> y = (y = Either \<or> x=y)"
-definition le_parity where
-"x \<sqsubseteq> y = (y = Either \<or> x=y)"
+text{* We also need @{text"<"}, which is defined canonically: *}
-text{* Now the instance proof, i.e.\ the proof that the definition fulfills
+definition less_parity where
+"x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))"
+
+text{*\noindent (The type annotation is necessary to fix the type of the polymorphic predicates.)
+
+Now the instance proof, i.e.\ the proof that the definition fulfills
the axioms (assumptions) of the class. The initial proof-step generates the
necessary proof obligations. *}
instance
proof
- fix x::parity show "x \<sqsubseteq> x" by(auto simp: le_parity_def)
+ fix x::parity show "x \<le> x" by(auto simp: less_eq_parity_def)
+next
+ fix x y z :: parity assume "x \<le> y" "y \<le> z" thus "x \<le> z"
+ by(auto simp: less_eq_parity_def)
next
- fix x y z :: parity assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- by(auto simp: le_parity_def)
+ fix x y :: parity assume "x \<le> y" "y \<le> x" thus "x = y"
+ by(auto simp: less_eq_parity_def)
+next
+ fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def)
qed
end
@@ -39,9 +53,9 @@
begin
definition join_parity where
-"x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)"
+"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)"
-definition Top_parity where
+definition top_parity where
"\<top> = Either"
text{* Now the instance proof. This time we take a lazy shortcut: we do not
@@ -52,13 +66,13 @@
instance
proof
- case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def)
+ case goal1 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
next
- case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def)
+ case goal2 (*join1*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
next
- case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def)
+ case goal3 (*join2*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
next
- case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def)
+ case goal4 (*join least*) thus ?case by(auto simp: less_eq_parity_def join_parity_def)
qed
end
@@ -92,10 +106,10 @@
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof txt{* of the locale axioms *}
fix a b :: parity
- assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
- by(auto simp: le_parity_def)
+ assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
+ by(auto simp: less_eq_parity_def)
next txt{* The rest in the lazy, implicit way *}
- case goal2 show ?case by(auto simp: Top_parity_def)
+ case goal2 show ?case by(auto simp: top_parity_def)
next
case goal3 show ?case by auto
next
@@ -127,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(vars c)) ^^ i) (bot c)"
value "show_acom (steps test2_parity 0)"
value "show_acom (steps test2_parity 1)"
@@ -147,7 +161,7 @@
case goal1 thus ?case
proof(cases a1 a2 b1 b2
rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
- qed (auto simp add:le_parity_def)
+ qed (auto simp add:less_eq_parity_def)
qed
definition m_parity :: "parity \<Rightarrow> nat" where
@@ -157,11 +171,11 @@
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
and m = m_parity and h = "1"
proof
- case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
+ case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
next
- case goal2 thus ?case by(auto simp add: m_parity_def le_parity_def)
+ case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
next
- case goal3 thus ?case by(auto simp add: m_parity_def le_parity_def)
+ case goal3 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
qed
thm AI_Some_measure
--- a/src/HOL/IMP/Abs_Int2.thy Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Wed Mar 06 16:10:56 2013 +0100
@@ -4,16 +4,21 @@
imports Abs_Int1
begin
-instantiation prod :: (preord,preord) preord
+instantiation prod :: (order,order) order
begin
-definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
+definition "less_eq_prod p1 p2 = (fst p1 \<le> fst p2 \<and> snd p1 \<le> snd p2)"
+definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
instance
proof
- case goal1 show ?case by(simp add: le_prod_def)
+ case goal1 show ?case by(rule less_prod_def)
+next
+ case goal2 show ?case by(simp add: less_eq_prod_def)
next
- case goal2 thus ?case unfolding le_prod_def by(metis le_trans)
+ case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
+next
+ case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
qed
end
@@ -23,13 +28,13 @@
class lattice = semilattice + bot +
fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
-assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
-and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
-and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+assumes meet_le1 [simp]: "x \<sqinter> y \<le> x"
+and meet_le2 [simp]: "x \<sqinter> y \<le> y"
+and meet_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
begin
-lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
-by (metis meet_greatest meet_le1 meet_le2 le_trans)
+lemma mono_meet: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> x \<sqinter> y \<le> x' \<sqinter> y'"
+by (metis meet_greatest meet_le1 meet_le2 order_trans)
end
@@ -83,7 +88,7 @@
"afilter (N n) a S = (if test_num' n a then S else None)" |
"afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
let a' = fun S x \<sqinter> a in
- if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
+ if a' = \<bottom> then None else Some(update S x a'))" |
"afilter (Plus e1 e2) a S =
(let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
in afilter e1 a1 (afilter e2 a2 S))"
@@ -110,8 +115,7 @@
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 update_def L_st_def
- split: option.splits prod.split)
+ (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)"
@@ -189,7 +193,7 @@
case Seq thus ?case by auto
next
case (If b _ C1 _ C2)
- hence 0: "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
+ hence 0: "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
by(simp, metis post_in_L join_ge1 join_ge2)
have "vars b \<subseteq> X" using If.prems by simp
note vars = `S \<in> L X` `vars b \<subseteq> X`
@@ -204,26 +208,26 @@
lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
proof(induction C arbitrary: S)
- case Assign thus ?case by(simp add: L_option_def L_st_def update_def split: option.splits)
+ case Assign thus ?case by(auto simp add: L_option_def L_st_def split: option.splits)
qed (auto simp add: bfilter_in_L)
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"
+ 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 \<sqsubseteq> 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"
+ (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"
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"
+ 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'])
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 "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])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -233,19 +237,19 @@
subsubsection "Monotonicity"
locale Abs_Int1_mono = Abs_Int1 +
-assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
-and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
- filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
-and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
- filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
+assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
+and mono_filter_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
+ filter_plus' r a1 a2 \<le> filter_plus' r' b1 b2"
+and mono_filter_less': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow>
+ filter_less' bv a1 a2 \<le> filter_less' bv b1 b2"
begin
lemma mono_aval':
- "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
-by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
+ "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)
lemma mono_aval'':
- "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<sqsubseteq> aval'' e S2"
+ "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
apply(cases S1)
apply simp
apply(cases S2)
@@ -253,37 +257,37 @@
by (simp add: mono_aval')
lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
- r1 \<sqsubseteq> r2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> afilter e r1 S1 \<sqsubseteq> afilter e r2 S2"
+ 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 mono_meet split: option.splits prod.splits)
apply (metis mono_gamma subsetD)
apply(drule (2) mono_fun_L)
-apply (metis mono_meet le_trans)
-apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)
+apply (metis mono_meet le_bot)
+apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
done
lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
- S1 \<sqsubseteq> S2 \<Longrightarrow> bfilter b bv S1 \<sqsubseteq> bfilter b bv S2"
+ 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 join_least le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] bfilter_in_L)
+apply(metis join_least order_trans[OF _ join_ge1] order_trans[OF _ join_ge2] bfilter_in_L)
apply (simp split: prod.splits)
-apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_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 afilter_in_L)
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 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+ S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
le_join_disj le_join_disj[OF post_in_L post_in_L] bfilter_in_L
split: option.split)
done
lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
- C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"
-by (metis top_in_L mono_step' preord_class.le_refl)
+ C1 \<le> C2 \<Longrightarrow> step' (Top X) C1 \<le> step' (Top X) C2"
+by (metis Top_in_L mono_step' order_refl)
end
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Mar 06 16:10:56 2013 +0100
@@ -1,297 +1,341 @@
(* Author: Tobias Nipkow *)
theory Abs_Int2_ivl
-imports Abs_Int2
+imports "~~/src/HOL/Library/Quotient_List"
+ "~~/src/HOL/Library/Extended"
+ Abs_Int2
begin
subsection "Interval Analysis"
-datatype lb = Minf | Lb int
-datatype ub = Pinf | Ub int
+type_synonym eint = "int extended"
+type_synonym eint2 = "eint * eint"
-datatype ivl = Ivl lb ub
+definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where
+"\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})"
-definition "\<gamma>_ivl i = (case i of
- Ivl (Lb l) (Ub h) \<Rightarrow> {l..h} |
- Ivl (Lb l) Pinf \<Rightarrow> {l..} |
- Ivl Minf (Ub h) \<Rightarrow> {..h} |
- Ivl Minf Pinf \<Rightarrow> UNIV)"
+definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
+"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)"
-abbreviation Ivl_Lb_Ub :: "int \<Rightarrow> int \<Rightarrow> ivl" ("{_\<dots>_}") where
-"{lo\<dots>hi} == Ivl (Lb lo) (Ub hi)"
-abbreviation Ivl_Lb_Pinf :: "int \<Rightarrow> ivl" ("{_\<dots>}") where
-"{lo\<dots>} == Ivl (Lb lo) Pinf"
-abbreviation Ivl_Minf_Ub :: "int \<Rightarrow> ivl" ("{\<dots>_}") where
-"{\<dots>hi} == Ivl Minf (Ub hi)"
-abbreviation Ivl_Minf_Pinf :: "ivl" ("{\<dots>}") where
-"{\<dots>} == Ivl Minf Pinf"
+lemma refl_eq_ivl[simp]: "eq_ivl p p"
+by(auto simp: eq_ivl_def)
-lemmas lub_splits = lb.splits ub.splits
-
-definition "num_ivl n = {n\<dots>n}"
+quotient_type ivl = eint2 / eq_ivl
+by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
-fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
-"in_ivl k (Ivl (Lb l) (Ub h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
-"in_ivl k (Ivl (Lb l) Pinf) \<longleftrightarrow> l \<le> k" |
-"in_ivl k (Ivl Minf (Ub h)) \<longleftrightarrow> k \<le> h" |
-"in_ivl k (Ivl Minf Pinf) \<longleftrightarrow> True"
+lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
+by(simp add: eq_ivl_def)
-
-instantiation lb :: linorder
-begin
+abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where
+"[l\<dots>h] == abs_ivl(l,h)"
-definition less_eq_lb where
-"l1 \<le> l2 = (case l1 of Minf \<Rightarrow> True | Lb i1 \<Rightarrow> (case l2 of Minf \<Rightarrow> False | Lb i2 \<Rightarrow> i1 \<le> i2))"
+lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
+by(auto simp: eq_ivl_def)
-definition less_lb :: "lb \<Rightarrow> lb \<Rightarrow> bool" where
-"((l1::lb) < l2) = (l1 \<le> l2 & ~ l1 \<ge> l2)"
+fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where
+"in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h"
-instance
-proof
- case goal1 show ?case by(rule less_lb_def)
-next
- case goal2 show ?case by(auto simp: less_eq_lb_def split:lub_splits)
-next
- case goal3 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
-next
- case goal4 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
-next
- case goal5 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
-qed
+lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep
+by(auto simp: eq_ivl_def \<gamma>_rep_def)
+
+definition is_empty_rep :: "eint2 \<Rightarrow> bool" where
+"is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)"
-end
-
-instantiation ub :: linorder
-begin
+lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} |
+ (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})"
+by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits)
-definition less_eq_ub where
-"u1 \<le> u2 = (case u2 of Pinf \<Rightarrow> True | Ub i2 \<Rightarrow> (case u1 of Pinf \<Rightarrow> False | Ub i1 \<Rightarrow> i1 \<le> i2))"
-
-definition less_ub :: "ub \<Rightarrow> ub \<Rightarrow> bool" where
-"((u1::ub) < u2) = (u1 \<le> u2 & ~ u1 \<ge> u2)"
+lift_definition is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
+apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
+apply(auto simp: not_less less_eq_extended_cases split: extended.splits)
+done
-instance
-proof
- case goal1 show ?case by(rule less_ub_def)
-next
- case goal2 show ?case by(auto simp: less_eq_ub_def split:lub_splits)
-next
- case goal3 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
-next
- case goal4 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
-next
- case goal5 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
-qed
+lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"
+by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits)
-end
+definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
-lemmas le_lub_defs = less_eq_lb_def less_eq_ub_def
+lift_definition empty_ivl :: ivl is empty_rep
+by simp
-lemma le_lub_simps[simp]:
- "Minf \<le> l" "Lb i \<le> Lb j = (i \<le> j)" "~ Lb i \<le> Minf"
- "h \<le> Pinf" "Ub i \<le> Ub j = (i \<le> j)" "~ Pinf \<le> Ub j"
-by(auto simp: le_lub_defs split: lub_splits)
-
-definition empty where "empty = {1\<dots>0}"
+lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
+by(auto simp add: is_empty_rep_def empty_rep_def)
-fun is_empty where
-"is_empty {l\<dots>h} = (h<l)" |
-"is_empty _ = False"
+lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})"
+by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits)
-lemma [simp]: "is_empty(Ivl l h) =
- (case l of Lb l \<Rightarrow> (case h of Ub h \<Rightarrow> h<l | Pinf \<Rightarrow> False) | Minf \<Rightarrow> False)"
-by(auto split: lub_splits)
-
-lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
-by(auto simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
+declare is_empty_rep_iff[THEN iffD1, simp]
instantiation ivl :: semilattice
begin
-fun le_aux where
-"le_aux (Ivl l1 h1) (Ivl l2 h2) = (l2 \<le> l1 & h1 \<le> h2)"
+definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
+"le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in
+ if is_empty_rep(l1,h1) then True else
+ if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)"
+
+lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2"
+apply rule
+apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1]
+apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def)
+apply(auto simp: not_less split: extended.splits)
+done
+
+lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep
+by(auto simp: eq_ivl_def le_iff_subset)
-definition le_ivl where
-"i1 \<sqsubseteq> i2 =
- (if is_empty i1 then True else
- if is_empty i2 then False else le_aux i1 i2)"
+definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))"
+
+definition join_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"join_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
+ else let (l1,h1) = p1; (l2,h2) = p2 in (min l1 l2, max h1 h2))"
-definition "i1 \<squnion> i2 =
- (if is_empty i1 then i2 else if is_empty i2 then i1
- else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (min l1 l2) (max h1 h2))"
+lift_definition join_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is join_rep
+by(auto simp: eq_ivl_iff join_rep_def)
-definition "\<top> = {\<dots>}"
+lift_definition top_ivl :: ivl is "(Minf,Pinf)"
+by(auto simp: eq_ivl_def)
+
+lemma is_empty_min_max:
+ "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
+by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
instance
proof
- case goal1 thus ?case
- by(cases x, simp add: le_ivl_def)
+ case goal1 show ?case by (rule less_ivl_def)
+next
+ case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
next
- case goal2 thus ?case
- by(cases x, cases y, cases z, auto simp: le_ivl_def split: if_splits)
+ case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
next
- case goal3 thus ?case
- by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
+ case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
next
- case goal4 thus ?case
- by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
+ case goal6 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
+next
+ case goal7 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
next
- case goal5 thus ?case
- by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits if_splits)
+ case goal8 thus ?case by transfer (auto simp add: le_rep_def join_rep_def)
next
- case goal6 thus ?case
- by(cases x, simp add: Top_ivl_def le_ivl_def le_lub_defs split: lub_splits)
+ case goal5 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
qed
end
+text{* Implement (naive) executable equality: *}
+instantiation ivl :: equal
+begin
+
+definition equal_ivl where
+"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
+
+instance
+proof
+ case goal1 show ?case by(simp add: equal_ivl_def eq_iff)
+qed
+
+end
+
+lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)"
+by(simp add: not_less)
+lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)"
+by(simp add: not_less)
instantiation ivl :: lattice
begin
-definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
- case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (max l1 l2) (min h1 h2))"
+definition meet_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
-definition "\<bottom> = empty"
+lemma \<gamma>_meet_rep: "\<gamma>_rep(meet_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
+by(auto simp:meet_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
+
+lift_definition meet_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is meet_rep
+by(auto simp: \<gamma>_meet_rep eq_ivl_def)
+
+definition "\<bottom> = empty_ivl"
instance
proof
case goal2 thus ?case
- by (simp add:meet_ivl_def empty_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
+ unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
next
case goal3 thus ?case
- by (simp add: empty_def meet_ivl_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
+ unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
next
case goal4 thus ?case
- by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_lub_defs max_def min_def split: lub_splits if_splits)
+ unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
next
- case goal1 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
+ case goal1 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
qed
end
-instantiation lb :: plus
+lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p"
+by (metis eq_ivl_iff is_empty_empty_rep)
+
+lemma le_ivl_nice: "[l1\<dots>h1] \<le> [l2\<dots>h2] \<longleftrightarrow>
+ (if [l1\<dots>h1] = \<bottom> then True else
+ if [l2\<dots>h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)"
+unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty)
+
+lemma join_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] =
+ (if [l1\<dots>h1] = \<bottom> then [l2\<dots>h2] else
+ if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])"
+unfolding bot_ivl_def by transfer (simp add: join_rep_def eq_ivl_empty)
+
+lemma meet_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
+by transfer (simp add: meet_rep_def)
+
+
+instantiation ivl :: plus
begin
-fun plus_lb where
-"Lb x + Lb y = Lb(x+y)" |
-"_ + _ = Minf"
+definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"plus_rep p1 p2 =
+ (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
+ let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))"
+
+lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep
+by(auto simp: plus_rep_def eq_ivl_iff)
instance ..
end
-instantiation ub :: plus
-begin
-
-fun plus_ub where
-"Ub x + Ub y = Ub(x+y)" |
-"_ + _ = Pinf"
-
-instance ..
-end
-
-instantiation ivl :: plus
-begin
+lemma plus_ivl_nice: "[l1\<dots>h1] + [l2\<dots>h2] =
+ (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then \<bottom> else [l1+l2 \<dots> h1+h2])"
+unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty)
-definition "i1+i2 = (if is_empty i1 | is_empty i2 then empty else
- case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))"
-
-instance ..
-end
+lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf"
+by(cases x) auto
+lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf"
+by(cases x) auto
-fun uminus_ub :: "ub \<Rightarrow> lb" where
-"uminus_ub(Ub( x)) = Lb(-x)" |
-"uminus_ub Pinf = Minf"
-
-fun uminus_lb :: "lb \<Rightarrow> ub" where
-"uminus_lb(Lb( x)) = Ub(-x)" |
-"uminus_lb Minf = Pinf"
+lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)"
+by(cases x) auto
+lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)"
+by(cases x) auto
instantiation ivl :: uminus
begin
-fun uminus_ivl where
-"-(Ivl l h) = Ivl (uminus_ub h) (uminus_lb l)"
-
-instance ..
-end
+definition uminus_rep :: "eint2 \<Rightarrow> eint2" where
+"uminus_rep p = (let (l,h) = p in (-h, -l))"
-instantiation ivl :: minus
-begin
+lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)"
+by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff
+ split: prod.split)
-definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where
-"(i1::ivl) - i2 = i1 + -i2"
+lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep
+by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases)
+ (auto simp: Icc_eq_Icc split: extended.splits)
instance ..
end
-lemma minus_ivl_cases: "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else
- case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))"
-by(auto simp: plus_ivl_def minus_ivl_def split: ivl.split lub_splits)
+lemma uminus_nice: "-[l\<dots>h] = [-h\<dots>-l]"
+by transfer (simp add: uminus_rep_def)
+
+instantiation ivl :: minus
+begin
+definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where "(iv1::ivl) - iv2 = iv1 + -iv2"
+instance ..
+end
+
-lemma gamma_minus_ivl:
- "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(i1 - i2)"
-by(auto simp add: minus_ivl_def plus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits)
+definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where
+"filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))"
+
+definition filter_less_rep :: "bool \<Rightarrow> eint2 \<Rightarrow> eint2 \<Rightarrow> eint2 * eint2" where
+"filter_less_rep res p1 p2 =
+ (if is_empty_rep p1 \<or> is_empty_rep p2 then (empty_rep,empty_rep) else
+ let (l1,h1) = p1; (l2,h2) = p2 in
+ if res
+ then ((l1, min h1 (h2 + Fin -1)), (max (l1 + Fin 1) l2, h2))
+ else ((max l1 l2, h1), (l2, min h1 h2)))"
-definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
- i1 \<sqinter> (i - i2), i2 \<sqinter> (i - i1))"
+lift_definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" is filter_less_rep
+by(auto simp: prod_pred_def filter_less_rep_def eq_ivl_iff)
+declare filter_less_ivl.abs_eq[code] (* bug in lifting *)
+
+lemma filter_less_ivl_nice: "filter_less_ivl b [l1\<dots>h1] [l2\<dots>h2] =
+ (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then (\<bottom>,\<bottom>) else
+ if b
+ then ([l1 \<dots> min h1 (h2 + Fin -1)], [max (l1 + Fin 1) l2 \<dots> h2])
+ else ([max l1 l2 \<dots> h1], [l2 \<dots> min h1 h2]))"
+unfolding prod_rel_eq[symmetric] bot_ivl_def
+by transfer (auto simp: filter_less_rep_def eq_ivl_empty)
-fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
-"filter_less_ivl res (Ivl l1 h1) (Ivl l2 h2) =
- (if is_empty(Ivl l1 h1) \<or> is_empty(Ivl l2 h2) then (empty, empty) else
- if res
- then (Ivl l1 (min h1 (h2 + Ub -1)), Ivl (max (l1 + Lb 1) l2) h2)
- else (Ivl (max l1 l2) h1, Ivl l2 (min h1 h2)))"
+lemma add_mono_le_Fin:
+ "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))"
+by(drule (1) add_mono) simp
+
+lemma add_mono_Fin_le:
+ "\<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
+
+lemma plus_rep_plus:
+ "\<lbrakk> i1 \<in> \<gamma>_rep (l1,h1); i2 \<in> \<gamma>_rep (l2, h2)\<rbrakk> \<Longrightarrow> i1 + i2 \<in> \<gamma>_rep (l1 + l2, h1 + h2)"
+by(simp add: \<gamma>_rep_def add_mono_Fin_le add_mono_le_Fin)
interpretation Val_abs
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
proof
- case goal1 thus ?case
- by(auto simp: \<gamma>_ivl_def le_ivl_def le_lub_defs split: ivl.split lub_splits if_splits)
+ case goal1 thus ?case by transfer (simp add: le_iff_subset)
next
- case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
+ case goal2 show ?case by transfer (simp add: \<gamma>_rep_def)
next
- case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
+ case goal3 show ?case by transfer (simp add: \<gamma>_rep_def)
next
case goal4 thus ?case
- by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split lub_splits)
+ apply transfer
+ apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
+ by(auto simp: empty_rep_def is_empty_rep_def)
qed
+
interpretation Val_abs1_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
defines aval_ivl is aval'
proof
- case goal1 thus ?case
- by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_def max_def split: ivl.split lub_splits)
+ case goal1 show ?case
+ by transfer (auto simp add:meet_rep_def \<gamma>_rep_cases split: prod.split extended.split)
next
- case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
+ case goal2 show ?case unfolding bot_ivl_def by transfer simp
qed
-lemma mono_minus_ivl: fixes i1 :: ivl
-shows "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> i1 - i2 \<sqsubseteq> i1' - i2'"
-apply(auto simp add: minus_ivl_cases empty_def le_ivl_def le_lub_defs split: ivl.splits)
- apply(simp split: lub_splits)
- apply(simp split: lub_splits)
-apply(simp split: lub_splits)
-done
+lemma \<gamma>_plus_rep: "i1 : \<gamma>_rep p1 \<Longrightarrow> i2 : \<gamma>_rep p2 \<Longrightarrow> i1+i2 \<in> \<gamma>_rep(plus_rep p1 p2)"
+by(auto simp: plus_rep_def plus_rep_plus split: prod.splits)
+lemma non_empty_meet: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow>
+ \<not> is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))"
+by (auto simp add: \<gamma>_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv)
+ (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_minus)
+
+lemma filter_plus: "\<lbrakk>eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and>
+ eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2;
+ n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a\<rbrakk>
+ \<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2"
+by (auto simp: eq_ivl_iff \<gamma>_meet_rep non_empty_meet add_ac)
+ (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_def add_commute)+
interpretation Val_abs1
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
proof
- case goal1 thus ?case
- by (simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
+ case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
next
- case goal2 thus ?case
- by(auto simp add: filter_plus_ivl_def)
- (metis gamma_minus_ivl add_diff_cancel add_commute)+
+ case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def prod_rel_eq[symmetric]
+ by transfer (simp add: filter_plus)
next
case goal3 thus ?case
- by(cases a1, cases a2, auto simp: \<gamma>_ivl_def min_def max_def split: if_splits lub_splits)
+ unfolding prod_rel_eq[symmetric]
+ apply transfer
+ apply (auto simp add: filter_less_rep_def eq_ivl_iff max_def min_def split: if_splits)
+ apply(auto simp: \<gamma>_rep_cases is_empty_rep_def split: extended.splits)
+ done
qed
interpretation Abs_Int1
@@ -308,25 +352,41 @@
text{* Monotonicity: *}
+lemma mono_meet_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (meet_rep p1 q1) (meet_rep p2 q2)"
+by(auto simp add: le_iff_subset \<gamma>_meet_rep)
+
+lemma mono_plus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (plus_rep p1 q1) (plus_rep p2 q2)"
+apply(auto simp: plus_rep_def le_iff_subset split: if_splits)
+by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
+
+lemma mono_minus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep (uminus_rep p1) (uminus_rep p2)"
+apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split)
+by(auto simp: \<gamma>_rep_cases split: extended.splits)
+
interpretation Abs_Int1_mono
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_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_lub_defs empty_def split: if_splits ivl.splits lub_splits)
+ case goal1 thus ?case by transfer (rule mono_plus_rep)
+next
+ case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def
+ by transfer (auto simp: mono_meet_rep mono_plus_rep mono_minus_rep)
next
- case goal2 thus ?case
- by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
-next
- case goal3 thus ?case
- apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
- by(auto simp add: empty_def le_ivl_def le_lub_defs min_def max_def split: lub_splits)
+ case goal3 thus ?case unfolding less_eq_prod_def
+ apply transfer
+ apply(auto simp:filter_less_rep_def le_iff_subset min_def max_def split: if_splits)
+ by(auto simp:is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
qed
subsubsection "Tests"
+(* Hide Fin in numerals on output *)
+declare
+Fin_numeral [code_post] Fin_neg_numeral [code_post]
+zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
+
value "show_acom_opt (AI_ivl test1_ivl)"
text{* Better than @{text AI_const}: *}
@@ -334,7 +394,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(vars c)) ^^ 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 Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Mar 06 16:10:56 2013 +0100
@@ -65,17 +65,17 @@
class narrow =
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
-class WN = widen + narrow + preord +
-assumes widen1: "x \<sqsubseteq> x \<nabla> y"
-assumes widen2: "y \<sqsubseteq> x \<nabla> y"
-assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
-assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+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"
+assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
-class WN_Lc = widen + narrow + preord + Lc +
-assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
-assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
-assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
-assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+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"
@@ -83,22 +83,25 @@
instantiation ivl :: WN
begin
-definition "widen_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 then ivl2 else
- if is_empty ivl2 then ivl1 else*)
- case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
- Ivl (if l2 \<le> l1 \<and> l2 \<noteq> l1 then Minf else l1)
- (if h1 \<le> h2 \<and> h1 \<noteq> h2 then Pinf else h1))"
+definition "widen_rep p1 p2 =
+ (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else
+ let (l1,h1) = p1; (l2,h2) = p2
+ in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))"
+
+lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep
+by(auto simp: widen_rep_def eq_ivl_iff)
-definition "narrow_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
- case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
- Ivl (if l1 = Minf then l2 else l1)
- (if h1 = Pinf then h2 else h1))"
+definition "narrow_rep p1 p2 =
+ (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
+ let (l1,h1) = p1; (l2,h2) = p2
+ in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))"
+
+lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep
+by(auto simp: narrow_rep_def eq_ivl_iff)
instance
-proof qed
- (auto simp add: widen_ivl_def narrow_ivl_def le_lub_defs le_ivl_def empty_def split: ivl.split lub_splits if_splits)
+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)+
end
@@ -106,23 +109,20 @@
instantiation st :: (WN)WN_Lc
begin
-definition "widen_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
+definition "widen_st F1 F2 = St (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
-definition "narrow_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
+definition "narrow_st F1 F2 = St (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
instance
proof
- case goal1 thus ?case
- by(simp add: widen_st_def le_st_def WN_class.widen1)
+ case goal1 thus ?case by(simp add: widen_st_def less_eq_st_def WN_class.widen1)
next
case goal2 thus ?case
- by(simp add: widen_st_def le_st_def WN_class.widen2 Lc_st_def L_st_def)
+ 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 le_st_def WN_class.narrow1)
+ case goal3 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow1)
next
- case goal4 thus ?case
- by(auto simp: narrow_st_def le_st_def WN_class.narrow2)
+ case goal4 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow2)
next
case goal5 thus ?case by(auto simp: widen_st_def Lc_st_def L_st_def)
next
@@ -196,14 +196,14 @@
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 \<sqsubseteq> C1 \<nabla> C2"
-by(induct C1 C2 rule: le_acom.induct)
+ \<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 \<sqsubseteq> C1 \<nabla> C2"
-by(induct C1 C2 rule: le_acom.induct)
+ \<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]:
@@ -229,10 +229,10 @@
case goal2 thus ?case by(auto simp: Lc_acom_def widen_acom2)
next
case goal3 thus ?case
- by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow1)
+ 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: le_acom.induct)(simp_all add: narrow_acom_def narrow2)
+ 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)
@@ -255,12 +255,12 @@
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: le_acom.induct)
+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: le_acom.induct)
+by(induction C1 C2 rule: less_eq_acom.induct)
(auto simp: narrow_acom_def)
lemma bot_in_Lc[simp]: "bot c \<in> Lc c"
@@ -269,18 +269,18 @@
subsubsection "Post-fixed point computation"
-definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,widen})option"
-where "iter_widen f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) (\<lambda>x. x \<nabla> f x)"
+definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option"
+where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)"
-definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,narrow})option"
-where "iter_narrow f = while_option (\<lambda>x. \<not> x \<sqsubseteq> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
+definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option"
+where "iter_narrow f = while_option (\<lambda>x. \<not> x \<le> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
-definition pfp_wn :: "('a::{preord,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
+definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
where "pfp_wn f x =
(case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
-lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<sqsubseteq> p"
+lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p"
by(auto simp add: iter_widen_def dest: while_option_stop)
lemma iter_widen_inv:
@@ -295,7 +295,7 @@
using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
by (metis assms(1))
-lemma strip_iter_widen: fixes f :: "'a::{preord,widen} acom \<Rightarrow> 'a acom"
+lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom"
assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
shows "strip C' = strip C"
proof-
@@ -305,12 +305,12 @@
qed
lemma iter_narrow_pfp:
-assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
+assumes mono: "!!x1 x2::_::WN_Lc. 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 \<sqsubseteq> p0" and "iter_narrow f p0 = Some p"
-shows "P p \<and> f p \<sqsubseteq> p"
+and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p"
+shows "P p \<and> f p \<le> p"
proof-
- let ?Q = "%p. P p \<and> f p \<sqsubseteq> p \<and> p \<sqsubseteq> p0"
+ let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
{ fix p assume "?Q p"
note P = conjunct1[OF this] and 12 = conjunct2[OF this]
note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
@@ -318,12 +318,12 @@
have "?Q ?p'"
proof auto
show "P ?p'" by (blast intro: P Pinv)
- have "f ?p' \<sqsubseteq> f p" by(rule mono[OF `P (p \<triangle> f p)` P narrow2[OF 1]])
- also have "\<dots> \<sqsubseteq> ?p'" by(rule narrow1[OF 1])
- finally show "f ?p' \<sqsubseteq> ?p'" .
- have "?p' \<sqsubseteq> p" by (rule narrow2[OF 1])
- also have "p \<sqsubseteq> p0" by(rule 2)
- finally show "?p' \<sqsubseteq> p0" .
+ 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])
+ finally show "f ?p' \<le> ?p'" .
+ have "?p' \<le> p" by (rule narrow2[OF 1])
+ also have "p \<le> p0" by(rule 2)
+ finally show "?p' \<le> p0" .
qed
}
thus ?thesis
@@ -332,11 +332,11 @@
qed
lemma pfp_wn_pfp:
-assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
+assumes mono: "!!x1 x2::_::WN_Lc. 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)"
-and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<sqsubseteq> p"
+and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p"
proof-
from pfp_wn obtain p0
where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
@@ -358,24 +358,24 @@
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(vars c))) (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 \<sqsubseteq> C"
+ 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"
+ have pfp: "step (\<gamma>\<^isub>o(Top(vars c))) (\<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(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 "... \<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(vars c)))) \<le> \<gamma>\<^isub>c C"
+ by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 pfp])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -391,14 +391,10 @@
subsubsection "Tests"
-(* Trick to make the code generator happy. *)
-lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y"
-by(rule refl)
-
definition "step_up_ivl n =
- ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
+ ((\<lambda>C. C \<nabla> step_ivl (Top(vars(strip C))) 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(vars(strip C))) 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
@@ -430,32 +426,31 @@
locale Measure_WN = Measure1 where m=m for m :: "'av::WN \<Rightarrow> nat" +
fixes n :: "'av \<Rightarrow> nat"
-assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
-assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
-assumes n_narrow: "y \<sqsubseteq> x \<Longrightarrow> ~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
+assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
+assumes n_mono: "x \<le> y \<Longrightarrow> n x \<le> n y"
+assumes n_narrow: "y \<le> x \<Longrightarrow> ~ x \<le> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
begin
lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
- ~ S2 \<sqsubseteq> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
-proof(auto simp add: le_st_def m_s_def L_st_def widen_st_def)
+ ~ 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)"
by (metis m1 WN_class.widen1)
- fix x assume "x \<in> dom S1" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
+ 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))" .
qed
-lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
+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)
+by(auto simp: m_o_def L_st_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 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
+ "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)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
@@ -475,25 +470,25 @@
definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where
"n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))"
-lemma n_s_mono: assumes "S1 \<sqsubseteq> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
+lemma n_s_mono: assumes "S1 \<le> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
proof-
- from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
- by(simp_all add: le_st_def)
+ from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<le> fun S2 x"
+ by(simp_all add: less_eq_st_def)
have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))"
- by(rule setsum_mono)(simp add: le_st_def n_mono)
+ by(rule setsum_mono)(simp add: less_eq_st_def n_mono)
thus ?thesis by(simp add: n_s_def)
qed
lemma n_s_narrow:
-assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
+assumes "finite(dom S1)" and "S2 \<le> S1" "\<not> S1 \<le> S1 \<triangle> S2"
shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1"
proof-
- from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
- by(simp_all add: le_st_def)
+ from `S2\<le>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<le> fun S1 x"
+ by(simp_all add: less_eq_st_def)
have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
- by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
- have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<sqsubseteq> S1 \<triangle> S2`
- by(force simp: le_st_def narrow_st_def intro: n_narrow)
+ by(auto simp: less_eq_st_def narrow_st_def n_mono WN_class.narrow2)
+ have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<le> S1 \<triangle> S2`
+ by(force 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)
@@ -504,12 +499,12 @@
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)"
-lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_s_mono)
+lemma n_o_mono: "S1 \<le> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
+by(induction S1 S2 rule: less_eq_option.induct)(auto simp: n_o_def n_s_mono)
lemma n_o_narrow:
"S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
- \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
+ \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> \<not> S1 \<le> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
apply(induction S1 S2 rule: narrow_option.induct)
apply(auto simp: n_o_def L_st_def n_s_narrow)
done
@@ -519,7 +514,7 @@
"n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))"
lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow>
- C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
+ C2 \<le> C1 \<Longrightarrow> \<not> C1 \<le> C1 \<triangle> C2 \<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)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
@@ -544,13 +539,13 @@
fixes m :: "'a::WN_Lc \<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 \<sqsubseteq> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
+and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
and "P C" shows "EX C'. iter_widen f C = Some C'"
proof(simp add: iter_widen_def,
rule measure_while_option_Some[where P = P and f=m])
show "P C" by(rule `P C`)
next
- fix C assume "P C" "\<not> f C \<sqsubseteq> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
+ fix C assume "P C" "\<not> f C \<le> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
by(simp add: P_f P_widen m_widen)
qed
@@ -558,19 +553,19 @@
fixes n :: "'a::WN_Lc \<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 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"
-and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<sqsubseteq> C1 \<Longrightarrow> ~ C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
-and init: "P C" "f C \<sqsubseteq> C" shows "EX C'. iter_narrow f C = Some C'"
+and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2"
+and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> ~ C1 \<le> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
+and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'"
proof(simp add: iter_narrow_def,
- rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<sqsubseteq> C"])
- show "P C \<and> f C \<sqsubseteq> C" using init by blast
+ rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"])
+ show "P C \<and> f C \<le> C" using init by blast
next
- fix C assume 1: "P C \<and> f C \<sqsubseteq> C" and 2: "\<not> C \<sqsubseteq> C \<triangle> f C"
+ fix C assume 1: "P C \<and> f C \<le> C" and 2: "\<not> C \<le> C \<triangle> f C"
hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
- moreover then have "f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C"
- by (metis narrow1 narrow2 1 mono preord_class.le_trans)
+ moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C"
+ by (metis narrow1 narrow2 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) \<sqsubseteq> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C"
+ 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
qed
@@ -581,39 +576,51 @@
subsubsection "Termination: Intervals"
-definition m_ivl :: "ivl \<Rightarrow> nat" where
-"m_ivl ivl = (case ivl of Ivl l h \<Rightarrow>
- (case l of Minf \<Rightarrow> 0 | Lb _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | Ub _ \<Rightarrow> 1))"
+definition m_rep :: "eint2 \<Rightarrow> nat" where
+"m_rep p = (if is_empty_rep p then 3 else
+ let (l,h) = p in (case l of Minf \<Rightarrow> 0 | _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | _ \<Rightarrow> 1))"
+
+lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep
+by(auto simp: m_rep_def eq_ivl_iff)
-lemma m_ivl_height: "m_ivl ivl \<le> 2"
-by(simp add: m_ivl_def split: ivl.split lub_splits)
+lemma m_ivl_nice: "m_ivl[l\<dots>h] = (if [l\<dots>h] = \<bottom> then 3 else
+ (if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))"
+unfolding bot_ivl_def
+by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split)
-lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
-by(auto simp: m_ivl_def le_lub_defs le_ivl_def
- split: ivl.split lub_splits if_splits)
+lemma m_ivl_height: "m_ivl iv \<le> 3"
+by transfer (simp add: m_rep_def split: prod.split extended.split)
+
+lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
+by transfer
+ (auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
+ split: prod.split extended.splits if_splits)
lemma m_ivl_widen:
- "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
-by(auto simp: m_ivl_def widen_ivl_def le_lub_defs le_ivl_def
- split: ivl.splits lub_splits if_splits)
+ "~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
+by transfer
+ (auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
+ split: prod.split extended.splits if_splits)
definition n_ivl :: "ivl \<Rightarrow> nat" where
-"n_ivl ivl = 2 - m_ivl ivl"
+"n_ivl ivl = 3 - m_ivl ivl"
-lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
+lemma n_ivl_mono: "x \<le> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
lemma n_ivl_narrow:
- "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
-by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_lub_defs le_ivl_def
- split: ivl.splits lub_splits if_splits)
+ "~ x \<le> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
+unfolding n_ivl_def
+by transfer
+ (auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset
+ split: prod.splits if_splits extended.splits)
interpretation Abs_Int2_measure
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-and m = m_ivl and n = n_ivl and h = 2
+and m = m_ivl and n = n_ivl and h = 3
proof
case goal1 thus ?case by(rule m_ivl_anti_mono)
next
@@ -629,14 +636,14 @@
lemma iter_winden_step_ivl_termination:
- "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
+ "\<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)
done
lemma iter_narrow_step_ivl_termination:
- "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
- \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
+ "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)
@@ -662,12 +669,11 @@
subsubsection "Counterexamples"
-text{* Widening is increasing by assumption,
-but @{prop"x \<sqsubseteq> f x"} is not an invariant of widening. It can already
-be lost after the first step: *}
+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 \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" shows "x \<nabla> f x \<sqsubseteq> f(x \<nabla> f x)"
+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]
(*
1 < 2 < 3,
@@ -682,9 +688,9 @@
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 \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" and "f(f x) \<sqsubseteq> f x"
-shows "f(x \<nabla> f x) \<sqsubseteq> x \<nabla> f x"
+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 Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_State.thy Wed Mar 06 16:10:56 2013 +0100
@@ -60,21 +60,21 @@
end
class semilatticeL = join + L +
-fixes top :: "vname set \<Rightarrow> 'a"
-assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
-and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
-and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<in> L X \<Longrightarrow> x \<sqsubseteq> top X"
-and top_in_L[simp]: "top X \<in> L X"
+fixes Top :: "vname set \<Rightarrow> 'a"
+assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<le> x \<squnion> y"
+and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<le> x \<squnion> y"
+and join_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 join_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>")
+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)"
+definition Top_option where "Top c = Some(Top c)"
instance proof
case goal1 thus ?case by(cases x, simp, cases y, simp_all)
@@ -83,9 +83,9 @@
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)
+ case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
next
- case goal5 thus ?case by(simp add: top_option_def)
+ 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
@@ -97,41 +97,77 @@
hide_type st --"to avoid long names"
-text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
+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)"
-datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set"
+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)
-fun "fun" where "fun (FunDom f X) = f"
-fun dom where "dom (FunDom f X) = X"
+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 st \<Rightarrow> vname \<Rightarrow> 'a" is fst ..
+
+lift_definition dom :: "'a st \<Rightarrow> vname set" is snd ..
-definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
+lemma dom_St[simp]: "dom(St f X) = X"
+by(simp add: St.rep_eq dom.rep_eq)
-value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
+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_opt = Option.map show_acom"
-definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
+lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
+by transfer auto
-lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
-by(rule ext)(auto simp: update_def)
+lemma dom_update[simp]: "dom (update S x y) = insert x (dom S)"
+by transfer auto
+
+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)}"
-lemma dom_update[simp]: "dom (update S x y) = dom S"
-by(simp add: update_def)
+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
+done
-definition "\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom F. f x \<in> \<gamma>(fun F x)}"
-
-
-instantiation st :: (preord) preord
+instantiation st :: (order) order
begin
-definition le_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
-"F \<sqsubseteq> G = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<sqsubseteq> fun G x))"
+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))"
+
+definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
instance
proof
- case goal2 thus ?case by(auto simp: le_st_def)(metis preord_class.le_trans)
-qed (auto simp: le_st_def)
+ case goal1 show ?case by(rule less_st_def)
+next
+ case goal2 show ?case by(auto simp: less_eq_st_def)
+next
+ case goal3 thus ?case by(fastforce simp: less_eq_st_def)
+next
+ case goal4 thus ?case by (metis less_eq_st_def antisym ext_st)
+qed
end
@@ -139,7 +175,7 @@
begin
definition join_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
-"F \<squnion> G = FunDom (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
+"F \<squnion> (G::'a st) = St (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
instance ..
@@ -149,7 +185,7 @@
begin
definition L_st :: "vname set \<Rightarrow> 'a st set" where
-"L X = {F. dom F = X}"
+"L(X::vname set) = {F. dom F = X}"
instance ..
@@ -158,11 +194,10 @@
instantiation st :: (semilattice) semilatticeL
begin
-definition top_st where "top X = FunDom (\<lambda>x. \<top>) X"
+definition Top_st :: "vname set \<Rightarrow> 'a st" where "Top(X) = St (\<lambda>x. \<top>) X"
instance
-proof
-qed (auto simp: le_st_def join_st_def top_st_def L_st_def)
+proof qed(auto simp add: less_eq_st_def join_st_def Top_st_def L_st_def)
end
@@ -175,12 +210,12 @@
But L is not executable. This looping defn makes it look as if it were. *)
-lemma mono_fun: "F \<sqsubseteq> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
-by(auto simp: le_st_def)
+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 mono_update[simp]:
- "a1 \<sqsubseteq> a2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> update S1 x a1 \<sqsubseteq> update S2 x a2"
-by(auto simp add: le_st_def update_def)
+ "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)
locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
@@ -195,22 +230,22 @@
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 c) = UNIV"
-by(auto simp: top_st_def \<gamma>_st_def)
+lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (Top X) = UNIV"
+by(auto simp: Top_st_def \<gamma>_st_def)
-lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
-by (simp add: top_option_def)
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (Top X) = UNIV"
+by (simp add: Top_option_def)
-lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
-apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
+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)
lemma mono_gamma_o:
- "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
+ "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
+by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
-lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
+lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
+by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
lemma in_gamma_option_iff:
"x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"