# HG changeset patch # User wenzelm # Date 1130257129 -7200 # Node ID d5d576b723719b2f04dd1d407717d9db9bf444c0 # Parent bdac047db2a5592d2a4f9bf19cdd7792bbdb5fe6 avoid legacy goals; diff -r bdac047db2a5 -r d5d576b72371 TFL/rules.ML --- a/TFL/rules.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/TFL/rules.ML Tue Oct 25 18:18:49 2005 +0200 @@ -814,13 +814,12 @@ fun prove strict (ptm, tac) = - let val result = - if strict then OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac]) - else - transform_error (fn () => - OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac])) () - handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg); - in #1 (freeze_thaw result) end; - + let + val {thy, t, ...} = Thm.rep_cterm ptm; + val result = + if strict then Goal.prove thy [] [] t (K tac) + else Goal.prove thy [] [] t (K tac) + handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg); + in #1 (freeze_thaw (standard result)) end; end; diff -r bdac047db2a5 -r d5d576b72371 src/HOL/Hyperreal/transfer.ML --- a/src/HOL/Hyperreal/transfer.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/Hyperreal/transfer.ML Tue Oct 25 18:18:49 2005 +0200 @@ -64,16 +64,14 @@ val {intros,unfolds,refolds,consts} = TransferData.get thy val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t)) val u = unstar_term consts t' - val ct = cterm_of thy (Logic.mk_equals (t,u)) val tacs = - [ rewrite_goals_tac atomizers + [ rewrite_goals_tac (ths @ refolds @ unfolds) + , rewrite_goals_tac atomizers , match_tac [transitive_thm] 1 , resolve_tac [transfer_start] 1 , REPEAT_ALL_NEW (resolve_tac intros) 1 , match_tac [reflexive_thm] 1 ] - in - OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs) - end + in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (fn _ => EVERY tacs) end fun transfer_tac ths = SUBGOAL (fn (t,i) => diff -r bdac047db2a5 -r d5d576b72371 src/HOL/Integ/cooper_proof.ML --- a/src/HOL/Integ/cooper_proof.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/Integ/cooper_proof.ML Tue Oct 25 18:18:49 2005 +0200 @@ -189,47 +189,21 @@ fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end; (* ------------------------------------------------------------------------- *) -(* Modified version of the simple version with minimal amount of checking and postprocessing*) +(*This function proove elementar will be used to generate proofs at + runtime*) (*It is thought to prove properties such as a dvd b + (essentially) that are only to make at runtime.*) (* ------------------------------------------------------------------------- *) - -fun simple_prove_goal_cterm2 G tacs = - let - fun check NONE = error "prove_goal: tactic failed" - | check (SOME (thm, _)) = (case nprems_of thm of - 0 => thm - | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!")) - in check (Seq.pull (EVERY tacs (trivial G))) end; - -(*-------------------------------------------------------------*) -(*-------------------------------------------------------------*) - -fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t); - -(* ------------------------------------------------------------------------- *) -(*This function proove elementar will be used to generate proofs at runtime*) -(*It is is based on the isabelle function proove_goalw_cterm and is thought to *) -(*prove properties such as a dvd b (essentially) that are only to make at -runtime.*) -(* ------------------------------------------------------------------------- *) -fun prove_elementar sg s fm2 = case s of +fun prove_elementar thy s fm2 = + Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY + (case s of (*"ss" like simplification with simpset*) "ss" => - let - val ss = presburger_ss addsimps - [zdvd_iff_zmod_eq_0,unity_coeff_ex] - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] - - end + let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex] + in [simp_tac ss 1, TRY (simple_arith_tac 1)] end (*"bl" like blast tactic*) (* Is only used in the harrisons like proof procedure *) - | "bl" => - let val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1] - end + | "bl" => [blast_tac HOL_cs 1] (*"ed" like Existence disjunctions ...*) (* Is only used in the harrisons like proof procedure *) @@ -244,51 +218,26 @@ etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1, REPEAT(EVERY[etac disjE 1, tac2]), tac2] end - - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct ex_disj_tacs - end + in ex_disj_tacs end - | "fa" => - let val ct = cert_Trueprop sg fm2 - in simple_prove_goal_cterm2 ct [simple_arith_tac 1] - - end + | "fa" => [simple_arith_tac 1] | "sa" => - let - val ss = presburger_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] + let val ss = presburger_ss addsimps zadd_ac + in [simp_tac ss 1, TRY (simple_arith_tac 1)] end - end (* like Existance Conjunction *) | "ec" => - let - val ss = presburger_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] - end + let val ss = presburger_ss addsimps zadd_ac + in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end | "ac" => - let - val ss = HOL_basic_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1] - end + let val ss = HOL_basic_ss addsimps zadd_ac + in [simp_tac ss 1] end | "lf" => - let - val ss = presburger_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] - - end; + let val ss = presburger_ss addsimps zadd_ac + in [simp_tac ss 1, TRY (simple_arith_tac 1)] end)); (*=============================================================*) (*-------------------------------------------------------------*) diff -r bdac047db2a5 -r d5d576b72371 src/HOL/Tools/Presburger/cooper_proof.ML --- a/src/HOL/Tools/Presburger/cooper_proof.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML Tue Oct 25 18:18:49 2005 +0200 @@ -189,47 +189,21 @@ fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end; (* ------------------------------------------------------------------------- *) -(* Modified version of the simple version with minimal amount of checking and postprocessing*) +(*This function proove elementar will be used to generate proofs at + runtime*) (*It is thought to prove properties such as a dvd b + (essentially) that are only to make at runtime.*) (* ------------------------------------------------------------------------- *) - -fun simple_prove_goal_cterm2 G tacs = - let - fun check NONE = error "prove_goal: tactic failed" - | check (SOME (thm, _)) = (case nprems_of thm of - 0 => thm - | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!")) - in check (Seq.pull (EVERY tacs (trivial G))) end; - -(*-------------------------------------------------------------*) -(*-------------------------------------------------------------*) - -fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t); - -(* ------------------------------------------------------------------------- *) -(*This function proove elementar will be used to generate proofs at runtime*) -(*It is is based on the isabelle function proove_goalw_cterm and is thought to *) -(*prove properties such as a dvd b (essentially) that are only to make at -runtime.*) -(* ------------------------------------------------------------------------- *) -fun prove_elementar sg s fm2 = case s of +fun prove_elementar thy s fm2 = + Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY + (case s of (*"ss" like simplification with simpset*) "ss" => - let - val ss = presburger_ss addsimps - [zdvd_iff_zmod_eq_0,unity_coeff_ex] - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] - - end + let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex] + in [simp_tac ss 1, TRY (simple_arith_tac 1)] end (*"bl" like blast tactic*) (* Is only used in the harrisons like proof procedure *) - | "bl" => - let val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1] - end + | "bl" => [blast_tac HOL_cs 1] (*"ed" like Existence disjunctions ...*) (* Is only used in the harrisons like proof procedure *) @@ -244,51 +218,26 @@ etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1, REPEAT(EVERY[etac disjE 1, tac2]), tac2] end - - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct ex_disj_tacs - end + in ex_disj_tacs end - | "fa" => - let val ct = cert_Trueprop sg fm2 - in simple_prove_goal_cterm2 ct [simple_arith_tac 1] - - end + | "fa" => [simple_arith_tac 1] | "sa" => - let - val ss = presburger_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] + let val ss = presburger_ss addsimps zadd_ac + in [simp_tac ss 1, TRY (simple_arith_tac 1)] end - end (* like Existance Conjunction *) | "ec" => - let - val ss = presburger_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] - end + let val ss = presburger_ss addsimps zadd_ac + in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end | "ac" => - let - val ss = HOL_basic_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1] - end + let val ss = HOL_basic_ss addsimps zadd_ac + in [simp_tac ss 1] end | "lf" => - let - val ss = presburger_ss addsimps zadd_ac - val ct = cert_Trueprop sg fm2 - in - simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] - - end; + let val ss = presburger_ss addsimps zadd_ac + in [simp_tac ss 1, TRY (simple_arith_tac 1)] end)); (*=============================================================*) (*-------------------------------------------------------------*) diff -r bdac047db2a5 -r d5d576b72371 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Oct 25 18:18:49 2005 +0200 @@ -68,16 +68,18 @@ val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $ Var (("P", 0), HOLogic.boolT)) val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs))); - val cert = cterm_of (Theory.sign_of thy); + val cert = cterm_of thy; val insts' = (map cert induct_Ps) ~~ (map cert insts); val induct' = refl RS ((List.nth (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp)) - in OldGoals.prove_goalw_cterm [] (cert t) (fn prems => - [rtac induct' 1, - REPEAT (rtac TrueI 1), - REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)), - REPEAT (rtac TrueI 1)]) + in + standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) + (fn prems => EVERY + [rtac induct' 1, + REPEAT (rtac TrueI 1), + REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)), + REPEAT (rtac TrueI 1)])) end; val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~ @@ -201,7 +203,7 @@ absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod (mk_Free "x" T1 i, Free ("y", T2)), set_t))) (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs)); - val cert = cterm_of (Theory.sign_of thy1) + val cert = cterm_of thy1 val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t)) ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts); val induct' = cterm_instantiate ((map cert induct_Ps) ~~ @@ -211,8 +213,8 @@ THEN rewtac (mk_meta_eq choice_eq), rec_intrs), descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts); - in split_conj_thm (OldGoals.prove_goalw_cterm [] - (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac])) + in split_conj_thm (standard (Goal.prove thy1 [] [] + (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))) end; val rec_total_thms = map (fn r => r RS theI') rec_unique_thms; @@ -244,12 +246,13 @@ val _ = message "Proving characteristic theorems for primrec combinators ..." - val rec_thms = map (fn t => OldGoals.prove_goalw_cterm reccomb_defs - (cterm_of (Theory.sign_of thy2) t) (fn _ => - [rtac the1_equality 1, + val rec_thms = map (fn t => standard (Goal.prove thy2 [] [] t + (fn _ => EVERY + [rewrite_goals_tac reccomb_defs, + rtac the1_equality 1, resolve_tac rec_unique_thms 1, resolve_tac rec_intrs 1, - REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)])) + REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))) (DatatypeProp.make_primrecs new_type_names descr sorts thy2) in @@ -318,9 +321,8 @@ end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~ (Library.take (length newTs, reccomb_names))); - val case_thms = map (map (fn t => OldGoals.prove_goalw_cterm (case_defs @ - (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t) - (fn _ => [rtac refl 1]))) + val case_thms = map (map (fn t => standard (Goal.prove thy2 [] [] t + (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))) (DatatypeProp.make_cases new_type_names descr sorts thy2) in @@ -345,15 +347,15 @@ fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) = let - val cert = cterm_of (Theory.sign_of thy); + val cert = cterm_of thy; val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))); val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion; - val tacsf = K [rtac exhaustion' 1, ALLGOALS (asm_simp_tac - (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))] + val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac + (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))]) in - (OldGoals.prove_goalw_cterm [] (cert t1) tacsf, - OldGoals.prove_goalw_cterm [] (cert t2) tacsf) + (standard (Goal.prove thy [] [] t1 tacf), + standard (Goal.prove thy [] [] t2 tacf)) end; val split_thm_pairs = map prove_split_thms @@ -419,8 +421,8 @@ val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; - val size_thms = map (fn t => OldGoals.prove_goalw_cterm rewrites - (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1])) + val size_thms = map (fn t => standard (Goal.prove thy' [] [] t + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) (DatatypeProp.make_size descr sorts thy') in @@ -432,8 +434,8 @@ fun prove_weak_case_congs new_type_names descr sorts thy = let fun prove_weak_case_cong t = - OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) - (fn prems => [rtac ((hd prems) RS arg_cong) 1]) + standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) + (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])) val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy) @@ -453,10 +455,10 @@ hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i] | tac i n = rtac disjI2 i THEN tac i (n - 1) in - OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ => - [rtac allI 1, + standard (Goal.prove thy [] [] t (fn _ => + EVERY [rtac allI 1, exh_tac (K exhaustion) 1, - ALLGOALS (fn i => tac i (i-1))]) + ALLGOALS (fn i => tac i (i-1))])) end; val nchotomys = @@ -475,13 +477,14 @@ val nchotomy'' = cterm_instantiate [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy' in - OldGoals.prove_goalw_cterm [] (cert t) (fn prems => - let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) - in [simp_tac (HOL_ss addsimps [hd prems]) 1, - cut_facts_tac [nchotomy''] 1, - REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1), - REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)] - end) + standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) + (fn prems => + let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) + in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1, + cut_facts_tac [nchotomy''] 1, + REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1), + REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)] + end)) end; val case_congs = map prove_case_cong (DatatypeProp.make_case_congs diff -r bdac047db2a5 -r d5d576b72371 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Oct 25 18:18:49 2005 +0200 @@ -279,22 +279,20 @@ val Abs_name = Sign.intern_const sg ("Abs_" ^ s); val inj_Abs_thm = - OldGoals.prove_goalw_cterm [] - (cterm_of sg - (HOLogic.mk_Trueprop + standard (Goal.prove sg [] [] + (HOLogic.mk_Trueprop (Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $ - Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))) - (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]); + Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))) + (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1])); val setT = HOLogic.mk_setT T val inj_Rep_thm = - OldGoals.prove_goalw_cterm [] - (cterm_of sg - (HOLogic.mk_Trueprop + standard (Goal.prove sg [] [] + (HOLogic.mk_Trueprop (Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $ - Const (Rep_name, RepT) $ Const ("UNIV", setT)))) - (fn _ => [rtac inj_inverseI 1, rtac thm2 1]) + Const (Rep_name, RepT) $ Const ("UNIV", setT))) + (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1])); in (inj_Abs_thm, inj_Rep_thm) end; @@ -375,8 +373,8 @@ (* prove characteristic equations *) val rewrites = def_thms @ (map mk_meta_eq rec_rewrites); - val char_thms' = map (fn eqn => OldGoals.prove_goalw_cterm rewrites - (cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns; + val char_thms' = map (fn eqn => standard (Goal.prove thy' [] [] eqn + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns; in (thy', char_thms' @ char_thms) end; @@ -397,13 +395,12 @@ val Ts = map (TFree o rpair HOLogic.typeS) (variantlist (replicate i "'t", used)); val f = Free ("f", Ts ---> U) - in OldGoals.prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies + in standard (Goal.prove sign [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.list_all (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))), HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, - r $ (a $ app_bnds f i)), f))))) (fn prems => - [cut_facts_tac prems 1, REPEAT (rtac ext 1), - REPEAT (etac allE 1), rtac thm 1, atac 1]) + r $ (a $ app_bnds f i)), f)))) + (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])) end in map (fn r => r RS subst) (thm :: map mk_thm arities) end; @@ -431,8 +428,8 @@ val inj_thms' = map (fn r => r RS injD) (map snd newT_iso_inj_thms @ inj_thms); - val inj_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) - (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ => + val inj_thm = standard (Goal.prove thy5 [] [] + (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, REPEAT (EVERY [rtac allI 1, rtac impI 1, @@ -451,20 +448,18 @@ REPEAT (eresolve_tac (mp :: allE :: map make_elim (Suml_inject :: Sumr_inject :: Lim_inject :: fun_cong :: inj_thms')) 1), - atac 1]))])])])]); + atac 1]))])])])])); val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm); val elem_thm = - OldGoals.prove_goalw_cterm [] - (cterm_of (Theory.sign_of thy5) - (HOLogic.mk_Trueprop (mk_conj ind_concl2))) + standard (Goal.prove thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2)) (fn _ => - [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, + EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, rewrite_goals_tac rewrites, REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW - ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]); + ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)])); in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm)) end; @@ -495,7 +490,7 @@ val iso_thms = if length descr = 1 then [] else Library.drop (length newTs, split_conj_thm - (OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ => + (standard (Goal.prove thy5 [] [] iso_t (fn _ => EVERY [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1, REPEAT (rtac TrueI 1), rewrite_goals_tac (mk_meta_eq choice_eq :: @@ -506,7 +501,7 @@ List.concat (map (mk_funs_inv o #1) newT_iso_axms)) 1), TRY (hyp_subst_tac 1), rtac (sym RS range_eqI) 1, - resolve_tac iso_char_thms 1])]))); + resolve_tac iso_char_thms 1])])))); val Abs_inverse_thms' = map #1 newT_iso_axms @ @@ -525,12 +520,12 @@ let val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms; val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms) - in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ => + in standard (Goal.prove thy5 [] [] eqn (fn _ => EVERY [resolve_tac inj_thms 1, rewrite_goals_tac rewrites, rtac refl 1, resolve_tac rep_intrs 2, - REPEAT (resolve_tac iso_elem_thms 1)]) + REPEAT (resolve_tac iso_elem_thms 1)])) end; (*--------------------------------------------------------------*) @@ -547,8 +542,8 @@ fun prove_distinct_thms (_, []) = [] | prove_distinct_thms (dist_rewrites', t::_::ts) = let - val dist_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ => - [simp_tac (HOL_ss addsimps dist_rewrites') 1]) + val dist_thm = standard (Goal.prove thy5 [] [] t (fn _ => + EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])) in dist_thm::(standard (dist_thm RS not_sym)):: (prove_distinct_thms (dist_rewrites', ts)) end; @@ -568,7 +563,7 @@ ((map (fn r => r RS injD) iso_inj_thms) @ [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject, Suml_inject, Sumr_inject])) - in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ => + in standard (Goal.prove thy5 [] [] t (fn _ => EVERY [rtac iffI 1, REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2, dresolve_tac rep_congs 1, dtac box_equals 1, @@ -576,7 +571,7 @@ REPEAT (eresolve_tac inj_thms 1), REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1), REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1), - atac 1]))]) + atac 1]))])) end; val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts) @@ -616,29 +611,31 @@ val cert = cterm_of (Theory.sign_of thy6); - val indrule_lemma = OldGoals.prove_goalw_cterm [] (cert + val indrule_lemma = standard (Goal.prove thy6 [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), - HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems => - [cut_facts_tac prems 1, REPEAT (etac conjE 1), + HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY + [REPEAT (etac conjE 1), REPEAT (EVERY [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1, - etac mp 1, resolve_tac iso_elem_thms 1])]); + etac mp 1, resolve_tac iso_elem_thms 1])])); val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma))); val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else map (Free o apfst fst o dest_Var) Ps; val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma; - val dt_induct = OldGoals.prove_goalw_cterm [] (cert - (DatatypeProp.make_ind descr sorts)) (fn prems => + val dt_induct_prop = DatatypeProp.make_ind descr sorts; + val dt_induct = standard (Goal.prove thy6 [] + (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) + (fn prems => EVERY [rtac indrule_lemma' 1, (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1, EVERY (map (fn (prem, r) => (EVERY [REPEAT (eresolve_tac Abs_inverse_thms 1), simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1, DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) - (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); + (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))])); val (thy7, [dt_induct']) = thy6 |> Theory.add_path big_name |> diff -r bdac047db2a5 -r d5d576b72371 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/Tools/inductive_package.ML Tue Oct 25 18:18:49 2005 +0200 @@ -248,7 +248,7 @@ | ap_split _ _ _ _ u = u; fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) = - if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, + if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms))) else t | mk_tuple _ _ _ (t::_) = t; @@ -286,7 +286,7 @@ val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\""; -val all_not_allowed = +val all_not_allowed = "Introduction rule must not have a leading \"!!\" quantifier"; fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize []; @@ -472,10 +472,11 @@ fun prove_mono setT fp_fun monos thy = (message " Proving monotonicity ..."; - OldGoals.prove_goalw_cterm [] (*NO quick_and_dirty_prove_goalw_cterm here!*) - (Thm.cterm_of thy (HOLogic.mk_Trueprop - (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun))) - (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)])); + standard (Goal.prove thy [] [] (*NO quick_and_dirty here!*) + (HOLogic.mk_Trueprop + (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)) + (fn _ => EVERY [rtac monoI 1, + REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]))); (* prove introduction rules *) @@ -491,20 +492,18 @@ | select_disj _ 1 = [rtac disjI1] | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); - val intrs = map (fn (i, intr) => OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs - (Thm.cterm_of thy intr) (fn prems => - [(*insert prems and underlying sets*) - cut_facts_tac prems 1, - stac unfold 1, - REPEAT (resolve_tac [vimageI2, CollectI] 1), - (*Now 1-2 subgoals: the disjunction, perhaps equality.*) - EVERY1 (select_disj (length intr_ts) i), - (*Not ares_tac, since refl must be tried before any equality assumptions; - backtracking may occur if the premises have extra variables!*) - DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1), - (*Now solve the equations like Inl 0 = Inl ?b2*) - REPEAT (rtac refl 1)]) - |> rulify) (1 upto (length intr_ts) ~~ intr_ts) + val intrs = (1 upto (length intr_ts) ~~ intr_ts) |> map (fn (i, intr) => + rulify (standard (SkipProof.prove thy [] [] intr (fn _ => EVERY + [rewrite_goals_tac rec_sets_defs, + stac unfold 1, + REPEAT (resolve_tac [vimageI2, CollectI] 1), + (*Now 1-2 subgoals: the disjunction, perhaps equality.*) + EVERY1 (select_disj (length intr_ts) i), + (*Not ares_tac, since refl must be tried before any equality assumptions; + backtracking may occur if the premises have extra variables!*) + DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1), + (*Now solve the equations like Inl 0 = Inl ?b2*) + REPEAT (rtac refl 1)])))) in (intrs, unfold) end; @@ -519,13 +518,16 @@ val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; in mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) => - OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs - (Thm.cterm_of thy t) (fn prems => + SkipProof.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) + (fn prems => EVERY [cut_facts_tac [hd prems] 1, + rewrite_goals_tac rec_sets_defs, dtac (unfold RS subst) 1, REPEAT (FIRSTGOAL (eresolve_tac rules1)), REPEAT (FIRSTGOAL (eresolve_tac rules2)), - EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) + EVERY (map (fn prem => + DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_sets_defs prem, conjI] 1)) (tl prems))]) + |> standard |> rulify |> RuleCases.name cases) end; @@ -624,9 +626,9 @@ mk_indrule cs cTs params intr_ts; val dummy = if !trace then - (writeln "ind_prems = "; - List.app (writeln o Sign.string_of_term thy) ind_prems) - else (); + (writeln "ind_prems = "; + List.app (writeln o Sign.string_of_term thy) ind_prems) + else (); (* make predicate for instantiation of abstract induction rule *) @@ -648,22 +650,24 @@ (* simplification rules for vimage and Collect *) val vimage_simps = if length cs < 2 then [] else - map (fn c => OldGoals.quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy + map (fn c => standard (SkipProof.prove thy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ - List.nth (preds, find_index_eq c cs))))) - (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs; + List.nth (preds, find_index_eq c cs)))) + (fn _ => EVERY + [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1]))) cs; val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct)); val dummy = if !trace then - (writeln "raw_fp_induct = "; print_thm raw_fp_induct) - else (); + (writeln "raw_fp_induct = "; print_thm raw_fp_induct) + else (); - val induct = OldGoals.quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy - (Logic.list_implies (ind_prems, ind_concl))) (fn prems => - [rtac (impI RS allI) 1, + val induct = standard (SkipProof.prove thy [] ind_prems ind_concl + (fn prems => EVERY + [rewrite_goals_tac [inductive_conj_def], + rtac (impI RS allI) 1, DETERM (etac raw_fp_induct 1), rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), fold_goals_tac rec_sets_defs, @@ -674,16 +678,16 @@ REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)), EVERY (map (fn prem => - DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); + DEPTH_SOLVE_1 (ares_tac [rewrite_rule [inductive_conj_def] prem, conjI, refl] 1)) prems)])); - val lemma = OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy - (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => - [cut_facts_tac prems 1, + val lemma = standard (SkipProof.prove thy [] [] + (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY + [rewrite_goals_tac rec_sets_defs, REPEAT (EVERY [REPEAT (resolve_tac [conjI, impI] 1), TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, rewrite_goals_tac sum_case_rewrites, - atac 1])]) + atac 1])])) in standard (split_rule factors (induct RS lemma)) end; diff -r bdac047db2a5 -r d5d576b72371 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/Tools/primrec_package.ML Tue Oct 25 18:18:49 2005 +0200 @@ -254,8 +254,8 @@ val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms'; val _ = message ("Proving equations for primrec function(s) " ^ commas_quote (map fst nameTs1) ^ " ..."); - val simps = map (fn (_, t) => OldGoals.prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t) - (fn _ => [rtac refl 1])) eqns; + val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns; val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy'; val thy''' = thy'' |> (#1 o PureThy.add_thmss [(("simps", simps'), diff -r bdac047db2a5 -r d5d576b72371 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/arith_data.ML Tue Oct 25 18:18:49 2005 +0200 @@ -49,13 +49,9 @@ (* prove conversions *) -val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; - -fun prove_conv expand_tac norm_tac sg ss tu = - mk_meta_eq (OldGoals.prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu)) - (K [expand_tac, norm_tac ss])) - handle ERROR => error ("The error(s) above occurred while trying to prove " ^ - (string_of_cterm (cterm_of sg (mk_eqv tu)))); +fun prove_conv expand_tac norm_tac sg ss tu = (* FIXME avoid standard *) + mk_meta_eq (standard (Goal.prove sg [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) + (K [expand_tac, norm_tac ss]))); val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s" (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); diff -r bdac047db2a5 -r d5d576b72371 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOL/simpdata.ML Tue Oct 25 18:18:49 2005 +0200 @@ -253,14 +253,15 @@ val aT = TFree ("'a", HOLogic.typeS); val x = Free ("x", aT); val y = Free ("y", aT) - in OldGoals.prove_goalw_cterm [simp_implies_def] - (cterm_of sign (Logic.mk_implies - (mk_simp_implies (Logic.mk_equals (x, y)), - mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))))) - (fn hyps => [REPEAT (ares_tac (meta_eq_to_obj_eq :: hyps) 1)]) + in standard (Goal.prove (Thm.theory_of_thm st) [] + [mk_simp_implies (Logic.mk_equals (x, y))] + (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) + (fn prems => EVERY + [rewrite_goals_tac [simp_implies_def], + REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])) end end; - + (*Congruence rules for = (instead of ==)*) fun mk_meta_cong rl = zero_var_indexes (let val rl' = Seq.hd (TRYALL (fn i => fn st => diff -r bdac047db2a5 -r d5d576b72371 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOLCF/domain/theorems.ML Tue Oct 25 18:18:49 2005 +0200 @@ -22,9 +22,12 @@ fun inferT sg pre_tm = #1 (Sign.infer_types (Sign.pp sg) sg (K NONE) (K NONE) [] true ([pre_tm],propT)); -fun pg'' thy defs t = let val sg = sign_of thy; - val ct = Thm.cterm_of sg (inferT sg t); - in OldGoals.prove_goalw_cterm defs ct end; +fun pg'' thy defs t tacs = + let val t' = inferT thy t in + standard (Goal.prove thy [] (Logic.strip_imp_prems t') (Logic.strip_imp_concl t') + (fn prems => rewrite_goals_tac defs THEN EVERY (tacs (map (rewrite_rule defs) prems)))) + end; + fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf | prems=> (cut_facts_tac prems 1)::tacsf); diff -r bdac047db2a5 -r d5d576b72371 src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/HOLCF/fixrec_package.ML Tue Oct 25 18:18:49 2005 +0200 @@ -105,11 +105,10 @@ PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy; val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms; - fun mk_cterm t = cterm_of thy' (infer thy' t); - val ctuple_unfold_ct = mk_cterm (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); - val ctuple_unfold_thm = OldGoals.prove_goalw_cterm [] ctuple_unfold_ct - (fn _ => [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, - simp_tac (simpset_of thy') 1]); + val ctuple_unfold = infer thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); + val ctuple_unfold_thm = standard (Goal.prove thy' [] [] ctuple_unfold + (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, + simp_tac (simpset_of thy') 1])); val ctuple_induct_thm = (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind); @@ -216,9 +215,8 @@ (* proves a block of pattern matching equations as theorems, using unfold *) fun make_simps thy (unfold_thm, eqns) = let - fun tacsf prems = - [rtac (unfold_thm RS ssubst_lhs) 1, simp_tac (simpset_of thy addsimps prems) 1]; - fun prove_term t = OldGoals.prove_goalw_cterm [] (cterm_of thy t) tacsf; + val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1]; + fun prove_term t = standard (Goal.prove thy [] [] t (K (EVERY tacs))); fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts); in map prove_eqn eqns @@ -275,8 +273,8 @@ val cname = case chead_of t of Const(c,_) => c | _ => fixrec_err "function is not declared as constant in theory"; val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold")); - val simp = OldGoals.prove_goalw_cterm [] (cterm_of thy eq) - (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); + val simp = standard (Goal.prove thy [] [] eq + (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1])); in simp end; fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = diff -r bdac047db2a5 -r d5d576b72371 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/ZF/Tools/datatype_package.ML Tue Oct 25 18:18:49 2005 +0200 @@ -270,19 +270,14 @@ val case_trans = hd con_defs RS Ind_Syntax.def_trans and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans; - (*Proves a single case equation. Could use simp_tac, but it's slower!*) - fun case_tacsf con_def _ = - [rewtac con_def, - rtac case_trans 1, - REPEAT (resolve_tac [refl, split_trans, - Su.case_inl RS trans, - Su.case_inr RS trans] 1)]; - - fun prove_case_eqn (arg,con_def) = - OldGoals.prove_goalw_cterm [] - (Ind_Syntax.traceIt "next case equation = " - (cterm_of (sign_of thy1) (mk_case_eqn arg))) - (case_tacsf con_def); + fun prove_case_eqn (arg, con_def) = + standard (Goal.prove thy1 [] [] + (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg)) + (*Proves a single case equation. Could use simp_tac, but it's slower!*) + (fn _ => EVERY + [rewtac con_def, + rtac case_trans 1, + REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)])); val free_iffs = map standard (con_defs RL [Ind_Syntax.def_swap_iff]); @@ -317,17 +312,14 @@ val recursor_trans = recursor_def RS def_Vrecursor RS trans; - (*Proves a single recursor equation.*) - fun recursor_tacsf _ = - [rtac recursor_trans 1, - simp_tac (rank_ss addsimps case_eqns) 1, - IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]; - fun prove_recursor_eqn arg = - OldGoals.prove_goalw_cterm [] - (Ind_Syntax.traceIt "next recursor equation = " - (cterm_of (sign_of thy1) (mk_recursor_eqn arg))) - recursor_tacsf + standard (Goal.prove thy1 [] [] + (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg)) + (*Proves a single recursor equation.*) + (fn _ => EVERY + [rtac recursor_trans 1, + simp_tac (rank_ss addsimps case_eqns) 1, + IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)])); in map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases) end @@ -342,10 +334,12 @@ (*Typical theorems have the form ~con1=con2, con1=con2==>False, con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *) fun mk_free s = - OldGoals.prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*) - con_defs s - (fn prems => [cut_facts_tac prems 1, - fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]); + let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*) + standard (Goal.prove thy [] [] (Sign.read_prop thy s) + (fn _ => EVERY + [rewrite_goals_tac con_defs, + fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])) + end; val simps = case_eqns @ recursor_eqns; diff -r bdac047db2a5 -r d5d576b72371 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/ZF/Tools/inductive_package.ML Tue Oct 25 18:18:49 2005 +0200 @@ -192,12 +192,10 @@ val dummy = writeln " Proving monotonicity..."; val bnd_mono = - OldGoals.prove_goalw_cterm [] - (cterm_of sign1 - (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))) - (fn _ => - [rtac (Collect_subset RS bnd_monoI) 1, - REPEAT (ares_tac (basic_monos @ monos) 1)]); + standard (Goal.prove sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)) + (fn _ => EVERY + [rtac (Collect_subset RS bnd_monoI) 1, + REPEAT (ares_tac (basic_monos @ monos) 1)])); val dom_subset = standard (big_rec_def RS Fp.subs); @@ -221,10 +219,8 @@ (*Type-checking is hardest aspect of proof; disjIn selects the correct disjunct after unfolding*) - fun intro_tacsf disjIn prems = - [(*insert prems and underlying sets*) - cut_facts_tac prems 1, - DETERM (stac unfold 1), + fun intro_tacsf disjIn = + [DETERM (stac unfold 1), REPEAT (resolve_tac [Part_eqI,CollectI] 1), (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*) rtac disjIn 2, @@ -251,12 +247,12 @@ and g rl = rl RS disjI2 in accesses_bal(f, g, asm_rl) end; - fun prove_intr (ct, tacsf) = OldGoals.prove_goalw_cterm part_rec_defs ct tacsf; - - val intrs = ListPair.map prove_intr - (map (cterm_of sign1) intr_tms, - map intro_tacsf (mk_disj_rls(length intr_tms))) - handle MetaSimplifier.SIMPLIFIER (msg,thm) => (print_thm thm; error msg); + val intrs = + (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms))) + |> ListPair.map (fn (t, tacs) => + standard (Goal.prove sign1 [] [] t + (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))) + handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg); (********) val dummy = writeln " Proving the elimination rule..."; @@ -345,23 +341,21 @@ ORELSE' etac FalseE)); val quant_induct = - OldGoals.prove_goalw_cterm part_rec_defs - (cterm_of sign1 - (Logic.list_implies - (ind_prems, - FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred))))) - (fn prems => - [rtac (impI RS allI) 1, - DETERM (etac raw_induct 1), - (*Push Part inside Collect*) - full_simp_tac (min_ss addsimps [Part_Collect]) 1, - (*This CollectE and disjE separates out the introduction rules*) - REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])), - (*Now break down the individual cases. No disjE here in case - some premise involves disjunction.*) - REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE] - ORELSE' bound_hyp_subst_tac)), - ind_tac (rev prems) (length prems) ]); + standard (Goal.prove sign1 [] ind_prems + (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred))) + (fn prems => EVERY + [rewrite_goals_tac part_rec_defs, + rtac (impI RS allI) 1, + DETERM (etac raw_induct 1), + (*Push Part inside Collect*) + full_simp_tac (min_ss addsimps [Part_Collect]) 1, + (*This CollectE and disjE separates out the introduction rules*) + REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])), + (*Now break down the individual cases. No disjE here in case + some premise involves disjunction.*) + REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE] + ORELSE' bound_hyp_subst_tac)), + ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)])); val dummy = if !Ind_Syntax.trace then (writeln "quant_induct = "; print_thm quant_induct) @@ -431,15 +425,12 @@ val lemma = (*makes the link between the two induction rules*) if need_mutual then (writeln " Proving the mutual induction rule..."; - OldGoals.prove_goalw_cterm part_rec_defs - (cterm_of sign1 (Logic.mk_implies (induct_concl, - mutual_induct_concl))) - (fn prems => - [cut_facts_tac prems 1, - REPEAT (rewrite_goals_tac [Pr.split_eq] THEN - lemma_tac 1)])) - else (writeln " [ No mutual induction rule needed ]"; - TrueI); + standard (Goal.prove sign1 [] [] + (Logic.mk_implies (induct_concl, mutual_induct_concl)) + (fn _ => EVERY + [rewrite_goals_tac part_rec_defs, + REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))) + else (writeln " [ No mutual induction rule needed ]"; TrueI); val dummy = if !Ind_Syntax.trace then (writeln "lemma = "; print_thm lemma) @@ -493,14 +484,11 @@ val mutual_induct_fsplit = if need_mutual then - OldGoals.prove_goalw_cterm [] - (cterm_of sign1 - (Logic.list_implies - (map (induct_prem (rec_tms~~preds)) intr_tms, - mutual_induct_concl))) - (fn prems => - [rtac (quant_induct RS lemma) 1, - mutual_ind_tac (rev prems) (length prems)]) + standard (Goal.prove sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms) + mutual_induct_concl + (fn prems => EVERY + [rtac (quant_induct RS lemma) 1, + mutual_ind_tac (rev prems) (length prems)])) else TrueI; (** Uncurrying the predicate in the ordinary induction rule **) diff -r bdac047db2a5 -r d5d576b72371 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Sat Oct 22 01:22:10 2005 +0200 +++ b/src/ZF/Tools/primrec_package.ML Tue Oct 25 18:18:49 2005 +0200 @@ -181,10 +181,10 @@ val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) val eqn_thms = - (message ("Proving equations for primrec function " ^ fname); - map (fn t => OldGoals.prove_goalw_cterm rewrites - (Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy1) t)) - (fn _ => [rtac refl 1])) eqn_terms); + (message ("Proving equations for primrec function " ^ fname); + eqn_terms |> map (fn t => + standard (Goal.prove thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])))); val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); val thy3 = thy2