--- a/src/HOL/Fun.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Fun.ML Thu Aug 08 23:46:09 2002 +0200
@@ -359,23 +359,25 @@
(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
local
- fun gen_fun_upd None T _ _ = None
- | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y)
- fun dest_fun_T1 (Type (_,T::Ts)) = T
- fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = let
- fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
- if v aconv x then Some g else gen_fun_upd (find g) T v w
- | find t = None
- in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
+ fun gen_fun_upd None T _ _ = None
+ | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y);
+ fun dest_fun_T1 (Type (_, T :: Ts)) = T;
+ fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
+ let
+ fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
+ if v aconv x then Some g else gen_fun_upd (find g) T v w
+ | find t = None;
+ in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end;
+
val ss = simpset ();
- val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1,
- simp_tac ss 1]
- fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
+ val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1);
in
val fun_upd2_simproc =
- Simplifier.simproc (Theory.sign_of (the_context ())) "fun_upd2" ["f(v := w, x := y)"]
- (fn sg => fn _ => fn t => case find_double t of (T, None) => None | (T, Some rhs) =>
- Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover));
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "fun_upd2" ["f(v := w, x := y)"]
+ (fn sg => fn _ => fn t =>
+ case find_double t of (T, None) => None
+ | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover));
end;
Addsimprocs[fun_upd2_simproc];
--- a/src/HOL/Hoare/Hoare.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Hoare/Hoare.ML Thu Aug 08 23:46:09 2002 +0200
@@ -125,9 +125,7 @@
Free ("P",varsT --> boolT) $ Bound 0));
val impl = implies $ (Mset_incl big_Collect) $
(Mset_incl small_Collect);
- val cimpl = cterm_of (#sign (rep_thm thm)) impl
- in prove_goalw_cterm [] cimpl (fn prems =>
- [cut_facts_tac prems 1,Blast_tac 1]) end;
+ in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
end;
@@ -139,8 +137,10 @@
(** input does not suffer any unexpected transformation **)
(*****************************************************************************)
-val Compl_Collect = prove_goal (the_context ()) "-(Collect b) = {x. ~(b x)}"
- (fn _ => [Fast_tac 1]);
+Goal "-(Collect b) = {x. ~(b x)}";
+by (Fast_tac 1);
+qed "Compl_Collect";
+
(**Simp_tacs**)
--- a/src/HOL/Integ/Bin.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Integ/Bin.ML Thu Aug 08 23:46:09 2002 +0200
@@ -334,19 +334,14 @@
structure Bin_Simprocs =
struct
- fun prove_conv name tacs sg (hyps: thm list) (t,u) =
+ fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
if t aconv u then None
else
- let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
- in Some
- (prove_goalw_cterm [] ct (K tacs)
- handle ERROR => error
- ("The error(s) above occurred while trying to prove " ^
- string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
- end
+ let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
+ in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
- (*version without the hyps argument*)
- fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []
+ fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
+ fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
@@ -363,7 +358,7 @@
val is_numeral = is_numeral
val numeral_0_eq_0 = int_numeral_0_eq_0
val numeral_1_eq_1 = int_numeral_1_eq_1
- val prove_conv = prove_conv_nohyps "int_abstract_numerals"
+ val prove_conv = prove_conv_nohyps_novars
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
val simplify_meta_eq = simplify_meta_eq
end
--- a/src/HOL/List.thy Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/List.thy Thu Aug 08 23:46:09 2002 +0200
@@ -393,11 +393,8 @@
val appT = [listT,listT] ---> listT
val app = Const("List.op @",appT)
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
- val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
- val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
- handle ERROR =>
- error("The error(s) above occurred while trying to prove " ^
- string_of_cterm ct);
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
+ val thm = Tactic.prove sg [] [] eq (K (rearr_tac 1));
in Some ((conv RS (thm RS trans)) RS eq_reflection) end;
in
--- a/src/HOL/Modelcheck/MuckeSyn.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Thu Aug 08 23:46:09 2002 +0200
@@ -154,8 +154,11 @@
qed "pair_eta_expand";
val pair_eta_expand_proc =
- Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
- (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None);
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "pair_eta_expand" ["f::'a*'b=>'c"]
+ (fn _ => fn _ => fn t =>
+ case t of Abs _ => Some (mk_meta_eq pair_eta_expand)
+ | _ => None);
val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
--- a/src/HOL/Product_Type.thy Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Product_Type.thy Thu Aug 08 23:46:09 2002 +0200
@@ -336,9 +336,9 @@
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None
| split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
| split_pat tp i _ = None;
- fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
- (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
- (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
+ fun metaeq sg lhs rhs = mk_meta_eq (Tactic.prove sg [] []
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
+ (K (simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1)));
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
| beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
--- a/src/HOL/Real/RealBin.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Real/RealBin.ML Thu Aug 08 23:46:09 2002 +0200
@@ -376,20 +376,6 @@
fun trans_tac None = all_tac
| trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
-fun prove_conv name tacs sg (hyps: thm list) (t,u) =
- if t aconv u then None
- else
- let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
- in Some
- (prove_goalw_cterm [] ct (K tacs)
- handle ERROR => error
- ("The error(s) above occurred while trying to prove " ^
- string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
- end;
-
-(*version without the hyps argument*)
-fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
-
(*Final simplification: cancel + and * *)
val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
@@ -421,7 +407,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = prove_conv "realeq_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
val bal_add1 = real_eq_add_iff1 RS trans
@@ -430,7 +416,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = prove_conv "realless_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
val bal_add1 = real_less_add_iff1 RS trans
@@ -439,7 +425,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = prove_conv "realle_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
val bal_add1 = real_le_add_iff1 RS trans
@@ -473,7 +459,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val left_distrib = left_real_add_mult_distrib RS trans
- val prove_conv = prove_conv_nohyps "real_combine_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps
val trans_tac = trans_tac
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
@@ -520,7 +506,7 @@
val is_numeral = Bin_Simprocs.is_numeral
val numeral_0_eq_0 = real_numeral_0_eq_0
val numeral_1_eq_1 = real_numeral_1_eq_1
- val prove_conv = prove_conv_nohyps "real_abstract_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
end
--- a/src/HOL/Tools/datatype_package.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML Thu Aug 08 23:46:09 2002 +0200
@@ -349,15 +349,15 @@
in (case (#distinct (datatype_info_sg_err sg tname1)) of
QuickAndDirty => Some (Thm.invoke_oracle
Datatype_thy distinctN (sg, ConstrDistinct eq_t))
- | FewConstrs thms => Some (prove_goalw_cterm [] eq_ct (K
- [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
- atac 2, resolve_tac thms 1, etac FalseE 1]))
- | ManyConstrs (thm, ss) => Some (prove_goalw_cterm [] eq_ct (K
- [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
+ | FewConstrs thms => Some (Tactic.prove sg [] [] eq_t (K
+ (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
+ atac 2, resolve_tac thms 1, etac FalseE 1])))
+ | ManyConstrs (thm, ss) => Some (Tactic.prove sg [] [] eq_t (K
+ (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
full_simp_tac ss 1,
REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
- etac FalseE 1])))
+ etac FalseE 1]))))
end
else None
end
--- a/src/HOLCF/adm.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOLCF/adm.ML Thu Aug 08 23:46:09 2002 +0200
@@ -104,8 +104,7 @@
| mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
val t' = mk_all params (Logic.list_implies (prems, t));
- val thm = transform_error (fn () => prove_goalw_cterm [] (cterm_of sign t')
- (fn ps => [cut_facts_tac ps 1, tac 1])) ()
+ val thm = Tactic.prove sign [] [] t' (K (tac 1));
in (ts, thm)::l end
handle ERROR_MESSAGE _ => l;
--- a/src/Provers/Arith/abel_cancel.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Thu Aug 08 23:46:09 2002 +0200
@@ -52,9 +52,6 @@
minus_add_distrib, minus_minus,
minus_0, add_0, add_0_right];
- (*prove while suppressing timing information*)
- fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
-
val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
val minus = Const ("uminus", Data.T --> Data.T);
@@ -114,15 +111,11 @@
val _ = if !trace then
tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
else ()
- val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
- val thm = prove ct
- (fn _ => [rtac eq_reflection 1,
- simp_tac prepare_ss 1,
- IF_UNSOLVED (simp_tac cancel_ss 1),
- IF_UNSOLVED (simp_tac inverse_ss 1)])
- handle ERROR =>
- error("cancel_sums simproc:\nfailed to prove " ^
- string_of_cterm ct)
+ val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs))
+ (fn _ => rtac eq_reflection 1 THEN
+ simp_tac prepare_ss 1 THEN
+ IF_UNSOLVED (simp_tac cancel_ss 1) THEN
+ IF_UNSOLVED (simp_tac inverse_ss 1))
in Some thm end
handle Cancel => None;
@@ -172,17 +165,13 @@
val _ = if !trace then
tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
else ()
- val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
- val thm = prove ct
- (fn _ => [rtac eq_reflection 1,
- resolve_tac eqI_rules 1,
- simp_tac prepare_ss 1,
- simp_tac sum_cancel_ss 1,
- IF_UNSOLVED (simp_tac add_ac_ss 1)])
- handle ERROR =>
- error("cancel_relations simproc:\nfailed to prove " ^
- string_of_cterm ct)
+ val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs))
+ (fn _ => rtac eq_reflection 1 THEN
+ resolve_tac eqI_rules 1 THEN
+ simp_tac prepare_ss 1 THEN
+ simp_tac sum_cancel_ss 1 THEN
+ IF_UNSOLVED (simp_tac add_ac_ss 1))
in Some thm end
handle Cancel => None;
--- a/src/Provers/Arith/assoc_fold.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/Provers/Arith/assoc_fold.ML Thu Aug 08 23:46:09 2002 +0200
@@ -25,12 +25,6 @@
val assoc_ss = Data.ss addsimps Data.add_ac;
- (*prove while suppressing timing information*)
- fun prove name ct tacf =
- setmp Library.timing false (prove_goalw_cterm [] ct) tacf
- handle ERROR =>
- error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
-
exception Assoc_fail;
fun mk_sum [] = raise Assoc_fail
@@ -60,10 +54,9 @@
else ()
val rhs = Data.plus $ mk_sum lits $ mk_sum others
val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
- val th = prove "assoc_fold"
- (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
- (fn _ => [rtac Data.eq_reflection 1,
- simp_tac assoc_ss 1])
+ val th = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs))
+ (fn _ => rtac Data.eq_reflection 1 THEN
+ simp_tac assoc_ss 1)
in Some th end
handle Assoc_fail => None;
--- a/src/Provers/quantifier1.ML Thu Aug 08 23:42:49 2002 +0200
+++ b/src/Provers/quantifier1.ML Thu Aug 08 23:46:09 2002 +0200
@@ -104,12 +104,7 @@
in exqu end;
fun prove_conv tac sg tu =
- let val meta_eq = cterm_of sg (Logic.mk_equals tu)
- in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])
- handle ERROR =>
- error("The error(s) above occurred while trying to prove " ^
- string_of_cterm meta_eq)
- end;
+ Tactic.prove sg [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)