--- a/src/HOL/Fun.thy Tue Feb 13 16:03:55 2024 +0100
+++ b/src/HOL/Fun.thy Tue Feb 13 17:18:57 2024 +0000
@@ -395,6 +395,11 @@
lemma bij_betw_comp_iff: "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
by (auto simp add: bij_betw_def inj_on_def)
+lemma bij_betw_Collect:
+ assumes "bij_betw f A B" "\<And>x. x \<in> A \<Longrightarrow> Q (f x) \<longleftrightarrow> P x"
+ shows "bij_betw f {x\<in>A. P x} {y\<in>B. Q y}"
+ using assms by (auto simp add: bij_betw_def inj_on_def)
+
lemma bij_betw_comp_iff2:
assumes bij: "bij_betw f' A' A''"
and img: "f ` A \<le> A'"
--- a/src/HOL/Fun_Def.thy Tue Feb 13 16:03:55 2024 +0100
+++ b/src/HOL/Fun_Def.thy Tue Feb 13 17:18:57 2024 +0000
@@ -304,7 +304,7 @@
done
-subsection \<open>Yet another induction principle on the natural numbers\<close>
+subsection \<open>Yet more induction principles on the natural numbers\<close>
lemma nat_descend_induct [case_names base descend]:
fixes P :: "nat \<Rightarrow> bool"
@@ -313,6 +313,13 @@
shows "P m"
using assms by induction_schema (force intro!: wf_measure [of "\<lambda>k. Suc n - k"])+
+lemma induct_nat_012[case_names 0 1 ge2]:
+ "P 0 \<Longrightarrow> P (Suc 0) \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))) \<Longrightarrow> P n"
+proof (induction_schema, pat_completeness)
+ show "wf (Wellfounded.measure id)"
+ by simp
+qed auto
+
subsection \<open>Tool setup\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Infinite_Typeclass.thy Tue Feb 13 17:18:57 2024 +0000
@@ -0,0 +1,47 @@
+(* Title: HOL/Library/Infinite_Typeclass.thy
+*)
+
+section \<open>Infinite Type Class\<close>
+text \<open>The type class of infinite sets (orginally from the Incredible Proof Machine)\<close>
+
+theory Infinite_Typeclass
+ imports Complex_Main
+begin
+
+class infinite =
+ assumes infinite_UNIV: "infinite (UNIV::'a set)"
+
+instance nat :: infinite
+ by (intro_classes) simp
+
+instance int :: infinite
+ by (intro_classes) simp
+
+instance rat :: infinite
+proof
+ show "infinite (UNIV::rat set)"
+ by (simp add: infinite_UNIV_char_0)
+qed
+
+instance real :: infinite
+proof
+ show "infinite (UNIV::real set)"
+ by (simp add: infinite_UNIV_char_0)
+qed
+
+instance complex :: infinite
+proof
+ show "infinite (UNIV::complex set)"
+ by (simp add: infinite_UNIV_char_0)
+qed
+
+instance option :: (infinite) infinite
+ by intro_classes (simp add: infinite_UNIV)
+
+instance prod :: (infinite, type) infinite
+ by intro_classes (simp add: finite_prod infinite_UNIV)
+
+instance list :: (type) infinite
+ by intro_classes (simp add: infinite_UNIV_listI)
+
+end
--- a/src/HOL/Library/Library.thy Tue Feb 13 16:03:55 2024 +0100
+++ b/src/HOL/Library/Library.thy Tue Feb 13 17:18:57 2024 +0000
@@ -41,6 +41,7 @@
Groups_Big_Fun
Indicator_Function
Infinite_Set
+ Infinite_Typeclass
Interval
Interval_Float
IArray
--- a/src/HOL/List.thy Tue Feb 13 16:03:55 2024 +0100
+++ b/src/HOL/List.thy Tue Feb 13 17:18:57 2024 +0000
@@ -4118,6 +4118,21 @@
successively P (remdups_adj xs) \<longleftrightarrow> successively P xs"
by (induction xs rule: remdups_adj.induct)(auto simp: successively_Cons)
+lemma successively_conv_nth:
+ "successively P xs \<longleftrightarrow> (\<forall>i. Suc i < length xs \<longrightarrow> P (xs ! i) (xs ! Suc i))"
+ by (induction P xs rule: successively.induct)
+ (force simp: nth_Cons split: nat.splits)+
+
+lemma successively_nth: "successively P xs \<Longrightarrow> Suc i < length xs \<Longrightarrow> P (xs ! i) (xs ! Suc i)"
+ unfolding successively_conv_nth by blast
+
+lemma distinct_adj_conv_nth:
+ "distinct_adj xs \<longleftrightarrow> (\<forall>i. Suc i < length xs \<longrightarrow> xs ! i \<noteq> xs ! Suc i)"
+ by (simp add: distinct_adj_def successively_conv_nth)
+
+lemma distinct_adj_nth: "distinct_adj xs \<Longrightarrow> Suc i < length xs \<Longrightarrow> xs ! i \<noteq> xs ! Suc i"
+ unfolding distinct_adj_conv_nth by blast
+
lemma remdups_adj_Cons':
"remdups_adj (x # xs) = x # remdups_adj (dropWhile (\<lambda>y. y = x) xs)"
by (induction xs) auto
@@ -4163,6 +4178,34 @@
\<Longrightarrow> remdups_adj (xs @ ys) = remdups_adj xs @ remdups_adj (dropWhile (\<lambda>y. y = last xs) ys)"
by (induction xs rule: remdups_adj.induct) (auto simp: remdups_adj_Cons')
+lemma remdups_filter_last:
+ "last [x\<leftarrow>remdups xs. P x] = last [x\<leftarrow>xs. P x]"
+by (induction xs, auto simp: filter_empty_conv)
+
+lemma remdups_append:
+ "set xs \<subseteq> set ys \<Longrightarrow> remdups (xs @ ys) = remdups ys"
+ by (induction xs, simp_all)
+
+lemma remdups_concat:
+ "remdups (concat (remdups xs)) = remdups (concat xs)"
+proof (induction xs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs)
+ show ?case
+ proof (cases "a \<in> set xs")
+ case True
+ then have "remdups (concat xs) = remdups (a @ concat xs)"
+ by (metis remdups_append concat.simps(2) insert_absorb set_simps(2) set_append set_concat sup_ge1)
+ then show ?thesis
+ by (simp add: Cons True)
+ next
+ case False
+ then show ?thesis
+ by (metis Cons remdups_append2 concat.simps(2) remdups.simps(2))
+ qed
+qed
subsection \<open>@{const distinct_adj}\<close>
@@ -4213,6 +4256,14 @@
lemma distinct_adj_map_iff: "inj_on f (set xs) \<Longrightarrow> distinct_adj (map f xs) \<longleftrightarrow> distinct_adj xs"
using distinct_adj_mapD distinct_adj_mapI by blast
+lemma distinct_adj_conv_length_remdups_adj:
+ "distinct_adj xs \<longleftrightarrow> length (remdups_adj xs) = length xs"
+proof (induction xs rule: remdups_adj.induct)
+ case (3 x y xs)
+ thus ?case
+ using remdups_adj_length[of "y # xs"] by auto
+qed auto
+
subsubsection \<open>\<^const>\<open>insert\<close>\<close>
@@ -4379,33 +4430,32 @@
lemma length_remove1:
"length(remove1 x xs) = (if x \<in> set xs then length xs - 1 else length xs)"
-by (induct xs) (auto dest!:length_pos_if_in_set)
+ by (induct xs) (auto dest!:length_pos_if_in_set)
lemma remove1_filter_not[simp]:
"\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
-by(induct xs) auto
+ by(induct xs) auto
lemma filter_remove1:
"filter Q (remove1 x xs) = remove1 x (filter Q xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma notin_set_remove1[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(remove1 y xs)"
-by(insert set_remove1_subset) fast
+ by(insert set_remove1_subset) fast
lemma distinct_remove1[simp]: "distinct xs \<Longrightarrow> distinct(remove1 x xs)"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma remove1_remdups:
"distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma remove1_idem: "x \<notin> set xs \<Longrightarrow> remove1 x xs = xs"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma remove1_split:
"a \<in> set xs \<Longrightarrow> remove1 a xs = ys \<longleftrightarrow> (\<exists>ls rs. xs = ls @ a # rs \<and> a \<notin> set ls \<and> ys = ls @ rs)"
-by (metis remove1.simps(2) remove1_append split_list_first)
-
+ by (metis remove1.simps(2) remove1_append split_list_first)
subsubsection \<open>\<^const>\<open>removeAll\<close>\<close>