22 *) |
22 *) |
23 |
23 |
24 |
24 |
25 Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); |
25 Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); |
26 |
26 |
27 goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x"; |
27 Goal "!x. mset (qsort le xs) x = mset xs x"; |
28 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
28 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
29 by (ALLGOALS Asm_simp_tac); |
29 by (ALLGOALS Asm_simp_tac); |
30 qed "qsort_permutes"; |
30 qed "qsort_permutes"; |
31 |
31 |
32 goal Qsort.thy "set(qsort le xs) = set xs"; |
32 Goal "set(qsort le xs) = set xs"; |
33 by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1); |
33 by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1); |
34 qed "set_qsort"; |
34 qed "set_qsort"; |
35 Addsimps [set_qsort]; |
35 Addsimps [set_qsort]; |
36 |
36 |
37 goal List.thy |
37 goal List.thy |
39 by (list.induct_tac "xs" 1); |
39 by (list.induct_tac "xs" 1); |
40 by (ALLGOALS Asm_simp_tac); |
40 by (ALLGOALS Asm_simp_tac); |
41 qed"Ball_set_filter"; |
41 qed"Ball_set_filter"; |
42 Addsimps [Ball_set_filter]; |
42 Addsimps [Ball_set_filter]; |
43 |
43 |
44 goal Qsort.thy |
44 Goal |
45 "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
45 "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
46 \ (!x:set xs. !y:set ys. le x y))"; |
46 \ (!x:set xs. !y:set ys. le x y))"; |
47 by (list.induct_tac "xs" 1); |
47 by (list.induct_tac "xs" 1); |
48 by (ALLGOALS Asm_simp_tac); |
48 by (ALLGOALS Asm_simp_tac); |
49 qed "sorted_append"; |
49 qed "sorted_append"; |
50 Addsimps [sorted_append]; |
50 Addsimps [sorted_append]; |
51 |
51 |
52 goal Qsort.thy |
52 Goal |
53 "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
53 "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
54 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
54 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
55 by (ALLGOALS Asm_simp_tac); |
55 by (ALLGOALS Asm_simp_tac); |
56 by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
56 by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
57 by (Fast_tac 1); |
57 by (Fast_tac 1); |