--- 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 @@
by (simp add: evnodd_def)
-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: tiling.intros)
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 (simp add: domino.horiz)
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)
apply (simp add: tiling.intros)
apply (simp add: Sigma_succ1)
@@ -148,7 +152,8 @@
apply (subgoal_tac "t \<in> 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 (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,