author | wenzelm |
Thu, 16 Mar 2000 00:35:27 +0100 | |
changeset 8490 | 6e0f23304061 |
parent 8399 | 86b04d47b853 |
child 8553 | a79f6fb4d426 |
permissions | -rw-r--r-- |
3423 | 1 |
(* Title: HOL/Induct/Mutil |
3120
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 1996 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 |
The Mutilated Chess Board Problem, formalized inductively |
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 |
Addsimps tiling.intrs; |
8399 | 10 |
AddIs tiling.intrs; |
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 |
(** The union of two disjoint tilings is a tiling **) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
|
8399 | 14 |
Goal "t: tiling A ==> u: tiling A --> t <= -u --> t Un u : tiling A"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
by (etac tiling.induct 1); |
8399 | 16 |
by (simp_tac (simpset() addsimps [Un_assoc]) 2); |
17 |
by Auto_tac; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
qed_spec_mp "tiling_UnI"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
19 |
|
8399 | 20 |
AddIs [tiling_UnI]; |
3120
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 |
(*** Chess boards ***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
23 |
|
5069 | 24 |
Goalw [below_def] "(i: below k) = (i<k)"; |
8399 | 25 |
by Auto_tac; |
3423 | 26 |
qed "below_less_iff"; |
27 |
AddIffs [below_less_iff]; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
28 |
|
5069 | 29 |
Goalw [below_def] "below 0 = {}"; |
8399 | 30 |
by Auto_tac; |
3423 | 31 |
qed "below_0"; |
32 |
Addsimps [below_0]; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
33 |
|
5069 | 34 |
Goalw [below_def] |
3423 | 35 |
"below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; |
7401 | 36 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
37 |
qed "Sigma_Suc1"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
38 |
|
5069 | 39 |
Goalw [below_def] |
3423 | 40 |
"A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; |
7401 | 41 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
42 |
qed "Sigma_Suc2"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
43 |
|
8399 | 44 |
Addsimps [Sigma_Suc1, Sigma_Suc2]; |
45 |
||
46 |
Goal "({i} Times {n}) Un ({i} Times {m}) = {(i,m), (i,n)}"; |
|
47 |
by Auto_tac; |
|
48 |
qed "sing_Times_lemma"; |
|
49 |
||
5069 | 50 |
Goal "{i} Times below(n+n) : tiling domino"; |
5184 | 51 |
by (induct_tac "n" 1); |
8399 | 52 |
by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym]))); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
53 |
by (resolve_tac tiling.intrs 1); |
8399 | 54 |
by (ALLGOALS |
55 |
(asm_simp_tac (simpset() addsimps [sing_Times_lemma, domino.horiz]))); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
56 |
qed "dominoes_tile_row"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
57 |
|
8399 | 58 |
AddSIs [dominoes_tile_row]; |
59 |
||
5069 | 60 |
Goal "(below m) Times below(n+n) : tiling domino"; |
5184 | 61 |
by (induct_tac "m" 1); |
8399 | 62 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
63 |
qed "dominoes_tile_matrix"; |
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 |
|
8399 | 66 |
(*** Basic properties of colored ***) |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
67 |
|
8399 | 68 |
Goalw [colored_def] "finite X ==> finite(colored b X)"; |
69 |
by Auto_tac; |
|
70 |
qed "finite_colored"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
71 |
|
8399 | 72 |
Goalw [colored_def] "colored b (A Un B) = colored b A Un colored b B"; |
73 |
by Auto_tac; |
|
74 |
qed "colored_Un"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
75 |
|
8399 | 76 |
Goalw [colored_def] "colored b (A - B) = colored b A - colored b B"; |
77 |
by Auto_tac; |
|
78 |
qed "colored_Diff"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
79 |
|
8399 | 80 |
Goalw [colored_def] "colored b {} = {}"; |
81 |
by Auto_tac; |
|
82 |
qed "colored_empty"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
83 |
|
8399 | 84 |
Goalw [colored_def] |
85 |
"colored b (insert (i,j) C) = \ |
|
86 |
\ (if (i+j) mod 2 = b then insert (i,j) (colored b C) else colored b C)"; |
|
87 |
by Auto_tac; |
|
88 |
qed "colored_insert"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
89 |
|
8399 | 90 |
Addsimps [finite_colored, colored_Un, colored_Diff, colored_empty, |
91 |
colored_insert]; |
|
3423 | 92 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
93 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
94 |
(*** Dominoes ***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
95 |
|
8399 | 96 |
Goal "d:domino ==> finite d"; |
97 |
by (etac domino.elim 1); |
|
98 |
by Auto_tac; |
|
99 |
qed "domino_finite"; |
|
100 |
Addsimps [domino_finite]; |
|
101 |
||
102 |
Goal "[| d:domino; b<2 |] ==> EX i j. colored b d = {(i,j)}"; |
|
103 |
by (etac domino.elim 1); |
|
104 |
by (auto_tac (claset(), simpset() addsimps [mod_Suc])); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
105 |
qed "domino_singleton"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
106 |
|
8399 | 107 |
Goal "d:domino \ |
108 |
\ ==> EX i j i' j'. colored 0 d = {(i,j)} & colored 1 d = {(i',j')}"; |
|
109 |
by (blast_tac (claset() addDs [domino_singleton]) 1); |
|
110 |
qed "domino_singleton_01"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
111 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
112 |
(*** Tilings of dominoes ***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
113 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
114 |
Goal "t:tiling domino ==> finite t"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
115 |
by (eresolve_tac [tiling.induct] 1); |
8399 | 116 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
117 |
qed "tiling_domino_finite"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
118 |
|
8399 | 119 |
Addsimps [tiling_domino_finite]; |
120 |
||
121 |
Goal "t: tiling domino ==> card(colored 0 t) = card(colored 1 t)"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
122 |
by (eresolve_tac [tiling.induct] 1); |
8399 | 123 |
by (dtac domino_singleton_01 2); |
7401 | 124 |
by Auto_tac; |
8399 | 125 |
(*this lemma tells us that both "inserts" are non-trivial*) |
126 |
by (subgoal_tac "ALL p b. p : colored b a --> p ~: colored b t" 1); |
|
127 |
by (Asm_simp_tac 1); |
|
128 |
by (auto_tac (claset(), simpset() addsimps [colored_def])); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
129 |
qed "tiling_domino_0_1"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
130 |
|
8399 | 131 |
(*Final argument is surprisingly complex*) |
132 |
Goal "[| t : tiling domino; \ |
|
133 |
\ (i+j) mod 2 = 0; (i'+j') mod 2 = 0; \ |
|
134 |
\ {(i,j),(i',j')} <= t; j' ~= j |] \ |
|
135 |
\ ==> (t - {(i,j)} - {(i',j')}) ~: tiling domino"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
136 |
by (rtac notI 1); |
8399 | 137 |
by (subgoal_tac "card (colored 0 (t - {(i,j)} - {(i',j')})) < \ |
138 |
\ card (colored 1 (t - {(i,j)} - {(i',j')}))" 1); |
|
139 |
by (force_tac (claset(), HOL_ss addsimps [tiling_domino_0_1]) 1); |
|
140 |
by (asm_simp_tac (simpset() addsimps [tiling_domino_0_1 RS sym]) 1); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
141 |
by (rtac less_trans 1); |
8399 | 142 |
by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], |
143 |
simpset() addsimps [colored_def]))); |
|
144 |
qed "gen_mutil_not_tiling"; |
|
145 |
||
146 |
(*Apply the general theorem to the well-known case*) |
|
147 |
Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n) |] \ |
|
148 |
\ ==> t - {(0,0)} - {(Suc(m+m), Suc(n+n))} ~: tiling domino"; |
|
149 |
by (rtac gen_mutil_not_tiling 1); |
|
150 |
by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1); |
|
151 |
by Auto_tac; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
152 |
qed "mutil_not_tiling"; |
8399 | 153 |