src/HOL/Data_Structures/Selection.thy
changeset 73123 b4066bad7f76
parent 73108 981a383610df
child 73526 a3cc9fa1295d
equal deleted inserted replaced
73122:cd0cd534f927 73123:b4066bad7f76
   671 
   671 
   672 lemma T_chop_le: "T_chop d xs \<le> 5 * length xs + 1"
   672 lemma T_chop_le: "T_chop d xs \<le> 5 * length xs + 1"
   673   by (induction d xs rule: T_chop.induct) (auto simp: T_chop_reduce T_take_eq T_drop_eq)
   673   by (induction d xs rule: T_chop.induct) (auto simp: T_chop_reduce T_take_eq T_drop_eq)
   674 
   674 
   675 text \<open>
   675 text \<open>
   676   The option ‘domintros’ here allows us to explicitly reason about where the function does and
   676   The option \<open>domintros\<close> here allows us to explicitly reason about where the function does and
   677   does not terminate. With this, we can skip the termination proof this time because we can
   677   does not terminate. With this, we can skip the termination proof this time because we can
   678   reuse the one for \<^const>\<open>mom_select\<close>.
   678   reuse the one for \<^const>\<open>mom_select\<close>.
   679 \<close>
   679 \<close>
   680 function (domintros) T_mom_select :: "nat \<Rightarrow> 'a :: linorder list \<Rightarrow> nat" where
   680 function (domintros) T_mom_select :: "nat \<Rightarrow> 'a :: linorder list \<Rightarrow> nat" where
   681   "T_mom_select k xs = (
   681   "T_mom_select k xs = (