tidied
authorpaulson
Thu Jan 28 18:28:06 1999 +0100 (1999-01-28)
changeset 616032c0b8f57bb7
parent 6159 833b76d0e6dc
child 6161 bc2a76ce1ea3
tidied
src/ZF/ex/Term.ML
     1.1 --- a/src/ZF/ex/Term.ML	Thu Jan 28 18:10:17 1999 +0100
     1.2 +++ b/src/ZF/ex/Term.ML	Thu Jan 28 18:28:06 1999 +0100
     1.3 @@ -7,6 +7,8 @@
     1.4  Illustrates the list functor (essentially the same type as in Trees & Forests)
     1.5  *)
     1.6  
     1.7 +AddTCs [term.Apply_I];
     1.8 +
     1.9  Goal "term(A) = A * list(term(A))";
    1.10  let open term;  val rew = rewrite_rule con_defs in  
    1.11  by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
    1.12 @@ -96,8 +98,7 @@
    1.13  by (REPEAT (ares_tac prems 1));
    1.14  by (etac list.induct 1);
    1.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps [term_rec])));
    1.16 -by (etac CollectE 1);
    1.17 -by (REPEAT (ares_tac [list.Cons_I, UN_I] 1));
    1.18 +by Auto_tac;
    1.19  qed "term_rec_type";
    1.20  
    1.21  val [rew,tslist] = Goal
    1.22 @@ -116,6 +117,7 @@
    1.23  by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
    1.24  qed "term_rec_simple_type";
    1.25  
    1.26 +AddTCs [term_rec_simple_type];
    1.27  
    1.28  (** term_map **)
    1.29  
    1.30 @@ -137,7 +139,7 @@
    1.31  bind_thm ("term_size", term_size_def RS def_term_rec);
    1.32  
    1.33  Goalw [term_size_def] "t: term(A) ==> term_size(t) : nat";
    1.34 -by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
    1.35 +by Auto_tac;
    1.36  qed "term_size_type";
    1.37  
    1.38  
    1.39 @@ -146,32 +148,29 @@
    1.40  bind_thm ("reflect", reflect_def RS def_term_rec);
    1.41  
    1.42  Goalw [reflect_def] "t: term(A) ==> reflect(t) : term(A)";
    1.43 -by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
    1.44 +by Auto_tac;
    1.45  qed "reflect_type";
    1.46  
    1.47  (** preorder **)
    1.48  
    1.49  bind_thm ("preorder", preorder_def RS def_term_rec);
    1.50  
    1.51 -Goalw [preorder_def]
    1.52 -    "t: term(A) ==> preorder(t) : list(A)";
    1.53 -by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
    1.54 +Goalw [preorder_def] "t: term(A) ==> preorder(t) : list(A)";
    1.55 +by Auto_tac;
    1.56  qed "preorder_type";
    1.57  
    1.58  (** postorder **)
    1.59  
    1.60  bind_thm ("postorder", postorder_def RS def_term_rec);
    1.61  
    1.62 -Goalw [postorder_def]
    1.63 -    "t: term(A) ==> postorder(t) : list(A)";
    1.64 -by (REPEAT (ares_tac [term_rec_simple_type] 1));
    1.65 -by (Asm_simp_tac 1);
    1.66 +Goalw [postorder_def] "t: term(A) ==> postorder(t) : list(A)";
    1.67 +by Auto_tac;
    1.68  qed "postorder_type";
    1.69  
    1.70  
    1.71  (** Term simplification **)
    1.72  
    1.73 -AddTCs [term.Apply_I, term_map_type, term_map_type2, term_size_type, 
    1.74 +AddTCs [term_map_type, term_map_type2, term_size_type, 
    1.75  	reflect_type, preorder_type, postorder_type];
    1.76  
    1.77  (*map_type2 and term_map_type2 instantiate variables*)
    1.78 @@ -189,7 +188,7 @@
    1.79  
    1.80  Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
    1.81  by (etac term_induct_eqn 1);
    1.82 -by (asm_simp_tac (simpset() addsimps []) 1);
    1.83 +by (Asm_simp_tac 1);
    1.84  qed "term_map_compose";
    1.85  
    1.86  Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
    1.87 @@ -202,7 +201,7 @@
    1.88  
    1.89  Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
    1.90  by (etac term_induct_eqn 1);
    1.91 -by (asm_simp_tac (simpset() addsimps []) 1);
    1.92 +by (Asm_simp_tac 1);
    1.93  qed "term_size_term_map";
    1.94  
    1.95  Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)";