src/ZF/Induct/Tree_Forest.thy
author wenzelm
Mon Nov 19 20:47:57 2001 +0100 (2001-11-19 ago)
changeset 12243 a2c0aaf94460
parent 12216 dda8c04a8fb4
child 12610 8b9845807f77
permissions -rw-r--r--
tuned;
     1 (*  Title:      ZF/Induct/Tree_Forest.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 *)
     6 
     7 header {* Trees and forests, a mutually recursive type definition *}
     8 
     9 theory Tree_Forest = Main:
    10 
    11 subsection {* Datatype definition *}
    12 
    13 consts
    14   tree :: "i => i"
    15   forest :: "i => i"
    16   tree_forest :: "i => i"
    17 
    18 datatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)")
    19   and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)")
    20 
    21 declare tree_forest.intros [simp, TC]
    22 
    23 lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)"
    24   by (simp only: tree_forest.defs)
    25 
    26 lemma forest_def: "forest(A) == Part(tree_forest(A), Inr)"
    27   by (simp only: tree_forest.defs)
    28 
    29 
    30 text {*
    31   \medskip @{term "tree_forest(A)"} as the union of @{term "tree(A)"}
    32   and @{term "forest(A)"}.
    33 *}
    34 
    35 lemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)"
    36   apply (unfold tree_forest.defs)
    37   apply (rule Part_subset)
    38   done
    39 
    40 lemma treeI [TC]: "x \<in> tree(A) ==> x \<in> tree_forest(A)"
    41   by (rule tree_subset_TF [THEN subsetD])
    42 
    43 lemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)"
    44   apply (unfold tree_forest.defs)
    45   apply (rule Part_subset)
    46   done
    47 
    48 lemma treeI [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
    49   by (rule forest_subset_TF [THEN subsetD])
    50 
    51 lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)"
    52   apply (insert tree_subset_TF forest_subset_TF)
    53   apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases)
    54   done
    55 
    56 lemma (notes rews = tree_forest.con_defs tree_def forest_def)
    57   tree_forest_unfold: "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
    58     -- {* NOT useful, but interesting \dots *}
    59   apply (unfold tree_def forest_def)
    60   apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
    61     elim: tree_forest.cases [unfolded rews])
    62   done
    63 
    64 lemma tree_forest_unfold':
    65   "tree_forest(A) =
    66     A \<times> Part(tree_forest(A), \<lambda>w. Inr(w)) +
    67     {0} + Part(tree_forest(A), \<lambda>w. Inl(w)) * Part(tree_forest(A), \<lambda>w. Inr(w))"
    68   by (rule tree_forest_unfold [unfolded tree_def forest_def])
    69 
    70 lemma tree_unfold: "tree(A) = {Inl(x). x \<in> A \<times> forest(A)}"
    71   apply (unfold tree_def forest_def)
    72   apply (rule Part_Inl [THEN subst])
    73   apply (rule tree_forest_unfold' [THEN subst_context])
    74   done
    75 
    76 lemma forest_unfold: "forest(A) = {Inr(x). x \<in> {0} + tree(A)*forest(A)}"
    77   apply (unfold tree_def forest_def)
    78   apply (rule Part_Inr [THEN subst])
    79   apply (rule tree_forest_unfold' [THEN subst_context])
    80   done
    81 
    82 text {*
    83   \medskip Type checking for recursor: Not needed; possibly interesting?
    84 *}
    85 
    86 lemma TF_rec_type:
    87   "[| z \<in> tree_forest(A);
    88       !!x f r. [| x \<in> A;  f \<in> forest(A);  r \<in> C(f)
    89                 |] ==> b(x,f,r) \<in> C(Tcons(x,f));
    90       c \<in> C(Fnil);
    91       !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1 \<in> C(t); r2 \<in> C(f)
    92                     |] ==> d(t,f,r1,r2) \<in> C(Fcons(t,f))
    93    |] ==> tree_forest_rec(b,c,d,z) \<in> C(z)"
    94   by (induct_tac z) simp_all
    95 
    96 lemma tree_forest_rec_type:
    97   "[| !!x f r. [| x \<in> A;  f \<in> forest(A);  r \<in> D(f)
    98                 |] ==> b(x,f,r) \<in> C(Tcons(x,f));
    99       c \<in> D(Fnil);
   100       !!t f r1 r2. [| t \<in> tree(A);  f \<in> forest(A);  r1 \<in> C(t); r2 \<in> D(f)
   101                     |] ==> d(t,f,r1,r2) \<in> D(Fcons(t,f))
   102    |] ==> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
   103           (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
   104     -- {* Mutually recursive version. *}
   105   apply (unfold Ball_def)
   106   apply (rule tree_forest.mutual_induct)
   107   apply simp_all
   108   done
   109 
   110 
   111 subsection {* Operations *}
   112 
   113 consts
   114   map :: "[i => i, i] => i"
   115   size :: "i => i"
   116   preorder :: "i => i"
   117   list_of_TF :: "i => i"
   118   of_list :: "i => i"
   119   reflect :: "i => i"
   120 
   121 primrec
   122   "list_of_TF (Tcons(x,f)) = [Tcons(x,f)]"
   123   "list_of_TF (Fnil) = []"
   124   "list_of_TF (Fcons(t,tf)) = Cons (t, list_of_TF(tf))"
   125 
   126 primrec
   127   "of_list([]) = Fnil"
   128   "of_list(Cons(t,l)) = Fcons(t, of_list(l))"
   129 
   130 primrec
   131   "map (h, Tcons(x,f)) = Tcons(h(x), map(h,f))"
   132   "map (h, Fnil) = Fnil"
   133   "map (h, Fcons(t,tf)) = Fcons (map(h, t), map(h, tf))"
   134 
   135 primrec
   136   "size (Tcons(x,f)) = succ(size(f))"
   137   "size (Fnil) = 0"
   138   "size (Fcons(t,tf)) = size(t) #+ size(tf)"
   139 
   140 primrec
   141   "preorder (Tcons(x,f)) = Cons(x, preorder(f))"
   142   "preorder (Fnil) = Nil"
   143   "preorder (Fcons(t,tf)) = preorder(t) @ preorder(tf)"
   144 
   145 primrec
   146   "reflect (Tcons(x,f)) = Tcons(x, reflect(f))"
   147   "reflect (Fnil) = Fnil"
   148   "reflect (Fcons(t,tf)) =
   149     of_list (list_of_TF (reflect(tf)) @ Cons(reflect(t), Nil))"
   150 
   151 
   152 text {*
   153   \medskip @{text list_of_TF} and @{text of_list}.
   154 *}
   155 
   156 lemma list_of_TF_type [TC]:
   157     "z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))"
   158   apply (erule tree_forest.induct)
   159   apply simp_all
   160   done
   161 
   162 lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
   163   apply (erule list.induct)
   164   apply simp_all
   165   done
   166 
   167 text {*
   168   \medskip @{text map}.
   169 *}
   170 
   171 lemma (assumes h_type: "!!x. x \<in> A ==> h(x): B")
   172     map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
   173   and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
   174   apply (induct rule: tree_forest.mutual_induct)
   175     apply (insert h_type)
   176     apply simp_all
   177   done
   178 
   179 text {*
   180   \medskip @{text size}.
   181 *}
   182 
   183 lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
   184   apply (erule tree_forest.induct)
   185   apply simp_all
   186   done
   187 
   188 
   189 text {*
   190   \medskip @{text preorder}.
   191 *}
   192 
   193 lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
   194   apply (erule tree_forest.induct)
   195   apply simp_all
   196   done
   197 
   198 
   199 text {*
   200   \medskip Theorems about @{text list_of_TF} and @{text of_list}.
   201 *}
   202 
   203 lemma forest_induct:
   204   "[| f \<in> forest(A);
   205       R(Fnil);
   206       !!t f. [| t \<in> tree(A);  f \<in> forest(A);  R(f) |] ==> R(Fcons(t,f))
   207    |] ==> R(f)"
   208   -- {* Essentially the same as list induction. *}
   209   apply (erule tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp])
   210     apply (rule TrueI)
   211    apply simp
   212   apply simp
   213   done
   214 
   215 lemma forest_iso: "f \<in> forest(A) ==> of_list(list_of_TF(f)) = f"
   216   apply (erule forest_induct)
   217    apply simp_all
   218   done
   219 
   220 lemma tree_list_iso: "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts"
   221   apply (erule list.induct)
   222    apply simp_all
   223   done
   224 
   225 
   226 text {*
   227   \medskip Theorems about @{text map}.
   228 *}
   229 
   230 lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
   231   apply (erule tree_forest.induct)
   232     apply simp_all
   233   done
   234 
   235 lemma map_compose:
   236     "z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
   237   apply (erule tree_forest.induct)
   238     apply simp_all
   239   done
   240 
   241 
   242 text {*
   243   \medskip Theorems about @{text size}.
   244 *}
   245 
   246 lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
   247   apply (erule tree_forest.induct)
   248     apply simp_all
   249   done
   250 
   251 lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))"
   252   apply (erule tree_forest.induct)
   253     apply (simp_all add: length_app)
   254   done
   255 
   256 text {*
   257   \medskip Theorems about @{text preorder}.
   258 *}
   259 
   260 lemma preorder_map:
   261     "z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))"
   262   apply (erule tree_forest.induct)
   263     apply (simp_all add: map_app_distrib)
   264   done
   265 
   266 end