--- a/NEWS Mon Jul 27 17:36:30 2009 +0200
+++ b/NEWS Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/FunDef.thy Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/IMP/Denotation.thy Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/IMP/Machines.thy Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/Lambda/Eta.thy Mon Jul 27 21:47:41 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/Predicate.thy Mon Jul 27 17:36:30 2009 +0200
+++ b/src/HOL/Predicate.thy Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/Relation.thy Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/UNITY/ListOrder.thy Mon Jul 27 21:47:41 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 17:36:30 2009 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jul 27 21:47:41 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