# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1588169777 -3600
# Node ID b11d7ffb48e0478a39a98003c02cc1f90bb8fef7
# Parent  7c25e3467cf0ca9e78d0eecc6547b595970a26c9
A little more tidying up

diff -r 7c25e3467cf0 -r b11d7ffb48e0 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Wed Apr 29 13:18:32 2020 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Wed Apr 29 15:16:17 2020 +0100
@@ -244,15 +244,21 @@
 declare enumerate_0 [simp del] enumerate_Suc [simp del]
 
 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
-  apply (induct n arbitrary: S)
-   apply (rule order_le_neq_trans)
-    apply (simp add: enumerate_0 Least_le enumerate_in_set)
-   apply (simp only: enumerate_Suc')
-   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
-    apply (blast intro: sym)
-   apply (simp add: enumerate_in_set del: Diff_iff)
-  apply (simp add: enumerate_Suc')
-  done
+proof (induction n arbitrary: S)
+  case 0
+  then have "enumerate S 0 \<le> enumerate S (Suc 0)"
+    by (simp add: enumerate_0 Least_le enumerate_in_set)
+  moreover have "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}"
+    by (meson "0.prems" enumerate_in_set infinite_remove)
+  then have "enumerate S 0 \<noteq> enumerate (S - {enumerate S 0}) 0"
+    by auto
+  ultimately show ?case
+    by (simp add: enumerate_Suc')
+next
+  case (Suc n)
+  then show ?case 
+    by (simp add: enumerate_Suc')
+qed
 
 lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   by (induct m n rule: less_Suc_induct) (auto intro: enumerate_step)
@@ -330,18 +336,25 @@
   qed
 qed
 
+lemma inj_enumerate:
+  fixes S :: "'a::wellorder set"
+  assumes S: "infinite S"
+  shows "inj (enumerate S)"
+  unfolding inj_on_def
+proof clarsimp
+  show "\<And>x y. enumerate S x = enumerate S y \<Longrightarrow> x = y"
+    by (metis neq_iff enumerate_mono[OF _ \<open>infinite S\<close>]) 
+qed
+
+text \<open>To generalise this, we'd need a condition that all initial segments were finite\<close>
 lemma bij_enumerate:
   fixes S :: "nat set"
   assumes S: "infinite S"
   shows "bij_betw (enumerate S) UNIV S"
 proof -
-  have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
-    using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
-  then have "inj (enumerate S)"
-    by (auto simp: inj_on_def)
-  moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
+  have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
     using enumerate_Ex[OF S] by auto
-  moreover note \<open>infinite S\<close>
+  moreover note \<open>infinite S\<close> inj_enumerate
   ultimately show ?thesis
     unfolding bij_betw_def by (auto intro: enumerate_in_set)
 qed
@@ -374,10 +387,13 @@
     assume "S \<in> \<F>"
     have "{T \<in> \<F>. S \<subseteq> T} = {}"
       if "\<not> (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)"
-      apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
-         apply (use assms that in auto)
-      apply (blast intro: dual_order.trans psubset_imp_subset)
-      done
+    proof -
+      have \<section>: "\<And>x. x \<in> \<F> \<and> S \<subseteq> x \<Longrightarrow> \<exists>y. y \<in> \<F> \<and> S \<subseteq> y \<and> x \<subset> y"
+        using that by (blast intro: dual_order.trans psubset_imp_subset)
+      show ?thesis
+      proof (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
+      qed (use assms in \<open>auto intro: \<section>\<close>)
+    qed
     with \<open>S \<in> \<F>\<close> show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y"
       by blast
   qed
diff -r 7c25e3467cf0 -r b11d7ffb48e0 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Apr 29 13:18:32 2020 +0200
+++ b/src/HOL/List.thy	Wed Apr 29 15:16:17 2020 +0100
@@ -6936,7 +6936,7 @@
 
 
 lemma listrel_eq_len:  "(xs, ys) \<in> listrel r \<Longrightarrow> length xs = length ys"
-by(induct rule: listrel.induct) auto
+  by(induct rule: listrel.induct) auto
 
 lemma listrel_iff_zip [code_unfold]: "(xs,ys) \<in> listrel r \<longleftrightarrow>
   length xs = length ys \<and> (\<forall>(x,y) \<in> set(zip xs ys). (x,y) \<in> r)" (is "?L \<longleftrightarrow> ?R")
@@ -6950,59 +6950,66 @@
 
 lemma listrel_iff_nth: "(xs,ys) \<in> listrel r \<longleftrightarrow>
   length xs = length ys \<and> (\<forall>n < length xs. (xs!n, ys!n) \<in> r)" (is "?L \<longleftrightarrow> ?R")
-by (auto simp add: all_set_conv_all_nth listrel_iff_zip)
-
+  by (auto simp add: all_set_conv_all_nth listrel_iff_zip)
 
 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
   by (meson listrel_iff_nth subrelI subset_eq)
 
-lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
-apply clarify
-apply (erule listrel.induct, auto)
-done
-
-lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)"
-apply (simp add: refl_on_def listrel_subset Ball_def)
-apply (rule allI)
-apply (induct_tac x)
-apply (auto intro: listrel.intros)
-done
+lemma listrel_subset:
+  assumes "r \<subseteq> A \<times> A" shows "listrel r \<subseteq> lists A \<times> lists A"
+proof clarify
+  show "a \<in> lists A \<and> b \<in> lists A" if "(a, b) \<in> listrel r" for a b
+    using that assms by (induction rule: listrel.induct, auto)
+qed
+
+lemma listrel_refl_on:
+  assumes "refl_on A r" shows "refl_on (lists A) (listrel r)"
+proof -
+  have "l \<in> lists A \<Longrightarrow> (l, l) \<in> listrel r" for l
+    using assms unfolding refl_on_def
+    by (induction l, auto intro: listrel.intros)
+  then show ?thesis
+    by (meson assms listrel_subset refl_on_def)
+qed
 
 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
   by (simp add: listrel_iff_nth sym_def)
 
-lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
-apply (simp add: trans_def)
-apply (intro allI)
-apply (rule impI)
-apply (erule listrel.induct)
-apply (blast intro: listrel.intros)+
-done
+lemma listrel_trans:
+  assumes "trans r" shows "trans (listrel r)"
+proof -
+  have "(x, z) \<in> listrel r" if "(x, y) \<in> listrel r" "(y, z) \<in> listrel r" for x y z
+    using that
+  proof induction
+    case (Cons x y xs ys)
+    then show ?case
+      by clarsimp (metis assms listrel.Cons listrel_iff_nth transD)
+  qed auto
+  then show ?thesis
+    using transI by blast
+qed
 
 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
-by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans)
+  by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans)
 
 lemma listrel_rtrancl_refl[iff]: "(xs,xs) \<in> listrel(r\<^sup>*)"
-using listrel_refl_on[of UNIV, OF refl_rtrancl]
-by(auto simp: refl_on_def)
+  using listrel_refl_on[of UNIV, OF refl_rtrancl]
+  by(auto simp: refl_on_def)
 
 lemma listrel_rtrancl_trans:
-  "\<lbrakk>(xs,ys) \<in> listrel(r\<^sup>*);  (ys,zs) \<in> listrel(r\<^sup>*)\<rbrakk>
-  \<Longrightarrow> (xs,zs) \<in> listrel(r\<^sup>*)"
-by (metis listrel_trans trans_def trans_rtrancl)
-
+  "\<lbrakk>(xs,ys) \<in> listrel(r\<^sup>*);  (ys,zs) \<in> listrel(r\<^sup>*)\<rbrakk> \<Longrightarrow> (xs,zs) \<in> listrel(r\<^sup>*)"
+  by (metis listrel_trans trans_def trans_rtrancl)
 
 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
-by (blast intro: listrel.intros)
+  by (blast intro: listrel.intros)
 
 lemma listrel_Cons:
-     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
-by (auto simp add: set_Cons_def intro: listrel.intros)
+  "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
+  by (auto simp add: set_Cons_def intro: listrel.intros)
 
 text \<open>Relating \<^term>\<open>listrel1\<close>, \<^term>\<open>listrel\<close> and closures:\<close>
 
-lemma listrel1_rtrancl_subset_rtrancl_listrel1:
-  "listrel1 (r\<^sup>*) \<subseteq> (listrel1 r)\<^sup>*"
+lemma listrel1_rtrancl_subset_rtrancl_listrel1: "listrel1 (r\<^sup>*) \<subseteq> (listrel1 r)\<^sup>*"
 proof (rule subrelI)
   fix xs ys assume 1: "(xs,ys) \<in> listrel1 (r\<^sup>*)"
   { fix x y us vs
@@ -7017,27 +7024,27 @@
 qed
 
 lemma rtrancl_listrel1_eq_len: "(x,y) \<in> (listrel1 r)\<^sup>* \<Longrightarrow> length x = length y"
-by (induct rule: rtrancl.induct) (auto intro: listrel1_eq_len)
+  by (induct rule: rtrancl.induct) (auto intro: listrel1_eq_len)
 
 lemma rtrancl_listrel1_ConsI1:
   "(xs,ys) \<in> (listrel1 r)\<^sup>* \<Longrightarrow> (x#xs,x#ys) \<in> (listrel1 r)\<^sup>*"
-apply(induct rule: rtrancl.induct)
- apply simp
-by (metis listrel1I2 rtrancl.rtrancl_into_rtrancl)
+proof (induction rule: rtrancl.induct)
+  case (rtrancl_into_rtrancl a b c)
+  then show ?case
+    by (metis listrel1I2 rtrancl.rtrancl_into_rtrancl)
+qed auto
 
 lemma rtrancl_listrel1_ConsI2:
-  "(x,y) \<in> r\<^sup>* \<Longrightarrow> (xs, ys) \<in> (listrel1 r)\<^sup>*
-  \<Longrightarrow> (x # xs, y # ys) \<in> (listrel1 r)\<^sup>*"
-  by (blast intro: rtrancl_trans rtrancl_listrel1_ConsI1
-    subsetD[OF listrel1_rtrancl_subset_rtrancl_listrel1 listrel1I1])
+  "(x,y) \<in> r\<^sup>* \<Longrightarrow> (xs, ys) \<in> (listrel1 r)\<^sup>* \<Longrightarrow> (x # xs, y # ys) \<in> (listrel1 r)\<^sup>*"
+  by (meson in_mono listrel1I1 listrel1_rtrancl_subset_rtrancl_listrel1 rtrancl_listrel1_ConsI1 rtrancl_trans)
 
 lemma listrel1_subset_listrel:
   "r \<subseteq> r' \<Longrightarrow> refl r' \<Longrightarrow> listrel1 r \<subseteq> listrel(r')"
-by(auto elim!: listrel1E simp add: listrel_iff_zip set_zip refl_on_def)
+  by(auto elim!: listrel1E simp add: listrel_iff_zip set_zip refl_on_def)
 
 lemma listrel_reflcl_if_listrel1:
   "(xs,ys) \<in> listrel1 r \<Longrightarrow> (xs,ys) \<in> listrel(r\<^sup>*)"
-by(erule listrel1E)(auto simp add: listrel_iff_zip set_zip)
+  by(erule listrel1E)(auto simp add: listrel_iff_zip set_zip)
 
 lemma listrel_rtrancl_eq_rtrancl_listrel1: "listrel (r\<^sup>*) = (listrel1 r)\<^sup>*"
 proof
@@ -7062,37 +7069,37 @@
 
 lemma rtrancl_listrel1_if_listrel:
   "(xs,ys) \<in> listrel r \<Longrightarrow> (xs,ys) \<in> (listrel1 r)\<^sup>*"
-by(metis listrel_rtrancl_eq_rtrancl_listrel1 subsetD[OF listrel_mono] r_into_rtrancl subsetI)
+  by(metis listrel_rtrancl_eq_rtrancl_listrel1 subsetD[OF listrel_mono] r_into_rtrancl subsetI)
 
 lemma listrel_subset_rtrancl_listrel1: "listrel r \<subseteq> (listrel1 r)\<^sup>*"
-by(fast intro:rtrancl_listrel1_if_listrel)
+  by(fast intro:rtrancl_listrel1_if_listrel)
 
 
 subsection \<open>Size function\<close>
 
 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_list f)"
-by (rule is_measure_trivial)
+  by (rule is_measure_trivial)
 
 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_option f)"
-by (rule is_measure_trivial)
+  by (rule is_measure_trivial)
 
 lemma size_list_estimation[termination_simp]:
   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < size_list f xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma size_list_estimation'[termination_simp]:
   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> size_list f xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma size_list_map[simp]: "size_list f (map g xs) = size_list (f \<circ> g) xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma size_list_append[simp]: "size_list f (xs @ ys) = size_list f xs + size_list f ys"
-by (induct xs, auto)
+  by (induct xs, auto)
 
 lemma size_list_pointwise[termination_simp]:
   "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> size_list f xs \<le> size_list g xs"
-by (induct xs) force+
+  by (induct xs) force+
 
 
 subsection \<open>Monad operation\<close>
@@ -7868,12 +7875,20 @@
 
 lemma lists_transfer [transfer_rule]:
   "(rel_set A ===> rel_set (list_all2 A)) lists lists"
-  apply (rule rel_funI, rule rel_setI)
-  apply (erule lists.induct, simp)
-  apply (simp only: rel_set_def list_all2_Cons1, metis lists.Cons)
-  apply (erule lists.induct, simp)
-  apply (simp only: rel_set_def list_all2_Cons2, metis lists.Cons)
-  done
+proof (rule rel_funI, rule rel_setI)
+  show "\<lbrakk>l \<in> lists X; rel_set A X Y\<rbrakk> \<Longrightarrow> \<exists>y\<in>lists Y. list_all2 A l y" for X Y l
+  proof (induction l rule: lists.induct)
+    case (Cons a l)
+    then show ?case
+      by (simp only: rel_set_def list_all2_Cons1, metis lists.Cons)
+  qed auto
+  show "\<lbrakk>l \<in> lists Y; rel_set A X Y\<rbrakk> \<Longrightarrow> \<exists>x\<in>lists X. list_all2 A x l" for X Y l
+  proof (induction l rule: lists.induct)
+    case (Cons a l)
+    then show ?case
+      by (simp only: rel_set_def list_all2_Cons2, metis lists.Cons)
+  qed auto
+qed
 
 lemma set_Cons_transfer [transfer_rule]:
   "(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))