(* Title: ZF/Induct/Mutil.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
*)
section \<open>The Mutilated Chess Board Problem, formalized inductively\<close>
theory Mutil imports ZF begin
text \<open>
Originator is Max Black, according to J A Robinson. Popularized as
the Mutilated Checkerboard Problem by J McCarthy.
\<close>
consts
domino :: i
tiling :: "i => i"
inductive
domains "domino" \<subseteq> "Pow(nat \<times> nat)"
intros
horiz: "[| i \ nat; j \ nat |] ==> {, } \ domino"
vertl: "[| i \ nat; j \ nat |] ==> {, } \ domino"
type_intros empty_subsetI cons_subsetI PowI SigmaI nat_succI
inductive
domains "tiling(A)" \<subseteq> "Pow(\<Union>(A))"
intros
empty: "0 \ tiling(A)"
Un: "[| a \ A; t \ tiling(A); a \ t = 0 |] ==> a \ t \ tiling(A)"
type_intros empty_subsetI Union_upper Un_least PowI
type_elims PowD [elim_format]
definition
evnodd :: "[i, i] => i" where
"evnodd(A,b) == {z \ A. \i j. z = \ (i #+ j) mod 2 = b}"
subsection \<open>Basic properties of evnodd\<close>
lemma evnodd_iff: ": evnodd(A,b) \ : A & (i#+j) mod 2 = b"
by (unfold evnodd_def) blast
lemma evnodd_subset: "evnodd(A, b) \ A"
by (unfold evnodd_def) blast
lemma Finite_evnodd: "Finite(X) ==> Finite(evnodd(X,b))"
by (rule lepoll_Finite, rule subset_imp_lepoll, rule evnodd_subset)
lemma evnodd_Un: "evnodd(A \ B, b) = evnodd(A,b) \ evnodd(B,b)"
by (simp add: evnodd_def Collect_Un)
lemma evnodd_Diff: "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"
by (simp add: evnodd_def Collect_Diff)
lemma evnodd_cons [simp]:
"evnodd(cons(,C), b) =
(if (i#+j) mod 2 = b then cons(<i,j>, evnodd(C,b)) else evnodd(C,b))"
by (simp add: evnodd_def Collect_cons)
lemma evnodd_0 [simp]: "evnodd(0, b) = 0"
by (simp add: evnodd_def)
subsection \<open>Dominoes\<close>
lemma domino_Finite: "d \ domino ==> Finite(d)"
by (blast intro!: Finite_cons Finite_0 elim: domino.cases)
lemma domino_singleton:
"[| d \ domino; b<2 |] ==> \i' j'. evnodd(d,b) = {}"
apply (erule domino.cases)
apply (rule_tac [2] k1 = "i#+j" in mod2_cases [THEN disjE])
apply (rule_tac k1 = "i#+j" in mod2_cases [THEN disjE])
apply (rule add_type | assumption)+
(*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
apply (auto simp add: mod_succ succ_neq_self dest: ltD)
done
subsection \<open>Tilings\<close>
text \<open>The union of two disjoint tilings is a tiling\<close>
lemma tiling_UnI:
"t \ tiling(A) ==> u \ tiling(A) ==> t \ u = 0 ==> t \ u \ tiling(A)"
apply (induct set: tiling)
apply (simp add: tiling.intros)
apply (simp add: Un_assoc subset_empty_iff [THEN iff_sym])
apply (blast intro: tiling.intros)
done
lemma tiling_domino_Finite: "t \ tiling(domino) ==> Finite(t)"
apply (induct set: tiling)
apply (rule Finite_0)
apply (blast intro!: Finite_Un intro: domino_Finite)
done
lemma tiling_domino_0_1: "t \ tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"
apply (induct set: tiling)
apply (simp add: evnodd_def)
apply (rule_tac b1 = 0 in domino_singleton [THEN exE])
prefer 2
apply simp
apply assumption
apply (rule_tac b1 = 1 in domino_singleton [THEN exE])
prefer 2
apply simp
apply assumption
apply safe
apply (subgoal_tac "\p b. p \ evnodd (a,b) \ p\evnodd (t,b)")
apply (simp add: evnodd_Un Un_cons tiling_domino_Finite
evnodd_subset [THEN subset_Finite] Finite_imp_cardinal_cons)
apply (blast dest!: evnodd_subset [THEN subsetD] elim: equalityE)
done
lemma dominoes_tile_row:
"[| i \ nat; n \ nat |] ==> {i} * (n #+ n) \ tiling(domino)"
apply (induct_tac n)
apply (simp add: tiling.intros)
apply (simp add: Un_assoc [symmetric] Sigma_succ2)
apply (rule tiling.intros)
prefer 2 apply assumption
apply (rename_tac n')
apply (subgoal_tac (*seems the easiest way of turning one to the other*)
"{i}*{succ (n'#+n') } \ {i}*{n'#+n'} =
{<i,n'#+n'>, <i,succ (n'#+n') >}")
prefer 2 apply blast
apply (simp add: domino.horiz)
apply (blast elim: mem_irrefl mem_asym)
done
lemma dominoes_tile_matrix:
"[| m \ nat; n \ nat |] ==> m * (n #+ n) \ tiling(domino)"
apply (induct_tac m)
apply (simp add: tiling.intros)
apply (simp add: Sigma_succ1)
apply (blast intro: tiling_UnI dominoes_tile_row elim: mem_irrefl)
done
lemma eq_lt_E: "[| x=y; x P"
by auto
theorem mutil_not_tiling: "[| m \ nat; n \ nat;
t = (succ(m)#+succ(m))*(succ(n)#+succ(n));
t' = t - {<0,0>} - {} |]
==> t' \ tiling(domino)"
apply (rule notI)
apply (drule tiling_domino_0_1)
apply (erule_tac x = "|A|" for A in eq_lt_E)
apply (subgoal_tac "t \ tiling (domino)")
prefer 2 (*Requires a small simpset that won't move the succ applications*)
apply (simp only: nat_succI add_type dominoes_tile_matrix)
apply (simp add: evnodd_Diff mod2_add_self mod2_succ_succ
tiling_domino_0_1 [symmetric])
apply (rule lt_trans)
apply (rule Finite_imp_cardinal_Diff,
simp add: tiling_domino_Finite Finite_evnodd Finite_Diff,
simp add: evnodd_iff nat_0_le [THEN ltD] mod2_add_self)+
done
end
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
