# HG changeset patch
# User krauss
# Date 1248724061 -7200
# Node ID 8f9b8d14fc9f06f21e31e2c0fca3a5f7046719c3
# Parent  9f6461b1c9ccbbaedbd62a07d4d2d8d24beff78e
"more standard" argument order of relation composition (op O)

diff -r 9f6461b1c9cc -r 8f9b8d14fc9f NEWS
--- 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.
 
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/FunDef.thy
--- 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)
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/IMP/Denotation.thy
--- 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))"
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/IMP/Machines.thy
--- 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"
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/Lambda/Eta.thy
--- 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
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/Predicate.thy
--- 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"
 
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/Relation.thy
--- 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)" 
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/Transitive_Closure.thy
--- 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^*"
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/UNITY/ListOrder.thy
--- 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)"
diff -r 9f6461b1c9cc -r 8f9b8d14fc9f src/HOL/Wellfounded.thy
--- 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