# HG changeset patch
# User wenzelm
# Date 981218416 -3600
# Node ID b5f5942781a068105d8cb23634e99ee04471df01
# Parent  971a50fda14655815fd84772bcd1111875c40a0c
Induct: converted some theories to new-style format;

diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/ABexp.ML
--- a/src/HOL/Induct/ABexp.ML	Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      HOL/Induct/ABexp.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen
-    Copyright   1998  TU Muenchen
-
-Arithmetic and boolean expressions
-*)
-
-(** substitution theorems for arithmetic and boolean expressions **)
-
-(* One variable *)
-Goal
-  "evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a &  \
- \ evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b";
-by (induct_tac "a b" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "subst1_aexp_bexp";
-
-(* All variables *)
-Goal
-  "evala env (substa s a) = evala (%x. evala env (s x)) a &  \
- \ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
-by (induct_tac "a b" 1);
-by (Auto_tac);
-qed "subst_all_aexp_bexp";
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/ABexp.thy
--- a/src/HOL/Induct/ABexp.thy	Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/ABexp.thy	Sat Feb 03 17:40:16 2001 +0100
@@ -2,52 +2,50 @@
     ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
     Copyright   1998  TU Muenchen
-
-Arithmetic and boolean expressions
 *)
 
-ABexp = Main +
+header {* Arithmetic and boolean expressions *}
+
+theory ABexp = Main:
 
