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