--- a/src/HOL/IMP/Abs_Int0.thy Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Thu Dec 29 17:43:40 2011 +0100
@@ -13,12 +13,12 @@
begin
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
-"aval' (N n) _ = num' n" |
+"aval' (N n) S = num' n" |
"aval' (V x) S = lookup S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
-by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
+by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def lookup_def)
end
@@ -46,22 +46,22 @@
text{* Soundness: *}
-lemma in_rep_update:
+lemma in_gamma_update:
"\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)"
-by(simp add: rep_st_def lookup_update)
+by(simp add: \<gamma>_st_def lookup_update)
text{* The soundness proofs are textually identical to the ones for the step
function operating on states as functions. *}
lemma step_preserves_le2:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
\<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
proof(induction c arbitrary: cs ca S sa)
case SKIP thus ?case
by(auto simp:strip_eq_SKIP)
next
case Assign thus ?case
- by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+ by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update
split: option.splits del:subsetD)
next
case Semi thus ?case apply (auto simp: strip_eq_Semi)
@@ -70,29 +70,29 @@
case (If b c1 c2)
then obtain cs1 cs2 ca1 ca2 P Pa where
"cs = IF b THEN cs1 ELSE cs2 {P}" "ca = IF b THEN ca1 ELSE ca2 {Pa}"
- "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+ "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
"strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
by (fastforce simp: strip_eq_If)
- moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
- moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
+ moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+ moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
ultimately show ?case using If.prems(1) by (simp add: If.IH subset_iff)
next
case (While b c1)
then obtain cs1 ca1 I P Ia Pa where
"cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
- "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+ "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
"strip cs1 = c1" "strip ca1 = c1"
by (fastforce simp: strip_eq_While)
- moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
- using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
- by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+ moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (sa \<squnion> post ca1)"
+ using `S \<subseteq> \<gamma>\<^isub>o sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+ by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
ultimately show ?case by (simp add: While.IH subset_iff)
qed
lemma step_preserves_le:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
\<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
by (metis le_strip step_preserves_le2 strip_acom)
@@ -106,12 +106,12 @@
proof(rule lfp_lowerbound[simplified,OF 3])
show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
proof(rule step_preserves_le[OF _ _ 3])
- show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
- show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+ show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+ show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
qed
qed
from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
- by (blast intro: mono_rep_c order_trans)
+ by (blast intro: mono_gamma_c order_trans)
qed
end
--- a/src/HOL/IMP/Abs_Int0_const.thy Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy Thu Dec 29 17:43:40 2011 +0100
@@ -8,9 +8,9 @@
datatype cval = Const val | Any
-fun rep_cval where
-"rep_cval (Const n) = {n}" |
-"rep_cval (Any) = UNIV"
+fun \<gamma>_cval where
+"\<gamma>_cval (Const n) = {n}" |
+"\<gamma>_cval (Any) = UNIV"
fun plus_cval where
"plus_cval (Const m) (Const n) = Const(m+n)" |
@@ -52,7 +52,7 @@
end
-interpretation Val_abs rep_cval Const plus_cval
+interpretation Val_abs \<gamma>_cval Const plus_cval
defines aval'_const is aval'
proof
case goal1 thus ?case
@@ -66,7 +66,7 @@
by(auto simp: plus_cval_cases split: cval.split)
qed
-interpretation Abs_Int rep_cval Const plus_cval
+interpretation Abs_Int \<gamma>_cval Const plus_cval
defines AI_const is AI
and step_const is step'
proof qed
@@ -74,7 +74,7 @@
text{* Monotonicity: *}
-interpretation Abs_Int_mono rep_cval Const plus_cval
+interpretation Abs_Int_mono \<gamma>_cval Const plus_cval
proof
case goal1 thus ?case
by(auto simp: plus_cval_cases split: cval.split)
--- a/src/HOL/IMP/Abs_Int0_fun.thy Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Thu Dec 29 17:43:40 2011 +0100
@@ -132,7 +132,7 @@
"None \<squnion> y = y" |
"x \<squnion> None = x"
-lemma [simp]: "x \<squnion> None = x"
+lemma join_None2[simp]: "x \<squnion> None = x"
by (cases x) simp_all
definition "\<top> = Some \<top>"
@@ -224,23 +224,23 @@
subsection "Abstract Interpretation"
-definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
-"rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
+definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
+"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"
-fun rep_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
-"rep_option rep None = {}" |
-"rep_option rep (Some a) = rep a"
+fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
+"\<gamma>_option \<gamma> None = {}" |
+"\<gamma>_option \<gamma> (Some a) = \<gamma> a"
text{* The interface for abstract values: *}
locale Val_abs =
-fixes rep :: "'a::SL_top \<Rightarrow> val set" ("\<gamma>")
- assumes mono_rep: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
- and rep_Top[simp]: "\<gamma> \<top> = UNIV"
+fixes \<gamma> :: "'a::SL_top \<Rightarrow> val set"
+ assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
+ and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'a"
and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- assumes rep_num': "n : \<gamma>(num' n)"
- and rep_plus':
+ assumes gamma_num': "n : \<gamma>(num' n)"
+ and gamma_plus':
"n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
type_synonym 'a st = "(vname \<Rightarrow> 'a)"
@@ -249,7 +249,7 @@
begin
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
-"aval' (N n) _ = num' n" |
+"aval' (N n) S = num' n" |
"aval' (V x) S = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
@@ -272,51 +272,51 @@
by(induct c arbitrary: S) (simp_all add: Let_def)
-abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
-where "\<gamma>\<^isub>f == rep_fun \<gamma>"
+abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+where "\<gamma>\<^isub>f == \<gamma>_fun \<gamma>"
-abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
-where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
+abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
-abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
-where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
+abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
-lemma rep_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
-by(simp add: Top_fun_def rep_fun_def)
+lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
+by(simp add: Top_fun_def \<gamma>_fun_def)
-lemma rep_u_Top[simp]: "\<gamma>\<^isub>u Top = UNIV"
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
by (simp add: Top_option_def)
(* FIXME (maybe also le \<rightarrow> sqle?) *)
-lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
-by(auto simp: le_fun_def rep_fun_def dest: mono_rep)
+lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
-lemma mono_rep_u:
- "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
-by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
+lemma mono_gamma_o:
+ "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>o sa \<subseteq> \<gamma>\<^isub>o sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f)
-lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
-by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
+lemma mono_gamma_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o)
text{* Soundness: *}
lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
-by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def)
+by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
-lemma in_rep_update:
+lemma in_gamma_update:
"\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(S(x := a))"
-by(simp add: rep_fun_def)
+by(simp add: \<gamma>_fun_def)
lemma step_preserves_le2:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
\<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
proof(induction c arbitrary: cs ca S sa)
case SKIP thus ?case
by(auto simp:strip_eq_SKIP)
next
case Assign thus ?case
- by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+ by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update
split: option.splits del:subsetD)
next
case Semi thus ?case apply (auto simp: strip_eq_Semi)
@@ -325,29 +325,29 @@
case (If b c1 c2)
then obtain cs1 cs2 ca1 ca2 P Pa where
"cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}"
- "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+ "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
"strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
by (fastforce simp: strip_eq_If)
- moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
- moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
- ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>u sa` by (simp add: If.IH subset_iff)
+ moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+ moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
+ ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o sa` by (simp add: If.IH subset_iff)
next
case (While b c1)
then obtain cs1 ca1 I P Ia Pa where
"cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
- "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+ "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
"strip cs1 = c1" "strip ca1 = c1"
by (fastforce simp: strip_eq_While)
- moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
- using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
- by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+ moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (sa \<squnion> post ca1)"
+ using `S \<subseteq> \<gamma>\<^isub>o sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+ by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
ultimately show ?case by (simp add: While.IH subset_iff)
qed
lemma step_preserves_le:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
\<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
by (metis le_strip step_preserves_le2 strip_acom)
@@ -361,12 +361,12 @@
proof(rule lfp_lowerbound[simplified,OF 3])
show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
proof(rule step_preserves_le[OF _ _ 3])
- show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
- show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+ show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+ show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
qed
qed
from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
- by (blast intro: mono_rep_c order_trans)
+ by (blast intro: mono_gamma_c order_trans)
qed
end
--- a/src/HOL/IMP/Abs_Int1.thy Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Thu Dec 29 17:43:40 2011 +0100
@@ -37,24 +37,24 @@
end
-locale Val_abs1_rep =
- Val_abs rep num' plus'
- for rep :: "'a::L_top_bot \<Rightarrow> val set" ("\<gamma>") and num' plus' +
-assumes inter_rep_subset_rep_meet:
- "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
-and rep_Bot[simp]: "rep \<bottom> = {}"
+locale Val_abs1_gamma =
+ Val_abs \<gamma> num' plus'
+ for \<gamma> :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
+assumes inter_gamma_subset_gamma_meet:
+ "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
+and gamma_Bot[simp]: "\<gamma> \<bottom> = {}"
begin
-lemma in_rep_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
-by (metis IntI inter_rep_subset_rep_meet set_mp)
+lemma in_gamma_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
+by (metis IntI inter_gamma_subset_gamma_meet set_mp)
-lemma rep_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
-by (metis equalityI inter_rep_subset_rep_meet le_inf_iff mono_rep meet_le1 meet_le2)
+lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2)
end
-locale Val_abs1 = Val_abs1_rep +
+locale Val_abs1 = Val_abs1_gamma +
fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
@@ -66,14 +66,14 @@
locale Abs_Int1 = Val_abs1
begin
-lemma in_rep_join_UpI: "s : \<gamma>\<^isub>u S1 | s : \<gamma>\<^isub>u S2 \<Longrightarrow> s : \<gamma>\<^isub>u(S1 \<squnion> S2)"
-by (metis (no_types) join_ge1 join_ge2 mono_rep_u set_rev_mp)
+lemma in_gamma_join_UpI: "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
+by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp)
fun aval'' :: "aexp \<Rightarrow> 'a st option \<Rightarrow> 'a" where
"aval'' e None = \<bottom>" |
"aval'' e (Some sa) = aval' e sa"
-lemma aval''_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
+lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
by(cases S)(simp add: aval'_sound)+
subsubsection "Backward analysis"
@@ -107,31 +107,31 @@
(let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
in afilter e1 res1 (afilter e2 res2 S))"
-lemma afilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>u (afilter e a S)"
+lemma afilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
proof(induction e arbitrary: a S)
case N thus ?case by simp
next
case (V x)
- obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>u S`
- by(auto simp: in_rep_up_iff)
- moreover hence "s x : \<gamma> (lookup S' x)" by(simp add: rep_st_def)
+ obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>o S`
+ by(auto simp: in_gamma_option_iff)
+ moreover hence "s x : \<gamma> (lookup S' x)" by(simp add: \<gamma>_st_def)
moreover have "s x : \<gamma> a" using V by simp
ultimately show ?case using V(1)
- by(simp add: lookup_update Let_def rep_st_def)
- (metis mono_rep emptyE in_rep_meet rep_Bot subset_empty)
+ by(simp add: lookup_update Let_def \<gamma>_st_def)
+ (metis mono_gamma emptyE in_gamma_meet gamma_Bot subset_empty)
next
case (Plus e1 e2) thus ?case
using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]]
by (auto split: prod.split)
qed
-lemma bfilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>u(bfilter b bv S)"
+lemma bfilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)"
proof(induction b arbitrary: S bv)
case Bc thus ?case by simp
next
case (Not b) thus ?case by simp
next
- case (And b1 b2) thus ?case by(fastforce simp: in_rep_join_UpI)
+ case (And b1 b2) thus ?case by(fastforce simp: in_gamma_join_UpI)
next
case (Less e1 e2) thus ?case
by (auto split: prod.split)
@@ -162,20 +162,20 @@
subsubsection "Soundness"
-lemma in_rep_update:
+lemma in_gamma_update:
"\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)"
-by(simp add: rep_st_def lookup_update)
+by(simp add: \<gamma>_st_def lookup_update)
lemma step_preserves_le2:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
\<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
proof(induction c arbitrary: cs ca S sa)
case SKIP thus ?case
by(auto simp:strip_eq_SKIP)
next
case Assign thus ?case
- by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+ by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update
split: option.splits del:subsetD)
next
case Semi thus ?case apply (auto simp: strip_eq_Semi)
@@ -184,30 +184,30 @@
case (If b c1 c2)
then obtain cs1 cs2 ca1 ca2 P Pa where
"cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}"
- "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+ "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
"strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
by (fastforce simp: strip_eq_If)
- moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
- moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
- ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>u sa`
+ moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+ moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
+ ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o sa`
by (simp add: If.IH subset_iff bfilter_sound)
next
case (While b c1)
then obtain cs1 ca1 I P Ia Pa where
"cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
- "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+ "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
"strip cs1 = c1" "strip ca1 = c1"
by (fastforce simp: strip_eq_While)
- moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
- using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
- by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+ moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (sa \<squnion> post ca1)"
+ using `S \<subseteq> \<gamma>\<^isub>o sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+ by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
ultimately show ?case by (simp add: While.IH subset_iff bfilter_sound)
qed
lemma step_preserves_le:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
\<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
by (metis le_strip step_preserves_le2 strip_acom)
@@ -221,12 +221,12 @@
proof(rule lfp_lowerbound[simplified,OF 3])
show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
proof(rule step_preserves_le[OF _ _ 3])
- show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
- show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+ show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+ show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
qed
qed
from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
- by (blast intro: mono_rep_c order_trans)
+ by (blast intro: mono_gamma_c order_trans)
qed
end
@@ -255,7 +255,7 @@
lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
apply(induction e arbitrary: r r' S S')
apply(auto simp: Let_def split: option.splits prod.splits)
-apply (metis mono_rep subsetD)
+apply (metis mono_gamma subsetD)
apply(drule_tac x = "list" in mono_lookup)
apply (metis mono_meet le_trans)
apply (metis mono_meet mono_lookup mono_update)
--- a/src/HOL/IMP/Abs_Int1_ivl.thy Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Thu Dec 29 17:43:40 2011 +0100
@@ -8,7 +8,7 @@
datatype ivl = I "int option" "int option"
-definition "rep_ivl i = (case i of
+definition "\<gamma>_ivl i = (case i of
I (Some l) (Some h) \<Rightarrow> {l..h} |
I (Some l) None \<Rightarrow> {l..} |
I None (Some h) \<Rightarrow> {..h} |
@@ -26,14 +26,14 @@
definition "num_ivl n = {n\<dots>n}"
definition
- [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
+ [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> \<gamma>_ivl i"
lemma contained_in_simps [code]:
"contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
"contained_in (I (Some l) None) k \<longleftrightarrow> l \<le> k"
"contained_in (I None (Some h)) k \<longleftrightarrow> k \<le> h"
"contained_in (I None None) k \<longleftrightarrow> True"
- by (simp_all add: contained_in_def rep_ivl_def)
+ by (simp_all add: contained_in_def \<gamma>_ivl_def)
instantiation option :: (plus)plus
begin
@@ -56,8 +56,8 @@
(case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
by(auto split:option.split)
-lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
-by(auto simp add: rep_ivl_def split: ivl.split option.split)
+lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
+by(auto simp add: \<gamma>_ivl_def split: ivl.split option.split)
definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
@@ -154,9 +154,9 @@
definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
-lemma rep_minus_ivl:
- "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
-by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
+lemma gamma_minus_ivl:
+ "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
+by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits option.splits)
definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
@@ -170,26 +170,26 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-interpretation Val_abs rep_ivl num_ivl plus_ivl
+interpretation Val_abs \<gamma>_ivl num_ivl plus_ivl
defines aval_ivl is aval'
proof
case goal1 thus ?case
- by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
+ by(auto simp: \<gamma>_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
next
- case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
+ case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
next
- case goal3 thus ?case by(simp add: rep_ivl_def num_ivl_def)
+ case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
next
case goal4 thus ?case
- by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
+ by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-interpretation Val_abs1_rep rep_ivl num_ivl plus_ivl
+interpretation Val_abs1_gamma \<gamma>_ivl num_ivl plus_ivl
proof
case goal1 thus ?case
- by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
+ by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
next
- case goal2 show ?case by(auto simp add: bot_ivl_def rep_ivl_def empty_def)
+ case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
qed
lemma mono_minus_ivl:
@@ -202,19 +202,19 @@
interpretation
- Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+ Val_abs1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
proof
case goal1 thus ?case
by(auto simp add: filter_plus_ivl_def)
- (metis rep_minus_ivl add_diff_cancel add_commute)+
+ (metis gamma_minus_ivl add_diff_cancel add_commute)+
next
case goal2 thus ?case
by(cases a1, cases a2,
- auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
+ auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed
interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+ Abs_Int1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
defines afilter_ivl is afilter
and bfilter_ivl is bfilter
and step_ivl is step'
@@ -226,7 +226,7 @@
text{* Monotonicity: *}
interpretation
- Abs_Int1_mono rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+ Abs_Int1_mono \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
proof
case goal1 thus ?case
by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
--- a/src/HOL/IMP/Abs_Int2.thy Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Thu Dec 29 17:43:40 2011 +0100
@@ -180,7 +180,7 @@
apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
by (metis (no_types) strip_lpfpc strip_map2_acom strip_while)
-locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
+locale Abs_Int2 = Abs_Int1_mono \<gamma> for \<gamma> :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
begin
definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
@@ -196,18 +196,18 @@
proof(rule lfp_lowerbound[simplified,OF 3])
show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
proof(rule step_preserves_le[OF _ _ 3])
- show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
- show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+ show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+ show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
qed
qed
from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
- by (blast intro: mono_rep_c order_trans)
+ by (blast intro: mono_gamma_c order_trans)
qed
end
interpretation
- Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl
+ Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl \<gamma>_ivl
defines AI_ivl' is AI_WN
proof qed
--- a/src/HOL/IMP/Abs_State.thy Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_State.thy Thu Dec 29 17:43:40 2011 +0100
@@ -30,7 +30,7 @@
lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
by(rule ext)(auto simp: lookup_def update_def)
-definition "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}"
+definition "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(lookup F x)}"
instantiation st :: (SL_top) SL_top
begin
@@ -61,35 +61,36 @@
context Val_abs
begin
-abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
-where "\<gamma>\<^isub>f == rep_st rep"
+abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>"
-abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
-where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
+abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
-abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
-where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
+abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
-lemma rep_f_Top[simp]: "rep_f Top = UNIV"
-by(auto simp: Top_st_def rep_st_def lookup_def)
+lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
+by(auto simp: Top_st_def \<gamma>_st_def lookup_def)
-lemma rep_u_Top[simp]: "rep_u Top = UNIV"
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
by (simp add: Top_option_def)
(* FIXME (maybe also le \<rightarrow> sqle?) *)
-lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
-apply(simp add:rep_st_def subset_iff lookup_def le_st_def split: if_splits)
-by (metis UNIV_I mono_rep rep_Top subsetD)
+lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+apply(simp add:\<gamma>_st_def subset_iff lookup_def le_st_def split: if_splits)
+by (metis UNIV_I mono_gamma gamma_Top subsetD)
-lemma mono_rep_u:
- "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
-by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
+lemma mono_gamma_o:
+ "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>o sa \<subseteq> \<gamma>\<^isub>o sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f)
-lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
-by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
+lemma mono_gamma_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o)
-lemma in_rep_up_iff: "x : rep_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
+lemma in_gamma_option_iff:
+ "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
by (cases u) auto
end