--- a/NEWS Mon Jul 27 23:17:40 2009 +0200
+++ b/NEWS Mon Jul 27 23:43:35 2009 +0200
@@ -67,6 +67,13 @@
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
+* Relation composition "R O S" now has a "more standard" argument order,
+i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
+INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
+may occationally break, since the O_assoc rule was not rewritten like this.
+Fix using O_assoc[symmetric].
+The same applies to the curried version "R OO S".
+
* GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
infinite sets. It is shown that they form a complete lattice.
--- a/src/HOL/FunDef.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/FunDef.thy Mon Jul 27 23:43:35 2009 +0200
@@ -193,9 +193,9 @@
subsection {* Reduction Pairs *}
definition
- "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
+ "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
-lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
+lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
unfolding reduction_pair_def by auto
lemma reduction_pair_lemma:
@@ -205,7 +205,7 @@
assumes "wf S"
shows "wf (R \<union> S)"
proof -
- from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
+ from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
unfolding reduction_pair_def by auto
with `wf S` have "wf (fst P \<union> S)"
by (auto intro: wf_union_compatible)
@@ -266,8 +266,8 @@
text {* Reduction Pairs *}
lemma max_ext_compat:
- assumes "S O R \<subseteq> R"
- shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
+ assumes "R O S \<subseteq> R"
+ shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
using assms
apply auto
apply (elim max_ext.cases)
@@ -287,8 +287,8 @@
by (auto simp: pair_less_def pair_leq_def)
lemma min_ext_compat:
- assumes "S O R \<subseteq> R"
- shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
+ assumes "R O S \<subseteq> R"
+ shows "min_ext R O (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
using assms
apply (auto simp: min_ext_def)
apply (drule_tac x=ya in bspec, assumption)
--- a/src/HOL/IMP/Denotation.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/IMP/Denotation.thy Mon Jul 27 23:43:35 2009 +0200
@@ -12,14 +12,14 @@
definition
Gamma :: "[bexp,com_den] => (com_den => com_den)" where
- "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
+ "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union>
{(s,t). s=t \<and> \<not>b s})"
primrec C :: "com => com_den"
where
C_skip: "C \<SKIP> = Id"
| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
-| C_comp: "C (c0;c1) = C(c1) O C(c0)"
+| C_comp: "C (c0;c1) = C(c0) O C(c1)"
| C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
{(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
| C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
--- a/src/HOL/IMP/Machines.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/IMP/Machines.thy Mon Jul 27 23:43:35 2009 +0200
@@ -6,7 +6,7 @@
"((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
apply(rule iffI)
apply(blast elim:rel_pow_E2)
-apply (fastsimp simp add:gr0_conv_Suc rel_pow_commute)
+apply (auto simp: rel_pow_commute[symmetric])
done
subsection "Instructions"
--- a/src/HOL/Lambda/Eta.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Lambda/Eta.thy Mon Jul 27 23:43:35 2009 +0200
@@ -371,7 +371,7 @@
theorem eta_postponement:
assumes "(sup beta eta)\<^sup>*\<^sup>* s t"
- shows "(eta\<^sup>*\<^sup>* OO beta\<^sup>*\<^sup>*) s t" using assms
+ shows "(beta\<^sup>*\<^sup>* OO eta\<^sup>*\<^sup>*) s t" using assms
proof induct
case base
show ?case by blast
--- a/src/HOL/Library/Kleene_Algebra.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy Mon Jul 27 23:43:35 2009 +0200
@@ -274,7 +274,19 @@
oops
lemma star_decomp: "star (a + b) = star a * star (b * star a)"
-oops
+proof (rule antisym)
+ have "1 + (a + b) * star a * star (b * star a) \<le>
+ 1 + a * star a * star (b * star a) + b * star a * star (b * star a)"
+ by (metis add_commute add_left_commute eq_iff left_distrib mult_assoc)
+ also have "\<dots> \<le> star a * star (b * star a)"
+ by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
+ finally show "star (a + b) \<le> star a * star (b * star a)"
+ by (metis mult_1_right mult_assoc star3')
+next
+ show "star a * star (b * star a) \<le> star (a + b)"
+ by (metis add_assoc add_est1 add_est2 add_left_commute less_star mult_mono'
+ star_absorb_one star_absorb_one' star_idemp star_mono star_mult_idem zero_minimum)
+qed
lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow> star y * star x \<le> star x * star y"
by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)
--- a/src/HOL/Library/RBT.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Library/RBT.thy Mon Jul 27 23:43:35 2009 +0200
@@ -916,9 +916,72 @@
"alist_of Empty = []"
| "alist_of (Tr _ l k v r) = alist_of l @ (k,v) # alist_of r"
+lemma map_of_alist_of_aux: "st (Tr c t1 k v t2) \<Longrightarrow> RBT.map_of (Tr c t1 k v t2) = RBT.map_of t2 ++ [k\<mapsto>v] ++ RBT.map_of t1"
+proof (rule ext)
+ fix x
+ assume ST: "st (Tr c t1 k v t2)"
+ let ?thesis = "RBT.map_of (Tr c t1 k v t2) x = (RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1) x"
+
+ have DOM_T1: "!!k'. k'\<in>dom (RBT.map_of t1) \<Longrightarrow> k>k'"
+ proof -
+ fix k'
+ from ST have "t1 |\<guillemotleft> k" by simp
+ with tlt_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
+ moreover assume "k'\<in>dom (RBT.map_of t1)"
+ ultimately show "k>k'" using RBT.mapof_keys ST by auto
+ qed
+
+ have DOM_T2: "!!k'. k'\<in>dom (RBT.map_of t2) \<Longrightarrow> k<k'"
+ proof -
+ fix k'
+ from ST have "k \<guillemotleft>| t2" by simp
+ with tgt_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
+ moreover assume "k'\<in>dom (RBT.map_of t2)"
+ ultimately show "k<k'" using RBT.mapof_keys ST by auto
+ qed
+
+ {
+ assume C: "x<k"
+ hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t1 x" by simp
+ moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
+ moreover have "x\<notin>dom (RBT.map_of t2)" proof
+ assume "x\<in>dom (RBT.map_of t2)"
+ with DOM_T2 have "k<x" by blast
+ with C show False by simp
+ qed
+ ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+ } moreover {
+ assume [simp]: "x=k"
+ hence "RBT.map_of (Tr c t1 k v t2) x = [k \<mapsto> v] x" by simp
+ moreover have "x\<notin>dom (RBT.map_of t1)" proof
+ assume "x\<in>dom (RBT.map_of t1)"
+ with DOM_T1 have "k>x" by blast
+ thus False by simp
+ qed
+ ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+ } moreover {
+ assume C: "x>k"
+ hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t2 x" by (simp add: less_not_sym[of k x])
+ moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
+ moreover have "x\<notin>dom (RBT.map_of t1)" proof
+ assume "x\<in>dom (RBT.map_of t1)"
+ with DOM_T1 have "k>x" by simp
+ with C show False by simp
+ qed
+ ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+ } ultimately show ?thesis using less_linear by blast
+qed
+
lemma map_of_alist_of:
shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t"
- oops
+proof (induct t)
+ case Empty thus ?case by (simp add: RBT.map_of_Empty)
+next
+ case (Tr c t1 k v t2)
+ hence "Map.map_of (alist_of (Tr c t1 k v t2)) = RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1" by simp
+ also note map_of_alist_of_aux[OF Tr.prems,symmetric]
+ finally show ?case .
+qed
lemma fold_alist_fold:
"foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (alist_of t)"
--- a/src/HOL/Map.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Map.thy Mon Jul 27 23:43:35 2009 +0200
@@ -307,6 +307,9 @@
lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
by (simp add: map_upds_def)
+lemma map_add_upd_left: "m\<notin>dom e2 \<Longrightarrow> e1(m \<mapsto> u1) ++ e2 = (e1 ++ e2)(m \<mapsto> u1)"
+by (rule ext) (auto simp: map_add_def dom_def split: option.split)
+
lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
unfolding map_add_def
apply (induct xs)
@@ -508,6 +511,12 @@
lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
by (rule ext) (force simp: map_add_def dom_def split: option.split)
+lemma map_add_dom_app_simps:
+ "\<lbrakk> m\<in>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+ "\<lbrakk> m\<notin>dom l1 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+ "\<lbrakk> m\<notin>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l1 m"
+by (auto simp add: map_add_def split: option.split_asm)
+
lemma dom_const [simp]:
"dom (\<lambda>x. Some y) = UNIV"
by auto
--- a/src/HOL/Predicate.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Predicate.thy Mon Jul 27 23:43:35 2009 +0200
@@ -221,11 +221,11 @@
subsubsection {* Composition *}
inductive
- pred_comp :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
+ pred_comp :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
(infixr "OO" 75)
- for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
+ for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
where
- pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
+ pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
inductive_cases pred_compE [elim!]: "(r OO s) a c"
--- a/src/HOL/Relation.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Relation.thy Mon Jul 27 23:43:35 2009 +0200
@@ -21,9 +21,9 @@
converse ("(_\<inverse>)" [1000] 999)
definition
- rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"
+ rel_comp :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
(infixr "O" 75) where
- "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
+ "r O s == {(x,z). EX y. (x, y) : r & (y, z) : s}"
definition
Image :: "[('a * 'b) set, 'a set] => 'b set"
@@ -140,15 +140,15 @@
subsection {* Composition of two relations *}
lemma rel_compI [intro]:
- "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s"
+ "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
by (unfold rel_comp_def) blast
lemma rel_compE [elim!]: "xz : r O s ==>
- (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r ==> P) ==> P"
+ (!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s ==> P) ==> P"
by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
lemma rel_compEpair:
- "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
+ "(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P"
by (iprover elim: rel_compE Pair_inject ssubst)
lemma R_O_Id [simp]: "R O Id = R"
@@ -173,7 +173,7 @@
by blast
lemma rel_comp_subset_Sigma:
- "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
+ "r \<subseteq> A \<times> B ==> s \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
by blast
lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)"
--- a/src/HOL/Transitive_Closure.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Jul 27 23:43:35 2009 +0200
@@ -159,7 +159,7 @@
apply (erule asm_rl exE disjE conjE base step)+
done
-lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
+lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
apply (rule subsetI)
apply (rule_tac p="x" in PairE, clarify)
apply (erule rtrancl_induct, auto)
@@ -291,7 +291,7 @@
by (blast elim: rtranclE converse_rtranclE
intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
-lemma rtrancl_unfold: "r^* = Id Un r O r^*"
+lemma rtrancl_unfold: "r^* = Id Un r^* O r"
by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
lemma rtrancl_Un_separatorE:
@@ -384,7 +384,7 @@
| (step) c where "(a, c) : r^+" and "(c, b) : r"
using assms by cases simp_all
-lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
+lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
apply (rule subsetI)
apply (rule_tac p = x in PairE)
apply clarify
@@ -392,7 +392,7 @@
apply auto
done
-lemma trancl_unfold: "r^+ = r Un r O r^+"
+lemma trancl_unfold: "r^+ = r Un r^+ O r"
by (auto intro: trancl_into_trancl elim: tranclE)
text {* Transitivity of @{term "r^+"} *}
@@ -676,7 +676,7 @@
primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
"relpow 0 R = Id"
- | "relpow (Suc n) R = R O (R ^^ n)"
+ | "relpow (Suc n) R = (R ^^ n) O R"
end
@@ -734,11 +734,11 @@
apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
done
-lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
+lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
by(induct n) auto
lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
- by (induct n) (simp, simp add: O_assoc [symmetric])
+by (induct n) (simp, simp add: O_assoc [symmetric])
lemma rtrancl_imp_UN_rel_pow:
assumes "p \<in> R^*"
--- a/src/HOL/UNITY/ListOrder.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/UNITY/ListOrder.thy Mon Jul 27 23:43:35 2009 +0200
@@ -117,7 +117,7 @@
(*Lemma proving transitivity and more*)
lemma genPrefix_trans_O [rule_format]:
"(x, y) : genPrefix r
- ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
+ ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
apply (erule genPrefix.induct)
prefer 3 apply (blast dest: append_genPrefix)
prefer 2 apply (blast intro: genPrefix.prepend, blast)
@@ -134,13 +134,15 @@
lemma prefix_genPrefix_trans [rule_format]:
"[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
apply (unfold prefix_def)
-apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
+apply (drule genPrefix_trans_O, assumption)
+apply simp
done
lemma genPrefix_prefix_trans [rule_format]:
"[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r"
apply (unfold prefix_def)
-apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
+apply (drule genPrefix_trans_O, assumption)
+apply simp
done
lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
--- a/src/HOL/Wellfounded.thy Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jul 27 23:43:35 2009 +0200
@@ -239,7 +239,7 @@
lemma wf_union_compatible:
assumes "wf R" "wf S"
- assumes "S O R \<subseteq> R"
+ assumes "R O S \<subseteq> R"
shows "wf (R \<union> S)"
proof (rule wfI_min)
fix x :: 'a and Q
@@ -258,8 +258,8 @@
assume "y \<in> Q"
with `y \<notin> ?Q'`
obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
- from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
- with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
+ from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
+ with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
with `z \<in> ?Q'` have "w \<notin> Q" by blast
with `w \<in> Q` show False by contradiction
qed
@@ -312,7 +312,7 @@
by (auto simp: Un_ac)
lemma wf_union_merge:
- "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
+ "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" (is "wf ?A = wf ?B")
proof
assume "wf ?A"
with wf_trancl have wfT: "wf (?A^+)" .
@@ -331,7 +331,7 @@
obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"
by (erule wfE_min)
then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
- and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
+ and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
by auto
@@ -353,7 +353,7 @@
with A1 show "y \<notin> Q" .
next
assume "(y, z') \<in> S"
- then have "(y, z) \<in> R O S" using `(z', z) \<in> R` ..
+ then have "(y, z) \<in> S O R" using `(z', z) \<in> R` ..
with A2 show "y \<notin> Q" .
qed
qed