--- a/NEWS Sun Jun 05 20:14:59 2022 +0200
+++ b/NEWS Sun Jun 05 20:16:48 2022 +0200
@@ -40,8 +40,23 @@
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
-* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
- type class preorder.
+* Theory "HOL.Relation":
+ - Added predicate reflp_on and redefined reflp to ab an abbreviation.
+ Lemma reflp_def is explicitly provided for backward compatibility
+ but its usage is discouraged. Minor INCOMPATIBILITY.
+ - Added predicate totalp_on and abbreviation totalp.
+ - Added lemmas.
+ preorder.asymp_greater
+ preorder.asymp_less
+ reflp_onD
+ reflp_onI
+ reflp_on_subset
+ total_on_subset
+ totalpD
+ totalpI
+ totalp_onD
+ totalp_onI
+ totalp_on_subset
* Theory "HOL-Library.Multiset":
- Consolidated operation and fact names.
--- a/src/HOL/Data_Structures/Selection.thy Sun Jun 05 20:14:59 2022 +0200
+++ b/src/HOL/Data_Structures/Selection.thy Sun Jun 05 20:16:48 2022 +0200
@@ -4,7 +4,7 @@
*)
section \<open>The Median-of-Medians Selection Algorithm\<close>
theory Selection
- imports Complex_Main Sorting Time_Funs
+ imports Complex_Main Time_Funs Sorting
begin
text \<open>
@@ -17,8 +17,8 @@
lemma replicate_numeral: "replicate (numeral n) x = x # replicate (pred_numeral n) x"
by (simp add: numeral_eq_Suc)
-lemma isort_correct: "isort xs = sort xs"
- using sorted_isort mset_isort by (metis properties_for_sort)
+lemma insort_correct: "insort xs = sort xs"
+ using sorted_insort mset_insort by (metis properties_for_sort)
lemma sum_list_replicate [simp]: "sum_list (replicate n x) = n * x"
by (induction n) auto
@@ -498,13 +498,13 @@
using the naive selection algorithm where we sort the list using insertion sort.
\<close>
definition slow_select where
- "slow_select k xs = isort xs ! k"
+ "slow_select k xs = insort xs ! k"
definition slow_median where
"slow_median xs = slow_select ((length xs - 1) div 2) xs"
lemma slow_select_correct: "slow_select k xs = select k xs"
- by (simp add: slow_select_def select_def isort_correct)
+ by (simp add: slow_select_def select_def insort_correct)
lemma slow_median_correct: "slow_median xs = median xs"
by (simp add: median_def slow_median_def slow_select_correct)
@@ -635,18 +635,18 @@
by (induction x xs rule: T_partition3.induct) auto
definition T_slow_select :: "nat \<Rightarrow> 'a :: linorder list \<Rightarrow> nat" where
- "T_slow_select k xs = T_isort xs + T_nth (isort xs) k + 1"
+ "T_slow_select k xs = T_insort xs + T_nth (insort xs) k + 1"
definition T_slow_median :: "'a :: linorder list \<Rightarrow> nat" where
"T_slow_median xs = T_slow_select ((length xs - 1) div 2) xs + 1"
lemma T_slow_select_le: "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 3"
proof -
- have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (isort xs) + 1) + 1"
+ have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (insort xs) + 1) + 1"
unfolding T_slow_select_def
- by (intro add_mono T_isort_length) (auto simp: T_nth_eq)
+ by (intro add_mono T_insort_length) (auto simp: T_nth_eq)
also have "\<dots> = length xs ^ 2 + 3 * length xs + 3"
- by (simp add: isort_correct algebra_simps power2_eq_square)
+ by (simp add: insort_correct algebra_simps power2_eq_square)
finally show ?thesis .
qed
--- a/src/HOL/Data_Structures/Sorting.thy Sun Jun 05 20:14:59 2022 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy Sun Jun 05 20:16:48 2022 +0200
@@ -15,40 +15,40 @@
subsection "Insertion Sort"
-fun insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort x [] = [x]" |
-"insort x (y#ys) =
- (if x \<le> y then x#y#ys else y#(insort x ys))"
+fun insort1 :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort1 x [] = [x]" |
+"insort1 x (y#ys) =
+ (if x \<le> y then x#y#ys else y#(insort1 x ys))"
-fun isort :: "'a::linorder list \<Rightarrow> 'a list" where
-"isort [] = []" |
-"isort (x#xs) = insort x (isort xs)"
+fun insort :: "'a::linorder list \<Rightarrow> 'a list" where
+"insort [] = []" |
+"insort (x#xs) = insort1 x (insort xs)"
subsubsection "Functional Correctness"
-lemma mset_insort: "mset (insort x xs) = {#x#} + mset xs"
+lemma mset_insort1: "mset (insort1 x xs) = {#x#} + mset xs"
apply(induction xs)
apply auto
done
-lemma mset_isort: "mset (isort xs) = mset xs"
+lemma mset_insort: "mset (insort xs) = mset xs"
apply(induction xs)
apply simp
-apply (simp add: mset_insort)
+apply (simp add: mset_insort1)
done
-lemma set_insort: "set (insort x xs) = {x} \<union> set xs"
-by(simp add: mset_insort flip: set_mset_mset)
+lemma set_insort1: "set (insort1 x xs) = {x} \<union> set xs"
+by(simp add: mset_insort1 flip: set_mset_mset)
-lemma sorted_insort: "sorted (insort a xs) = sorted xs"
+lemma sorted_insort1: "sorted (insort1 a xs) = sorted xs"
apply(induction xs)
-apply(auto simp add: set_insort)
+apply(auto simp add: set_insort1)
done
-lemma sorted_isort: "sorted (isort xs)"
+lemma sorted_insort: "sorted (insort xs)"
apply(induction xs)
-apply(auto simp: sorted_insort)
+apply(auto simp: sorted_insort1)
done
@@ -57,49 +57,49 @@
text \<open>We count the number of function calls.\<close>
text\<open>
-\<open>insort x [] = [x]\<close>
-\<open>insort x (y#ys) =
- (if x \<le> y then x#y#ys else y#(insort x ys))\<close>
+\<open>insort1 x [] = [x]\<close>
+\<open>insort1 x (y#ys) =
+ (if x \<le> y then x#y#ys else y#(insort1 x ys))\<close>
\<close>
-fun T_insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where
-"T_insort x [] = 1" |
-"T_insort x (y#ys) =
- (if x \<le> y then 0 else T_insort x ys) + 1"
+fun T_insort1 :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where
+"T_insort1 x [] = 1" |
+"T_insort1 x (y#ys) =
+ (if x \<le> y then 0 else T_insort1 x ys) + 1"
text\<open>
-\<open>isort [] = []\<close>
-\<open>isort (x#xs) = insort x (isort xs)\<close>
+\<open>insort [] = []\<close>
+\<open>insort (x#xs) = insort1 x (insort xs)\<close>
\<close>
-fun T_isort :: "'a::linorder list \<Rightarrow> nat" where
-"T_isort [] = 1" |
-"T_isort (x#xs) = T_isort xs + T_insort x (isort xs) + 1"
+fun T_insort :: "'a::linorder list \<Rightarrow> nat" where
+"T_insort [] = 1" |
+"T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1"
-lemma T_insort_length: "T_insort x xs \<le> length xs + 1"
+lemma T_insort1_length: "T_insort1 x xs \<le> length xs + 1"
apply(induction xs)
apply auto
done
-lemma length_insort: "length (insort x xs) = length xs + 1"
+lemma length_insort1: "length (insort1 x xs) = length xs + 1"
apply(induction xs)
apply auto
done
-lemma length_isort: "length (isort xs) = length xs"
+lemma length_insort: "length (insort xs) = length xs"
apply(induction xs)
-apply (auto simp: length_insort)
+apply (auto simp: length_insort1)
done
-lemma T_isort_length: "T_isort xs \<le> (length xs + 1) ^ 2"
+lemma T_insort_length: "T_insort xs \<le> (length xs + 1) ^ 2"
proof(induction xs)
case Nil show ?case by simp
next
case (Cons x xs)
- have "T_isort (x#xs) = T_isort xs + T_insort x (isort xs) + 1" by simp
- also have "\<dots> \<le> (length xs + 1) ^ 2 + T_insort x (isort xs) + 1"
+ have "T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1" by simp
+ also have "\<dots> \<le> (length xs + 1) ^ 2 + T_insort1 x (insort xs) + 1"
using Cons.IH by simp
also have "\<dots> \<le> (length xs + 1) ^ 2 + length xs + 1 + 1"
- using T_insort_length[of x "isort xs"] by (simp add: length_isort)
+ using T_insort1_length[of x "insort xs"] by (simp add: length_insort)
also have "\<dots> \<le> (length(x#xs) + 1) ^ 2"
by (simp add: power2_eq_square)
finally show ?case .
@@ -379,61 +379,65 @@
subsection "Insertion Sort w.r.t. Keys and Stability"
-text \<open>Note that \<^const>\<open>insort_key\<close> is already defined in theory \<^theory>\<open>HOL.List\<close>.
-Thus some of the lemmas are already present as well.\<close>
+hide_const List.insort_key
-fun isort_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"isort_key f [] = []" |
-"isort_key f (x # xs) = insort_key f x (isort_key f xs)"
+fun insort1_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort1_key f x [] = [x]" |
+"insort1_key f x (y # ys) = (if f x \<le> f y then x # y # ys else y # insort1_key f x ys)"
+
+fun insort_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort_key f [] = []" |
+"insort_key f (x # xs) = insort1_key f x (insort_key f xs)"
subsubsection "Standard functional correctness"
-lemma mset_insort_key: "mset (insort_key f x xs) = {#x#} + mset xs"
+lemma mset_insort1_key: "mset (insort1_key f x xs) = {#x#} + mset xs"
by(induction xs) simp_all
-lemma mset_isort_key: "mset (isort_key f xs) = mset xs"
-by(induction xs) (simp_all add: mset_insort_key)
-
-lemma set_isort_key: "set (isort_key f xs) = set xs"
-by (rule mset_eq_setD[OF mset_isort_key])
+lemma mset_insort_key: "mset (insort_key f xs) = mset xs"
+by(induction xs) (simp_all add: mset_insort1_key)
-lemma sorted_insort_key: "sorted (map f (insort_key f a xs)) = sorted (map f xs)"
-by(induction xs)(auto simp: set_insort_key)
+(* Inductive proof simpler than derivation from mset lemma: *)
+lemma set_insort1_key: "set (insort1_key f x xs) = {x} \<union> set xs"
+by (induction xs) auto
-lemma sorted_isort_key: "sorted (map f (isort_key f xs))"
-by(induction xs)(simp_all add: sorted_insort_key)
+lemma sorted_insort1_key: "sorted (map f (insort1_key f a xs)) = sorted (map f xs)"
+by(induction xs)(auto simp: set_insort1_key)
+
+lemma sorted_insort_key: "sorted (map f (insort_key f xs))"
+by(induction xs)(simp_all add: sorted_insort1_key)
subsubsection "Stability"
-lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
+lemma insort1_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort1_key f a xs = a # xs"
by (cases xs) auto
-lemma filter_insort_key_neg:
- "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
+lemma filter_insort1_key_neg:
+ "\<not> P x \<Longrightarrow> filter P (insort1_key f x xs) = filter P xs"
by (induction xs) simp_all
-lemma filter_insort_key_pos:
- "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
-by (induction xs) (auto, subst insort_is_Cons, auto)
+lemma filter_insort1_key_pos:
+ "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort1_key f x xs) = insort1_key f x (filter P xs)"
+by (induction xs) (auto, subst insort1_is_Cons, auto)
-lemma sort_key_stable: "filter (\<lambda>y. f y = k) (isort_key f xs) = filter (\<lambda>y. f y = k) xs"
+lemma sort_key_stable: "filter (\<lambda>y. f y = k) (insort_key f xs) = filter (\<lambda>y. f y = k) xs"
proof (induction xs)
case Nil thus ?case by simp
next
case (Cons a xs)
thus ?case
proof (cases "f a = k")
- case False thus ?thesis by (simp add: Cons.IH filter_insort_key_neg)
+ case False thus ?thesis by (simp add: Cons.IH filter_insort1_key_neg)
next
case True
- have "filter (\<lambda>y. f y = k) (isort_key f (a # xs))
- = filter (\<lambda>y. f y = k) (insort_key f a (isort_key f xs))" by simp
- also have "\<dots> = insort_key f a (filter (\<lambda>y. f y = k) (isort_key f xs))"
- by (simp add: True filter_insort_key_pos sorted_isort_key)
- also have "\<dots> = insort_key f a (filter (\<lambda>y. f y = k) xs)" by (simp add: Cons.IH)
- also have "\<dots> = a # (filter (\<lambda>y. f y = k) xs)" by(simp add: True insort_is_Cons)
+ have "filter (\<lambda>y. f y = k) (insort_key f (a # xs))
+ = filter (\<lambda>y. f y = k) (insort1_key f a (insort_key f xs))" by simp
+ also have "\<dots> = insort1_key f a (filter (\<lambda>y. f y = k) (insort_key f xs))"
+ by (simp add: True filter_insort1_key_pos sorted_insort_key)
+ also have "\<dots> = insort1_key f a (filter (\<lambda>y. f y = k) xs)" by (simp add: Cons.IH)
+ also have "\<dots> = a # (filter (\<lambda>y. f y = k) xs)" by(simp add: True insort1_is_Cons)
also have "\<dots> = filter (\<lambda>y. f y = k) (a # xs)" by (simp add: True)
finally show ?thesis .
qed
--- a/src/HOL/Relation.thy Sun Jun 05 20:14:59 2022 +0200
+++ b/src/HOL/Relation.thy Sun Jun 05 20:16:48 2022 +0200
@@ -155,8 +155,16 @@
abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close>
where "refl \<equiv> refl_on UNIV"
-definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
- where "reflp r \<longleftrightarrow> (\<forall>x. r x x)"
+definition reflp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+ where "reflp_on A R \<longleftrightarrow> (\<forall>x\<in>A. R x x)"
+
+abbreviation reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+ where "reflp \<equiv> reflp_on UNIV"
+
+lemma reflp_def[no_atp]: "reflp R \<longleftrightarrow> (\<forall>x. R x x)"
+ by (simp add: reflp_on_def)
+
+text \<open>@{thm [source] reflp_def} is for backward compatibility.\<close>
lemma reflp_refl_eq [pred_set_conv]: "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
by (simp add: refl_on_def reflp_def)
@@ -164,6 +172,13 @@
lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
unfolding refl_on_def by (iprover intro!: ballI)
+lemma reflp_onI:
+ "(\<And>x y. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
+ by (simp add: reflp_on_def)
+
+lemma reflpI[intro?]: "(\<And>x. R x x) \<Longrightarrow> reflp R"
+ by (rule reflp_onI)
+
lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r"
unfolding refl_on_def by blast
@@ -173,18 +188,20 @@
lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
unfolding refl_on_def by blast
-lemma reflpI [intro?]: "(\<And>x. r x x) \<Longrightarrow> reflp r"
- by (auto intro: refl_onI simp add: reflp_def)
+lemma reflp_onD:
+ "reflp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> R x x"
+ by (simp add: reflp_on_def)
+
+lemma reflpD[dest?]: "reflp R \<Longrightarrow> R x x"
+ by (simp add: reflp_onD)
lemma reflpE:
assumes "reflp r"
obtains "r x x"
using assms by (auto dest: refl_onD simp add: reflp_def)
-lemma reflpD [dest?]:
- assumes "reflp r"
- shows "r x x"
- using assms by (auto elim: reflpE)
+lemma reflp_on_subset: "reflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> reflp_on B R"
+ by (auto intro: reflp_onI dest: reflp_onD)
lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)"
unfolding refl_on_def by blast
@@ -506,6 +523,12 @@
lemma totalpD: "totalp R \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x"
by (simp add: totalp_onD)
+lemma total_on_subset: "total_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> total_on B r"
+ by (auto simp: total_on_def)
+
+lemma totalp_on_subset: "totalp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> totalp_on B R"
+ by (auto intro: totalp_onI dest: totalp_onD)
+
lemma total_on_empty [simp]: "total_on {} r"
by (simp add: total_on_def)
--- a/src/HOL/Tools/BNF/bnf_util.ML Sun Jun 05 20:14:59 2022 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Sun Jun 05 20:16:48 2022 +0200
@@ -389,7 +389,7 @@
fun mk_pred name R =
Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
-val mk_reflp = mk_pred \<^const_name>\<open>reflp\<close>;
+val mk_reflp = mk_pred \<^const_abbrev>\<open>reflp\<close>;
val mk_symp = mk_pred \<^const_name>\<open>symp\<close>;
val mk_transp = mk_pred \<^const_name>\<open>transp\<close>;
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Sun Jun 05 20:14:59 2022 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun Jun 05 20:16:48 2022 +0200
@@ -758,7 +758,7 @@
handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
in
case reflp_tm of
- Const (\<^const_name>\<open>reflp\<close>, _) $ _ => ()
+ \<^Const_>\<open>reflp_on _ for \<^Const>\<open>top_class.top _\<close> _\<close> => ()
| _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
end