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

src/HOL/ex/Sorting.ML

author | paulson |

Mon, 20 Mar 2000 10:32:02 +0100 | |

changeset 8525 | 209eb2db72e6 |

parent 8415 | 852c63072334 |

child 12486 | 0ed8bdd883e0 |

permissions | -rw-r--r-- |

renamed a variable to avoid possible free/bound confusion

(* Title: HOL/ex/sorting.ML ID: $Id$ Author: Tobias Nipkow Copyright 1994 TU Muenchen Some general lemmas *) Goal "multiset (xs@ys) x = multiset xs x + multiset ys x"; by (induct_tac "xs" 1); by Auto_tac; qed "multiset_append"; Goal "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z"; by (induct_tac "xs" 1); by Auto_tac; qed "multiset_compl_add"; Addsimps [multiset_append, multiset_compl_add]; Goal "set xs = {x. multiset xs x ~= 0}"; by (induct_tac "xs" 1); by Auto_tac; qed "set_via_multiset"; (* Equivalence of two definitions of `sorted' *) Goal "transf(le) ==> sorted1 le xs = sorted le xs"; by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split]))); by (rewrite_goals_tac [transf_def]); by (Blast_tac 1); qed "sorted1_is_sorted"; Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ \ (ALL x:set xs. ALL y:set ys. le x y))"; by (induct_tac "xs" 1); by Auto_tac; qed "sorted_append"; Addsimps [sorted_append];