src/HOL/Induct/Mutil.ML
changeset 3357 c224dddc5f71
parent 3120 c58423c20740
child 3414 804c8a178a7f
equal deleted inserted replaced
3356:9b899eb8a036 3357:c224dddc5f71
   139 by (Simp_tac 2 THEN assume_tac 1);
   139 by (Simp_tac 2 THEN assume_tac 1);
   140 by (Step_tac 1);
   140 by (Step_tac 1);
   141 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
   141 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
   142 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
   142 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
   143                                      tiling_domino_finite,
   143                                      tiling_domino_finite,
   144                                      evnodd_subset RS finite_subset,
   144                                      evnodd_subset RS finite_subset]) 1);
   145                                      card_insert_disjoint]) 1);
       
   146 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
   145 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
   147 qed "tiling_domino_0_1";
   146 qed "tiling_domino_0_1";
   148 
   147 
   149 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
   148 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
   150 \                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
   149 \                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \