Quellcode-Bibliothek Mutil.thy Sprache: Isabelle

(*  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\ \ {\i,j\, } \ domino"
    vertl: "\i \ nat; j \ nat\ \ {\i,j\, } \ 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\ \ (i #+ j) mod 2 = b}"

subsection \<open>Basic properties of evnodd\<close>

lemma evnodd_iff: "\i,j\: evnodd(A,b) \ \i,j\: 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(\i,j\,C), b) =
    (if (i#+j) mod 2 = b then cons(\<langle>i,j\<rangle>, 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\} - {}\
      \<Longrightarrow> t' \<notin> 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

quality93%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.11Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.