|
1 (* Title: HOL/ex/Perm.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 |
|
6 Permutations: example of an inductive definition |
|
7 *) |
|
8 |
|
9 (*It would be nice to prove |
|
10 xs <~~> ys = (!x. count xs x = count ys x) |
|
11 See mset on HOL/ex/Sorting.thy |
|
12 *) |
|
13 |
|
14 open Perm; |
|
15 |
|
16 goal Perm.thy "l <~~> l"; |
|
17 by (list.induct_tac "l" 1); |
|
18 by (REPEAT (ares_tac perm.intrs 1)); |
|
19 qed "perm_refl"; |
|
20 |
|
21 |
|
22 (** Some examples of rule induction on permutations **) |
|
23 |
|
24 (*The form of the premise lets the induction bind xs and ys.*) |
|
25 goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]"; |
|
26 by (etac perm.induct 1); |
|
27 by (ALLGOALS Asm_simp_tac); |
|
28 qed "perm_Nil_lemma"; |
|
29 |
|
30 (*A more general version is actually easier to understand!*) |
|
31 goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)"; |
|
32 by (etac perm.induct 1); |
|
33 by (ALLGOALS Asm_simp_tac); |
|
34 qed "perm_length"; |
|
35 |
|
36 goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs"; |
|
37 by (etac perm.induct 1); |
|
38 by (REPEAT (ares_tac perm.intrs 1)); |
|
39 qed "perm_sym"; |
|
40 |
|
41 goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys"; |
|
42 by (etac perm.induct 1); |
|
43 by (Fast_tac 4); |
|
44 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); |
|
45 val perm_mem_lemma = result(); |
|
46 |
|
47 bind_thm ("perm_mem", perm_mem_lemma RS mp); |
|
48 |
|
49 (** Ways of making new permutations **) |
|
50 |
|
51 (*We can insert the head anywhere in the list*) |
|
52 goal Perm.thy "a # xs @ ys <~~> xs @ a # ys"; |
|
53 by (list.induct_tac "xs" 1); |
|
54 by (simp_tac (!simpset addsimps [perm_refl]) 1); |
|
55 by (Simp_tac 1); |
|
56 by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1); |
|
57 qed "perm_append_Cons"; |
|
58 |
|
59 (*single steps |
|
60 by (rtac perm.trans 1); |
|
61 by (rtac perm.swap 1); |
|
62 by (rtac perm.Cons 1); |
|
63 *) |
|
64 |
|
65 goal Perm.thy "xs@ys <~~> ys@xs"; |
|
66 by (list.induct_tac "xs" 1); |
|
67 by (simp_tac (!simpset addsimps [perm_refl]) 1); |
|
68 by (Simp_tac 1); |
|
69 by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1); |
|
70 qed "perm_append_swap"; |
|
71 |
|
72 |
|
73 goal Perm.thy "a # xs <~~> xs @ [a]"; |
|
74 by (rtac perm.trans 1); |
|
75 by (rtac perm_append_swap 2); |
|
76 by (simp_tac (!simpset addsimps [perm_refl]) 1); |
|
77 qed "perm_append_single"; |
|
78 |
|
79 goal Perm.thy "rev xs <~~> xs"; |
|
80 by (list.induct_tac "xs" 1); |
|
81 by (simp_tac (!simpset addsimps [perm_refl]) 1); |
|
82 by (Simp_tac 1); |
|
83 by (rtac (perm_append_single RS perm_sym RS perm.trans) 1); |
|
84 by (etac perm.Cons 1); |
|
85 qed "perm_rev"; |
|
86 |
|
87 goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys"; |
|
88 by (list.induct_tac "l" 1); |
|
89 by (Simp_tac 1); |
|
90 by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1); |
|
91 qed "perm_append1"; |
|
92 |
|
93 goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l"; |
|
94 by (rtac (perm_append_swap RS perm.trans) 1); |
|
95 by (etac (perm_append1 RS perm.trans) 1); |
|
96 by (rtac perm_append_swap 1); |
|
97 qed "perm_append2"; |
|
98 |