--- 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
--- /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
--- /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