equal
deleted
inserted
replaced
48 qed "sing_Times_lemma"; |
48 qed "sing_Times_lemma"; |
49 |
49 |
50 Goal "{i} Times below(n+n) : tiling domino"; |
50 Goal "{i} Times below(n+n) : tiling domino"; |
51 by (induct_tac "n" 1); |
51 by (induct_tac "n" 1); |
52 by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym]))); |
52 by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym]))); |
53 by (resolve_tac tiling.intrs 1); |
53 by (rtac tiling.Un 1); |
54 by (ALLGOALS |
54 by (ALLGOALS |
55 (asm_simp_tac (simpset() addsimps [sing_Times_lemma, domino.horiz]))); |
55 (asm_simp_tac (simpset() addsimps [sing_Times_lemma, domino.horiz]))); |
56 qed "dominoes_tile_row"; |
56 qed "dominoes_tile_row"; |
57 |
57 |
58 AddSIs [dominoes_tile_row]; |
58 AddSIs [dominoes_tile_row]; |
110 qed "domino_singleton_01"; |
110 qed "domino_singleton_01"; |
111 |
111 |
112 (*** Tilings of dominoes ***) |
112 (*** Tilings of dominoes ***) |
113 |
113 |
114 Goal "t:tiling domino ==> finite t"; |
114 Goal "t:tiling domino ==> finite t"; |
115 by (eresolve_tac [tiling.induct] 1); |
115 by (etac tiling.induct 1); |
116 by Auto_tac; |
116 by Auto_tac; |
117 qed "tiling_domino_finite"; |
117 qed "tiling_domino_finite"; |
118 |
118 |
119 Addsimps [tiling_domino_finite]; |
119 Addsimps [tiling_domino_finite]; |
120 |
120 |
121 Goal "t: tiling domino ==> card(colored 0 t) = card(colored 1 t)"; |
121 Goal "t: tiling domino ==> card(colored 0 t) = card(colored 1 t)"; |
122 by (eresolve_tac [tiling.induct] 1); |
122 by (etac tiling.induct 1); |
123 by (dtac domino_singleton_01 2); |
123 by (dtac domino_singleton_01 2); |
124 by Auto_tac; |
124 by Auto_tac; |
125 (*this lemma tells us that both "inserts" are non-trivial*) |
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); |
126 by (subgoal_tac "ALL p b. p : colored b a --> p ~: colored b t" 1); |
127 by (Asm_simp_tac 1); |
127 by (Asm_simp_tac 1); |