35 "below(Suc n) <*> B = ({n} <*> B) Un ((below n) <*> B)"; |
35 "below(Suc n) <*> B = ({n} <*> B) Un ((below n) <*> B)"; |
36 by Auto_tac; |
36 by Auto_tac; |
37 qed "Sigma_Suc1"; |
37 qed "Sigma_Suc1"; |
38 |
38 |
39 Goalw [below_def] |
39 Goalw [below_def] |
40 "A <*> below(#2+n) = (A <*> {n}) Un (A <*> {Suc n}) Un (A <*> (below n))"; |
40 "A <*> below(Suc n) = (A <*> {n}) Un (A <*> (below n))"; |
41 by Auto_tac; |
41 by Auto_tac; |
42 by (arith_tac 1); |
|
43 qed "Sigma_Suc2"; |
42 qed "Sigma_Suc2"; |
44 |
43 |
45 Addsimps [Sigma_Suc1, Sigma_Suc2]; |
44 Addsimps [Sigma_Suc1, Sigma_Suc2]; |
46 |
45 |
47 Goal "({i} <*> {m}) Un ({i} <*> {n}) = {(i,m), (i,n)}"; |
46 Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}"; |
48 by Auto_tac; |
47 by Auto_tac; |
49 qed "sing_Times_lemma"; |
48 qed "sing_Times_lemma"; |
50 |
49 |
51 Goal "{i} <*> below(#2*n) : tiling domino"; |
50 Goal "{i} <*> below(#2*n) : tiling domino"; |
52 by (induct_tac "n" 1); |
51 by (induct_tac "n" 1); |
53 by (ALLGOALS Asm_simp_tac); |
52 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym]))); |
54 by (rtac tiling.Un 1); |
53 by (rtac tiling.Un 1); |
55 by (ALLGOALS (asm_simp_tac (simpset() addsimps [sing_Times_lemma]))); |
54 by (ALLGOALS (asm_simp_tac (simpset() addsimps [sing_Times_lemma]))); |
56 qed "dominoes_tile_row"; |
55 qed "dominoes_tile_row"; |
57 |
56 |
58 AddSIs [dominoes_tile_row]; |
57 AddSIs [dominoes_tile_row]; |