# HG changeset patch
# User wenzelm
# Date 1006199277 -3600
# Node ID a2c0aaf94460771fdaaa590e2f9a90d2212ffef6
# Parent  282a92bc5655acadf3b13513d60eae0d01866992
tuned;

diff -r 282a92bc5655 -r a2c0aaf94460 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Mon Nov 19 20:47:39 2001 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Mon Nov 19 20:47:57 2001 +0100
@@ -37,7 +37,7 @@
   apply (rule Part_subset)
   done
 
-lemma treeI [TC]: "x : tree(A) ==> x : tree_forest(A)"
+lemma treeI [TC]: "x \<in> tree(A) ==> x \<in> tree_forest(A)"
   by (rule tree_subset_TF [THEN subsetD])
 
 lemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)"
@@ -45,7 +45,7 @@
   apply (rule Part_subset)
   done
 
-lemma treeI [TC]: "x : forest(A) ==> x : tree_forest(A)"
+lemma treeI [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
   by (rule forest_subset_TF [THEN subsetD])
 
 lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)"
@@ -54,7 +54,7 @@
   done
 
 lemma (notes rews = tree_forest.con_defs tree_def forest_def)
-  tree_forest_unfold: "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))"
+  tree_forest_unfold: "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
     -- {* NOT useful, but interesting \dots *}
   apply (unfold tree_def forest_def)
   apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
@@ -86,23 +86,23 @@
 lemma TF_rec_type:
   "[| z \<in> tree_forest(A);
       !!x f r. [| x \<in> A;  f \<in> forest(A);  r \<in> C(f)
-                |] ==> b(x,f,r): C(Tcons(x,f));
+                |] ==> b(x,f,r) \<in> C(Tcons(x,f));
       c \<in> C(Fnil);
-      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1: C(t); r2: C(f)
-                    |] ==> d(t,f,r1,r2): C(Fcons(t,f))
+      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1 \<in> C(t); r2 \<in> C(f)
+                    |] ==> d(t,f,r1,r2) \<in> C(Fcons(t,f))
    |] ==> tree_forest_rec(b,c,d,z) \<in> C(z)"
   by (induct_tac z) simp_all
 
 lemma tree_forest_rec_type:
   "[| !!x f r. [| x \<in> A;  f \<in> forest(A);  r \<in> D(f)
-                |] ==> b(x,f,r): C(Tcons(x,f));
+                |] ==> b(x,f,r) \<in> C(Tcons(x,f));
       c \<in> D(Fnil);
-      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1: C(t); r2: D(f)
-                    |] ==> d(t,f,r1,r2): D(Fcons(t,f))
-   |] ==> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t)  \<in> C(t)) &
+      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1 \<in> C(t); r2 \<in> D(f)
+                    |] ==> d(t,f,r1,r2) \<in> D(Fcons(t,f))
+   |] ==> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
           (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
     -- {* Mutually recursive version. *}
-  apply (unfold Ball_def)  (* FIXME *)
+  apply (unfold Ball_def)
   apply (rule tree_forest.mutual_induct)
   apply simp_all
   done
@@ -159,7 +159,7 @@
   apply simp_all
   done
 
-lemma map_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
+lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
   apply (erule list.induct)
   apply simp_all
   done
@@ -168,16 +168,14 @@
   \medskip @{text map}.
 *}
 
-lemma map_type:
-  "[| !!x. x \<in> A ==> h(x): B |] ==>
-     (\<forall>t \<in> tree(A). map(h,t) \<in> tree(B)) &
-     (\<forall>f \<in> forest(A). map(h,f) \<in> forest(B))"
-  apply (unfold Ball_def)  (* FIXME *)
-  apply (rule tree_forest.mutual_induct)
-  apply simp_all
+lemma (assumes h_type: "!!x. x \<in> A ==> h(x): B")
+    map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
+  and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
+  apply (induct rule: tree_forest.mutual_induct)
+    apply (insert h_type)
+    apply simp_all
   done
 
-
 text {*
   \medskip @{text size}.
 *}
diff -r 282a92bc5655 -r a2c0aaf94460 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Mon Nov 19 20:47:39 2001 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Mon Nov 19 20:47:57 2001 +0100
@@ -66,7 +66,7 @@
   val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists);
 
   val dummy =
-    writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ big_rec_name);
+    writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name);
 
   val case_varname = "f";                (*name for case variables*)
 
diff -r 282a92bc5655 -r a2c0aaf94460 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:39 2001 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:57 2001 +0100
@@ -152,7 +152,7 @@
 
 
   val dummy = conditional verbose (fn () =>
-    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ big_rec_name));
+    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name));
 
   (*Forbid the inductive definition structure from clashing with a theory
     name.  This restriction may become obsolete as ML is de-emphasized.*)
diff -r 282a92bc5655 -r a2c0aaf94460 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Mon Nov 19 20:47:39 2001 +0100
+++ b/src/ZF/ind_syntax.ML	Mon Nov 19 20:47:57 2001 +0100
@@ -1,9 +1,9 @@
-(*  Title:      ZF/ind-syntax.ML
+(*  Title:      ZF/ind_syntax.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Abstract Syntax functions for Inductive Definitions
+Abstract Syntax functions for Inductive Definitions.
 *)
 
 (*The structure protects these items from redeclaration (somewhat!).  The