--- a/src/ZF/ex/Ntree.ML Wed Aug 17 10:33:23 1994 +0200
+++ b/src/ZF/ex/Ntree.ML Wed Aug 17 10:34:44 1994 +0200
@@ -11,6 +11,8 @@
open Ntree;
+(** ntree **)
+
goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
let open ntree; val rew = rewrite_rule con_defs in
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
@@ -20,24 +22,24 @@
(*A nicer induction rule than the standard one*)
val major::prems = goal Ntree.thy
- "[| t: ntree(A); \
+ "[| t: ntree(A); \
\ !!x n h. [| x: A; n: nat; h: n -> ntree(A); ALL i:n. P(h`i) \
-\ |] ==> P(Branch(x,h)) \
+\ |] ==> P(Branch(x,h)) \
\ |] ==> P(t)";
by (rtac (major RS ntree.induct) 1);
by (etac UN_E 1);
by (REPEAT_SOME (ares_tac prems));
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
by (fast_tac (ZF_cs addDs [apply_type]) 1);
-val ntree_induct2 = result();
+val ntree_induct = result();
(*Induction on ntree(A) to prove an equation*)
val major::prems = goal Ntree.thy
- "[| t: ntree(A); f: ntree(A)->B; g: ntree(A)->B; \
+ "[| t: ntree(A); f: ntree(A)->B; g: ntree(A)->B; \
\ !!x n h. [| x: A; n: nat; h: n -> ntree(A); f O h = g O h |] ==> \
-\ f ` Branch(x,h) = g ` Branch(x,h) \
+\ f ` Branch(x,h) = g ` Branch(x,h) \
\ |] ==> f`t=g`t";
-by (rtac (major RS ntree_induct2) 1);
+by (rtac (major RS ntree_induct) 1);
by (REPEAT_SOME (ares_tac prems));
by (cut_facts_tac prems 1);
br fun_extension 1;
@@ -61,9 +63,55 @@
by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1));
val ntree_univ = result();
-val ntree_subset_univ =
- [ntree_mono, ntree_univ] MRS subset_trans |> standard;
+val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard;
+
+
+(** maptree **)
+
+goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
+let open maptree; val rew = rewrite_rule con_defs in
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+ addEs [rew elim]) 1)
+end;
+val maptree_unfold = result();
-goal Ntree.thy "!!t A B. [| t: ntree(A); A <= univ(B) |] ==> t: univ(B)";
-by (REPEAT (ares_tac [ntree_subset_univ RS subsetD] 1));
-val ntree_into_univ = result();
+(*A nicer induction rule than the standard one*)
+val major::prems = goal Ntree.thy
+ "[| t: maptree(A); \
+\ !!x n h. [| x: A; h: maptree(A) -||> maptree(A); \
+\ ALL y: field(h). P(y) \
+\ |] ==> P(Sons(x,h)) \
+\ |] ==> P(t)";
+by (rtac (major RS maptree.induct) 1);
+by (REPEAT_SOME (ares_tac prems));
+by (eresolve_tac [Collect_subset RS FiniteFun_mono1 RS subsetD] 1);
+by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
+by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
+by (fast_tac ZF_cs 1);
+val maptree_induct = result();
+
+
+(** maptree2 **)
+
+goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
+let open maptree2; val rew = rewrite_rule con_defs in
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+ addEs [rew elim]) 1)
+end;
+val maptree2_unfold = result();
+
+(*A nicer induction rule than the standard one*)
+val major::prems = goal Ntree.thy
+ "[| t: maptree2(A,B); \
+\ !!x n h. [| x: A; h: B -||> maptree2(A,B); ALL y:range(h). P(y) \
+\ |] ==> P(Sons2(x,h)) \
+\ |] ==> P(t)";
+by (rtac (major RS maptree2.induct) 1);
+by (REPEAT_SOME (ares_tac prems));
+by (eresolve_tac [[subset_refl, Collect_subset] MRS
+ FiniteFun_mono RS subsetD] 1);
+by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
+by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
+by (fast_tac ZF_cs 1);
+val maptree2_induct = result();
+
--- a/src/ZF/ex/Ntree.thy Wed Aug 17 10:33:23 1994 +0200
+++ b/src/ZF/ex/Ntree.thy Wed Aug 17 10:34:44 1994 +0200
@@ -5,19 +5,30 @@
Datatype definition n-ary branching trees
Demonstrates a simple use of function space in a datatype definition
- and also "nested" monotonicity theorems
Based upon ex/Term.thy
*)
Ntree = InfDatatype +
consts
- ntree :: "i=>i"
+ ntree :: "i=>i"
+ maptree :: "i=>i"
+ maptree2 :: "[i,i] => i"
datatype
"ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
- monos "[[subset_refl, Pi_mono] MRS UN_mono]"
+ monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
type_intrs "[nat_fun_univ RS subsetD]"
type_elims "[UN_E]"
+datatype
+ "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
+ monos "[FiniteFun_mono1]" (*Use monotonicity in BOTH args*)
+ type_intrs "[FiniteFun_univ1 RS subsetD]"
+
+datatype
+ "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
+ monos "[subset_refl RS FiniteFun_mono]"
+ type_intrs "[FiniteFun_in_univ']"
+
end