src/HOL/Induct/Mutil.ML
changeset 3414 804c8a178a7f
parent 3357 c224dddc5f71
child 3423 3684a4420a67
equal deleted inserted replaced
3413:c1f63cc3a768 3414:804c8a178a7f
   115                           setloop split_tac [expand_if]) 1
   115                           setloop split_tac [expand_if]) 1
   116            THEN Blast_tac 1));
   116            THEN Blast_tac 1));
   117 qed "domino_singleton";
   117 qed "domino_singleton";
   118 
   118 
   119 goal thy "!!d. d:domino ==> finite d";
   119 goal thy "!!d. d:domino ==> finite d";
   120 by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
   120 by (blast_tac (!claset addSEs [domino.elim]) 1);
   121                       addSEs [domino.elim]) 1);
       
   122 qed "domino_finite";
   121 qed "domino_finite";
   123 
   122 
   124 
   123 
   125 (*** Tilings of dominoes ***)
   124 (*** Tilings of dominoes ***)
   126 
   125 
   127 goal thy "!!t. t:tiling domino ==> finite t";
   126 goal thy "!!t. t:tiling domino ==> finite t";
   128 by (eresolve_tac [tiling.induct] 1);
   127 by (eresolve_tac [tiling.induct] 1);
   129 by (rtac finite_emptyI 1);
   128 by (rtac Finites.emptyI 1);
   130 by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
   129 by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
   131 qed "tiling_domino_finite";
   130 qed "tiling_domino_finite";
   132 
   131 
   133 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
   132 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
   134 by (eresolve_tac [tiling.induct] 1);
   133 by (eresolve_tac [tiling.induct] 1);