--- a/src/ZF/ex/ROOT.ML Thu Nov 15 17:59:56 2001 +0100
+++ b/src/ZF/ex/ROOT.ML Thu Nov 15 18:08:19 2001 +0100
@@ -15,8 +15,6 @@
time_use_thy "BinEx"; (*Binary integer arithmetic*)
(** Datatypes **)
-time_use_thy "Term"; (*terms: recursion over the list functor*)
-time_use_thy "TF"; (*trees/forests: mutual recursion*)
time_use_thy "Ntree"; (*variable-branching trees; function demo*)
time_use_thy "Brouwer"; (*Infinite-branching trees*)
--- a/src/ZF/ex/TF.ML Thu Nov 15 17:59:56 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(* Title: ZF/ex/tf.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Trees & forests, a mutually recursive type definition.
-*)
-
-Addsimps tree_forest.intrs;
-AddTCs tree_forest.intrs;
-
-(** tree_forest(A) as the union of tree(A) and forest(A) **)
-
-val [_, tree_def, forest_def] = tree_forest.defs;
-
-Goalw [tree_def] "tree(A) \\<subseteq> tree_forest(A)";
-by (rtac Part_subset 1);
-qed "tree_subset_TF";
-
-Goalw [forest_def] "forest(A) \\<subseteq> tree_forest(A)";
-by (rtac Part_subset 1);
-qed "forest_subset_TF";
-
-Goal "tree(A) Un forest(A) = tree_forest(A)";
-by (safe_tac (subset_cs addSIs [equalityI, tree_subset_TF, forest_subset_TF]));
-by (fast_tac (claset() addSIs tree_forest.intrs addEs [tree_forest.elim]) 1);
-qed "TF_equals_Un";
-
-(** NOT useful, but interesting... **)
-
-Goalw [tree_def, forest_def]
- "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
-let open tree_forest;
- val rew = rewrite_rule (con_defs @ tl defs) in
-by (fast_tac (claset() addSIs (map rew intrs RL [PartD1]) addEs [rew elim]) 1)
-end;
-qed "tree_forest_unfold";
-
-val tree_forest_unfold' = rewrite_rule [tree_def, forest_def]
- tree_forest_unfold;
-
-Goalw [tree_def, forest_def]
- "tree(A) = {Inl(x). x \\<in> A*forest(A)}";
-by (rtac (Part_Inl RS subst) 1);
-by (rtac (tree_forest_unfold' RS subst_context) 1);
-qed "tree_unfold";
-
-Goalw [tree_def, forest_def]
- "forest(A) = {Inr(x). x \\<in> {0} + tree(A)*forest(A)}";
-by (rtac (Part_Inr RS subst) 1);
-by (rtac (tree_forest_unfold' RS subst_context) 1);
-qed "forest_unfold";
-
-
-(** Type checking for recursor: Not needed; possibly interesting (??) **)
-
-val major::prems = goal TF.thy
- "[| 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 (rtac (major RS tree_forest.induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-qed "TF_rec_type";
-
-(*Mutually recursive version*)
-val prems = goal TF.thy
- "[| !!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))";
-by (rewtac Ball_def);
-by (rtac tree_forest.mutual_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-qed "tree_forest_rec_type";
-
-
-(** list_of_TF and of_list **)
-
-Goal "z \\<in> tree_forest(A) ==> list_of_TF(z) \\<in> list(tree(A))";
-by (etac tree_forest.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "list_of_TF_type";
-
-Goal "l \\<in> list(tree(A)) ==> of_list(l) \\<in> forest(A)";
-by (etac list.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "of_list_type";
-
-
-(** map **)
-
-val prems = Goal
- "[| !!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))";
-by (rewtac Ball_def);
-by (rtac tree_forest.mutual_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-qed "map_type";
-
-
-(** size **)
-
-Goal "z \\<in> tree_forest(A) ==> size(z) \\<in> nat";
-by (etac tree_forest.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "size_type";
-
-
-(** preorder **)
-
-Goal "z \\<in> tree_forest(A) ==> preorder(z) \\<in> list(A)";
-by (etac tree_forest.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "preorder_type";
-
-
-(** Term simplification **)
-
-val treeI = tree_subset_TF RS subsetD
-and forestI = forest_subset_TF RS subsetD;
-
-AddTCs [treeI, forestI, list_of_TF_type, map_type, size_type, preorder_type];
-
-(** theorems about list_of_TF and of_list **)
-
-(*essentially the same as list induction*)
-val major::prems = Goal
- "[| f \\<in> forest(A); \
-\ R(Fnil); \
-\ !!t f. [| t \\<in> tree(A); f \\<in> forest(A); R(f) |] ==> R(Fcons(t,f)) \
-\ |] ==> R(f)";
-by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
-by (REPEAT (ares_tac (TrueI::prems) 1));
-qed "forest_induct";
-
-Goal "f \\<in> forest(A) ==> of_list(list_of_TF(f)) = f";
-by (etac forest_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "forest_iso";
-
-Goal "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts";
-by (etac list.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "tree_list_iso";
-
-(** theorems about map **)
-
-Goal "z \\<in> tree_forest(A) ==> map(%u. u, z) = z";
-by (etac tree_forest.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "map_ident";
-
-Goal "z \\<in> tree_forest(A) ==> map(h, map(j,z)) = map(%u. h(j(u)), z)";
-by (etac tree_forest.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "map_compose";
-
-(** theorems about size **)
-
-Goal "z \\<in> tree_forest(A) ==> size(map(h,z)) = size(z)";
-by (etac tree_forest.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "size_map";
-
-Goal "z \\<in> tree_forest(A) ==> size(z) = length(preorder(z))";
-by (etac tree_forest.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
-qed "size_length";
-
-(** theorems about preorder **)
-
-Goal "z \\<in> tree_forest(A) ==> preorder(TF.map(h,z)) = List.map(h, preorder(z))";
-by (etac tree_forest.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
-qed "preorder_map";
--- a/src/ZF/ex/TF.thy Thu Nov 15 17:59:56 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: ZF/ex/TF.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Trees & forests, a mutually recursive type definition.
-*)
-
-TF = Main +
-consts
- tree, forest, 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)")
-
-
-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))"
-
-end
--- a/src/ZF/ex/Term.ML Thu Nov 15 17:59:56 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,240 +0,0 @@
-(* Title: ZF/ex/Term.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Datatype definition of terms over an alphabet.
-Illustrates the list functor (essentially the same type as in Trees & Forests)
-*)
-
-AddTCs [term.Apply_I];
-
-Goal "term(A) = A * list(term(A))";
-let open term; val rew = rewrite_rule con_defs in
-by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
-end;
-qed "term_unfold";
-
-(*Induction on term(A) followed by induction on List *)
-val major::prems = Goal
- "[| 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)";
-by (rtac (major RS term.induct) 1);
-by (etac list.induct 1);
-by (etac CollectE 2);
-by (REPEAT (ares_tac (prems@[list_CollectD]) 1));
-qed "term_induct2";
-
-(*Induction on term(A) to prove an equation*)
-val major::prems = Goal
- "[| 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)";
-by (rtac (major RS term.induct) 1);
-by (resolve_tac prems 1);
-by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1));
-qed "term_induct_eqn";
-
-(** Lemmas to justify using "term" in other recursive type definitions **)
-
-Goalw term.defs "A \\<subseteq> B ==> term(A) \\<subseteq> term(B)";
-by (rtac lfp_mono 1);
-by (REPEAT (rtac term.bnd_mono 1));
-by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
-qed "term_mono";
-
-(*Easily provable by induction also*)
-Goalw (term.defs@term.con_defs) "term(univ(A)) \\<subseteq> univ(A)";
-by (rtac lfp_lowerbound 1);
-by (rtac (A_subset_univ RS univ_mono) 2);
-by Safe_tac;
-by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1));
-qed "term_univ";
-
-val term_subset_univ =
- term_mono RS (term_univ RSN (2,subset_trans)) |> standard;
-
-Goal "[| t \\<in> term(A); A \\<subseteq> univ(B) |] ==> t \\<in> univ(B)";
-by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1));
-qed "term_into_univ";
-
-
-(*** term_rec -- by Vset recursion ***)
-
-(*Lemma: map works correctly on the underlying list of terms*)
-Goal "[| l \\<in> list(A); Ord(i) |] ==> \
-\ rank(l)<i --> map(%z. (\\<lambda>x \\<in> Vset(i).h(x)) ` z, l) = map(h,l)";
-by (etac list.induct 1);
-by (Simp_tac 1);
-by (rtac impI 1);
-by (subgoal_tac "rank(a)<i & rank(l) < i" 1);
-by (asm_simp_tac (simpset() addsimps [rank_of_Ord]) 1);
-by (full_simp_tac (simpset() addsimps list.con_defs) 1);
-by (blast_tac (claset() addDs (rank_rls RL [lt_trans])) 1);
-qed "map_lemma";
-
-(*Typing premise is necessary to invoke map_lemma*)
-Goal "ts \\<in> list(A) ==> \
-\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
-by (rtac (term_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac term.con_defs);
-by (asm_simp_tac (simpset() addsimps [rank_pair2, map_lemma]) 1);;
-qed "term_rec";
-
-(*Slightly odd typing condition on r in the second premise!*)
-val major::prems = Goal
- "[| 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)";
-by (rtac (major RS term.induct) 1);
-by (ftac list_CollectD 1);
-by (stac term_rec 1);
-by (REPEAT (ares_tac prems 1));
-by (etac list.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [term_rec])));
-by Auto_tac;
-qed "term_rec_type";
-
-val [rew,tslist] = Goal
- "[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \
-\ j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))";
-by (rewtac rew);
-by (rtac (tslist RS term_rec) 1);
-qed "def_term_rec";
-
-val prems = Goal
- "[| 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";
-by (REPEAT (ares_tac (term_rec_type::prems) 1));
-by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
-qed "term_rec_simple_type";
-
-AddTCs [term_rec_simple_type];
-
-(** term_map **)
-
-bind_thm ("term_map", term_map_def RS def_term_rec);
-
-val prems = Goalw [term_map_def]
- "[| t \\<in> term(A); !!x. x \\<in> A ==> f(x): B |] ==> term_map(f,t) \\<in> term(B)";
-by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1));
-qed "term_map_type";
-
-Goal "t \\<in> term(A) ==> term_map(f,t) \\<in> term({f(u). u \\<in> A})";
-by (etac term_map_type 1);
-by (etac RepFunI 1);
-qed "term_map_type2";
-
-
-(** term_size **)
-
-bind_thm ("term_size", term_size_def RS def_term_rec);
-
-Goalw [term_size_def] "t \\<in> term(A) ==> term_size(t) \\<in> nat";
-by Auto_tac;
-qed "term_size_type";
-
-
-(** reflect **)
-
-bind_thm ("reflect", reflect_def RS def_term_rec);
-
-Goalw [reflect_def] "t \\<in> term(A) ==> reflect(t) \\<in> term(A)";
-by Auto_tac;
-qed "reflect_type";
-
-(** preorder **)
-
-bind_thm ("preorder", preorder_def RS def_term_rec);
-
-Goalw [preorder_def] "t \\<in> term(A) ==> preorder(t) \\<in> list(A)";
-by Auto_tac;
-qed "preorder_type";
-
-(** postorder **)
-
-bind_thm ("postorder", postorder_def RS def_term_rec);
-
-Goalw [postorder_def] "t \\<in> term(A) ==> postorder(t) \\<in> list(A)";
-by Auto_tac;
-qed "postorder_type";
-
-
-(** Term simplification **)
-
-AddTCs [term_map_type, term_map_type2, term_size_type,
- reflect_type, preorder_type, postorder_type];
-
-(*map_type2 and term_map_type2 instantiate variables*)
-Addsimps [term_rec, term_map, term_size, reflect, preorder, postorder];
-
-
-(** theorems about term_map **)
-
-Addsimps [thm "List.map_compose"]; (*there is also TF.map_compose*)
-
-Goal "t \\<in> term(A) ==> term_map(%u. u, t) = t";
-by (etac term_induct_eqn 1);
-by (Asm_simp_tac 1);
-qed "term_map_ident";
-
-Goal "t \\<in> term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
-by (etac term_induct_eqn 1);
-by (Asm_simp_tac 1);
-qed "term_map_compose";
-
-Goal "t \\<in> term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
-by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym]) 1);
-qed "term_map_reflect";
-
-
-(** theorems about term_size **)
-
-Goal "t \\<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)";
-by (etac term_induct_eqn 1);
-by (Asm_simp_tac 1);
-qed "term_size_term_map";
-
-Goal "t \\<in> term(A) ==> term_size(reflect(t)) = term_size(t)";
-by (etac term_induct_eqn 1);
-by (asm_simp_tac(simpset() addsimps [rev_map_distrib RS sym, list_add_rev]) 1);
-qed "term_size_reflect";
-
-Goal "t \\<in> term(A) ==> term_size(t) = length(preorder(t))";
-by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [length_flat]) 1);
-qed "term_size_length";
-
-
-(** theorems about reflect **)
-
-Goal "t \\<in> term(A) ==> reflect(reflect(t)) = t";
-by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib]) 1);
-qed "reflect_reflect_ident";
-
-
-(** theorems about preorder **)
-
-Goal "t \\<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
-by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_flat]) 1);
-qed "preorder_term_map";
-
-Goal "t \\<in> term(A) ==> preorder(reflect(t)) = rev(postorder(t))";
-by (etac term_induct_eqn 1);
-by (asm_simp_tac(simpset() addsimps [rev_app_distrib, rev_flat,
- rev_map_distrib RS sym]) 1);
-qed "preorder_reflect_eq_rev_postorder";
-
-
-writeln"Reached end of file.";
--- a/src/ZF/ex/Term.thy Thu Nov 15 17:59:56 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: ZF/ex/Term.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Terms over an alphabet.
-Illustrates the list functor (essentially the same type as in Trees & Forests)
-*)
-
-Term = Main +
-consts
- term :: i=>i
-
-datatype
- "term(A)" = Apply ("a \\<in> A", "l \\<in> list(term(A))")
- monos list_mono
-
- type_elims "[make_elim (list_univ RS subsetD)]"
-(*Or could have
- type_intrs "[list_univ RS subsetD]"
-*)
-
-constdefs
- term_rec :: [i, [i,i,i]=>i] => i
- "term_rec(t,d) ==
- Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z. g`z, zs)), t))"
-
- term_map :: [i=>i, i] => i
- "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
-
- term_size :: i=>i
- "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
-
- reflect :: i=>i
- "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
-
- preorder :: i=>i
- "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
-
- postorder :: i=>i
- "postorder(t) == term_rec(t, %x zs rs. flat(rs) @ [x])"
-
-end