# HG changeset patch
# User paulson
# Date 917449102 -3600
# Node ID 6a00a5baef2b19a3b414135e669538ad68c5d550
# Parent  bff90585cce590ac4822e14cc5bc2c1f0e5de188
automatic insertion of datatype intr rules into claset

diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/Coind/ECR.ML
--- a/src/ZF/Coind/ECR.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/Coind/ECR.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -4,22 +4,15 @@
     Copyright   1995  University of Cambridge
 *)
 
-open Dynamic ECR;
-
 (* Specialised co-induction rule *)
 
-Goal "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
-\    <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
-\    {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
-\    Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==>  \
-\ <v_clos(x, e, ve),t>:HasTyRel";
-by (rtac HasTyRel.coinduct 1);
-by (rtac singletonI 1);
-by (fast_tac (claset() addIs Val_ValEnv.intrs) 1);
-by (rtac disjI2 1);
-by (etac singletonE 1); 
-by (REPEAT_FIRST (resolve_tac [conjI,exI]));
-by (REPEAT (atac 1));
+Goal "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;  \
+\        <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
+\        {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
+\        Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]    \
+\     ==> <v_clos(x, e, ve),t>:HasTyRel";
+by (rtac (singletonI RS HasTyRel.coinduct) 1);
+by (ALLGOALS Blast_tac);
 qed "htr_closCI";
 
 (* Specialised elimination rules *)
diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/Coind/MT.ML
--- a/src/ZF/Coind/MT.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/Coind/MT.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -28,8 +28,7 @@
 by (Blast_tac 1);
 qed "consistency_fn";
 
-AddIs (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs);
-AddDs [te_owrE,(ElabRel.dom_subset RS subsetD)];
+AddDs [te_owrE, ElabRel.dom_subset RS subsetD];
 
 Addsimps [ve_dom_owr, ve_app_owr1, ve_app_owr2, 
           te_app_owr1, te_app_owr2];
@@ -71,9 +70,7 @@
 by (rtac v_closNE 1);
 by (rtac subsetI 1);
 by (etac RepFunE 1);
-by (excluded_middle_tac "f=y" 1);
-by (rtac UnI1 2);
-by (rtac UnI2 1);
+by (case_tac "f=y" 1);
 by Auto_tac;
 qed "consistency_fix";
 
@@ -147,6 +144,6 @@
 \     |] ==> isof(c,t)";
 by (rtac htr_constE 1);
 by (dtac consistency 1);
-by (fast_tac (claset() addSIs [basic_consistency_lem]) 1);
+by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
 by (assume_tac 1);
 qed "basic_consistency";
diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/Coind/Values.ML
--- a/src/ZF/Coind/Values.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/Coind/Values.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -42,54 +42,35 @@
 
 (* Nonempty sets *)
 
-val prems = goal Values.thy "A ~= 0 ==> EX a. a:A";
-by (cut_facts_tac prems 1);
-by (rtac (foundation RS disjE) 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
-qed "set_notemptyE";
-
-Goalw (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
+Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
   "v_clos(x,e,ve) ~= 0";
-by (rtac not_emptyI 1);
-by (rtac UnI2 1);
-by (rtac SigmaI 1);
-by (rtac singletonI 1);
-by (rtac UnI1 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "v_closNE";
 
-Goalw (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
+Addsimps [v_closNE];
+AddSEs [v_closNE RS notE];
+
+Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
   "c:Const ==> v_const(c) ~= 0";
 by (dtac constNEE 1);
-by (etac not_emptyE 1);
-by (rtac not_emptyI 1);
-by (rtac UnI2 1);
-by (rtac SigmaI 1);
-by (rtac singletonI 1);
-by (rtac UnI2 1);
-by (rtac SigmaI 1);
-by (rtac singletonI 1);
-by (assume_tac 1);
+by Auto_tac;
 qed "v_constNE";
 
+Addsimps [v_constNE];
+
 (* Proving that the empty set is not a value *)
 
 Goal "v:Val ==> v ~= 0";
 by (etac ValE 1);
-by (ALLGOALS hyp_subst_tac);
-by (etac v_constNE 1);
-by (rtac v_closNE 1);
+by Auto_tac;
 qed "ValNEE";
 
 (* Equalities for value environments *)
 
 Goal "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
 by (etac ValEnvE 1);
-by (Asm_full_simp_tac 1);
-by (stac map_domain_owr 1);
-by (assume_tac 1);
-by (rtac Un_commute 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [map_domain_owr]));
 qed "ve_dom_owr";
 
 Goal "ve:ValEnv \
diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/Resid/Residuals.ML
--- a/src/ZF/Resid/Residuals.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/Resid/Residuals.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -9,7 +9,7 @@
 (*       Setting up rule lists                                               *)
 (* ------------------------------------------------------------------------- *)
 
-AddIs (Sres.intrs @ redexes.intrs @ Sreg.intrs @ [subst_type]); 
+AddIs (Sres.intrs @ Sreg.intrs @ [subst_type]); 
 AddSEs (map Sres.mk_cases
 	     ["residuals(Var(n),Var(n),v)",
 	      "residuals(Fun(t),Fun(u),v)",
diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -355,7 +355,7 @@
 
   val free_SEs = Ind_Syntax.mk_free_SEs free_iffs;
 
-  val {elim, induct, mutual_induct, ...} = ind_result
+  val {intrs, elim, induct, mutual_induct, ...} = ind_result
 
   (*Typical theorems have the form ~con1=con2, con1=con2==>False,
     con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
@@ -390,7 +390,10 @@
  in
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Theory.add_path big_rec_base_name
-        |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
+        |> PureThy.add_thmss [(("simps", simps), 
+			       [Simplifier.simp_add_global])]
+        |> PureThy.add_thmss [(("intrs", intrs), 
+			       [Classical.safe_intro_global])]
         |> DatatypesData.put 
 	    (Symtab.update
 	     ((big_rec_name, dt_info), DatatypesData.get thy1)) 
diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/ex/Primrec.ML
--- a/src/ZF/ex/Primrec.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/ex/Primrec.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -199,8 +199,7 @@
 by (etac (bspec RS lt_trans2) 1);
 by (rtac (add_le_self2 RS succ_leI) 2);
 by Auto_tac;
-qed "PROJ_case_lemma";
-val PROJ_case = PROJ_case_lemma RS bspec;
+qed_spec_mp "PROJ_case";
 
 (** COMP case **)
 
@@ -211,8 +210,8 @@
 \                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
 by (etac list.induct 1);
 by (res_inst_tac [("x","0")] bexI 1);
-by (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]) 1);
-by Auto_tac;
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le])));
+by (Clarify_tac 1);
 by (rtac (ballI RS bexI) 1);
 by (rtac (add_lt_mono RS lt_trans) 1);
 by (REPEAT (FIRSTGOAL (etac bspec)));
