equal
deleted
inserted
replaced
129 (*Requires a small simpset that won't move the succ applications*) |
129 (*Requires a small simpset that won't move the succ applications*) |
130 by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, |
130 by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, |
131 dominoes_tile_matrix]) 2); |
131 dominoes_tile_matrix]) 2); |
132 by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1); |
132 by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1); |
133 by (asm_simp_tac (simpset() addsimps add_ac) 2); |
133 by (asm_simp_tac (simpset() addsimps add_ac) 2); |
134 by (asm_full_simp_tac |
134 by (asm_lr_simp_tac |
135 (simpset() addsimps [evnodd_Diff, mod2_add_self, |
135 (simpset() addsimps [evnodd_Diff, mod2_add_self, |
136 mod2_succ_succ, tiling_domino_0_1 RS sym]) 1); |
136 mod2_succ_succ, tiling_domino_0_1 RS sym]) 1); |
137 by (rtac lt_trans 1); |
137 by (rtac lt_trans 1); |
138 by (REPEAT |
138 by (REPEAT |
139 (rtac Finite_imp_cardinal_Diff 1 |
139 (rtac Finite_imp_cardinal_Diff 1 |