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