ZF/ex/Ntree: two new examples, maptree and maptree2
authorlcp
Wed Aug 17 10:34:44 1994 +0200 (1994-08-17 ago)
changeset 53901906e4644e0
parent 538 b4fe3da03449
child 540 e30c23731c2d
ZF/ex/Ntree: two new examples, maptree and maptree2
src/ZF/ex/Ntree.ML
src/ZF/ex/Ntree.thy
     1.1 --- a/src/ZF/ex/Ntree.ML	Wed Aug 17 10:33:23 1994 +0200
     1.2 +++ b/src/ZF/ex/Ntree.ML	Wed Aug 17 10:34:44 1994 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4  
     1.5  open Ntree;
     1.6  
     1.7 +(** ntree **)
     1.8 +
     1.9  goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
    1.10  let open ntree;  val rew = rewrite_rule con_defs in  
    1.11  by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
    1.12 @@ -20,24 +22,24 @@
    1.13  
    1.14  (*A nicer induction rule than the standard one*)
    1.15  val major::prems = goal Ntree.thy
    1.16 -    "[| t: ntree(A);  \
    1.17 +    "[| t: ntree(A); 							\
    1.18  \       !!x n h. [| x: A;  n: nat;  h: n -> ntree(A);  ALL i:n. P(h`i)  \
    1.19 -\                |] ==> P(Branch(x,h))  \
    1.20 +\                |] ==> P(Branch(x,h))  				\
    1.21  \    |] ==> P(t)";
    1.22  by (rtac (major RS ntree.induct) 1);
    1.23  by (etac UN_E 1);
    1.24  by (REPEAT_SOME (ares_tac prems));
    1.25  by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
    1.26  by (fast_tac (ZF_cs addDs [apply_type]) 1);
    1.27 -val ntree_induct2 = result();
    1.28 +val ntree_induct = result();
    1.29  
    1.30  (*Induction on ntree(A) to prove an equation*)
    1.31  val major::prems = goal Ntree.thy
    1.32 -  "[| t: ntree(A);  f: ntree(A)->B;  g: ntree(A)->B;		\
    1.33 +  "[| t: ntree(A);  f: ntree(A)->B;  g: ntree(A)->B;			  \
    1.34  \     !!x n h. [| x: A;  n: nat;  h: n -> ntree(A);  f O h = g O h |] ==> \
    1.35 -\              f ` Branch(x,h) = g ` Branch(x,h)  		\
    1.36 +\              f ` Branch(x,h) = g ` Branch(x,h)  			  \
    1.37  \  |] ==> f`t=g`t";
    1.38 -by (rtac (major RS ntree_induct2) 1);
    1.39 +by (rtac (major RS ntree_induct) 1);
    1.40  by (REPEAT_SOME (ares_tac prems));
    1.41  by (cut_facts_tac prems 1);
    1.42  br fun_extension 1;
    1.43 @@ -61,9 +63,55 @@
    1.44  by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1));
    1.45  val ntree_univ = result();
    1.46  
    1.47 -val ntree_subset_univ = 
    1.48 -    [ntree_mono, ntree_univ] MRS subset_trans |> standard;
    1.49 +val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard;
    1.50 +
    1.51 +
    1.52 +(** maptree **)
    1.53 +
    1.54 +goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
    1.55 +let open maptree;  val rew = rewrite_rule con_defs in  
    1.56 +by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
    1.57 +                     addEs [rew elim]) 1)
    1.58 +end;
    1.59 +val maptree_unfold = result();
    1.60  
    1.61 -goal Ntree.thy "!!t A B. [| t: ntree(A);  A <= univ(B) |] ==> t: univ(B)";
    1.62 -by (REPEAT (ares_tac [ntree_subset_univ RS subsetD] 1));
    1.63 -val ntree_into_univ = result();
    1.64 +(*A nicer induction rule than the standard one*)
    1.65 +val major::prems = goal Ntree.thy
    1.66 +    "[| t: maptree(A); 							\
    1.67 +\       !!x n h. [| x: A;  h: maptree(A) -||> maptree(A);  		\
    1.68 +\                   ALL y: field(h). P(y)  				\
    1.69 +\                |] ==> P(Sons(x,h))  					\
    1.70 +\    |] ==> P(t)";
    1.71 +by (rtac (major RS maptree.induct) 1);
    1.72 +by (REPEAT_SOME (ares_tac prems));
    1.73 +by (eresolve_tac [Collect_subset RS FiniteFun_mono1 RS subsetD] 1);
    1.74 +by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
    1.75 +by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
    1.76 +by (fast_tac ZF_cs 1);
    1.77 +val maptree_induct = result();
    1.78 +
    1.79 +
    1.80 +(** maptree2 **)
    1.81 +
    1.82 +goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
    1.83 +let open maptree2;  val rew = rewrite_rule con_defs in  
    1.84 +by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
    1.85 +                     addEs [rew elim]) 1)
    1.86 +end;
    1.87 +val maptree2_unfold = result();
    1.88 +
    1.89 +(*A nicer induction rule than the standard one*)
    1.90 +val major::prems = goal Ntree.thy
    1.91 +    "[| t: maptree2(A,B); 						  \
    1.92 +\       !!x n h. [| x: A;  h: B -||> maptree2(A,B);  ALL y:range(h). P(y) \
    1.93 +\                |] ==> P(Sons2(x,h))  					  \
    1.94 +\    |] ==> P(t)";
    1.95 +by (rtac (major RS maptree2.induct) 1);
    1.96 +by (REPEAT_SOME (ares_tac prems));
    1.97 +by (eresolve_tac [[subset_refl, Collect_subset] MRS
    1.98 +		  FiniteFun_mono RS subsetD] 1);
    1.99 +by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
   1.100 +by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
   1.101 +by (fast_tac ZF_cs 1);
   1.102 +val maptree2_induct = result();
   1.103 +
     2.1 --- a/src/ZF/ex/Ntree.thy	Wed Aug 17 10:33:23 1994 +0200
     2.2 +++ b/src/ZF/ex/Ntree.thy	Wed Aug 17 10:34:44 1994 +0200
     2.3 @@ -5,19 +5,30 @@
     2.4  
     2.5  Datatype definition n-ary branching trees
     2.6  Demonstrates a simple use of function space in a datatype definition
     2.7 -   and also "nested" monotonicity theorems
     2.8  
     2.9  Based upon ex/Term.thy
    2.10  *)
    2.11  
    2.12  Ntree = InfDatatype +
    2.13  consts
    2.14 -  ntree :: "i=>i"
    2.15 +  ntree    :: "i=>i"
    2.16 +  maptree  :: "i=>i"
    2.17 +  maptree2 :: "[i,i] => i"
    2.18  
    2.19  datatype
    2.20    "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
    2.21 -  monos	      "[[subset_refl, Pi_mono] MRS UN_mono]"
    2.22 +  monos	      "[[subset_refl, Pi_mono] MRS UN_mono]"	(*MUST have this form*)
    2.23    type_intrs  "[nat_fun_univ RS subsetD]"
    2.24    type_elims  "[UN_E]"
    2.25  
    2.26 +datatype
    2.27 +  "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
    2.28 +  monos	      "[FiniteFun_mono1]"	(*Use monotonicity in BOTH args*)
    2.29 +  type_intrs  "[FiniteFun_univ1 RS subsetD]"
    2.30 +
    2.31 +datatype
    2.32 +  "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
    2.33 +  monos	      "[subset_refl RS FiniteFun_mono]"
    2.34 +  type_intrs  "[FiniteFun_in_univ']"
    2.35 +
    2.36  end