"more standard" argument order of relation composition (op O)
authorkrauss
Mon Jul 27 21:47:41 2009 +0200 (2009-07-27 ago)
changeset 322358f9b8d14fc9f
parent 32230 9f6461b1c9cc
child 32236 0203e1006f1b
child 32239 d2a99fdddd69
"more standard" argument order of relation composition (op O)
NEWS
src/HOL/FunDef.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Machines.thy
src/HOL/Lambda/Eta.thy
src/HOL/Predicate.thy
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/NEWS	Mon Jul 27 21:47:41 2009 +0200
     1.3 @@ -67,6 +67,13 @@
     1.4  multiplicative monoids retains syntax "^" and is now defined generic
     1.5  in class power.  INCOMPATIBILITY.
     1.6  
     1.7 +* Relation composition "R O S" now has a "more standard" argument order,
     1.8 +i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
     1.9 +INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
    1.10 +may occationally break, since the O_assoc rule was not rewritten like this.
    1.11 +Fix using O_assoc[symmetric].
    1.12 +The same applies to the curried version "R OO S".
    1.13 +
    1.14  * GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
    1.15  infinite sets. It is shown that they form a complete lattice.
    1.16  
     2.1 --- a/src/HOL/FunDef.thy	Mon Jul 27 17:36:30 2009 +0200
     2.2 +++ b/src/HOL/FunDef.thy	Mon Jul 27 21:47:41 2009 +0200
     2.3 @@ -193,9 +193,9 @@
     2.4  subsection {* Reduction Pairs *}
     2.5  
     2.6  definition
     2.7 -  "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
     2.8 +  "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
     2.9  
    2.10 -lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
    2.11 +lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
    2.12  unfolding reduction_pair_def by auto
    2.13  
    2.14  lemma reduction_pair_lemma:
    2.15 @@ -205,7 +205,7 @@
    2.16    assumes "wf S"
    2.17    shows "wf (R \<union> S)"
    2.18  proof -
    2.19 -  from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
    2.20 +  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
    2.21      unfolding reduction_pair_def by auto
    2.22    with `wf S` have "wf (fst P \<union> S)" 
    2.23      by (auto intro: wf_union_compatible)
    2.24 @@ -266,8 +266,8 @@
    2.25  text {* Reduction Pairs *}
    2.26  
    2.27  lemma max_ext_compat: 
    2.28 -  assumes "S O R \<subseteq> R"
    2.29 -  shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
    2.30 +  assumes "R O S \<subseteq> R"
    2.31 +  shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
    2.32  using assms 
    2.33  apply auto
    2.34  apply (elim max_ext.cases)
    2.35 @@ -287,8 +287,8 @@
    2.36  by (auto simp: pair_less_def pair_leq_def)
    2.37  
    2.38  lemma min_ext_compat: 
    2.39 -  assumes "S O R \<subseteq> R"
    2.40 -  shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
    2.41 +  assumes "R O S \<subseteq> R"
    2.42 +  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
    2.43  using assms 
    2.44  apply (auto simp: min_ext_def)
    2.45  apply (drule_tac x=ya in bspec, assumption)
     3.1 --- a/src/HOL/IMP/Denotation.thy	Mon Jul 27 17:36:30 2009 +0200
     3.2 +++ b/src/HOL/IMP/Denotation.thy	Mon Jul 27 21:47:41 2009 +0200
     3.3 @@ -12,14 +12,14 @@
     3.4  
     3.5  definition
     3.6    Gamma :: "[bexp,com_den] => (com_den => com_den)" where
     3.7 -  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
     3.8 +  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union>
     3.9                         {(s,t). s=t \<and> \<not>b s})"
    3.10  
    3.11  primrec C :: "com => com_den"
    3.12  where
    3.13    C_skip:   "C \<SKIP>   = Id"
    3.14  | C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    3.15 -| C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    3.16 +| C_comp:   "C (c0;c1)   = C(c0) O C(c1)"
    3.17  | C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    3.18                                                  {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    3.19  | C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
     4.1 --- a/src/HOL/IMP/Machines.thy	Mon Jul 27 17:36:30 2009 +0200
     4.2 +++ b/src/HOL/IMP/Machines.thy	Mon Jul 27 21:47:41 2009 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4    "((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))"
     4.5  apply(rule iffI)
     4.6   apply(blast elim:rel_pow_E2)
     4.7 -apply (fastsimp simp add:gr0_conv_Suc rel_pow_commute)
     4.8 +apply (auto simp: rel_pow_commute[symmetric])
     4.9  done
    4.10  
    4.11  subsection "Instructions"
     5.1 --- a/src/HOL/Lambda/Eta.thy	Mon Jul 27 17:36:30 2009 +0200
     5.2 +++ b/src/HOL/Lambda/Eta.thy	Mon Jul 27 21:47:41 2009 +0200
     5.3 @@ -371,7 +371,7 @@
     5.4  
     5.5  theorem eta_postponement:
     5.6    assumes "(sup beta eta)\<^sup>*\<^sup>* s t"
     5.7 -  shows "(eta\<^sup>*\<^sup>* OO beta\<^sup>*\<^sup>*) s t" using assms
     5.8 +  shows "(beta\<^sup>*\<^sup>* OO eta\<^sup>*\<^sup>*) s t" using assms
     5.9  proof induct
    5.10    case base
    5.11    show ?case by blast
     6.1 --- a/src/HOL/Predicate.thy	Mon Jul 27 17:36:30 2009 +0200
     6.2 +++ b/src/HOL/Predicate.thy	Mon Jul 27 21:47:41 2009 +0200
     6.3 @@ -221,11 +221,11 @@
     6.4  subsubsection {* Composition  *}
     6.5  
     6.6  inductive
     6.7 -  pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
     6.8 +  pred_comp  :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
     6.9      (infixr "OO" 75)
    6.10 -  for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
    6.11 +  for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
    6.12  where
    6.13 -  pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
    6.14 +  pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
    6.15  
    6.16  inductive_cases pred_compE [elim!]: "(r OO s) a c"
    6.17  
     7.1 --- a/src/HOL/Relation.thy	Mon Jul 27 17:36:30 2009 +0200
     7.2 +++ b/src/HOL/Relation.thy	Mon Jul 27 21:47:41 2009 +0200
     7.3 @@ -21,9 +21,9 @@
     7.4    converse  ("(_\<inverse>)" [1000] 999)
     7.5  
     7.6  definition
     7.7 -  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"
     7.8 +  rel_comp  :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
     7.9      (infixr "O" 75) where
    7.10 -  "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
    7.11 +  "r O s == {(x,z). EX y. (x, y) : r & (y, z) : s}"
    7.12  
    7.13  definition
    7.14    Image :: "[('a * 'b) set, 'a set] => 'b set"
    7.15 @@ -140,15 +140,15 @@
    7.16  subsection {* Composition of two relations *}
    7.17  
    7.18  lemma rel_compI [intro]:
    7.19 -  "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s"
    7.20 +  "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
    7.21  by (unfold rel_comp_def) blast
    7.22  
    7.23  lemma rel_compE [elim!]: "xz : r O s ==>
    7.24 -  (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
    7.25 +  (!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s  ==> P) ==> P"
    7.26  by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
    7.27  
    7.28  lemma rel_compEpair:
    7.29 -  "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
    7.30 +  "(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P"
    7.31  by (iprover elim: rel_compE Pair_inject ssubst)
    7.32  
    7.33  lemma R_O_Id [simp]: "R O Id = R"
    7.34 @@ -173,7 +173,7 @@
    7.35  by blast
    7.36  
    7.37  lemma rel_comp_subset_Sigma:
    7.38 -    "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
    7.39 +    "r \<subseteq> A \<times> B ==> s \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
    7.40  by blast
    7.41  
    7.42  lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 
     8.1 --- a/src/HOL/Transitive_Closure.thy	Mon Jul 27 17:36:30 2009 +0200
     8.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jul 27 21:47:41 2009 +0200
     8.3 @@ -159,7 +159,7 @@
     8.4    apply (erule asm_rl exE disjE conjE base step)+
     8.5    done
     8.6  
     8.7 -lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
     8.8 +lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
     8.9    apply (rule subsetI)
    8.10    apply (rule_tac p="x" in PairE, clarify)
    8.11    apply (erule rtrancl_induct, auto) 
    8.12 @@ -291,7 +291,7 @@
    8.13    by (blast elim: rtranclE converse_rtranclE
    8.14      intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
    8.15  
    8.16 -lemma rtrancl_unfold: "r^* = Id Un r O r^*"
    8.17 +lemma rtrancl_unfold: "r^* = Id Un r^* O r"
    8.18    by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
    8.19  
    8.20  lemma rtrancl_Un_separatorE:
    8.21 @@ -384,7 +384,7 @@
    8.22    | (step) c where "(a, c) : r^+" and "(c, b) : r"
    8.23    using assms by cases simp_all
    8.24  
    8.25 -lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
    8.26 +lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
    8.27    apply (rule subsetI)
    8.28    apply (rule_tac p = x in PairE)
    8.29    apply clarify
    8.30 @@ -392,7 +392,7 @@
    8.31     apply auto
    8.32    done
    8.33  
    8.34 -lemma trancl_unfold: "r^+ = r Un r O r^+"
    8.35 +lemma trancl_unfold: "r^+ = r Un r^+ O r"
    8.36    by (auto intro: trancl_into_trancl elim: tranclE)
    8.37  
    8.38  text {* Transitivity of @{term "r^+"} *}
    8.39 @@ -676,7 +676,7 @@
    8.40  
    8.41  primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
    8.42      "relpow 0 R = Id"
    8.43 -  | "relpow (Suc n) R = R O (R ^^ n)"
    8.44 +  | "relpow (Suc n) R = (R ^^ n) O R"
    8.45  
    8.46  end
    8.47  
    8.48 @@ -734,11 +734,11 @@
    8.49    apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
    8.50    done
    8.51  
    8.52 -lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
    8.53 +lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
    8.54  by(induct n) auto
    8.55  
    8.56  lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
    8.57 -  by (induct n) (simp, simp add: O_assoc [symmetric])
    8.58 +by (induct n) (simp, simp add: O_assoc [symmetric])
    8.59  
    8.60  lemma rtrancl_imp_UN_rel_pow:
    8.61    assumes "p \<in> R^*"
     9.1 --- a/src/HOL/UNITY/ListOrder.thy	Mon Jul 27 17:36:30 2009 +0200
     9.2 +++ b/src/HOL/UNITY/ListOrder.thy	Mon Jul 27 21:47:41 2009 +0200
     9.3 @@ -117,7 +117,7 @@
     9.4  (*Lemma proving transitivity and more*)
     9.5  lemma genPrefix_trans_O [rule_format]: 
     9.6       "(x, y) : genPrefix r  
     9.7 -      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
     9.8 +      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
     9.9  apply (erule genPrefix.induct)
    9.10    prefer 3 apply (blast dest: append_genPrefix)
    9.11   prefer 2 apply (blast intro: genPrefix.prepend, blast)
    9.12 @@ -134,13 +134,15 @@
    9.13  lemma prefix_genPrefix_trans [rule_format]: 
    9.14       "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
    9.15  apply (unfold prefix_def)
    9.16 -apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
    9.17 +apply (drule genPrefix_trans_O, assumption)
    9.18 +apply simp
    9.19  done
    9.20  
    9.21  lemma genPrefix_prefix_trans [rule_format]: 
    9.22       "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
    9.23  apply (unfold prefix_def)
    9.24 -apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
    9.25 +apply (drule genPrefix_trans_O, assumption)
    9.26 +apply simp
    9.27  done
    9.28  
    9.29  lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
    10.1 --- a/src/HOL/Wellfounded.thy	Mon Jul 27 17:36:30 2009 +0200
    10.2 +++ b/src/HOL/Wellfounded.thy	Mon Jul 27 21:47:41 2009 +0200
    10.3 @@ -239,7 +239,7 @@
    10.4  
    10.5  lemma wf_union_compatible:
    10.6    assumes "wf R" "wf S"
    10.7 -  assumes "S O R \<subseteq> R"
    10.8 +  assumes "R O S \<subseteq> R"
    10.9    shows "wf (R \<union> S)"
   10.10  proof (rule wfI_min)
   10.11    fix x :: 'a and Q 
   10.12 @@ -258,8 +258,8 @@
   10.13        assume "y \<in> Q"
   10.14        with `y \<notin> ?Q'` 
   10.15        obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   10.16 -      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
   10.17 -      with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
   10.18 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
   10.19 +      with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
   10.20        with `z \<in> ?Q'` have "w \<notin> Q" by blast 
   10.21        with `w \<in> Q` show False by contradiction
   10.22      qed
   10.23 @@ -312,7 +312,7 @@
   10.24    by (auto simp: Un_ac)
   10.25  
   10.26  lemma wf_union_merge: 
   10.27 -  "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
   10.28 +  "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" (is "wf ?A = wf ?B")
   10.29  proof
   10.30    assume "wf ?A"
   10.31    with wf_trancl have wfT: "wf (?A^+)" .
   10.32 @@ -331,7 +331,7 @@
   10.33      obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
   10.34        by (erule wfE_min)
   10.35      then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
   10.36 -      and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
   10.37 +      and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
   10.38        and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
   10.39        by auto
   10.40      
   10.41 @@ -353,7 +353,7 @@
   10.42            with A1 show "y \<notin> Q" .
   10.43          next
   10.44            assume "(y, z') \<in> S" 
   10.45 -          then have "(y, z) \<in> R O S" using  `(z', z) \<in> R` ..
   10.46 +          then have "(y, z) \<in> S O R" using  `(z', z) \<in> R` ..
   10.47            with A2 show "y \<notin> Q" .
   10.48          qed
   10.49        qed