src/HOL/Data_Structures/Sorting.thy
 changeset 68970 b0dfe57dfa09 parent 68968 6c4421b006fb child 68971 938f4058c07c
equal inserted replaced
`   257 text \<open>For the termination proof of \<open>merge_all\<close> below.\<close>`
`   257 text \<open>For the termination proof of \<open>merge_all\<close> below.\<close>`
`   258 lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2"`
`   258 lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2"`
`   259 by (induction xs rule: merge_adj.induct) auto`
`   259 by (induction xs rule: merge_adj.induct) auto`
`   260 `
`   260 `
`   261 fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where`
`   261 fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where`
`   262 "merge_all [] = undefined" |`
`   262 "merge_all [] = []" |`
`   263 "merge_all [xs] = xs" |`
`   263 "merge_all [xs] = xs" |`
`   264 "merge_all xss = merge_all (merge_adj xss)"`
`   264 "merge_all xss = merge_all (merge_adj xss)"`
`   265 `
`   265 `
`   266 definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where`
`   266 definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where`
`   267 "msort_bu xs = (if xs = [] then [] else merge_all (map (\<lambda>x. [x]) xs))"`
`   267 "msort_bu xs = (if xs = [] then [] else merge_all (map (\<lambda>x. [x]) xs))"`