# HG changeset patch
# User lcp
# Date 777112484 -7200
# Node ID 01906e4644e05c0517bf68eaf550e599b75024e3
# Parent  b4fe3da03449501b0b00750dccd63c909c0b1a6b
ZF/ex/Ntree: two new examples, maptree and maptree2

diff -r b4fe3da03449 -r 01906e4644e0 src/ZF/ex/Ntree.ML
--- 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();
+
diff -r b4fe3da03449 -r 01906e4644e0 src/ZF/ex/Ntree.thy
--- 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