578 |
578 |
579 end |
579 end |
580 |
580 |
581 subsubsection \<open>Totality\<close> |
581 subsubsection \<open>Totality\<close> |
582 |
582 |
583 definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" |
583 definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where |
584 where "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)" |
584 "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)" |
585 |
585 |
586 lemma total_onI [intro?]: |
586 abbreviation total :: "'a rel \<Rightarrow> bool" where |
587 "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r" |
587 "total \<equiv> total_on UNIV" |
588 unfolding total_on_def by blast |
588 |
589 |
589 definition totalp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
590 abbreviation "total \<equiv> total_on UNIV" |
|
591 |
|
592 definition totalp_on where |
|
593 "totalp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> R x y \<or> R y x)" |
590 "totalp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> R x y \<or> R y x)" |
594 |
591 |
595 abbreviation totalp where |
592 abbreviation totalp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
596 "totalp \<equiv> totalp_on UNIV" |
593 "totalp \<equiv> totalp_on UNIV" |
597 |
594 |
598 lemma totalp_on_refl_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r" |
595 lemma totalp_on_refl_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r" |
599 by (simp add: totalp_on_def total_on_def) |
596 by (simp add: totalp_on_def total_on_def) |
600 |
597 |
601 lemma totalp_onI: |
598 lemma total_onI [intro?]: |
602 "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp_on A R" |
599 "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r" |
|
600 unfolding total_on_def by blast |
|
601 |
|
602 lemma totalI: "(\<And>x y. x \<noteq> y \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total r" |
|
603 by (rule total_onI) |
|
604 |
|
605 lemma totalp_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp_on A R" |
603 by (simp add: totalp_on_def) |
606 by (simp add: totalp_on_def) |
604 |
607 |
605 lemma totalpI: "(\<And>x y. x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp R" |
608 lemma totalpI: "(\<And>x y. x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp R" |
606 by (rule totalp_onI) |
609 by (rule totalp_onI) |
607 |
610 |