src/HOL/Data_Structures/Sorting.thy
changeset 68968 6c4421b006fb
parent 68967 cd32e6b34b5c
child 68970 b0dfe57dfa09
equal deleted inserted replaced
68967:cd32e6b34b5c 68968:6c4421b006fb
   275 
   275 
   276 lemma mset_merge_all:
   276 lemma mset_merge_all:
   277   "xss \<noteq> [] \<Longrightarrow> mset (merge_all xss) = (\<Union># (mset (map mset xss)))"
   277   "xss \<noteq> [] \<Longrightarrow> mset (merge_all xss) = (\<Union># (mset (map mset xss)))"
   278 by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
   278 by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
   279 
   279 
       
   280 lemma mset_msort_bu: "mset (msort_bu xs) = mset xs"
       
   281 by(simp add: msort_bu_def mset_merge_all comp_def)
       
   282 
   280 lemma sorted_merge_adj:
   283 lemma sorted_merge_adj:
   281   "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs"
   284   "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs"
   282 by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge)
   285 by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge)
   283 
   286 
   284 lemma sorted_merge_all:
   287 lemma sorted_merge_all:
   286 apply(induction xss rule: merge_all.induct)
   289 apply(induction xss rule: merge_all.induct)
   287 using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj)
   290 using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj)
   288 
   291 
   289 lemma sorted_msort_bu: "sorted (msort_bu xs)"
   292 lemma sorted_msort_bu: "sorted (msort_bu xs)"
   290 by(simp add: msort_bu_def sorted_merge_all)
   293 by(simp add: msort_bu_def sorted_merge_all)
   291 
       
   292 lemma mset_msort_bu: "mset (msort_bu xs) = mset xs"
       
   293 by(simp add: msort_bu_def mset_merge_all comp_def)
       
   294 
   294 
   295 
   295 
   296 subsubsection "Time Complexity"
   296 subsubsection "Time Complexity"
   297 
   297 
   298 fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where
   298 fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where