# HG changeset patch # User wenzelm # Date 1028843169 -7200 # Node ID bb72bd43c6c314fb7f4b40aa63a167a271e01250 # Parent 7123ae179212f23a661420b31c98b41ed7bd4ec8 use Tactic.prove instead of prove_goalw_cterm in internal proofs! diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Fun.ML --- 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]; diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Hoare/Hoare.ML --- 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**) diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Integ/Bin.ML --- 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 diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/List.thy --- 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 diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Modelcheck/MuckeSyn.ML --- 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]; diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Product_Type.thy --- 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 diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Real/RealBin.ML --- 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 diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Tools/datatype_package.ML --- 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 diff -r 7123ae179212 -r bb72bd43c6c3 src/HOLCF/adm.ML --- 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; diff -r 7123ae179212 -r bb72bd43c6c3 src/Provers/Arith/abel_cancel.ML --- 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; diff -r 7123ae179212 -r bb72bd43c6c3 src/Provers/Arith/assoc_fold.ML --- 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; diff -r 7123ae179212 -r bb72bd43c6c3 src/Provers/quantifier1.ML --- 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)