-datatype
-  'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
-          | Sum ('a aexp) ('a aexp)
-          | Diff ('a aexp) ('a aexp)
-          | Var 'a
-          | Num nat
-and
-  'a bexp = Less ('a aexp) ('a aexp)
-          | And ('a bexp) ('a bexp)
-          | Neg ('a bexp)
+datatype 'a aexp =
+    IF "'a bexp"  "'a aexp"  "'a aexp"
+  | Sum "'a aexp"  "'a aexp"
+  | Diff "'a aexp"  "'a aexp"
+  | Var 'a
+  | Num nat
+and 'a bexp =
+    Less "'a aexp"  "'a aexp"
+  | And "'a bexp"  "'a bexp"
+  | Neg "'a bexp"
 
 
-(** evaluation of arithmetic and boolean expressions **)
+text {* \medskip Evaluation of arithmetic and boolean expressions *}
 
 consts
-  evala :: ('a => nat) => 'a aexp => nat
-  evalb :: ('a => nat) => 'a bexp => bool
+  evala :: "('a => nat) => 'a aexp => nat"
+  evalb :: "('a => nat) => 'a bexp => bool"
 
 primrec
-  "evala env (IF b a1 a2) =
-     (if evalb env b then evala env a1 else evala env a2)"
+  "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
   "evala env (Sum a1 a2) = evala env a1 + evala env a2"
   "evala env (Diff a1 a2) = evala env a1 - evala env a2"
   "evala env (Var v) = env v"
   "evala env (Num n) = n"
 
   "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
-  "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
-  "evalb env (Neg b) = (~ evalb env b)"
+  "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
+  "evalb env (Neg b) = (\<not> evalb env b)"
 
 
-(** substitution on arithmetic and boolean expressions **)
+text {* \medskip Substitution on arithmetic and boolean expressions *}
 
 consts
-  substa :: ('a => 'b aexp) => 'a aexp => 'b aexp
-  substb :: ('a => 'b aexp) => 'a bexp => 'b bexp
+  substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
+  substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
 
 primrec
-  "substa f (IF b a1 a2) =
-     IF (substb f b) (substa f a1) (substa f a2)"
+  "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
   "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
   "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
   "substa f (Var v) = f v"
@@ -57,4 +55,20 @@
   "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
   "substb f (Neg b) = Neg (substb f b)"
 
+lemma subst1_aexp_bexp:
+  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a \<and>
+  evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
+    --  {* one variable *}
+  apply (induct a and b)
+         apply simp_all
+  done
+
+lemma subst_all_aexp_bexp:
+  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a \<and>
+  evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
+    -- {* all variables *}
+  apply (induct a and b)
+         apply auto
+  done
+
 end
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(*  Title:      HOL/Induct/Mutil
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
-*)
-
-Addsimps (tiling.intrs @ domino.intrs);
-AddIs    tiling.intrs;
-
-(** The union of two disjoint tilings is a tiling **)
-
-Goal "t: tiling A ==> u: tiling A --> t Int u = {} --> t Un u : tiling A";
-by (etac tiling.induct 1);
-by (simp_tac (simpset() addsimps [Un_assoc]) 2);
-by Auto_tac;
-qed_spec_mp "tiling_UnI";
-
-AddIs [tiling_UnI];
-
-(*** Chess boards ***)
-
-Goalw [lessThan_def]
-    "lessThan(Suc n) <*> B = ({n} <*> B) Un ((lessThan n) <*> B)";
-by Auto_tac;
-qed "Sigma_Suc1";
-
-Goalw [lessThan_def]
-    "A <*> lessThan(Suc n) = (A <*> {n}) Un (A <*> (lessThan n))";
-by Auto_tac;
-qed "Sigma_Suc2";
-
-Addsimps [Sigma_Suc1, Sigma_Suc2];
-
-Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
-by Auto_tac;
-qed "sing_Times_lemma";
-
-Goal "{i} <*> lessThan(#2*n) : tiling domino";
-by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
-by (rtac tiling.Un 1);
-by (auto_tac (claset(), simpset() addsimps [sing_Times_lemma]));  
-qed "dominoes_tile_row";
-
-AddSIs [dominoes_tile_row]; 
-
-Goal "(lessThan m) <*> lessThan(#2*n) : tiling domino";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "dominoes_tile_matrix";
-
-
-(*** "coloured" and Dominoes ***)
-
-Goalw [coloured_def]
-    "coloured b Int (insert (i,j) t) = \
-\      (if (i+j) mod #2 = b then insert (i,j) (coloured b Int t) \
-\                           else coloured b Int t)";
-by Auto_tac;
-qed "coloured_insert";
-Addsimps [coloured_insert];
-
-Goal "d:domino ==> (EX i j. coloured 0 Int d = {(i,j)}) & \
-\                  (EX m n. coloured 1 Int d = {(m,n)})";
-by (etac domino.elim 1);
-by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
-qed "domino_singletons";
-
-Goal "d:domino ==> finite d";
-by (etac domino.elim 1);
-by Auto_tac;
-qed "domino_finite";
-Addsimps [domino_finite];
-
-
-(*** Tilings of dominoes ***)
-
-Goal "t:tiling domino ==> finite t";
-by (etac tiling.induct 1);
-by Auto_tac;
-qed "tiling_domino_finite";
-
-Addsimps [tiling_domino_finite, Int_Un_distrib, Diff_Int_distrib];
-
-Goal "t: tiling domino ==> card(coloured 0 Int t) = card(coloured 1 Int t)";
-by (etac tiling.induct 1);
-by (dtac domino_singletons 2);
-by Auto_tac;
-(*this lemma tells us that both "inserts" are non-trivial*)
-by (subgoal_tac "ALL p C. C Int a = {p} --> p ~: t" 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "tiling_domino_0_1";
-
-(*Final argument is surprisingly complex*)
-Goal "[| t : tiling domino;       \
-\        (i+j) mod #2 = 0;  (m+n) mod #2 = 0;  \
-\        {(i,j),(m,n)} <= t |]    \
-\     ==> (t - {(i,j)} - {(m,n)}) ~: tiling domino";
-by (rtac notI 1);
-by (subgoal_tac "card (coloured 0 Int (t - {(i,j)} - {(m,n)})) < \
-\                card (coloured 1 Int (t - {(i,j)} - {(m,n)}))" 1);
-by (force_tac (claset(), HOL_ss addsimps [tiling_domino_0_1]) 1);
-by (asm_simp_tac (simpset() addsimps [tiling_domino_0_1 RS sym]) 1);
-by (asm_full_simp_tac (simpset() addsimps [coloured_def, card_Diff2_less]) 1); 
-qed "gen_mutil_not_tiling";
-
-(*Apply the general theorem to the well-known case*)
-Goal "t = lessThan(#2 * Suc m) <*> lessThan(#2 * Suc n) \
-\     ==> t - {(0,0)} - {(Suc(#2*m), Suc(#2*n))} ~: tiling domino";
-by (rtac gen_mutil_not_tiling 1);
-by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1);
-by Auto_tac;
-qed "mutil_not_tiling";
-
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Mutil.thy	Sat Feb 03 17:40:16 2001 +0100
@@ -1,29 +1,150 @@
-(*  Title:      HOL/Induct/Mutil
+(*  Title:      HOL/Induct/Mutil.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
-  Originator is Max Black, according to J A Robinson.
-  Popularized as the Mutilated Checkerboard Problem by J McCarthy
 *)
 
-Mutil = Main +
+header {* The Mutilated Chess Board Problem *}
+
+theory Mutil = Main:
 
-consts     tiling :: "'a set set => 'a set set"
+text {*
+  The Mutilated Chess Board Problem, formalized inductively.
+
+  Originator is Max Black, according to J A Robinson.  Popularized as
+  the Mutilated Checkerboard Problem by J McCarthy.
+*}
+
+consts tiling :: "'a set set => 'a set set"
 inductive "tiling A"
-  intrs
-    empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
+  intros [simp, intro]
+    empty: "{} \<in> tiling A"
+    Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
 
-consts    domino :: "(nat*nat)set set"
+consts domino :: "(nat \<times> nat) set set"
 inductive domino
-  intrs
-    horiz  "{(i, j), (i, Suc j)} : domino"
-    vertl  "{(i, j), (Suc i, j)} : domino"
+  intros [simp]
+    horiz: "{(i, j), (i, Suc j)} \<in> domino"
+    vertl: "{(i, j), (Suc i, j)} \<in> domino"
 
 constdefs
-  coloured  :: "nat => (nat*nat)set"
-   "coloured b == {(i,j). (i+j) mod #2 = b}"
+  coloured :: "nat => (nat \<times> nat) set"
+   "coloured b == {(i, j). (i + j) mod #2 = b}"
+
+
+text {* \medskip The union of two disjoint tilings is a tiling *}
+
+lemma tiling_UnI [rule_format, intro]:
+  "t \<in> tiling A ==> u \<in> tiling A --> t \<inter> u = {} --> t \<union> u \<in> tiling A"
+  apply (erule tiling.induct)
+   prefer 2
+   apply (simp add: Un_assoc)
+  apply auto
+  done
+
+
+text {* \medskip Chess boards *}
+
+lemma Sigma_Suc1 [simp]:
+  "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
+  apply (unfold lessThan_def)
+  apply auto
+  done
+
+lemma Sigma_Suc2 [simp]:
+  "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
+  apply (unfold lessThan_def)
+  apply auto
+  done
+
+lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
+  apply auto
+  done
+
+lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (#2 * n) \<in> tiling domino"
+  apply (induct n)
+   apply (simp_all add: Un_assoc [symmetric])
+  apply (rule tiling.Un)
+    apply (auto simp add: sing_Times_lemma)
+  done
+
+lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (#2 * n) \<in> tiling domino"
+  apply (induct m)
+   apply auto
+  done
+
+
+text {* \medskip @{term coloured} and Dominoes *}
+
+lemma coloured_insert [simp]:
+  "coloured b \<inter> (insert (i, j) t) =
+   (if (i + j) mod #2 = b then insert (i, j) (coloured b \<inter> t)
+    else coloured b \<inter> t)"
+  apply (unfold coloured_def)
+  apply auto
+  done
+
+lemma domino_singletons:
+  "d \<in> domino ==>
+    (\<exists>i j. coloured 0 \<inter> d = {(i, j)}) \<and>
+    (\<exists>m n. coloured 1 \<inter> d = {(m, n)})"
+  apply (erule domino.cases)
+   apply (auto simp add: mod_Suc)
+  done
+
+lemma domino_finite [simp]: "d \<in> domino ==> finite d"
+  apply (erule domino.cases)
+   apply auto
+  done
+
+
+text {* \medskip Tilings of dominoes *}
+
+lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
+  apply (erule tiling.induct)
+   apply auto
+  done
+
+declare
+  Int_Un_distrib [simp]
+  Diff_Int_distrib [simp]
+
+lemma tiling_domino_0_1:
+  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
+  apply (erule tiling.induct)
+   apply (drule_tac [2] domino_singletons)
+   apply auto
+  apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
+    -- {* this lemma tells us that both ``inserts'' are non-trivial *}
+   apply (simp (no_asm_simp))
+  apply blast
+  done
+
+
+text {* \medskip Final argument is surprisingly complex *}
+
+theorem gen_mutil_not_tiling:
+  "t \<in> tiling domino ==>
+    (i + j) mod #2 = 0 ==> (m + n) mod #2 = 0 ==>
+    {(i, j), (m, n)} \<subseteq> t
+  ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
+  apply (rule notI)
+  apply (subgoal_tac
+    "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
+      card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
+   apply (force simp only: tiling_domino_0_1)
+  apply (simp add: tiling_domino_0_1 [symmetric])
+  apply (simp add: coloured_def card_Diff2_less)
+  done
+
+text {* Apply the general theorem to the well-known case *}
+
+theorem mutil_not_tiling:
+  "t = lessThan (#2 * Suc m) \<times> lessThan (#2 * Suc n)
+    ==> t - {(0, 0)} - {(Suc (#2 * m), Suc (#2 * n))} \<notin> tiling domino"
+  apply (rule gen_mutil_not_tiling)
+     apply (blast intro!: dominoes_tile_matrix)
+    apply auto
+  done
 
 end
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/ROOT.ML	Sat Feb 03 17:40:16 2001 +0100
@@ -1,16 +1,12 @@
-(*  Title:      HOL/Induct/ROOT.ML
 
-Examples of Inductive and Coinductive Definitions.
-*)
-
+time_use_thy "Mutil";
+time_use_thy "Term";
+time_use_thy "ABexp";
+time_use_thy "Tree";
 time_use_thy "Sigma_Algebra";
 time_use_thy "Perm";
 time_use_thy "Comb";
-time_use_thy "Mutil";
 time_use_thy "PropLog";
 time_use_thy "SList";
 time_use_thy "LFilter";
-time_use_thy "Term";
-time_use_thy "ABexp";
 time_use_thy "Exp";
-time_use_thy "Tree";
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/Sigma_Algebra.thy
--- a/src/HOL/Induct/Sigma_Algebra.thy	Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Sigma_Algebra.thy	Sat Feb 03 17:40:16 2001 +0100
@@ -4,6 +4,8 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
+header {* Sigma algebras *}
+
 theory Sigma_Algebra = Main:
 
 text {*
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*  Title:      HOL/Induct/Term.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen
-    Copyright   1998  TU Muenchen
-
-Terms over a given alphabet -- function applications
-*)
-
-(** a simple theorem about composition of substitutions **)
-
-Goal "(subst_term ((subst_term f1) o f2) t) =  \
-  \  (subst_term f1 (subst_term f2 t)) &  \
-  \  (subst_term_list ((subst_term f1) o f2) ts) =  \
-  \  (subst_term_list f1 (subst_term_list f2 ts))";
-by (induct_tac "t ts" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "subst_comp";
-
-(**** alternative induction rule ****)
-
-bind_thm ("term_induct2", prove_goal thy
-  "[| !!v. P (Var v);  \
-   \  !!f ts. list_all P ts ==> P (App f ts) |] ==>  \
-   \    P t & list_all P ts"
-  (fn prems =>
-    [induct_tac "t ts" 1,
-     resolve_tac prems 1,
-     resolve_tac prems 1,
-     atac 1,
-     ALLGOALS Asm_simp_tac]) RS conjunct1);
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Term.thy	Sat Feb 03 17:40:16 2001 +0100
@@ -2,23 +2,23 @@
     ID:         $Id$
     Author:     Stefan Berghofer,  TU Muenchen
     Copyright   1998  TU Muenchen
-
-Terms over a given alphabet -- function applications
 *)
 
-Term = Main +
+header {* Terms over a given alphabet *}
+
+theory Term = Main:
 
-datatype
-  ('a, 'b) term = Var 'a
-                | App 'b ((('a, 'b) term) list)
+datatype ('a, 'b) "term" =
+    Var 'a
+  | App 'b "('a, 'b) term list"
 
 
-(** substitution function on terms **)
+text {* \medskip Substitution function on terms *}
 
 consts
-  subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
+  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
   subst_term_list ::
-    "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
+    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
 
 primrec
   "subst_term f (Var a) = f a"
@@ -28,4 +28,35 @@
   "subst_term_list f (t # ts) =
      subst_term f t # subst_term_list f ts"
 
+
+text {* \medskip A simple theorem about composition of substitutions *}
+
+lemma subst_comp:
+  "(subst_term ((subst_term f1) \<circ> f2) t) =
+    (subst_term f1 (subst_term f2 t)) \<and>
+  (subst_term_list ((subst_term f1) \<circ> f2) ts) =
+    (subst_term_list f1 (subst_term_list f2 ts))"
+  apply (induct t and ts rule: term.induct)
+     apply simp_all
+  done
+
+
+text {* \medskip Alternative induction rule *}
+
+lemma term_induct2:
+  "(!!v. P (Var v)) ==>
+    (!!f ts. list_all P ts ==> P (App f ts))
+  ==> P t"
+proof -
+  case antecedent
+  have "P t \<and> list_all P ts"
+    apply (induct t and ts rule: term.induct)
+       apply (rule antecedent)
+      apply (rule antecedent)
+      apply assumption
+     apply simp_all
+    done
+  thus ?thesis ..
+qed
+
 end
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/Tree.ML
--- a/src/HOL/Induct/Tree.ML	Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      HOL/Induct/Tree.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer,  TU Muenchen
-    Copyright   1999  TU Muenchen
-
-Infinitely branching trees
-*)
-
-Goal "map_tree g (map_tree f t) = map_tree (g o f) t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "tree_map_compose";
-
-val prems = Goal "(!!x. P x ==> Q (f x)) ==>  \
-   \    exists_tree P ts --> exists_tree Q (map_tree f ts)";
-by (induct_tac "ts" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-by (Fast_tac 1);
-qed "exists_map";
-
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Tree.thy	Sat Feb 03 17:40:16 2001 +0100
@@ -2,26 +2,39 @@
     ID:         $Id$
     Author:     Stefan Berghofer,  TU Muenchen
     Copyright   1999  TU Muenchen
-
-Infinitely branching trees
 *)
 
-Tree = Main +
+header {* Infinitely branching trees *}
+
+theory Tree = Main:
 
-datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
+datatype 'a tree =
+    Atom 'a
+  | Branch "nat => 'a tree"
 
 consts
   map_tree :: "('a => 'b) => 'a tree => 'b tree"
-
 primrec
   "map_tree f (Atom a) = Atom (f a)"
-  "map_tree f (Branch ts) = Branch (%x. map_tree f (ts x))"
+  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
+
+lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
+  apply (induct t)
+   apply simp_all
+  done
 
 consts
   exists_tree :: "('a => bool) => 'a tree => bool"
-
 primrec
   "exists_tree P (Atom a) = P a"
-  "exists_tree P (Branch ts) = (? x. exists_tree P (ts x))"
+  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
+
+lemma exists_map:
+  "(!!x. P x ==> Q (f x)) ==>
+    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
+  apply (induct ts)
+   apply simp_all
+  apply blast
+  done
 
 end
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/Induct/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/document/root.tex	Sat Feb 03 17:40:16 2001 +0100
@@ -0,0 +1,27 @@
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym,pdfsetup}
+
+%for best-style documents ...
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+\title{Examples of Inductive and Coinductive Definitions}
+\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}
+\maketitle
+
+\begin{abstract}
+  This is a collection of small examples to demonstrate Isabelle/HOL's
+  (co)inductive definitions package.  Large examples appear on many other
+  sessions, such as Lambda, IMP, and Auth.
+\end{abstract}
+
+\tableofcontents
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+\end{document}
diff -r 971a50fda146 -r b5f5942781a0 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/IsaMakefile	Sat Feb 03 17:40:16 2001 +0100
@@ -205,11 +205,11 @@
 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
-  Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
-  Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
-  Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
-  Induct/Sigma_Algebra.thy Induct/SList.ML Induct/SList.thy \
-  Induct/ABexp.ML Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
+  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Perm.ML \
+  Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
+  Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
+  Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
+  Induct/Tree.thy Induct/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL Induct