author wenzelm Wed, 14 Nov 2001 23:15:19 +0100 changeset 12185 54bd9aa3343d parent 12184 f4aaa2647fd2 child 12186 9b7026a0b0ed
tuned;
 src/HOL/Induct/document/root.tex file | annotate | diff | comparison | revisions src/ZF/Induct/Mutil.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Induct/document/root.tex	Wed Nov 14 23:14:59 2001 +0100
+++ b/src/HOL/Induct/document/root.tex	Wed Nov 14 23:15:19 2001 +0100
@@ -8,7 +8,7 @@

\begin{document}

-\title{Examples of Inductive and Coinductive Definitions}
+\title{Examples of Inductive and Coinductive Definitions in HOL}
\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}
\maketitle

--- a/src/ZF/Induct/Mutil.thy	Wed Nov 14 23:14:59 2001 +0100
+++ b/src/ZF/Induct/Mutil.thy	Wed Nov 14 23:15:19 2001 +0100
@@ -37,7 +37,7 @@
"evnodd(A,b) == {z \<in> A. \<exists>i j. z = <i,j> \<and> (i #+ j) mod 2 = b}"

-subsubsection {* Basic properties of evnodd *}
+subsection {* Basic properties of evnodd *}

lemma evnodd_iff: "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b"
by (unfold evnodd_def) blast
@@ -63,12 +63,13 @@

-subsubsection {* Dominoes *}
+subsection {* Dominoes *}

lemma domino_Finite: "d \<in> domino ==> Finite(d)"
by (blast intro!: Finite_cons Finite_0 elim: domino.cases)

-lemma domino_singleton: "[| d \<in> domino; b<2 |] ==> \<exists>i' j'. evnodd(d,b) = {<i',j'>}"
+lemma domino_singleton:
+    "[| d \<in> domino; b<2 |] ==> \<exists>i' j'. evnodd(d,b) = {<i',j'>}"
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])
@@ -78,7 +79,7 @@
done

-subsubsection {* Tilings *}
+subsection {* Tilings *}

text {* The union of two disjoint tilings is a tiling *}

@@ -114,7 +115,8 @@
apply (blast dest!: evnodd_subset [THEN subsetD] elim: equalityE)
done

-lemma dominoes_tile_row: "[| i \<in> nat;  n \<in> nat |] ==> {i} * (n #+ n) \<in> tiling(domino)"
+lemma dominoes_tile_row:
+    "[| i \<in> nat;  n \<in> nat |] ==> {i} * (n #+ n) \<in> tiling(domino)"
apply (induct_tac n)
apply (simp add: Un_assoc [symmetric] Sigma_succ2)
@@ -122,13 +124,15 @@
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') } Un {i}*{n'#+n'} = {<i,n'#+n'>, <i,succ (n'#+n') >}")
+     "{i}*{succ (n'#+n') } Un {i}*{n'#+n'} =
+       {<i,n'#+n'>, <i,succ (n'#+n') >}")
prefer 2 apply blast
apply (blast elim: mem_irrefl mem_asym)
done

-lemma dominoes_tile_matrix: "[| m \<in> nat;  n \<in> nat |] ==> m * (n #+ n) \<in> tiling(domino)"
+lemma dominoes_tile_matrix:
+    "[| m \<in> nat;  n \<in> nat |] ==> m * (n #+ n) \<in> tiling(domino)"
apply (induct_tac m)
simp add: tiling_domino_Finite Finite_evnodd Finite_Diff,