datatype package improvements
authorpaulson
Wed Jan 13 11:57:09 1999 +0100 (1999-01-13)
changeset 61125e4871c5136b
parent 6111 5347c9a22897
child 6113 b321f5aaa5f4
datatype package improvements
src/ZF/AC/AC16_WO4.ML
src/ZF/AC/WO1_AC.ML
src/ZF/Cardinal.ML
src/ZF/Coind/Language.thy
src/ZF/Coind/Types.thy
src/ZF/Coind/Values.thy
src/ZF/Datatype.ML
src/ZF/IMP/Com.thy
src/ZF/Integ/Bin.ML
src/ZF/List.ML
src/ZF/OrdQuant.ML
src/ZF/QPair.ML
src/ZF/QUniv.thy
src/ZF/ROOT.ML
src/ZF/Resid/Redex.thy
src/ZF/Resid/Substitution.ML
src/ZF/Resid/Terms.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/typechk.ML
src/ZF/WF.ML
src/ZF/ex/BT.ML
src/ZF/ex/BT.thy
src/ZF/ex/Ntree.ML
src/ZF/ex/Primrec.ML
src/ZF/ex/Ramsey.ML
src/ZF/ex/TF.thy
src/ZF/ex/Term.ML
src/ZF/ex/Term.thy
src/ZF/ind_syntax.ML
src/ZF/pair.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/ZF/AC/AC16_WO4.ML	Wed Jan 13 11:56:28 1999 +0100
     1.2 +++ b/src/ZF/AC/AC16_WO4.ML	Wed Jan 13 11:57:09 1999 +0100
     1.3 @@ -328,11 +328,10 @@
     1.4  by (res_inst_tac 
     1.5       [("f3", "lam b:y-a. THE c. c: s(u) & a <= c & b:c")]
     1.6       (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
     1.7 -by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
     1.8 -by (rtac CollectI 1);
     1.9 +by (simp_tac (simpset() addsimps [inj_def]) 1);
    1.10 +by (rtac conjI 1);
    1.11  by (rtac lam_type 1);
    1.12 -by (forward_tac [ex1_superset_a RS theI] 1
    1.13 -        THEN REPEAT (Fast_tac 1));
    1.14 +by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (Fast_tac 1));
    1.15  by (Asm_simp_tac 1);
    1.16  by (Clarify_tac 1);
    1.17  by (rtac cons_eqE 1);
    1.18 @@ -387,17 +386,16 @@
    1.19  \     ==> {v:s(u). a <= v} lepoll {v:Pow(x). v eqpoll m}";
    1.20  by (res_inst_tac [("f3","lam w:{v:s(u). a <= v}. w Int (x - {u})")] 
    1.21          (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
    1.22 -by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
    1.23 -by (rtac CollectI 1);
    1.24 +by (simp_tac (simpset() addsimps [inj_def]) 1);
    1.25 +by (rtac conjI 1);
    1.26  by (rtac lam_type 1);
    1.27  by (rtac CollectI 1);
    1.28  by (Fast_tac 1);
    1.29  by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1));
    1.30 -by (simp_tac (simpset() delsimps ball_simps) 1);
    1.31  by (REPEAT (resolve_tac [ballI, impI] 1));
    1.32 -(** LEVEL 9 **)
    1.33 -by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1
    1.34 -        THEN REPEAT (assume_tac 1));
    1.35 +(** LEVEL 8 **)
    1.36 +by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1);
    1.37 +by (EVERY (map Blast_tac [4,3,2,1]));
    1.38  by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
    1.39  by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1));
    1.40  by (etac ex1_two_eq 1);
     2.1 --- a/src/ZF/AC/WO1_AC.ML	Wed Jan 13 11:56:28 1999 +0100
     2.2 +++ b/src/ZF/AC/WO1_AC.ML	Wed Jan 13 11:57:09 1999 +0100
     2.3 @@ -56,9 +56,9 @@
     2.4  by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 2);
     2.5  by (resolve_tac [eqpoll_sym RS eqpoll_trans] 1);
     2.6  by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 1);
     2.7 -by (resolve_tac [cadd_def RS def_imp_eq RS subst] 1);
     2.8 +by (fold_tac [cadd_def]);
     2.9  by (resolve_tac [Card_cardinal RSN (2, Inf_Card_is_InfCard) RS 
    2.10 -                        InfCard_cdouble_eq RS ssubst] 1);
    2.11 +		 InfCard_cdouble_eq RS ssubst] 1);
    2.12  by (rtac eqpoll_refl 2);
    2.13  by (rtac notI 1);
    2.14  by (etac notE 1);
     3.1 --- a/src/ZF/Cardinal.ML	Wed Jan 13 11:56:28 1999 +0100
     3.2 +++ b/src/ZF/Cardinal.ML	Wed Jan 13 11:57:09 1999 +0100
     3.3 @@ -8,8 +8,6 @@
     3.4  This theory does NOT assume the Axiom of Choice
     3.5  *)
     3.6  
     3.7 -open Cardinal;
     3.8 -
     3.9  (*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
    3.10  
    3.11  (** Lemma: Banach's Decomposition Theorem **)
    3.12 @@ -457,11 +455,9 @@
    3.13  by (rtac ballI 1);
    3.14  by (eres_inst_tac [("n","n")] natE 1);
    3.15  by (asm_simp_tac (simpset() addsimps [lepoll_def, inj_def, 
    3.16 -                                  succI1 RS Pi_empty2]) 1);
    3.17 +				      succI1 RS Pi_empty2]) 1);
    3.18  by (blast_tac (claset() addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
    3.19 -qed "nat_lepoll_imp_le_lemma";
    3.20 -
    3.21 -bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
    3.22 +qed_spec_mp "nat_lepoll_imp_le";
    3.23  
    3.24  Goal "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
    3.25  by (rtac iffI 1);
     4.1 --- a/src/ZF/Coind/Language.thy	Wed Jan 13 11:56:28 1999 +0100
     4.2 +++ b/src/ZF/Coind/Language.thy	Wed Jan 13 11:57:09 1999 +0100
     4.3 @@ -18,11 +18,12 @@
     4.4  consts
     4.5    Exp   :: i                    (* Datatype of expressions *)
     4.6    ExVar :: i                    (* Abstract type of variables *)
     4.7 -datatype <= "univ(Const Un ExVar)"
     4.8 -  "Exp" = e_const("c:Const")
     4.9 -        | e_var("x:ExVar")
    4.10 -        | e_fn("x:ExVar","e:Exp")
    4.11 -        | e_fix("x1:ExVar","x2:ExVar","e:Exp")
    4.12 -        | e_app("e1:Exp","e2:Exp")
    4.13 +
    4.14 +datatype
    4.15 +  "Exp" = e_const ("c:Const")
    4.16 +        | e_var ("x:ExVar")
    4.17 +        | e_fn ("x:ExVar","e:Exp")
    4.18 +        | e_fix ("x1:ExVar","x2:ExVar","e:Exp")
    4.19 +        | e_app ("e1:Exp","e2:Exp")
    4.20  
    4.21  end
     5.1 --- a/src/ZF/Coind/Types.thy	Wed Jan 13 11:56:28 1999 +0100
     5.2 +++ b/src/ZF/Coind/Types.thy	Wed Jan 13 11:57:09 1999 +0100
     5.3 @@ -9,18 +9,20 @@
     5.4  consts
     5.5    Ty :: i                       (* Datatype of types *)
     5.6    TyConst :: i          (* Abstract type of type constants *)
     5.7 -datatype <= "univ(TyConst)"
     5.8 -  "Ty" = t_const("tc:TyConst")
     5.9 -       | t_fun("t1:Ty","t2:Ty")
    5.10 +
    5.11 +datatype
    5.12 +  "Ty" = t_const ("tc:TyConst")
    5.13 +       | t_fun ("t1:Ty","t2:Ty")
    5.14    
    5.15  
    5.16  (* Definition of type environments and associated operators *)
    5.17  
    5.18  consts
    5.19    TyEnv :: i
    5.20 -datatype <= "univ(Ty Un ExVar)"
    5.21 +
    5.22 +datatype
    5.23    "TyEnv" = te_emp
    5.24 -          | te_owr("te:TyEnv","x:ExVar","t:Ty") 
    5.25 +          | te_owr ("te:TyEnv","x:ExVar","t:Ty") 
    5.26  
    5.27  consts
    5.28    te_dom :: i => i
     6.1 --- a/src/ZF/Coind/Values.thy	Wed Jan 13 11:56:28 1999 +0100
     6.2 +++ b/src/ZF/Coind/Values.thy	Wed Jan 13 11:57:09 1999 +0100
     6.3 @@ -10,11 +10,12 @@
     6.4  
     6.5  consts
     6.6    Val, ValEnv, Val_ValEnv  :: i
     6.7 -codatatype <= "quniv(Const Un ExVar Un Exp)"
     6.8 -    "Val" = v_const("c:Const")
     6.9 -          | v_clos("x:ExVar","e:Exp","ve:ValEnv")
    6.10 +
    6.11 +codatatype
    6.12 +    "Val" = v_const ("c:Const")
    6.13 +          | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
    6.14    and
    6.15 -    "ValEnv" = ve_mk("m:PMap(ExVar,Val)")
    6.16 +    "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
    6.17    monos      "[map_mono]"
    6.18    type_intrs "[A_into_univ, mapQU]"
    6.19  
     7.1 --- a/src/ZF/Datatype.ML	Wed Jan 13 11:56:28 1999 +0100
     7.2 +++ b/src/ZF/Datatype.ML	Wed Jan 13 11:57:09 1999 +0100
     7.3 @@ -15,8 +15,9 @@
     7.4         Pair_in_univ, Inl_in_univ, Inr_in_univ, 
     7.5         zero_in_univ, A_into_univ, nat_into_univ, UnCI];
     7.6  
     7.7 -  (*Needed for mutual recursion*)
     7.8 -  val elims = [make_elim InlD, make_elim InrD];
     7.9 +
    7.10 +  val elims = [make_elim InlD, make_elim InrD,   (*for mutual recursion*)
    7.11 +	       SigmaE, sumE];			 (*allows * and + in spec*)
    7.12    end;
    7.13  
    7.14  
    7.15 @@ -36,7 +37,8 @@
    7.16         QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    7.17         zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
    7.18  
    7.19 -  val elims = [make_elim QInlD, make_elim QInrD];
    7.20 +  val elims = [make_elim QInlD, make_elim QInrD,   (*for mutual recursion*)
    7.21 +	       QSigmaE, qsumE];			   (*allows * and + in spec*)
    7.22    end;
    7.23  
    7.24  structure CoData_Package = 
     8.1 --- a/src/ZF/IMP/Com.thy	Wed Jan 13 11:56:28 1999 +0100
     8.2 +++ b/src/ZF/IMP/Com.thy	Wed Jan 13 11:57:09 1999 +0100
     8.3 @@ -78,7 +78,7 @@
     8.4  (** Commands **)
     8.5  consts  com :: i
     8.6  
     8.7 -datatype <= "univ(loc Un aexp Un bexp)"
     8.8 +datatype 
     8.9    "com" = skip
    8.10          | asgt  ("x:loc", "a:aexp")             (infixl 60)
    8.11          | semic ("c0:com", "c1:com")            ("_; _"  [60, 60] 10)
     9.1 --- a/src/ZF/Integ/Bin.ML	Wed Jan 13 11:56:28 1999 +0100
     9.2 +++ b/src/ZF/Integ/Bin.ML	Wed Jan 13 11:57:09 1999 +0100
     9.3 @@ -77,7 +77,7 @@
     9.4  by (rename_tac "w'" 3);
     9.5  by (induct_tac "w'" 3);
     9.6  by Auto_tac;
     9.7 -bind_thm ("bin_add_type", result() RS bspec);
     9.8 +qed_spec_mp "bin_add_type";
     9.9  Addsimps [bin_add_type];
    9.10  
    9.11  Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
    9.12 @@ -169,8 +169,7 @@
    9.13  by (rtac ballI 1);
    9.14  by (induct_tac "wa" 1);
    9.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
    9.16 -bind_thm("integ_of_add", result() RS bspec);
    9.17 -
    9.18 +qed_spec_mp "integ_of_add";
    9.19  Addsimps [integ_of_add];
    9.20  
    9.21  
    10.1 --- a/src/ZF/List.ML	Wed Jan 13 11:56:28 1999 +0100
    10.2 +++ b/src/ZF/List.ML	Wed Jan 13 11:57:09 1999 +0100
    10.3 @@ -34,11 +34,11 @@
    10.4  by (rtac lfp_lowerbound 1);
    10.5  by (rtac (A_subset_univ RS univ_mono) 2);
    10.6  by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
    10.7 -                            Pair_in_univ]) 1);
    10.8 +				Pair_in_univ]) 1);
    10.9  qed "list_univ";
   10.10  
   10.11  (*These two theorems justify datatypes involving list(nat), list(A), ...*)
   10.12 -bind_thm ("list_subset_univ", ([list_mono, list_univ] MRS subset_trans));
   10.13 +bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans);
   10.14  
   10.15  Goal "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)";
   10.16  by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
   10.17 @@ -177,6 +177,7 @@
   10.18  by (induct_tac "l" 1);
   10.19  by (ALLGOALS Asm_simp_tac);
   10.20  qed "map_ident";
   10.21 +Addsimps [map_ident];
   10.22  
   10.23  Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
   10.24  by (induct_tac "l" 1);
   10.25 @@ -203,7 +204,7 @@
   10.26  (** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
   10.27  
   10.28  (* c : list(Collect(B,P)) ==> c : list(B) *)
   10.29 -bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
   10.30 +bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD);
   10.31  
   10.32  Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
   10.33  by (induct_tac "l" 1);
   10.34 @@ -222,13 +223,9 @@
   10.35  by (ALLGOALS Asm_simp_tac);
   10.36  qed "length_app";
   10.37  
   10.38 -(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
   10.39 -   Used for rewriting below*)
   10.40 -val add_commute_succ = nat_succI RSN (2,add_commute);
   10.41 -
   10.42  Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
   10.43  by (induct_tac "xs" 1);
   10.44 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ])));
   10.45 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
   10.46  qed "length_rev";
   10.47  
   10.48  Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
   10.49 @@ -244,22 +241,19 @@
   10.50  by (etac list.induct 1);
   10.51  by (ALLGOALS Asm_simp_tac);
   10.52  by (Blast_tac 1);
   10.53 -qed "drop_length_Cons_lemma";
   10.54 -bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec));
   10.55 +qed_spec_mp "drop_length_Cons";
   10.56  
   10.57 -Goal "l: list(A) ==> ALL i: length(l).  EX z zs. drop(i,l) = Cons(z,zs)";
   10.58 +Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
   10.59  by (etac list.induct 1);
   10.60  by (ALLGOALS Asm_simp_tac);
   10.61 -by (rtac conjI 1);
   10.62 +by Safe_tac;
   10.63  by (etac drop_length_Cons 1);
   10.64 -by (rtac ballI 1);
   10.65  by (rtac natE 1);
   10.66  by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
   10.67  by (assume_tac 1);
   10.68  by (ALLGOALS Asm_simp_tac);
   10.69  by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type])));
   10.70 -qed "drop_length_lemma";
   10.71 -bind_thm ("drop_length", (drop_length_lemma RS bspec));
   10.72 +qed_spec_mp "drop_length";
   10.73  
   10.74  
   10.75  (*** theorems about app ***)
   10.76 @@ -268,6 +262,7 @@
   10.77  by (etac list.induct 1);
   10.78  by (ALLGOALS Asm_simp_tac);
   10.79  qed "app_right_Nil";
   10.80 +Addsimps [app_right_Nil];
   10.81  
   10.82  Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
   10.83  by (induct_tac "xs" 1);
   10.84 @@ -292,18 +287,20 @@
   10.85  *)
   10.86  Goal "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
   10.87  by (etac list.induct 1);
   10.88 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc])));
   10.89 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
   10.90  qed "rev_app_distrib";
   10.91  
   10.92  Goal "l: list(A) ==> rev(rev(l))=l";
   10.93  by (induct_tac "l" 1);
   10.94  by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
   10.95  qed "rev_rev_ident";
   10.96 +Addsimps [rev_rev_ident];
   10.97  
   10.98  Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
   10.99  by (induct_tac "ls" 1);
  10.100 -by (ALLGOALS (asm_simp_tac (simpset() addsimps 
  10.101 -       [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
  10.102 +by (ALLGOALS
  10.103 +    (asm_simp_tac (simpset() addsimps 
  10.104 +		   [map_app_distrib, flat_app_distrib, rev_app_distrib])));
  10.105  qed "rev_flat";
  10.106  
  10.107  
    11.1 --- a/src/ZF/OrdQuant.ML	Wed Jan 13 11:56:28 1999 +0100
    11.2 +++ b/src/ZF/OrdQuant.ML	Wed Jan 13 11:57:09 1999 +0100
    11.3 @@ -5,8 +5,6 @@
    11.4  Quantifiers and union operator for ordinals. 
    11.5  *)
    11.6  
    11.7 -open OrdQuant;
    11.8 -
    11.9  (*** universal quantifier for ordinals ***)
   11.10  
   11.11  qed_goalw "oallI" thy [oall_def]
    12.1 --- a/src/ZF/QPair.ML	Wed Jan 13 11:56:28 1999 +0100
    12.2 +++ b/src/ZF/QPair.ML	Wed Jan 13 11:57:09 1999 +0100
    12.3 @@ -122,11 +122,9 @@
    12.4  (*** Eliminator - qsplit ***)
    12.5  
    12.6  (*A META-equality, so that it applies to higher types as well...*)
    12.7 -qed_goalw "qsplit" thy [qsplit_def]
    12.8 -    "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
    12.9 - (fn _ => [ (Simp_tac 1),
   12.10 -            (rtac reflexive_thm 1) ]);
   12.11 -
   12.12 +Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)";
   12.13 +by (Simp_tac 1);
   12.14 +qed "qsplit";
   12.15  Addsimps [qsplit];
   12.16  
   12.17  qed_goal "qsplit_type" thy
    13.1 --- a/src/ZF/QUniv.thy	Wed Jan 13 11:56:28 1999 +0100
    13.2 +++ b/src/ZF/QUniv.thy	Wed Jan 13 11:57:09 1999 +0100
    13.3 @@ -8,8 +8,20 @@
    13.4  
    13.5  QUniv = Univ + QPair + mono + equalities +
    13.6  
    13.7 +(*Disjoint sums as a datatype*)
    13.8 +rep_datatype 
    13.9 +  elim		sumE
   13.10 +  induct	TrueI
   13.11 +  case_eqns	case_Inl, case_Inr
   13.12 +
   13.13 +(*Variant disjoint sums as a datatype*)
   13.14 +rep_datatype 
   13.15 +  elim		qsumE
   13.16 +  induct	TrueI
   13.17 +  case_eqns	qcase_QInl, qcase_QInr
   13.18 +
   13.19  constdefs
   13.20    quniv :: i => i
   13.21 -  "quniv(A) == Pow(univ(eclose(A)))"
   13.22 +   "quniv(A) == Pow(univ(eclose(A)))"
   13.23  
   13.24  end
    14.1 --- a/src/ZF/ROOT.ML	Wed Jan 13 11:56:28 1999 +0100
    14.2 +++ b/src/ZF/ROOT.ML	Wed Jan 13 11:57:09 1999 +0100
    14.3 @@ -28,10 +28,10 @@
    14.4  use_thy "Fixedpt";
    14.5  use     "Tools/inductive_package";
    14.6  use_thy "Inductive";
    14.7 -use "Tools/induct_tacs";
    14.8 -use "Tools/primrec_package";
    14.9 +use     "Tools/induct_tacs";
   14.10 +use     "Tools/primrec_package";
   14.11  use_thy "QUniv";
   14.12 -use "Tools/datatype_package";
   14.13 +use     "Tools/datatype_package";
   14.14  use_thy "Datatype";
   14.15  use_thy "InfDatatype";
   14.16  use_thy "List";
    15.1 --- a/src/ZF/Resid/Redex.thy	Wed Jan 13 11:56:28 1999 +0100
    15.2 +++ b/src/ZF/Resid/Redex.thy	Wed Jan 13 11:57:09 1999 +0100
    15.3 @@ -13,8 +13,6 @@
    15.4    "redexes" = Var ("n: nat")            
    15.5              | Fun ("t: redexes")
    15.6              | App ("b:bool" ,"f:redexes" , "a:redexes")
    15.7 -  type_intrs "[bool_into_univ]"
    15.8 -  
    15.9  
   15.10  
   15.11  consts
    16.1 --- a/src/ZF/Resid/Substitution.ML	Wed Jan 13 11:56:28 1999 +0100
    16.2 +++ b/src/ZF/Resid/Substitution.ML	Wed Jan 13 11:57:09 1999 +0100
    16.3 @@ -107,13 +107,13 @@
    16.4  by (ALLGOALS
    16.5      (asm_simp_tac (simpset() addsimps [lift_rec_Var,
    16.6  				       lift_rec_Fun, lift_rec_App])));
    16.7 -bind_thm ("lift_rec_type", result() RS bspec);
    16.8 +qed_spec_mp "lift_rec_type";
    16.9  
   16.10  Goal "v:redexes ==>  ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
   16.11  by (etac redexes.induct 1);
   16.12  by (ALLGOALS(asm_simp_tac 
   16.13      (simpset() addsimps [subst_Var, lift_rec_type])));
   16.14 -bind_thm ("subst_type", result() RS bspec RS bspec);
   16.15 +qed_spec_mp "subst_type";
   16.16  
   16.17  
   16.18  Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
    17.1 --- a/src/ZF/Resid/Terms.ML	Wed Jan 13 11:56:28 1999 +0100
    17.2 +++ b/src/ZF/Resid/Terms.ML	Wed Jan 13 11:57:09 1999 +0100
    17.3 @@ -30,13 +30,12 @@
    17.4  Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
    17.5  by (etac lambda.induct 1);
    17.6  by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
    17.7 -bind_thm ("liftL_type", result() RS bspec);
    17.8 +qed_spec_mp "liftL_type";
    17.9  
   17.10  Goal "v:lambda ==>  ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
   17.11  by (etac lambda.induct 1);
   17.12  by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
   17.13 -qed "substL_typea";
   17.14 -bind_thm ("substL_type", result() RS bspec RS bspec);
   17.15 +qed_spec_mp "substL_type";
   17.16  
   17.17  
   17.18  (* ------------------------------------------------------------------------- *)
    18.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Jan 13 11:56:28 1999 +0100
    18.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Jan 13 11:57:09 1999 +0100
    18.3 @@ -19,7 +19,7 @@
    18.4      recursor_eqns : thm list,          (*equations for the recursor*)
    18.5      free_iffs  : thm list,             (*freeness rewrite rules*)
    18.6      free_SEs   : thm list,             (*freeness destruct rules*)
    18.7 -    mk_free    : string -> thm};      (*makes freeness theorems*)
    18.8 +    mk_free    : string -> thm};       (*function to make freeness theorems*)
    18.9  
   18.10  
   18.11  signature DATATYPE_ARG =
   18.12 @@ -302,7 +302,7 @@
   18.13  	   (cterm_of (sign_of thy1) (mk_case_eqn arg)))
   18.14  	(case_tacsf con_def);
   18.15  
   18.16 -  val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
   18.17 +  val free_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
   18.18  
   18.19    val case_eqns = 
   18.20        map prove_case_eqn 
   18.21 @@ -353,10 +353,7 @@
   18.22    val constructors =
   18.23        map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
   18.24  
   18.25 -  val free_iffs = con_iffs @ 
   18.26 -    [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
   18.27 -
   18.28 -  val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
   18.29 +  val free_SEs = Ind_Syntax.mk_free_SEs free_iffs;
   18.30  
   18.31    val {elim, induct, mutual_induct, ...} = ind_result
   18.32  
   18.33 @@ -366,7 +363,7 @@
   18.34        prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
   18.35                    con_defs s
   18.36  	(fn prems => [cut_facts_tac prems 1, 
   18.37 -		      fast_tac (ZF_cs addSEs free_SEs) 1]);
   18.38 +		      fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
   18.39  
   18.40    val simps = case_eqns @ recursor_eqns;
   18.41  
   18.42 @@ -413,11 +410,12 @@
   18.43  		  monos, type_intrs, type_elims) thy =
   18.44    let val sign = sign_of thy
   18.45        val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
   18.46 +      val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
   18.47        val dom_sum = 
   18.48            if sdom = "" then
   18.49 -	      Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "Fixedpt.lfp") rec_tms
   18.50 +	      Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") 
   18.51 +	                             (rec_tms, con_ty_lists)
   18.52            else readtm sign Ind_Syntax.iT sdom
   18.53 -      and con_ty_lists	= Ind_Syntax.read_constructs sign scon_ty_lists
   18.54    in 
   18.55        add_datatype_i (dom_sum, rec_tms, con_ty_lists, 
   18.56  		      monos, type_intrs, type_elims) thy
    19.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Jan 13 11:56:28 1999 +0100
    19.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Jan 13 11:57:09 1999 +0100
    19.3 @@ -111,7 +111,9 @@
    19.4  	if exh then #exhaustion (datatype_info_sg sign tn)
    19.5  	       else #induct  (datatype_info_sg sign tn)
    19.6      val (Const("op :",_) $ Var(ixn,_) $ _) = 
    19.7 -	FOLogic.dest_Trueprop (hd (prems_of rule))
    19.8 +        (case prems_of rule of
    19.9 +	     [] => error "induction is not available for this datatype"
   19.10 +	   | major::_ => FOLogic.dest_Trueprop major)
   19.11      val ind_vname = Syntax.string_of_vname ixn
   19.12      val vname' = (*delete leading question mark*)
   19.13  	String.substring (ind_vname, 1, size ind_vname-1)
   19.14 @@ -139,9 +141,11 @@
   19.15  	map (head_of o const_of o FOLogic.dest_Trueprop o
   19.16  	     #prop o rep_thm) case_eqns;
   19.17  
   19.18 -    val Const ("op :", _) $ _ $ Const(big_rec_name, _) =
   19.19 +    val Const ("op :", _) $ _ $ data =
   19.20  	FOLogic.dest_Trueprop (hd (prems_of elim));	
   19.21      
   19.22 +    val Const(big_rec_name, _) = head_of data;
   19.23 +
   19.24      val simps = case_eqns @ recursor_eqns;
   19.25  
   19.26      val dt_info =
    20.1 --- a/src/ZF/Tools/typechk.ML	Wed Jan 13 11:56:28 1999 +0100
    20.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jan 13 11:57:09 1999 +0100
    20.3 @@ -29,5 +29,6 @@
    20.4    drawback: does not simplify conjunctions*)
    20.5  fun type_auto_tac tyrls hyps = SELECT_GOAL
    20.6      (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    20.7 -           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
    20.8 +           ORELSE ares_tac [TrueI,refl,reflexive_thm,iff_refl,
    20.9 +			    ballI,allI,conjI,impI] 1));
   20.10  
    21.1 --- a/src/ZF/WF.ML	Wed Jan 13 11:56:28 1999 +0100
    21.2 +++ b/src/ZF/WF.ML	Wed Jan 13 11:57:09 1999 +0100
    21.3 @@ -203,8 +203,8 @@
    21.4  
    21.5  (** r-``{a} is the set of everything under a in r **)
    21.6  
    21.7 -bind_thm ("underI", (vimage_singleton_iff RS iffD2));
    21.8 -bind_thm ("underD", (vimage_singleton_iff RS iffD1));
    21.9 +bind_thm ("underI", vimage_singleton_iff RS iffD2);
   21.10 +bind_thm ("underD", vimage_singleton_iff RS iffD1);
   21.11  
   21.12  (** is_recfun **)
   21.13  
   21.14 @@ -223,7 +223,7 @@
   21.15  (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   21.16    spec RS mp  instantiates induction hypotheses*)
   21.17  fun indhyp_tac hyps =
   21.18 -    resolve_tac (TrueI::refl::hyps) ORELSE' 
   21.19 +    resolve_tac (TrueI::refl::reflexive_thm::hyps) ORELSE' 
   21.20      (cut_facts_tac hyps THEN'
   21.21         DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
   21.22                          eresolve_tac [underD, transD, spec RS mp]));
   21.23 @@ -238,8 +238,7 @@
   21.24  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   21.25  by (rewtac restrict_def);
   21.26  by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
   21.27 -qed "is_recfun_equal_lemma";
   21.28 -bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
   21.29 +qed_spec_mp "is_recfun_equal";
   21.30  
   21.31  val prems as [wfr,transr,recf,recg,_] = goal WF.thy
   21.32      "[| wf(r);  trans(r);       \
    22.1 --- a/src/ZF/ex/BT.ML	Wed Jan 13 11:56:28 1999 +0100
    22.2 +++ b/src/ZF/ex/BT.ML	Wed Jan 13 11:57:09 1999 +0100
    22.3 @@ -8,6 +8,17 @@
    22.4  
    22.5  Addsimps bt.intrs;
    22.6  
    22.7 +Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
    22.8 +by (induct_tac "l" 1);
    22.9 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs)));
   22.10 +qed_spec_mp "Br_neq_left";
   22.11 +
   22.12 +(*Proving a freeness theorem*)
   22.13 +val Br_iff = bt.mk_free "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'";
   22.14 +
   22.15 +(*An elimination rule, for type-checking*)
   22.16 +val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
   22.17 +
   22.18  (**  Lemmas to justify using "bt" in other recursive type definitions **)
   22.19  
   22.20  Goalw bt.defs "A<=B ==> bt(A) <= bt(B)";
   22.21 @@ -26,7 +37,7 @@
   22.22  bind_thm ("bt_subset_univ", [bt_mono, bt_univ] MRS subset_trans);
   22.23  
   22.24  
   22.25 -(*Type checking -- proved by induction, as usual*)
   22.26 +(*Type checking for recursor -- example only; not really needed*)
   22.27  val major::prems = goal BT.thy
   22.28      "[| t: bt(A);    \
   22.29  \       c: C(Lf);       \
   22.30 @@ -58,14 +69,13 @@
   22.31  Goal "t: bt(A) ==> bt_reflect(t) : bt(A)";
   22.32  by (induct_tac "t" 1);
   22.33  by Auto_tac;
   22.34 -by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
   22.35  qed "bt_reflect_type";
   22.36  
   22.37  
   22.38  (** BT simplification **)
   22.39  
   22.40  
   22.41 -Addsimps [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
   22.42 +Addsimps [n_nodes_type, n_leaves_type, bt_reflect_type];
   22.43  
   22.44  
   22.45  (*** theorems about n_leaves ***)
    23.1 --- a/src/ZF/ex/BT.thy	Wed Jan 13 11:56:28 1999 +0100
    23.2 +++ b/src/ZF/ex/BT.thy	Wed Jan 13 11:57:09 1999 +0100
    23.3 @@ -6,18 +6,18 @@
    23.4  Binary trees
    23.5  *)
    23.6  
    23.7 -BT = Datatype +
    23.8 +BT = Main +
    23.9 +consts
   23.10 +    bt          :: i=>i
   23.11 +
   23.12 +datatype
   23.13 +  "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
   23.14 +
   23.15  consts
   23.16      n_nodes     :: i=>i
   23.17      n_leaves    :: i=>i
   23.18      bt_reflect  :: i=>i
   23.19  
   23.20 -    bt          :: i=>i
   23.21 -
   23.22 -datatype
   23.23 -  "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
   23.24 -  
   23.25 -
   23.26  primrec
   23.27    "n_nodes(Lf) = 0"
   23.28    "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
    24.1 --- a/src/ZF/ex/Ntree.ML	Wed Jan 13 11:56:28 1999 +0100
    24.2 +++ b/src/ZF/ex/Ntree.ML	Wed Jan 13 11:57:09 1999 +0100
    24.3 @@ -9,8 +9,6 @@
    24.4  Based upon ex/Term.ML
    24.5  *)
    24.6  
    24.7 -open Ntree;
    24.8 -
    24.9  (** ntree **)
   24.10  
   24.11  Goal "ntree(A) = A * (UN n: nat. n -> ntree(A))";
    25.1 --- a/src/ZF/ex/Primrec.ML	Wed Jan 13 11:56:28 1999 +0100
    25.2 +++ b/src/ZF/ex/Primrec.ML	Wed Jan 13 11:57:09 1999 +0100
    25.3 @@ -70,8 +70,7 @@
    25.4  by (etac (succ_leI RS lt_trans1) 2);
    25.5  by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
    25.6  by Auto_tac;
    25.7 -qed "lt_ack2_lemma";
    25.8 -bind_thm ("lt_ack2", (lt_ack2_lemma RS bspec));
    25.9 +qed_spec_mp "lt_ack2";
   25.10  
   25.11  (*PROPERTY A 5-, the single-step lemma*)
   25.12  Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
    26.1 --- a/src/ZF/ex/Ramsey.ML	Wed Jan 13 11:56:28 1999 +0100
    26.2 +++ b/src/ZF/ex/Ramsey.ML	Wed Jan 13 11:57:09 1999 +0100
    26.3 @@ -103,11 +103,7 @@
    26.4  (*proving the condition*)
    26.5  by (Asm_simp_tac 1);
    26.6  by (etac Atleast_superset 1 THEN Fast_tac 1);
    26.7 -qed "pigeon2_lemma";
    26.8 -
    26.9 -(* [| m:nat;  n:nat;  Atleast(m #+ n #- succ(0), A Un B) |] ==> 
   26.10 -   Atleast(m,A) | Atleast(n,B) *)
   26.11 -bind_thm ("pigeon2", (pigeon2_lemma RS bspec RS spec RS spec RS mp));
   26.12 +qed_spec_mp "pigeon2";
   26.13  
   26.14  
   26.15  (**** Ramsey's Theorem ****)
    27.1 --- a/src/ZF/ex/TF.thy	Wed Jan 13 11:56:28 1999 +0100
    27.2 +++ b/src/ZF/ex/TF.thy	Wed Jan 13 11:57:09 1999 +0100
    27.3 @@ -8,6 +8,15 @@
    27.4  
    27.5  TF = List +
    27.6  consts
    27.7 +  tree, forest, tree_forest    :: i=>i
    27.8 +
    27.9 +datatype
   27.10 +  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
   27.11 +and
   27.12 +  "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
   27.13 +
   27.14 +
   27.15 +consts
   27.16    map      :: [i=>i, i] => i
   27.17    size     :: i=>i
   27.18    preorder :: i=>i
   27.19 @@ -15,13 +24,6 @@
   27.20    of_list  :: i=>i
   27.21    reflect  :: i=>i
   27.22  
   27.23 -  tree, forest, tree_forest    :: i=>i
   27.24 -
   27.25 -datatype
   27.26 -  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
   27.27 -and
   27.28 -  "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
   27.29 -
   27.30  primrec
   27.31    "list_of_TF (Tcons(x,f))  = [Tcons(x,f)]"
   27.32    "list_of_TF (Fnil)        = []"
    28.1 --- a/src/ZF/ex/Term.ML	Wed Jan 13 11:56:28 1999 +0100
    28.2 +++ b/src/ZF/ex/Term.ML	Wed Jan 13 11:57:09 1999 +0100
    28.3 @@ -7,8 +7,6 @@
    28.4  Illustrates the list functor (essentially the same type as in Trees & Forests)
    28.5  *)
    28.6  
    28.7 -open Term;
    28.8 -
    28.9  Goal "term(A) = A * list(term(A))";
   28.10  let open term;  val rew = rewrite_rule con_defs in  
   28.11  by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
   28.12 @@ -121,7 +119,7 @@
   28.13  
   28.14  (** term_map **)
   28.15  
   28.16 -bind_thm ("term_map", (term_map_def RS def_term_rec));
   28.17 +bind_thm ("term_map", term_map_def RS def_term_rec);
   28.18  
   28.19  val prems = Goalw [term_map_def]
   28.20      "[| t: term(A);  !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
   28.21 @@ -136,7 +134,7 @@
   28.22  
   28.23  (** term_size **)
   28.24  
   28.25 -bind_thm ("term_size", (term_size_def RS def_term_rec));
   28.26 +bind_thm ("term_size", term_size_def RS def_term_rec);
   28.27  
   28.28  Goalw [term_size_def] "t: term(A) ==> term_size(t) : nat";
   28.29  by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
   28.30 @@ -145,7 +143,7 @@
   28.31  
   28.32  (** reflect **)
   28.33  
   28.34 -bind_thm ("reflect", (reflect_def RS def_term_rec));
   28.35 +bind_thm ("reflect", reflect_def RS def_term_rec);
   28.36  
   28.37  Goalw [reflect_def] "t: term(A) ==> reflect(t) : term(A)";
   28.38  by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
   28.39 @@ -153,41 +151,53 @@
   28.40  
   28.41  (** preorder **)
   28.42  
   28.43 -bind_thm ("preorder", (preorder_def RS def_term_rec));
   28.44 +bind_thm ("preorder", preorder_def RS def_term_rec);
   28.45  
   28.46  Goalw [preorder_def]
   28.47      "t: term(A) ==> preorder(t) : list(A)";
   28.48  by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
   28.49  qed "preorder_type";
   28.50  
   28.51 +(** postorder **)
   28.52 +
   28.53 +bind_thm ("postorder", postorder_def RS def_term_rec);
   28.54 +
   28.55 +Goalw [postorder_def]
   28.56 +    "t: term(A) ==> postorder(t) : list(A)";
   28.57 +by (REPEAT (ares_tac [term_rec_simple_type] 1));
   28.58 +by (Asm_simp_tac 1);
   28.59 +qed "postorder_type";
   28.60 +
   28.61  
   28.62  (** Term simplification **)
   28.63  
   28.64  val term_typechecks =
   28.65      [term.Apply_I, term_map_type, term_map_type2, term_size_type, 
   28.66 -     reflect_type, preorder_type];
   28.67 +     reflect_type, preorder_type, postorder_type];
   28.68  
   28.69  (*map_type2 and term_map_type2 instantiate variables*)
   28.70  simpset_ref() := simpset()
   28.71 -      addsimps [term_rec, term_map, term_size, reflect, preorder]
   28.72 +      addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]
   28.73        setSolver type_auto_tac (list_typechecks@term_typechecks);
   28.74  
   28.75  
   28.76  (** theorems about term_map **)
   28.77  
   28.78 +Addsimps [thm "List.map_compose"];  (*there is also TF.map_compose*)
   28.79 +
   28.80  Goal "t: term(A) ==> term_map(%u. u, t) = t";
   28.81  by (etac term_induct_eqn 1);
   28.82 -by (asm_simp_tac (simpset() addsimps [map_ident]) 1);
   28.83 +by (Asm_simp_tac 1);
   28.84  qed "term_map_ident";
   28.85  
   28.86  Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
   28.87  by (etac term_induct_eqn 1);
   28.88 -by (asm_simp_tac (simpset() addsimps [map_compose]) 1);
   28.89 +by (asm_simp_tac (simpset() addsimps []) 1);
   28.90  qed "term_map_compose";
   28.91  
   28.92  Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
   28.93  by (etac term_induct_eqn 1);
   28.94 -by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose]) 1);
   28.95 +by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym]) 1);
   28.96  qed "term_map_reflect";
   28.97  
   28.98  
   28.99 @@ -195,18 +205,17 @@
  28.100  
  28.101  Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
  28.102  by (etac term_induct_eqn 1);
  28.103 -by (asm_simp_tac (simpset() addsimps [map_compose]) 1);
  28.104 +by (asm_simp_tac (simpset() addsimps []) 1);
  28.105  qed "term_size_term_map";
  28.106  
  28.107  Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)";
  28.108  by (etac term_induct_eqn 1);
  28.109 -by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose,
  28.110 -                                    list_add_rev]) 1);
  28.111 +by (asm_simp_tac(simpset() addsimps [rev_map_distrib RS sym, list_add_rev]) 1);
  28.112  qed "term_size_reflect";
  28.113  
  28.114  Goal "t: term(A) ==> term_size(t) = length(preorder(t))";
  28.115  by (etac term_induct_eqn 1);
  28.116 -by (asm_simp_tac (simpset() addsimps [length_flat, map_compose]) 1);
  28.117 +by (asm_simp_tac (simpset() addsimps [length_flat]) 1);
  28.118  qed "term_size_length";
  28.119  
  28.120  
  28.121 @@ -214,8 +223,7 @@
  28.122  
  28.123  Goal "t: term(A) ==> reflect(reflect(t)) = t";
  28.124  by (etac term_induct_eqn 1);
  28.125 -by (asm_simp_tac (simpset() addsimps [rev_map_distrib, map_compose,
  28.126 -                                    map_ident, rev_rev_ident]) 1);
  28.127 +by (asm_simp_tac (simpset() addsimps [rev_map_distrib]) 1);
  28.128  qed "reflect_reflect_ident";
  28.129  
  28.130  
  28.131 @@ -223,9 +231,14 @@
  28.132  
  28.133  Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
  28.134  by (etac term_induct_eqn 1);
  28.135 -by (asm_simp_tac (simpset() addsimps [map_compose, map_flat]) 1);
  28.136 +by (asm_simp_tac (simpset() addsimps [map_flat]) 1);
  28.137  qed "preorder_term_map";
  28.138  
  28.139 -(** preorder(reflect(t)) = rev(postorder(t)) **)
  28.140 +Goal "t: term(A) ==> preorder(reflect(t)) = rev(postorder(t))";
  28.141 +by (etac term_induct_eqn 1);
  28.142 +by (asm_simp_tac(simpset() addsimps [rev_app_distrib, rev_flat, 
  28.143 +				     rev_map_distrib RS sym]) 1);
  28.144 +qed "preorder_reflect_eq_rev_postorder";
  28.145 +
  28.146  
  28.147  writeln"Reached end of file.";
    29.1 --- a/src/ZF/ex/Term.thy	Wed Jan 13 11:56:28 1999 +0100
    29.2 +++ b/src/ZF/ex/Term.thy	Wed Jan 13 11:57:09 1999 +0100
    29.3 @@ -9,12 +9,6 @@
    29.4  
    29.5  Term = List +
    29.6  consts
    29.7 -  term_rec  :: [i, [i,i,i]=>i] => i
    29.8 -  term_map  :: [i=>i, i] => i
    29.9 -  term_size :: i=>i
   29.10 -  reflect   :: i=>i
   29.11 -  preorder  :: i=>i
   29.12 -
   29.13    term      :: i=>i
   29.14  
   29.15  datatype
   29.16 @@ -26,6 +20,14 @@
   29.17      type_intrs  "[list_univ RS subsetD]"
   29.18  *)
   29.19  
   29.20 +consts
   29.21 +  term_rec  :: [i, [i,i,i]=>i] => i
   29.22 +  term_map  :: [i=>i, i] => i
   29.23 +  term_size :: i=>i
   29.24 +  reflect   :: i=>i
   29.25 +  preorder  :: i=>i
   29.26 +  postorder :: i=>i
   29.27 +
   29.28  defs
   29.29    term_rec_def
   29.30     "term_rec(t,d) == 
   29.31 @@ -39,4 +41,6 @@
   29.32  
   29.33    preorder_def  "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
   29.34  
   29.35 +  postorder_def "postorder(t) == term_rec(t, %x zs rs. flat(rs) @ [x])"
   29.36 +
   29.37  end
    30.1 --- a/src/ZF/ind_syntax.ML	Wed Jan 13 11:56:28 1999 +0100
    30.2 +++ b/src/ZF/ind_syntax.ML	Wed Jan 13 11:57:09 1999 +0100
    30.3 @@ -107,17 +107,32 @@
    30.4  and quniv       = Const("QUniv.quniv", iT-->iT);
    30.5  
    30.6  (*Make a datatype's domain: form the union of its set parameters*)
    30.7 -fun union_params rec_tm =
    30.8 +fun union_params (rec_tm, cs) =
    30.9    let val (_,args) = strip_comb rec_tm
   30.10 -  in  case (filter (fn arg => type_of arg = iT) args) of
   30.11 -         []    => empty
   30.12 -       | iargs => fold_bal (app Un) iargs
   30.13 +      fun is_ind arg = (type_of arg = iT)
   30.14 +  in  case filter is_ind (args @ cs) of
   30.15 +         []     => empty
   30.16 +       | u_args => fold_bal (app Un) u_args
   30.17    end;
   30.18  
   30.19 -(*Previously these both did    replicate (length rec_tms);  however now
   30.20 -  [q]univ itself constitutes the sum domain for mutual recursion!*)
   30.21 -fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
   30.22 -  | data_domain true  rec_tms = quniv $ union_params (hd rec_tms);
   30.23 +(*univ or quniv constitutes the sum domain for mutual recursion;
   30.24 +  it is applied to the datatype parameters and to Consts occurring in the
   30.25 +  definition other than Nat.nat and the datatype sets themselves.
   30.26 +  FIXME: could insert all constant set expressions, e.g. nat->nat.*)
   30.27 +fun data_domain co (rec_tms, con_ty_lists) = 
   30.28 +    let val rec_names = (*nat doesn't have to be added*)
   30.29 +	    "Nat.nat" :: map (#1 o dest_Const o head_of) rec_tms
   30.30 +	val u = if co then quniv else univ
   30.31 +	fun is_OK (Const(a,T)) = not (a mem_string rec_names)
   30.32 +	  | is_OK _            = false
   30.33 +	val add_term_consts_2 =
   30.34 +	    foldl_aterms (fn (cs, Const c) => Const c ins cs | (cs, _) => cs);
   30.35 +	fun fourth (_, name, args, prems) = prems
   30.36 +	fun add_consts_in_cts cts = 
   30.37 +	    foldl (foldl add_term_consts_2) ([], map fourth (flat cts));
   30.38 +	val cs = filter is_OK (add_consts_in_cts con_ty_lists)
   30.39 +    in  u $ union_params (hd rec_tms, cs)  end;
   30.40 +
   30.41  
   30.42  (*Could go to FOL, but it's hardly general*)
   30.43  val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
   30.44 @@ -141,3 +156,6 @@
   30.45  
   30.46  end;
   30.47  
   30.48 +
   30.49 +(*For convenient access by the user*)
   30.50 +val trace_induct = Ind_Syntax.trace;
    31.1 --- a/src/ZF/pair.ML	Wed Jan 13 11:56:28 1999 +0100
    31.2 +++ b/src/ZF/pair.ML	Wed Jan 13 11:57:09 1999 +0100
    31.3 @@ -135,10 +135,9 @@
    31.4  (*** Eliminator - split ***)
    31.5  
    31.6  (*A META-equality, so that it applies to higher types as well...*)
    31.7 -qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
    31.8 - (fn _ => [ (Simp_tac 1),
    31.9 -            (rtac reflexive_thm 1) ]);
   31.10 -
   31.11 +Goalw [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)";
   31.12 +by (Simp_tac 1);
   31.13 +qed "split";
   31.14  Addsimps [split];
   31.15  
   31.16  qed_goal "split_type" thy
    32.1 --- a/src/ZF/thy_syntax.ML	Wed Jan 13 11:56:28 1999 +0100
    32.2 +++ b/src/ZF/thy_syntax.ML	Wed Jan 13 11:57:09 1999 +0100
    32.3 @@ -140,7 +140,7 @@
    32.4    (("elim" $$-- ident) -- 
    32.5     ("induct" $$-- ident) --
    32.6     ("case_eqns" $$-- list1 ident) -- 
    32.7 -   ("recursor_eqns" $$-- list1 ident)) >> mk_rep_dt_string;
    32.8 +   optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
    32.9  
   32.10  
   32.11  (** primrec **)