--- 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 *)
--- 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";
--- 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 \
--- 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)",
--- 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))
--- 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);
--- 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";
--- 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";