tuned;
authorwenzelm
Mon Nov 19 20:47:57 2001 +0100 (2001-11-19 ago)
changeset 12243a2c0aaf94460
parent 12242 282a92bc5655
child 12244 179f142ffb03
tuned;
src/ZF/Induct/Tree_Forest.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/ZF/Induct/Tree_Forest.thy	Mon Nov 19 20:47:39 2001 +0100
     1.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Mon Nov 19 20:47:57 2001 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4    apply (rule Part_subset)
     1.5    done
     1.6  
     1.7 -lemma treeI [TC]: "x : tree(A) ==> x : tree_forest(A)"
     1.8 +lemma treeI [TC]: "x \<in> tree(A) ==> x \<in> tree_forest(A)"
     1.9    by (rule tree_subset_TF [THEN subsetD])
    1.10  
    1.11  lemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)"
    1.12 @@ -45,7 +45,7 @@
    1.13    apply (rule Part_subset)
    1.14    done
    1.15  
    1.16 -lemma treeI [TC]: "x : forest(A) ==> x : tree_forest(A)"
    1.17 +lemma treeI [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
    1.18    by (rule forest_subset_TF [THEN subsetD])
    1.19  
    1.20  lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)"
    1.21 @@ -54,7 +54,7 @@
    1.22    done
    1.23  
    1.24  lemma (notes rews = tree_forest.con_defs tree_def forest_def)
    1.25 -  tree_forest_unfold: "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))"
    1.26 +  tree_forest_unfold: "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
    1.27      -- {* NOT useful, but interesting \dots *}
    1.28    apply (unfold tree_def forest_def)
    1.29    apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
    1.30 @@ -86,23 +86,23 @@
    1.31  lemma TF_rec_type:
    1.32    "[| z \<in> tree_forest(A);
    1.33        !!x f r. [| x \<in> A;  f \<in> forest(A);  r \<in> C(f)
    1.34 -                |] ==> b(x,f,r): C(Tcons(x,f));
    1.35 +                |] ==> b(x,f,r) \<in> C(Tcons(x,f));
    1.36        c \<in> C(Fnil);
    1.37 -      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1: C(t); r2: C(f)
    1.38 -                    |] ==> d(t,f,r1,r2): C(Fcons(t,f))
    1.39 +      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1 \<in> C(t); r2 \<in> C(f)
    1.40 +                    |] ==> d(t,f,r1,r2) \<in> C(Fcons(t,f))
    1.41     |] ==> tree_forest_rec(b,c,d,z) \<in> C(z)"
    1.42    by (induct_tac z) simp_all
    1.43  
    1.44  lemma tree_forest_rec_type:
    1.45    "[| !!x f r. [| x \<in> A;  f \<in> forest(A);  r \<in> D(f)
    1.46 -                |] ==> b(x,f,r): C(Tcons(x,f));
    1.47 +                |] ==> b(x,f,r) \<in> C(Tcons(x,f));
    1.48        c \<in> D(Fnil);
    1.49 -      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1: C(t); r2: D(f)
    1.50 -                    |] ==> d(t,f,r1,r2): D(Fcons(t,f))
    1.51 -   |] ==> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t)  \<in> C(t)) &
    1.52 +      !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1 \<in> C(t); r2 \<in> D(f)
    1.53 +                    |] ==> d(t,f,r1,r2) \<in> D(Fcons(t,f))
    1.54 +   |] ==> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
    1.55            (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
    1.56      -- {* Mutually recursive version. *}
    1.57 -  apply (unfold Ball_def)  (* FIXME *)
    1.58 +  apply (unfold Ball_def)
    1.59    apply (rule tree_forest.mutual_induct)
    1.60    apply simp_all
    1.61    done
    1.62 @@ -159,7 +159,7 @@
    1.63    apply simp_all
    1.64    done
    1.65  
    1.66 -lemma map_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
    1.67 +lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
    1.68    apply (erule list.induct)
    1.69    apply simp_all
    1.70    done
    1.71 @@ -168,16 +168,14 @@
    1.72    \medskip @{text map}.
    1.73  *}
    1.74  
    1.75 -lemma map_type:
    1.76 -  "[| !!x. x \<in> A ==> h(x): B |] ==>
    1.77 -     (\<forall>t \<in> tree(A). map(h,t) \<in> tree(B)) &
    1.78 -     (\<forall>f \<in> forest(A). map(h,f) \<in> forest(B))"
    1.79 -  apply (unfold Ball_def)  (* FIXME *)
    1.80 -  apply (rule tree_forest.mutual_induct)
    1.81 -  apply simp_all
    1.82 +lemma (assumes h_type: "!!x. x \<in> A ==> h(x): B")
    1.83 +    map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
    1.84 +  and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
    1.85 +  apply (induct rule: tree_forest.mutual_induct)
    1.86 +    apply (insert h_type)
    1.87 +    apply simp_all
    1.88    done
    1.89  
    1.90 -
    1.91  text {*
    1.92    \medskip @{text size}.
    1.93  *}
     2.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Nov 19 20:47:39 2001 +0100
     2.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Nov 19 20:47:57 2001 +0100
     2.3 @@ -66,7 +66,7 @@
     2.4    val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists);
     2.5  
     2.6    val dummy =
     2.7 -    writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ big_rec_name);
     2.8 +    writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name);
     2.9  
    2.10    val case_varname = "f";                (*name for case variables*)
    2.11  
     3.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:39 2001 +0100
     3.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:57 2001 +0100
     3.3 @@ -152,7 +152,7 @@
     3.4  
     3.5  
     3.6    val dummy = conditional verbose (fn () =>
     3.7 -    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ big_rec_name));
     3.8 +    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name));
     3.9  
    3.10    (*Forbid the inductive definition structure from clashing with a theory
    3.11      name.  This restriction may become obsolete as ML is de-emphasized.*)
     4.1 --- a/src/ZF/ind_syntax.ML	Mon Nov 19 20:47:39 2001 +0100
     4.2 +++ b/src/ZF/ind_syntax.ML	Mon Nov 19 20:47:57 2001 +0100
     4.3 @@ -1,9 +1,9 @@
     4.4 -(*  Title:      ZF/ind-syntax.ML
     4.5 +(*  Title:      ZF/ind_syntax.ML
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1993  University of Cambridge
     4.9  
    4.10 -Abstract Syntax functions for Inductive Definitions
    4.11 +Abstract Syntax functions for Inductive Definitions.
    4.12  *)
    4.13  
    4.14  (*The structure protects these items from redeclaration (somewhat!).  The