equal
deleted
inserted
replaced
90 apply (simp add: Un_assoc subset_empty_iff [THEN iff_sym]) |
90 apply (simp add: Un_assoc subset_empty_iff [THEN iff_sym]) |
91 apply (blast intro: tiling.intros) |
91 apply (blast intro: tiling.intros) |
92 done |
92 done |
93 |
93 |
94 lemma tiling_domino_Finite: "t \<in> tiling(domino) ==> Finite(t)" |
94 lemma tiling_domino_Finite: "t \<in> tiling(domino) ==> Finite(t)" |
95 apply (induct rule: tiling.induct) |
95 apply (induct set: tiling) |
96 apply (rule Finite_0) |
96 apply (rule Finite_0) |
97 apply (blast intro!: Finite_Un intro: domino_Finite) |
97 apply (blast intro!: Finite_Un intro: domino_Finite) |
98 done |
98 done |
99 |
99 |
100 lemma tiling_domino_0_1: "t \<in> tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|" |
100 lemma tiling_domino_0_1: "t \<in> tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|" |
101 apply (induct rule: tiling.induct) |
101 apply (induct set: tiling) |
102 apply (simp add: evnodd_def) |
102 apply (simp add: evnodd_def) |
103 apply (rule_tac b1 = 0 in domino_singleton [THEN exE]) |
103 apply (rule_tac b1 = 0 in domino_singleton [THEN exE]) |
104 prefer 2 |
104 prefer 2 |
105 apply simp |
105 apply simp |
106 apply assumption |
106 apply assumption |