# HG changeset patch
# User wenzelm
# Date 1005844180 -3600
# Node ID 7198f403a2f957aceeb3f0b86f7135c6d02b3e75
# Parent  b544785b6cc988da84cf58e534d74b8326fe227e
added Term and Tree_Forest (from converted ZF/ex);

diff -r b544785b6cc9 -r 7198f403a2f9 src/ZF/Induct/ROOT.ML
--- a/src/ZF/Induct/ROOT.ML	Thu Nov 15 18:08:19 2001 +0100
+++ b/src/ZF/Induct/ROOT.ML	Thu Nov 15 18:09:40 2001 +0100
@@ -1,13 +1,15 @@
-(*  Title:      ZF/ex/ROOT
+(*  Title:      ZF/Induct/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 
-Inductive definitions
+Inductive definitions.
 *)
 
 time_use_thy "Datatypes";
 time_use_thy "Binary_Trees";
+time_use_thy "Term";            (*recursion over the list functor*)
+time_use_thy "Tree_Forest"      (*mutual recursion*)
 time_use_thy "Mutil";           (*mutilated chess board*)
 
 (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
diff -r b544785b6cc9 -r 7198f403a2f9 src/ZF/Induct/Term.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Term.thy	Thu Nov 15 18:09:40 2001 +0100
@@ -0,0 +1,303 @@
+(*  Title:      ZF/Induct/Term.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+*)
+
+header {* Terms over an alphabet *}
+
+theory Term = Main:
+
+text {*
+  Illustrates the list functor (essentially the same type as in @{text
+  Trees_Forest}).
+*}
+
+consts
+  "term" :: "i => i"
+
+datatype "term(A)" = Apply ("a \<in> A", "l \<in> list(term(A))")
+  monos list_mono
+  type_elims list_univ [THEN subsetD, elim_format]
+
+declare Apply [TC]
+
+constdefs
+  term_rec :: "[i, [i, i, i] => i] => i"
+  "term_rec(t,d) ==
+    Vrec(t, \<lambda>t g. term_case(\<lambda>x zs. d(x, zs, map(\<lambda>z. g`z, zs)), t))"
+
+  term_map :: "[i => i, i] => i"
+  "term_map(f,t) == term_rec(t, \<lambda>x zs rs. Apply(f(x), rs))"
+
+  term_size :: "i => i"
+  "term_size(t) == term_rec(t, \<lambda>x zs rs. succ(list_add(rs)))"
+
+  reflect :: "i => i"
+  "reflect(t) == term_rec(t, \<lambda>x zs rs. Apply(x, rev(rs)))"
+
+  preorder :: "i => i"
+  "preorder(t) == term_rec(t, \<lambda>x zs rs. Cons(x, flat(rs)))"
+
+  postorder :: "i => i"
+  "postorder(t) == term_rec(t, \<lambda>x zs rs. flat(rs) @ [x])"
+
+lemma term_unfold: "term(A) = A * list(term(A))"
+  by (fast intro!: term.intros [unfolded term.con_defs]
+    elim: term.cases [unfolded term.con_defs])
+
+lemma term_induct2:
+  "[| t \<in> term(A);
+      !!x.      [| x \<in> A |] ==> P(Apply(x,Nil));
+      !!x z zs. [| x \<in> A;  z \<in> term(A);  zs: list(term(A));  P(Apply(x,zs))
+                |] ==> P(Apply(x, Cons(z,zs)))
+     |] ==> P(t)"
+  -- {* Induction on @{term "term(A)"} followed by induction on @{term list}. *}
+  apply (induct_tac t)
+  apply (erule list.induct)
+   apply (auto dest: list_CollectD)
+  done
+
+lemma term_induct_eqn:
+  "[| t \<in> term(A);
+      !!x zs. [| x \<in> A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==>
+              f(Apply(x,zs)) = g(Apply(x,zs))
+   |] ==> f(t) = g(t)"
+  -- {* Induction on @{term "term(A)"} to prove an equation. *}
+  apply (induct_tac t)
+  apply (auto dest: map_list_Collect list_CollectD)
+  done
+
+text {*
+  \medskip Lemmas to justify using @{term "term"} in other recursive
+  type definitions.
+*}
+
+lemma term_mono: "A \<subseteq> B ==> term(A) \<subseteq> term(B)"
+  apply (unfold term.defs)
+  apply (rule lfp_mono)
+    apply (rule term.bnd_mono)+
+  apply (rule univ_mono basic_monos| assumption)+
+  done
+
+lemma term_univ: "term(univ(A)) \<subseteq> univ(A)"
+  -- {* Easily provable by induction also *}
+  apply (unfold term.defs term.con_defs)
+  apply (rule lfp_lowerbound)
+   apply (rule_tac [2] A_subset_univ [THEN univ_mono])
+  apply safe
+  apply (assumption | rule Pair_in_univ list_univ [THEN subsetD])+
+  done
+
+lemma term_subset_univ: "A \<subseteq> univ(B) ==> term(A) \<subseteq> univ(B)"
+  apply (rule subset_trans)
+   apply (erule term_mono)
+  apply (rule term_univ)
+  done
+
+lemma term_into_univ: "[| t \<in> term(A);  A \<subseteq> univ(B) |] ==> t \<in> univ(B)"
+  by (rule term_subset_univ [THEN subsetD])
+
+text {*
+  \medskip @{text term_rec} -- by @{text Vset} recursion.
+*}
+
+lemma map_lemma: "[| l \<in> list(A);  Ord(i);  rank(l)<i |]
+    ==> map(\<lambda>z. (\<lambda>x \<in> Vset(i).h(x)) ` z, l) = map(h,l)"
+  -- {* @{term map} works correctly on the underlying list of terms. *}
+  apply (induct set: list)
+   apply simp
+  apply (subgoal_tac "rank (a) <i & rank (l) < i")
+   apply (simp add: rank_of_Ord)
+  apply (simp add: list.con_defs)
+  apply (blast dest: rank_rls [THEN lt_trans])
+  done
+
+lemma term_rec [simp]: "ts \<in> list(A) ==>
+  term_rec(Apply(a,ts), d) = d(a, ts, map (\<lambda>z. term_rec(z,d), ts))"
+  -- {* Typing premise is necessary to invoke @{text map_lemma}. *}
+  apply (rule term_rec_def [THEN def_Vrec, THEN trans])
+  apply (unfold term.con_defs)
+  apply (simp add: rank_pair2 map_lemma)
+  done
+
+lemma term_rec_type:
+  "[| t \<in> term(A);
+      !!x zs r. [| x \<in> A;  zs: list(term(A));
+                   r \<in> list(\<Union>t \<in> term(A). C(t)) |]
+                ==> d(x, zs, r): C(Apply(x,zs))
+   |] ==> term_rec(t,d) \<in> C(t)"
+  -- {* Slightly odd typing condition on @{text r} in the second premise! *}
+proof -
+  assume a: "!!x zs r. [| x \<in> A;  zs: list(term(A));
+                   r \<in> list(\<Union>t \<in> term(A). C(t)) |]
+                ==> d(x, zs, r): C(Apply(x,zs))"
+  assume "t \<in> term(A)"
+  thus ?thesis
+    apply induct
+    apply (frule list_CollectD)
+    apply (subst term_rec)
+     apply (assumption | rule a)+
+    apply (erule list.induct)
+     apply (simp add: term_rec)
+   apply (auto simp add: term_rec)
+   done
+qed
+
+lemma def_term_rec:
+  "[| !!t. j(t)==term_rec(t,d);  ts: list(A) |] ==>
+    j(Apply(a,ts)) = d(a, ts, map(\<lambda>Z. j(Z), ts))"
+  apply (simp only:)
+  apply (erule term_rec)
+  done
+
+lemma term_rec_simple_type [TC]:
+  "[| t \<in> term(A);
+      !!x zs r. [| x \<in> A;  zs: list(term(A));  r \<in> list(C) |]
+                ==> d(x, zs, r): C
+   |] ==> term_rec(t,d) \<in> C"
+  apply (erule term_rec_type)
+  apply (drule subset_refl [THEN UN_least, THEN list_mono, THEN subsetD])
+  apply simp
+  done
+
+
+text {*
+  \medskip @{term term_map}.
+*}
+
+lemma term_map [simp]:
+    "ts \<in> list(A) \<Longrightarrow> term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))"
+  by (rule term_map_def [THEN def_term_rec])
+
+lemma term_map_type [TC]:
+    "[| t \<in> term(A);  !!x. x \<in> A ==> f(x): B |] ==> term_map(f,t) \<in> term(B)"
+  apply (unfold term_map_def)
+  apply (erule term_rec_simple_type)
+  apply fast
+  done
+
+lemma term_map_type2 [TC]:
+    "t \<in> term(A) ==> term_map(f,t) \<in> term({f(u). u \<in> A})"
+  apply (erule term_map_type)
+  apply (erule RepFunI)
+  done
+
+text {*
+  \medskip @{term term_size}.
+*}
+
+lemma term_size [simp]:
+    "ts \<in> list(A) \<Longrightarrow> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))"
+  by (rule term_size_def [THEN def_term_rec])
+
+lemma term_size_type [TC]: "t \<in> term(A) ==> term_size(t) \<in> nat"
+  by (auto simp add: term_size_def)
+
+
+text {*
+  \medskip @{text reflect}.
+*}
+
+lemma reflect [simp]:
+    "ts \<in> list(A) \<Longrightarrow> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))"
+  by (rule reflect_def [THEN def_term_rec])
+
+lemma reflect_type [TC]: "t \<in> term(A) ==> reflect(t) \<in> term(A)"
+  by (auto simp add: reflect_def)
+
+
+text {*
+  \medskip @{text preorder}.
+*}
+
+lemma preorder [simp]:
+    "ts \<in> list(A) \<Longrightarrow> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))"
+  by (rule preorder_def [THEN def_term_rec])
+
+lemma preorder_type [TC]: "t \<in> term(A) ==> preorder(t) \<in> list(A)"
+  by (simp add: preorder_def)
+
+
+text {*
+  \medskip @{text postorder}.
+*}
+
+lemma postorder [simp]:
+    "ts \<in> list(A) \<Longrightarrow> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]"
+  by (rule postorder_def [THEN def_term_rec])
+
+lemma postorder_type [TC]: "t \<in> term(A) ==> postorder(t) \<in> list(A)"
+  by (simp add: postorder_def)
+
+
+text {*
+  \medskip Theorems about @{text term_map}.
+*}
+
+declare List.map_compose [simp]
+
+lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t"
+  apply (erule term_induct_eqn)
+  apply simp
+  done
+
+lemma term_map_compose:
+    "t \<in> term(A) ==> term_map(f, term_map(g,t)) = term_map(\<lambda>u. f(g(u)), t)"
+  apply (erule term_induct_eqn)
+  apply simp
+  done
+
+lemma term_map_reflect:
+    "t \<in> term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"
+  apply (erule term_induct_eqn)
+  apply (simp add: rev_map_distrib [symmetric])
+  done
+
+
+text {*
+  \medskip Theorems about @{text term_size}.
+*}
+
+lemma term_size_term_map: "t \<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)"
+  apply (erule term_induct_eqn)
+  apply simp
+  done
+
+lemma term_size_reflect: "t \<in> term(A) ==> term_size(reflect(t)) = term_size(t)"
+  apply (erule term_induct_eqn)
+  apply (simp add: rev_map_distrib [symmetric] list_add_rev)
+  done
+
+lemma term_size_length: "t \<in> term(A) ==> term_size(t) = length(preorder(t))"
+  apply (erule term_induct_eqn)
+  apply (simp add: length_flat)
+  done
+
+
+text {*
+  \medskip Theorems about @{text reflect}.
+*}
+
+lemma reflect_reflect_ident: "t \<in> term(A) ==> reflect(reflect(t)) = t"
+  apply (erule term_induct_eqn)
+  apply (simp add: rev_map_distrib)
+  done
+
+
+text {*
+  \medskip Theorems about preorder.
+*}
+
+lemma preorder_term_map: "t \<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"
+  apply (erule term_induct_eqn)
+  apply (simp add: map_flat)
+  done
+
+lemma preorder_reflect_eq_rev_postorder:
+    "t \<in> term(A) ==> preorder(reflect(t)) = rev(postorder(t))"
+  apply (erule term_induct_eqn)
+  apply (simp add: rev_app_distrib rev_flat rev_map_distrib [symmetric])
+  done
+
+end
diff -r b544785b6cc9 -r 7198f403a2f9 src/ZF/Induct/Tree_Forest.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Tree_Forest.thy	Thu Nov 15 18:09:40 2001 +0100
@@ -0,0 +1,267 @@
+(*  Title:      ZF/Induct/Tree_Forest.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+*)
+
+header {* Trees and forests, a mutually recursive type definition *}
+
+theory Tree_Forest = Main:
+
+subsection {* Datatype definition *}
+
+consts
+  tree :: "i => i"
+  forest :: "i => i"
+  tree_forest :: "i => i"
+
+datatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)")
+  and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)")
+
+declare tree_forest.intros [simp, TC]
+
+lemma tree_def: "tree(A) \<equiv> Part(tree_forest(A), Inl)"
+  by (simp only: tree_forest.defs)
+
+lemma forest_def: "forest(A) \<equiv> Part(tree_forest(A), Inr)"
+  by (simp only: tree_forest.defs)
+
+
+text {*
+  \medskip @{term "tree_forest(A)" as the union of @{term "tree(A)"}
+  and @{term "forest(A)"}.
+*}
+
+lemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)"
+  apply (unfold tree_forest.defs)
+  apply (rule Part_subset)
+  done
+
+lemma treeI [TC]: "x : tree(A) ==> x : tree_forest(A)"
+  by (rule tree_subset_TF [THEN subsetD])
+
+lemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)"
+  apply (unfold tree_forest.defs)
+  apply (rule Part_subset)
+  done
+
+lemma treeI [TC]: "x : forest(A) ==> x : tree_forest(A)"
+  by (rule forest_subset_TF [THEN subsetD])
+
+lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)"
+  apply (insert tree_subset_TF forest_subset_TF)
+  apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases)
+  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))"
+    -- {* NOT useful, but interesting \dots *}
+  apply (unfold tree_def forest_def)
+  apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
+    elim: tree_forest.cases [unfolded rews])
+  done
+
+lemma tree_forest_unfold':
+  "tree_forest(A) =
+    A \<times> Part(tree_forest(A), \<lambda>w. Inr(w)) +
+    {0} + Part(tree_forest(A), \<lambda>w. Inl(w)) * Part(tree_forest(A), \<lambda>w. Inr(w))"
+  by (rule tree_forest_unfold [unfolded tree_def forest_def])
+
+lemma tree_unfold: "tree(A) = {Inl(x). x \<in> A \<times> forest(A)}"
+  apply (unfold tree_def forest_def)
+  apply (rule Part_Inl [THEN subst])
+  apply (rule tree_forest_unfold' [THEN subst_context])
+  done
+
+lemma forest_unfold: "forest(A) = {Inr(x). x \<in> {0} + tree(A)*forest(A)}"
+  apply (unfold tree_def forest_def)
+  apply (rule Part_Inr [THEN subst])
+  apply (rule tree_forest_unfold' [THEN subst_context])
+  done
+
+text {*
+  \medskip Type checking for recursor: Not needed; possibly interesting?
+*}
+
+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));
+      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))
+   |] ==> 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));
+      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)) &
+          (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
+    -- {* Mutually recursive version. *}
+  apply (unfold Ball_def)  (* FIXME *)
+  apply (rule tree_forest.mutual_induct)
+  apply simp_all
+  done
+
+
+subsection {* Operations *}
+
+consts
+  map :: "[i => i, i] => i"
+  size :: "i => i"
+  preorder :: "i => i"
+  list_of_TF :: "i => i"
+  of_list :: "i => i"
+  reflect :: "i => i"
+
+primrec
+  "list_of_TF (Tcons(x,f)) = [Tcons(x,f)]"
+  "list_of_TF (Fnil) = []"
+  "list_of_TF (Fcons(t,tf)) = Cons (t, list_of_TF(tf))"
+
+primrec
+  "of_list([]) = Fnil"
+  "of_list(Cons(t,l)) = Fcons(t, of_list(l))"
+
+primrec
+  "map (h, Tcons(x,f)) = Tcons(h(x), map(h,f))"
+  "map (h, Fnil) = Fnil"
+  "map (h, Fcons(t,tf)) = Fcons (map(h, t), map(h, tf))"
+
+primrec
+  "size (Tcons(x,f)) = succ(size(f))"
+  "size (Fnil) = 0"
+  "size (Fcons(t,tf)) = size(t) #+ size(tf)"
+
+primrec
+  "preorder (Tcons(x,f)) = Cons(x, preorder(f))"
+  "preorder (Fnil) = Nil"
+  "preorder (Fcons(t,tf)) = preorder(t) @ preorder(tf)"
+
+primrec
+  "reflect (Tcons(x,f)) = Tcons(x, reflect(f))"
+  "reflect (Fnil) = Fnil"
+  "reflect (Fcons(t,tf)) =
+    of_list (list_of_TF (reflect(tf)) @ Cons(reflect(t), Nil))"
+
+
+text {*
+  \medskip @{text list_of_TF} and @{text of_list}.
+*}
+
+lemma list_of_TF_type [TC]:
+    "z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))"
+  apply (erule tree_forest.induct)
+  apply simp_all
+  done
+
+lemma map_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
+  apply (erule list.induct)
+  apply simp_all
+  done
+
+text {*
+  \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
+  done
+
+
+text {*
+  \medskip @{text size}.
+*}
+
+lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
+  apply (erule tree_forest.induct)
+  apply simp_all
+  done
+
+
+text {*
+  \medskip @{text preorder}.
+*}
+
+lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
+  apply (erule tree_forest.induct)
+  apply simp_all
+  done
+
+
+text {*
+  \medskip Theorems about @{text list_of_TF} and @{text of_list}.
+*}
+
+lemma forest_induct:
+  "[| f \<in> forest(A);
+      R(Fnil);
+      !!t f. [| t \<in> tree(A);  f \<in> forest(A);  R(f) |] ==> R(Fcons(t,f))
+   |] ==> R(f)"
+  -- {* Essentially the same as list induction. *}
+  apply (erule tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp])
+    apply (rule TrueI)
+   apply simp
+  apply simp
+  done
+
+lemma forest_iso: "f \<in> forest(A) ==> of_list(list_of_TF(f)) = f"
+  apply (erule forest_induct)
+   apply simp_all
+  done
+
+lemma tree_list_iso: "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts"
+  apply (erule list.induct)
+   apply simp_all
+  done
+
+
+text {*
+  \medskip Theorems about @{text map}.
+*}
+
+lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
+  apply (erule tree_forest.induct)
+    apply simp_all
+  done
+
+lemma map_compose: "z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
+  apply (erule tree_forest.induct)
+    apply simp_all
+  done
+
+
+text {*
+  \medskip Theorems about @{text size}.
+*}
+
+lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
+  apply (erule tree_forest.induct)
+    apply simp_all
+  done
+
+lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))"
+  apply (erule tree_forest.induct)
+    apply (simp_all add: length_app)
+  done
+
+text {*
+  \medskip Theorems about @{text preorder}.
+*}
+
+lemma preorder_map:
+    "z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))"
+  apply (erule tree_forest.induct)
+    apply (simp_all add: map_app_distrib)
+  done
+
+end