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)