author | wenzelm |
Fri, 15 Dec 2000 17:59:30 +0100 | |
changeset 10680 | 26e4aecf3207 |
parent 9747 | 043098ba5098 |
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 |
|
8527 | 9 |
(*It would be nice to prove (for "multiset", defined on HOL/ex/Sorting.thy) |
10 |
xs <~~> ys = (ALL x. multiset xs x = multiset ys x) |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
11 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
|
8527 | 13 |
AddIs perm.intrs; |
14 |
||
5069 | 15 |
Goal "l <~~> l"; |
5184 | 16 |
by (induct_tac "l" 1); |
8527 | 17 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
qed "perm_refl"; |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
19 |
AddIffs [perm_refl]; |
3120
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 |
(** Some examples of rule induction on permutations **) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
23 |
(*The form of the premise lets the induction bind xs and ys.*) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
24 |
Goal "xs <~~> ys ==> xs=[] --> ys=[]"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
25 |
by (etac perm.induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
26 |
by (ALLGOALS Asm_simp_tac); |
8527 | 27 |
bind_thm ("xperm_empty_imp", (* [] <~~> ys ==> ys=[] *) |
28 |
[refl, result()] MRS rev_mp); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
29 |
|
8527 | 30 |
(*This more general theorem is easier to understand!*) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
31 |
Goal "xs <~~> ys ==> length(xs) = length(ys)"; |
3120
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 |
|
8527 | 36 |
Goal "[] <~~> xs ==> xs=[]"; |
37 |
by (dtac perm_length 1); |
|
38 |
by Auto_tac; |
|
39 |
qed "perm_empty_imp"; |
|
40 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
41 |
Goal "xs <~~> ys ==> ys <~~> xs"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
42 |
by (etac perm.induct 1); |
8527 | 43 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
44 |
qed "perm_sym"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
45 |
|
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
46 |
Goal "xs <~~> ys ==> x mem xs --> x mem ys"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
47 |
by (etac perm.induct 1); |
8527 | 48 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
49 |
val perm_mem_lemma = result(); |
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 |
bind_thm ("perm_mem", perm_mem_lemma RS mp); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
52 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
53 |
(** Ways of making new permutations **) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
54 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
55 |
(*We can insert the head anywhere in the list*) |
5069 | 56 |
Goal "a # xs @ ys <~~> xs @ a # ys"; |
5184 | 57 |
by (induct_tac "xs" 1); |
8527 | 58 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
59 |
qed "perm_append_Cons"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
60 |
|
5069 | 61 |
Goal "xs@ys <~~> ys@xs"; |
5184 | 62 |
by (induct_tac "xs" 1); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
63 |
by (ALLGOALS Simp_tac); |
8527 | 64 |
by (blast_tac (claset() addIs [perm_append_Cons]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
65 |
qed "perm_append_swap"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
66 |
|
5069 | 67 |
Goal "a # xs <~~> xs @ [a]"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
68 |
by (rtac perm.trans 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
69 |
by (rtac perm_append_swap 2); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
70 |
by (Simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
71 |
qed "perm_append_single"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
72 |
|
5069 | 73 |
Goal "rev xs <~~> xs"; |
5184 | 74 |
by (induct_tac "xs" 1); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
75 |
by (ALLGOALS Simp_tac); |
8527 | 76 |
by (blast_tac (claset() addIs [perm_sym, perm_append_single]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
77 |
qed "perm_rev"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
78 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
79 |
Goal "xs <~~> ys ==> l@xs <~~> l@ys"; |
5184 | 80 |
by (induct_tac "l" 1); |
8527 | 81 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
82 |
qed "perm_append1"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
83 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
84 |
Goal "xs <~~> ys ==> xs@l <~~> ys@l"; |
8527 | 85 |
by (blast_tac (claset() addSIs [perm_append_swap, perm_append1]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
86 |
qed "perm_append2"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
87 |
|
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
88 |
(** Further results mostly by Thomas Marthedal Rasmussen **) |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
89 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
90 |
Goal "([] <~~> xs) = (xs = [])"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
91 |
by (blast_tac (claset() addIs [perm_empty_imp]) 1); |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
92 |
qed "perm_empty"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
93 |
AddIffs [perm_empty]; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
94 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
95 |
Goal "(xs <~~> []) = (xs = [])"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
96 |
by Auto_tac; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
97 |
by (etac (perm_sym RS perm_empty_imp) 1); |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
98 |
qed "perm_empty2"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
99 |
AddIffs [perm_empty2]; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
100 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
101 |
Goal "ys <~~> xs ==> xs=[y] --> ys=[y]"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
102 |
by (etac perm.induct 1); |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
103 |
by Auto_tac; |
8413 | 104 |
qed_spec_mp "perm_sing_imp"; |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
105 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
106 |
Goal "(ys <~~> [y]) = (ys = [y])"; |
8413 | 107 |
by (blast_tac (claset() addIs [perm_sing_imp]) 1); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
108 |
qed "perm_sing_eq"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
109 |
AddIffs [perm_sing_eq]; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
110 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
111 |
Goal "([y] <~~> ys) = (ys = [y])"; |
8527 | 112 |
by (blast_tac (claset() addDs [perm_sym]) 1); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
113 |
qed "perm_sing_eq2"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
114 |
AddIffs [perm_sing_eq2]; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
115 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
116 |
Goal "x:set ys --> ys <~~> x#(remove x ys)"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
117 |
by (induct_tac "ys" 1); |
8527 | 118 |
by Auto_tac; |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
119 |
qed_spec_mp "perm_remove"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
120 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
121 |
Goal "remove x (remove y l) = remove y (remove x l)"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
122 |
by (induct_tac "l" 1); |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
123 |
by Auto_tac; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
124 |
qed "remove_commute"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
125 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
126 |
(*Congruence rule*) |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
127 |
Goal "xs <~~> ys ==> remove z xs <~~> remove z ys"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
128 |
by (etac perm.induct 1); |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
129 |
by Auto_tac; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
130 |
qed "perm_remove_perm"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
131 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
132 |
Goal "remove z (z#xs) = xs"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
133 |
by Auto_tac; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
134 |
qed "remove_hd"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
135 |
Addsimps [remove_hd]; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
136 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
137 |
Goal "z#xs <~~> z#ys ==> xs <~~> ys"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
138 |
by (dres_inst_tac [("z","z")] perm_remove_perm 1); |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
139 |
by Auto_tac; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
140 |
qed "cons_perm_imp_perm"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
141 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
142 |
Goal "(z#xs <~~> z#ys) = (xs <~~> ys)"; |
8527 | 143 |
by (blast_tac (claset() addIs [cons_perm_imp_perm]) 1); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
144 |
qed "cons_perm_eq"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
145 |
AddIffs [cons_perm_eq]; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
146 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
147 |
Goal "ALL xs ys. zs@xs <~~> zs@ys --> xs <~~> ys"; |
9747 | 148 |
by (rev_induct_tac "zs" 1); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
149 |
by (ALLGOALS Full_simp_tac); |
8527 | 150 |
by (Blast_tac 1); |
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
151 |
qed_spec_mp "append_perm_imp_perm"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
152 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
153 |
Goal "(zs@xs <~~> zs@ys) = (xs <~~> ys)"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
154 |
by (blast_tac (claset() addIs [append_perm_imp_perm, perm_append1]) 1); |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
155 |
qed "perm_append1_eq"; |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
5223
diff
changeset
|
156 |
AddIffs [perm_append1_eq]; |
8413 | 157 |
|
158 |
Goal "(xs@zs <~~> ys@zs) = (xs <~~> ys)"; |
|
159 |
by (safe_tac (claset() addSIs [perm_append2])); |
|
160 |
by (rtac append_perm_imp_perm 1); |
|
161 |
by (rtac (perm_append_swap RS perm.trans) 1); |
|
8527 | 162 |
(*The previous step helps this blast_tac call succeed quickly.*) |
163 |
by (blast_tac (claset() addIs [perm_append_swap]) 1); |
|
8413 | 164 |
qed "perm_append2_eq"; |
165 |
AddIffs [perm_append2_eq]; |