src/HOL/FunDef.thy
 changeset 32235 8f9b8d14fc9f parent 31775 2b04504fcb69 child 33083 1fad3160d873
```     1.1 --- a/src/HOL/FunDef.thy	Mon Jul 27 17:36:30 2009 +0200
1.2 +++ b/src/HOL/FunDef.thy	Mon Jul 27 21:47:41 2009 +0200
1.3 @@ -193,9 +193,9 @@
1.4  subsection {* Reduction Pairs *}
1.5
1.6  definition
1.7 -  "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
1.8 +  "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
1.9
1.10 -lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
1.11 +lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
1.12  unfolding reduction_pair_def by auto
1.13
1.14  lemma reduction_pair_lemma:
1.15 @@ -205,7 +205,7 @@
1.16    assumes "wf S"
1.17    shows "wf (R \<union> S)"
1.18  proof -
1.19 -  from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
1.20 +  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
1.21      unfolding reduction_pair_def by auto
1.22    with `wf S` have "wf (fst P \<union> S)"
1.23      by (auto intro: wf_union_compatible)
1.24 @@ -266,8 +266,8 @@
1.25  text {* Reduction Pairs *}
1.26
1.27  lemma max_ext_compat:
1.28 -  assumes "S O R \<subseteq> R"
1.29 -  shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
1.30 +  assumes "R O S \<subseteq> R"
1.31 +  shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
1.32  using assms
1.33  apply auto
1.34  apply (elim max_ext.cases)
1.35 @@ -287,8 +287,8 @@
1.36  by (auto simp: pair_less_def pair_leq_def)
1.37
1.38  lemma min_ext_compat:
1.39 -  assumes "S O R \<subseteq> R"
1.40 -  shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
1.41 +  assumes "R O S \<subseteq> R"
1.42 +  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
1.43  using assms
1.44  apply (auto simp: min_ext_def)
1.45  apply (drule_tac x=ya in bspec, assumption)
```