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