# HG changeset patch # User wenzelm # Date 1005844099 -3600 # Node ID b544785b6cc988da84cf58e534d74b8326fe227e # Parent 8213fd95acb56d2688998116e2d20f91f9814784 TF and Term moved to ZF/Induct; diff -r 8213fd95acb5 -r b544785b6cc9 src/ZF/ex/ROOT.ML --- 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*) diff -r 8213fd95acb5 -r b544785b6cc9 src/ZF/ex/TF.ML --- 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) \\ tree_forest(A)"; -by (rtac Part_subset 1); -qed "tree_subset_TF"; - -Goalw [forest_def] "forest(A) \\ 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 \\ 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 \\ {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 \\ tree_forest(A); \ -\ !!x f r. [| x \\ A; f \\ forest(A); r \\ C(f) \ -\ |] ==> b(x,f,r): C(Tcons(x,f)); \ -\ c \\ C(Fnil); \ -\ !!t f r1 r2. [| t \\ tree(A); f \\ forest(A); r1: C(t); r2: C(f) \ -\ |] ==> d(t,f,r1,r2): C(Fcons(t,f)) \ -\ |] ==> tree_forest_rec(b,c,d,z) \\ 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 \\ A; f \\ forest(A); r \\ D(f) \ -\ |] ==> b(x,f,r): C(Tcons(x,f)); \ -\ c \\ D(Fnil); \ -\ !!t f r1 r2. [| t \\ tree(A); f \\ forest(A); r1: C(t); r2: D(f) \ -\ |] ==> d(t,f,r1,r2): D(Fcons(t,f)) \ -\ |] ==> (\\t \\ tree(A). tree_forest_rec(b,c,d,t) \\ C(t)) & \ -\ (\\f \\ forest(A). tree_forest_rec(b,c,d,f) \\ 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 \\ tree_forest(A) ==> list_of_TF(z) \\ list(tree(A))"; -by (etac tree_forest.induct 1); -by (ALLGOALS Asm_simp_tac); -qed "list_of_TF_type"; - -Goal "l \\ list(tree(A)) ==> of_list(l) \\ forest(A)"; -by (etac list.induct 1); -by (ALLGOALS Asm_simp_tac); -qed "of_list_type"; - - -(** map **) - -val prems = Goal - "[| !!x. x \\ A ==> h(x): B |] ==> \ -\ (\\t \\ tree(A). map(h,t) \\ tree(B)) & \ -\ (\\f \\ forest(A). map(h,f) \\ 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 \\ tree_forest(A) ==> size(z) \\ nat"; -by (etac tree_forest.induct 1); -by (ALLGOALS Asm_simp_tac); -qed "size_type"; - - -(** preorder **) - -Goal "z \\ tree_forest(A) ==> preorder(z) \\ 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 \\ forest(A); \ -\ R(Fnil); \ -\ !!t f. [| t \\ tree(A); f \\ 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 \\ 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 \\ tree_forest(A) ==> map(%u. u, z) = z"; -by (etac tree_forest.induct 1); -by (ALLGOALS Asm_simp_tac); -qed "map_ident"; - -Goal "z \\ 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 \\ 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 \\ 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 \\ 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"; diff -r 8213fd95acb5 -r b544785b6cc9 src/ZF/ex/TF.thy --- 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 \\ A", "f \\ forest(A)") -and - "forest(A)" = Fnil | Fcons ("t \\ tree(A)", "f \\ 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 diff -r 8213fd95acb5 -r b544785b6cc9 src/ZF/ex/Term.ML --- 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 \\ term(A); \ -\ !!x. [| x \\ A |] ==> P(Apply(x,Nil)); \ -\ !!x z zs. [| x \\ A; z \\ 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 \\ term(A); \ -\ !!x zs. [| x \\ 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 \\ B ==> term(A) \\ 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)) \\ 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 \\ term(A); A \\ univ(B) |] ==> t \\ 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 \\ list(A); Ord(i) |] ==> \ -\ rank(l) map(%z. (\\x \\ 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) 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 \\ term(A); \ -\ !!x zs r. [| x \\ A; zs: list(term(A)); \ -\ r \\ list(\\t \\ term(A). C(t)) |] \ -\ ==> d(x, zs, r): C(Apply(x,zs)) \ -\ |] ==> term_rec(t,d) \\ 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 \\ term(A); \ -\ !!x zs r. [| x \\ A; zs: list(term(A)); r \\ list(C) |] \ -\ ==> d(x, zs, r): C \ -\ |] ==> term_rec(t,d) \\ 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 \\ term(A); !!x. x \\ A ==> f(x): B |] ==> term_map(f,t) \\ term(B)"; -by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1)); -qed "term_map_type"; - -Goal "t \\ term(A) ==> term_map(f,t) \\ term({f(u). u \\ 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 \\ term(A) ==> term_size(t) \\ nat"; -by Auto_tac; -qed "term_size_type"; - - -(** reflect **) - -bind_thm ("reflect", reflect_def RS def_term_rec); - -Goalw [reflect_def] "t \\ term(A) ==> reflect(t) \\ term(A)"; -by Auto_tac; -qed "reflect_type"; - -(** preorder **) - -bind_thm ("preorder", preorder_def RS def_term_rec); - -Goalw [preorder_def] "t \\ term(A) ==> preorder(t) \\ list(A)"; -by Auto_tac; -qed "preorder_type"; - -(** postorder **) - -bind_thm ("postorder", postorder_def RS def_term_rec); - -Goalw [postorder_def] "t \\ term(A) ==> postorder(t) \\ 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 \\ 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 \\ 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 \\ 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 \\ 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 \\ 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 \\ 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 \\ 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 \\ 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 \\ 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."; diff -r 8213fd95acb5 -r b544785b6cc9 src/ZF/ex/Term.thy --- 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 \\ A", "l \\ 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