# HG changeset patch
# User paulson
# Date 1707844737 0
# Node ID 66cbd1ef0db19ef4a3b383373d05f8acec99273c
# Parent  f933e915362456c2b377162e89439b8e568fac7b# Parent  76a1c0ea67774778cbdbffa95f04d3c0a39f4818
merged

diff -r f933e9153624 -r 66cbd1ef0db1 src/HOL/Fun.thy
--- 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'"
diff -r f933e9153624 -r 66cbd1ef0db1 src/HOL/Fun_Def.thy
--- 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>
 
diff -r f933e9153624 -r 66cbd1ef0db1 src/HOL/Library/Infinite_Typeclass.thy
--- /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
diff -r f933e9153624 -r 66cbd1ef0db1 src/HOL/Library/Library.thy
--- 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
diff -r f933e9153624 -r 66cbd1ef0db1 src/HOL/List.thy
--- 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>