summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Data_Structures/Sorting.thy

changeset 68970 | b0dfe57dfa09 |

parent 68968 | 6c4421b006fb |

child 68971 | 938f4058c07c |

equal
deleted
inserted
replaced

68969:7a9118e63cad | 68970:b0dfe57dfa09 |
---|---|

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))" |