@@ -255,7 +254,7 @@
 (*base case*)
 by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec,
 	    assume_tac, rtac (add_le_self RS ack_lt_mono1)]);
-by Auto_tac;
+by (ALLGOALS Asm_simp_tac);
 (*ind step*)
 by (rtac (succ_leI RS lt_trans1) 1);
 by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/ex/PropLog.ML
--- a/src/ZF/ex/PropLog.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/ex/PropLog.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -75,11 +75,11 @@
 (*The deduction theorem*)
 Goal "[| cons(p,H) |- q;  p:prop |] ==>  H |- p=>q";
 by (etac thms.induct 1);
-by (fast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1);
-by (fast_tac (claset() addIs [thms.K RS weaken_right]) 1);
-by (fast_tac (claset() addIs [thms.S RS weaken_right]) 1);
-by (fast_tac (claset() addIs [thms.DN RS weaken_right]) 1);
-by (fast_tac (claset() addIs [thms.S RS thms_MP RS thms_MP]) 1);
+by (blast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.K RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.S RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.DN RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.S RS thms_MP RS thms_MP]) 1);
 qed "deduction";
 
 
@@ -128,11 +128,11 @@
 (*Typical example of strengthening the induction formula*)
 Goal "p: prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)";
 by (Simp_tac 1);
-by (etac prop.induct 1);
+by (induct_tac "p" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
 by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, 
 			       Fls_Imp RS weaken_left_Un2]));
-by (ALLGOALS (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
+by (ALLGOALS (blast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
 					weaken_right, Imp_Fls])));
 qed "hyps_thms_if";
 
@@ -165,14 +165,14 @@
 (*For the case hyps(p,t)-cons(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
 Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
-by (etac prop.induct 1);
+by (induct_tac "p" 1);
 by Auto_tac;
 qed "hyps_Diff";
 
 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
   we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
 Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
-by (etac prop.induct 1);
+by (induct_tac "p" 1);
 by Auto_tac;
 qed "hyps_cons";
 
@@ -189,10 +189,10 @@
 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
  could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
 Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
-by (etac prop.induct 1);
+by (induct_tac "p" 1);
 by (asm_simp_tac (simpset() addsimps [UN_I]) 2);
 by (ALLGOALS Asm_simp_tac);
-by (fast_tac (claset() addIs Fin.intrs) 1);
+by (blast_tac (claset() addIs Fin.intrs) 1);
 qed "hyps_finite";
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
@@ -230,8 +230,7 @@
 
 (*A semantic analogue of the Deduction Theorem*)
 Goalw [logcon_def] "[| cons(p,H) |= q |] ==> H |= p=>q";
-by (Simp_tac 1);
-by (Fast_tac 1);
+by Auto_tac;
 qed "logcon_Imp";
 
 Goal "H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
diff -r bff90585cce5 -r 6a00a5baef2b src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Wed Jan 27 10:31:31 1999 +0100
+++ b/src/ZF/ex/TF.ML	Wed Jan 27 15:58:22 1999 +0100
@@ -127,11 +127,7 @@
 val treeI = tree_subset_TF RS subsetD
 and forestI = forest_subset_TF RS subsetD;
 
-val typechecks =
-    [treeI, forestI,
-     list_of_TF_type, map_type, size_type, preorder_type];
-
-Addsimps typechecks;
+AddTCs [treeI, forestI, list_of_TF_type, map_type, size_type, preorder_type];
 
 (** theorems about list_of_TF and of_list **)
 
@@ -176,16 +172,12 @@
 
 Goal "z: tree_forest(A) ==> size(z) = length(preorder(z))";
 by (etac tree_forest.induct 1);
-by (ALLGOALS   (*TYPECHECKING: why so explicit?*)
-    (asm_simp_tac
-     (simpset() addsimps [treeI RS preorder_type RS length_app])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
 qed "size_length";
 
 (** theorems about preorder **)
 
 Goal "z: tree_forest(A) ==> preorder(TF.map(h,z)) = List.map(h, preorder(z))";
 by (etac tree_forest.induct 1);
-by (ALLGOALS  (*TYPECHECKING: why so explicit?*)
-    (asm_simp_tac
-     (simpset() addsimps [treeI RS preorder_type RS map_app_distrib])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
 qed "preorder_map";