# HG changeset patch # User wenzelm # Date 1152356073 -7200 # Node ID 9c8909fc5865efbd7f8288e1d29f0c9b1ceed45f # Parent e66efbafbf1fee21f1c35c9d7a9ce16a8d72b244 Goal.prove_global; diff -r e66efbafbf1f -r 9c8909fc5865 TFL/rules.ML --- a/TFL/rules.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/TFL/rules.ML Sat Jul 08 12:54:33 2006 +0200 @@ -817,9 +817,9 @@ 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) + if strict then Goal.prove_global thy [] [] t (K tac) + else Goal.prove_global thy [] [] t (K tac) handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg); - in #1 (freeze_thaw (standard result)) end; + in #1 (freeze_thaw result) end; end; diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Jul 08 12:54:33 2006 +0200 @@ -175,7 +175,7 @@ val proof = fn _ => auto_tac (claset(),simp_s); in - ((name, standard (Goal.prove thy5 [] [] statement proof)), []) + ((name, Goal.prove_global thy5 [] [] statement proof), []) end) ak_names_types); (* declares a perm-axclass for every atom-kind *) @@ -236,7 +236,7 @@ val proof = fn _ => auto_tac (claset(),simp_s); in - ((name, standard (Goal.prove thy7 [] [] statement proof)), []) + ((name, Goal.prove_global thy7 [] [] statement proof), []) end) ak_names_types); (* declares an fs-axclass for every atom-kind *) @@ -281,7 +281,7 @@ val proof = fn _ => auto_tac (claset(),simp_s); in - ((name, standard (Goal.prove thy11 [] [] statement proof)), []) + ((name, Goal.prove_global thy11 [] [] statement proof), []) end) ak_names_types); (* declares for every atom-kind combination an axclass *) @@ -332,7 +332,7 @@ val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1]; in - PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy' + PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' end) ak_names_types thy) ak_names_types thy12b; @@ -363,7 +363,7 @@ val proof = fn _ => auto_tac (claset(),simp_s); in - PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy' + PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' end else ([],thy'))) (* do nothing branch, if ak_name = ak_name' *) diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Sat Jul 08 12:54:33 2006 +0200 @@ -255,7 +255,7 @@ val unfolded_perm_eq_thms = if length descr = length new_type_names then [] else map standard (List.drop (split_conj_thm - (Goal.prove thy2 [] [] + (Goal.prove_global thy2 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (c as (s, T), x) => let val [T1, T2] = binder_types T @@ -275,7 +275,7 @@ val perm_empty_thms = List.concat (map (fn a => let val permT = mk_permT (Type (a, [])) in map standard (List.take (split_conj_thm - (Goal.prove thy2 [] [] + (Goal.prove_global thy2 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn ((s, T), x) => HOLogic.mk_eq (Const (s, permT --> T --> T) $ @@ -307,7 +307,7 @@ val pt2_ax = PureThy.get_thm thy2 (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a)); in List.take (map standard (split_conj_thm - (Goal.prove thy2 [] [] + (Goal.prove_global thy2 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn ((s, T), x) => let val perm = Const (s, permT --> T --> T) @@ -343,7 +343,7 @@ val pt3_ax = PureThy.get_thm thy2 (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a)); in List.take (map standard (split_conj_thm - (Goal.prove thy2 [] [] (Logic.mk_implies + (Goal.prove_global thy2 [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq", permT --> permT --> HOLogic.boolT) $ pi1 $ pi2), HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj @@ -393,7 +393,7 @@ at_inst RS (pt_inst RS pt_perm_compose) RS sym, at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym] end)) - val thms = split_conj_thm (standard (Goal.prove thy [] [] + val thms = split_conj_thm (Goal.prove_global thy [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn ((s, T), x) => let @@ -408,7 +408,7 @@ end) (perm_names ~~ Ts ~~ perm_indnames)))) (fn _ => EVERY [indtac induction perm_indnames 1, - ALLGOALS (asm_full_simp_tac simps)]))) + ALLGOALS (asm_full_simp_tac simps)])) in foldl (fn ((s, tvs), thy) => AxClass.prove_arity (s, replicate (length tvs) (cp_class :: classes), [cp_class]) @@ -517,7 +517,7 @@ (perm_indnames ~~ descr); fun mk_perm_closed name = map (fn th => standard (th RS mp)) - (List.take (split_conj_thm (Goal.prove thy4 [] [] + (List.take (split_conj_thm (Goal.prove_global thy4 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (S, x) => let @@ -766,12 +766,12 @@ let val inj_thms = map (fn r => r RS iffD1) abs_inject_thms; val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms - in standard (Goal.prove thy8 [] [] eqn (fn _ => EVERY + in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY [resolve_tac inj_thms 1, rewrite_goals_tac rewrites, rtac refl 3, resolve_tac rep_intrs 2, - REPEAT (resolve_tac rep_thms 1)])) + REPEAT (resolve_tac rep_thms 1)]) end; val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns; @@ -785,11 +785,11 @@ val permT = mk_permT (Type (atom, [])); val pi = Free ("pi", permT); in - standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq + Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x), Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))) (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @ - perm_closed_thms @ Rep_thms)) 1)) + perm_closed_thms @ Rep_thms)) 1) end) Rep_thms; val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm @@ -807,8 +807,8 @@ fun prove_distinct_thms (_, []) = [] | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) = let - val dist_thm = standard (Goal.prove thy8 [] [] t (fn _ => - simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)) + val dist_thm = Goal.prove_global thy8 [] [] t (fn _ => + simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1) in dist_thm::(standard (dist_thm RS not_sym)):: (prove_distinct_thms (p, ts)) end; @@ -849,7 +849,7 @@ val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts; val c = Const (cname, map fastype_of l_args ---> T) in - standard (Goal.prove thy8 [] [] + Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (perm (list_comb (c, l_args)), list_comb (c, r_args)))) (fn _ => EVERY @@ -860,7 +860,7 @@ (symmetric perm_fun_def :: abs_perm)) 1), TRY (simp_tac (HOL_basic_ss addsimps (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @ - perm_closed_thms)) 1)])) + perm_closed_thms)) 1)]) end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss)) end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); @@ -898,7 +898,7 @@ val Ts = map fastype_of args1; val c = Const (cname, Ts ---> T) in - standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq + Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)), foldr1 HOLogic.mk_conj eqs))) (fn _ => EVERY @@ -908,7 +908,7 @@ alpha @ abs_perm @ abs_fresh @ rep_inject_thms @ perm_rep_perm_thms)) 1), TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def :: - expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])) + expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)]) end) (constrs ~~ constr_rep_thms) end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); @@ -946,7 +946,7 @@ fun fresh t = Const ("Nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $ Free ("a", atomT) $ t; - val supp_thm = standard (Goal.prove thy8 [] [] + val supp_thm = Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (supp c, if null dts then Const ("{}", HOLogic.mk_setT atomT) @@ -955,15 +955,15 @@ simp_tac (HOL_basic_ss addsimps (supp_def :: Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un :: symmetric empty_def :: Finites.emptyI :: simp_thms @ - abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)) + abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1) in (supp_thm, - standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq + Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (fresh c, if null dts then HOLogic.true_const else foldr1 HOLogic.mk_conj (map fresh args2)))) (fn _ => - simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1))) + simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1)) end) atoms) constrs) end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps'))); @@ -985,14 +985,14 @@ val (indrule_lemma_prems, indrule_lemma_concls) = Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs')); - val indrule_lemma = standard (Goal.prove thy8 [] [] + val indrule_lemma = Goal.prove_global thy8 [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY [REPEAT (etac conjE 1), REPEAT (EVERY [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1, - etac mp 1, resolve_tac Rep_thms 1])])); + etac mp 1, resolve_tac Rep_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 @@ -1003,7 +1003,7 @@ val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms; val dt_induct_prop = DatatypeProp.make_ind descr' sorts'; - val dt_induct = standard (Goal.prove thy8 [] + val dt_induct = Goal.prove_global thy8 [] (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) (fn prems => EVERY [rtac indrule_lemma' 1, @@ -1012,7 +1012,7 @@ [REPEAT (eresolve_tac Abs_inverse_thms' 1), simp_tac (HOL_basic_ss addsimps [symmetric r]) 1, DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) - (prems ~~ constr_defs))])); + (prems ~~ constr_defs))]); val case_names_induct = mk_case_names_induct descr''; @@ -1028,7 +1028,7 @@ val finite_supp_thms = map (fn atom => let val atomT = Type (atom, []) in map standard (List.take - (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop + (split_conj_thm (Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T), Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT)))) @@ -1258,7 +1258,7 @@ val _ = warning "proving strong induction theorem ..."; - val induct_aux = standard (Goal.prove thy9 [] ind_prems' ind_concl' + val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn prems => EVERY ([mk_subgoal 1 (K (K (K aux_ind_concl))), indtac dt_induct tnames 1] @ @@ -1310,7 +1310,7 @@ (constrs ~~ constrs'))) (descr'' ~~ ndescr)) @ [REPEAT (eresolve_tac [conjE, allE_Nil] 1), REPEAT (etac allE 1), - REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)]))); + REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)])); val induct_aux' = Thm.instantiate ([], map (fn (s, T) => @@ -1323,12 +1323,12 @@ cterm_of thy9 (Const ("Nominal.supp", fastype_of f'))) end) fresh_fs) induct_aux; - val induct = standard (Goal.prove thy9 [] ind_prems ind_concl + val induct = Goal.prove_global thy9 [] ind_prems ind_concl (fn prems => EVERY [rtac induct_aux' 1, REPEAT (resolve_tac induct_aux_lemmas 1), REPEAT ((resolve_tac prems THEN_ALL_NEW - (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])) + (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)]) val (_, thy10) = thy9 |> Theory.add_path big_name |> @@ -1430,19 +1430,19 @@ HOLogic.mk_mem (HOLogic.mk_prod (mk_perm [] (pi, x), mk_perm [] (pi, y)), R')) end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs)); val ths = map (fn th => standard (th RS mp)) (split_conj_thm - (Goal.prove thy11 [] [] + (Goal.prove_global thy11 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))) (fn _ => rtac rec_induct 1 THEN REPEAT (NominalPermeq.perm_simp_tac (simpset_of thy11) 1 THEN (resolve_tac rec_intrs THEN_ALL_NEW asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1)))) - val ths' = map (fn ((P, Q), th) => standard - (Goal.prove thy11 [] [] + val ths' = map (fn ((P, Q), th) => + Goal.prove_global thy11 [] [] (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)) (fn _ => dtac (Thm.instantiate ([], [(cterm_of thy11 (Var (("pi", 0), permT)), cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN - NominalPermeq.perm_simp_tac HOL_ss 1))) (ps ~~ ths) + NominalPermeq.perm_simp_tac HOL_ss 1)) (ps ~~ ths) in (ths, ths') end) dt_atomTs); (** finite support **) @@ -1458,7 +1458,7 @@ (rec_fns ~~ rec_fn_Ts) in map (fn th => standard (th RS mp)) (split_conj_thm - (Goal.prove thy11 [] fins + (Goal.prove_global thy11 [] fins (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (((T, U), R), i) => let diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Jul 08 12:54:33 2006 +0200 @@ -74,12 +74,12 @@ (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp)) in - standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) + Goal.prove_global 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)])) + REPEAT (rtac TrueI 1)]) end; val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~ @@ -216,8 +216,8 @@ THEN rewtac (mk_meta_eq choice_eq), rec_intrs), descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts); - in split_conj_thm (standard (Goal.prove thy1 [] [] - (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))) + in split_conj_thm (Goal.prove_global 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; @@ -250,13 +250,13 @@ val _ = message "Proving characteristic theorems for primrec combinators ..." - val rec_thms = map (fn t => standard (Goal.prove thy2 [] [] t + val rec_thms = map (fn t => Goal.prove_global 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 @@ -329,8 +329,8 @@ end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~ (Library.take (length newTs, reccomb_names))); - 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])))) + val case_thms = map (map (fn t => Goal.prove_global 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 @@ -362,8 +362,8 @@ val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))]) in - (standard (Goal.prove thy [] [] t1 tacf), - standard (Goal.prove thy [] [] t2 tacf)) + (Goal.prove_global thy [] [] t1 tacf, + Goal.prove_global thy [] [] t2 tacf) end; val split_thm_pairs = map prove_split_thms @@ -432,8 +432,8 @@ val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; - val size_thms = map (fn t => standard (Goal.prove thy' [] [] t - (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) + val size_thms = map (fn t => Goal.prove_global thy' [] [] t + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) (DatatypeProp.make_size descr sorts thy') in @@ -447,8 +447,8 @@ fun prove_weak_case_congs new_type_names descr sorts thy = let fun prove_weak_case_cong t = - standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) - (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])) + Goal.prove_global 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) @@ -468,10 +468,10 @@ hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i] | tac i n = rtac disjI2 i THEN tac i (n - 1) in - standard (Goal.prove thy [] [] t (fn _ => + Goal.prove_global 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 = @@ -490,14 +490,14 @@ val nchotomy'' = cterm_instantiate [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy' in - standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) + Goal.prove_global 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) end; val case_congs = map prove_case_cong (DatatypeProp.make_case_congs diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Jul 08 12:54:33 2006 +0200 @@ -278,20 +278,20 @@ val Abs_name = Sign.intern_const sg ("Abs_" ^ s); val inj_Abs_thm = - 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 _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1])); + Goal.prove_global sg [] [] + (HOLogic.mk_Trueprop + (Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $ + 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 = - standard (Goal.prove sg [] [] - (HOLogic.mk_Trueprop - (Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $ - Const (Rep_name, RepT) $ Const ("UNIV", setT))) - (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1])); + Goal.prove_global sg [] [] + (HOLogic.mk_Trueprop + (Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $ + Const (Rep_name, RepT) $ Const ("UNIV", setT))) + (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]); in (inj_Abs_thm, inj_Rep_thm) end; @@ -372,8 +372,8 @@ (* prove characteristic equations *) val rewrites = def_thms @ (map mk_meta_eq rec_rewrites); - val char_thms' = map (fn eqn => standard (Goal.prove thy' [] [] eqn - (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns; + val char_thms' = map (fn eqn => Goal.prove_global thy' [] [] eqn + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns; in (thy', char_thms' @ char_thms) end; @@ -394,12 +394,12 @@ val Ts = map (TFree o rpair HOLogic.typeS) (variantlist (replicate i "'t", used)); val f = Free ("f", Ts ---> U) - in standard (Goal.prove sign [] [] (Logic.mk_implies + in Goal.prove_global 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 _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])) + (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; @@ -427,7 +427,7 @@ val inj_thms' = map (fn r => r RS injD) (map snd newT_iso_inj_thms @ inj_thms); - val inj_thm = standard (Goal.prove thy5 [] [] + val inj_thm = Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, REPEAT (EVERY @@ -447,18 +447,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 = - standard (Goal.prove thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2)) - (fn _ => - 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)])); + Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2)) + (fn _ => + 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)]); in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm)) end; @@ -489,7 +489,7 @@ val iso_thms = if length descr = 1 then [] else Library.drop (length newTs, split_conj_thm - (standard (Goal.prove thy5 [] [] iso_t (fn _ => EVERY + (Goal.prove_global 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 :: @@ -500,7 +500,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 @ @@ -519,12 +519,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 standard (Goal.prove thy5 [] [] eqn (fn _ => EVERY + in Goal.prove_global 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; (*--------------------------------------------------------------*) @@ -541,8 +541,8 @@ fun prove_distinct_thms (_, []) = [] | prove_distinct_thms (dist_rewrites', t::_::ts) = let - val dist_thm = standard (Goal.prove thy5 [] [] t (fn _ => - EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])) + val dist_thm = Goal.prove_global 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; @@ -562,7 +562,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 standard (Goal.prove thy5 [] [] t (fn _ => EVERY + in Goal.prove_global 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, @@ -570,7 +570,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) @@ -612,14 +612,14 @@ val cert = cterm_of (Theory.sign_of thy6); - val indrule_lemma = standard (Goal.prove thy6 [] [] + val indrule_lemma = Goal.prove_global thy6 [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), 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 @@ -627,7 +627,7 @@ val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma; val dt_induct_prop = DatatypeProp.make_ind descr sorts; - val dt_induct = standard (Goal.prove thy6 [] + val dt_induct = Goal.prove_global thy6 [] (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) (fn prems => EVERY [rtac indrule_lemma' 1, @@ -636,7 +636,7 @@ [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 ([dt_induct'], thy7) = thy6 diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOL/Tools/primrec_package.ML Sat Jul 08 12:54:33 2006 +0200 @@ -259,8 +259,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) => standard (Goal.prove thy' [] [] t - (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns; + val simps = map (fn (_, t) => Goal.prove_global thy' [] [] t + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns; val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy'; val thy''' = thy'' |> (snd o PureThy.add_thmss [(("simps", simps'), diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOL/Tools/typedef_package.ML Sat Jul 08 12:54:33 2006 +0200 @@ -163,7 +163,7 @@ (Abs_name, oldT --> newT, NoSyn)]) |> add_def (Logic.mk_defpair (setC, set)) ||>> PureThy.add_axioms_i [((typedef_name, typedef_prop), - [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] + [apsnd (fn cond_axm => nonempty RS cond_axm)])] ||> Theory.add_deps "" (dest_Const RepC) typedef_deps ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps |-> (fn (set_def, [type_definition]) => fn thy1 => @@ -243,7 +243,7 @@ val (cset, goal, _, typedef_result) = prepare_typedef prep_term def name typ set opt_morphs thy; val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); - val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg => + val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset)); in Context.Theory thy diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOL/simpdata.ML Sat Jul 08 12:54:33 2006 +0200 @@ -264,12 +264,12 @@ val aT = TFree ("'a", HOLogic.typeS); val x = Free ("x", aT); val y = Free ("y", aT) - in standard (Goal.prove (Thm.theory_of_thm st) [] + in Goal.prove_global (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)])) + REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) end end; diff -r e66efbafbf1f -r 9c8909fc5865 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOLCF/domain/theorems.ML Sat Jul 08 12:54:33 2006 +0200 @@ -72,9 +72,7 @@ fun tac prems = rewrite_goals_tac defs THEN EVERY (tacs (map (rewrite_rule defs) prems)); - in - standard (Goal.prove thy [] asms prop tac) - end; + in Goal.prove_global thy [] asms prop tac end; fun pg' thy defs t tacsf = let diff -r e66efbafbf1f -r 9c8909fc5865 src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/HOLCF/fixrec_package.ML Sat Jul 08 12:54:33 2006 +0200 @@ -101,9 +101,9 @@ val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms; val ctuple_unfold = infer thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); - val ctuple_unfold_thm = standard (Goal.prove thy' [] [] ctuple_unfold + val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, - simp_tac (simpset_of thy') 1])); + simp_tac (simpset_of thy') 1]); val ctuple_induct_thm = (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind); @@ -211,7 +211,7 @@ fun make_simps thy (unfold_thm, eqns) = let 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_term t = Goal.prove_global thy [] [] t (K (EVERY tacs)); fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts); in map prove_eqn eqns @@ -268,8 +268,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 = standard (Goal.prove thy [] [] eq - (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1])); + val simp = Goal.prove_global 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 e66efbafbf1f -r 9c8909fc5865 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Sat Jul 08 12:54:33 2006 +0200 @@ -699,8 +699,8 @@ let val cos' = rev cos in (op @) (fold (mk_eq vs) (product cos' cos') ([], [])) end; fun mk_eq_thms tac vs_cos = - map (fn t => Goal.prove thy [] [] - (ObjectLogic.ensure_propT thy t) (K tac) |> standard) (mk_eqs vs_cos); + map (fn t => Goal.prove_global thy [] [] + (ObjectLogic.ensure_propT thy t) (K tac)) (mk_eqs vs_cos); in case getf_first (map (fn f => f thy) (the_datatypes_extrs thy)) dtco of NONE => NONE diff -r e66efbafbf1f -r 9c8909fc5865 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/ZF/Tools/datatype_package.ML Sat Jul 08 12:54:33 2006 +0200 @@ -271,13 +271,13 @@ and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans; fun prove_case_eqn (arg, con_def) = - standard (Goal.prove thy1 [] [] + Goal.prove_global 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)])); + 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]); @@ -313,13 +313,13 @@ val recursor_trans = recursor_def RS def_Vrecursor RS trans; fun prove_recursor_eqn arg = - standard (Goal.prove thy1 [] [] + Goal.prove_global 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)])); + IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]); in map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases) end @@ -335,10 +335,10 @@ con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *) fun mk_free s = 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) + Goal.prove_global thy [] [] (Sign.read_prop thy s) (fn _ => EVERY [rewrite_goals_tac con_defs, - fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])) + fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]) end; val simps = case_eqns @ recursor_eqns; diff -r e66efbafbf1f -r 9c8909fc5865 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/ZF/Tools/inductive_package.ML Sat Jul 08 12:54:33 2006 +0200 @@ -194,10 +194,10 @@ val dummy = writeln " Proving monotonicity..."; val bnd_mono = - standard (Goal.prove sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)) + Goal.prove_global 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)])); + REPEAT (ares_tac (basic_monos @ monos) 1)]); val dom_subset = standard (big_rec_def RS Fp.subs); @@ -252,8 +252,8 @@ 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)))) + Goal.prove_global sign1 [] [] t + (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs))) handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg); (********) @@ -343,7 +343,7 @@ ORELSE' etac FalseE)); val quant_induct = - standard (Goal.prove sign1 [] ind_prems + Goal.prove_global sign1 [] ind_prems (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred))) (fn prems => EVERY [rewrite_goals_tac part_rec_defs, @@ -357,7 +357,7 @@ 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)])); + 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) @@ -427,11 +427,11 @@ val lemma = (*makes the link between the two induction rules*) if need_mutual then (writeln " Proving the mutual induction rule..."; - standard (Goal.prove sign1 [] [] + Goal.prove_global 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)]))) + 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 @@ -486,11 +486,11 @@ val mutual_induct_fsplit = if need_mutual then - standard (Goal.prove sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms) + Goal.prove_global 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)])) + mutual_ind_tac (rev prems) (length prems)]) else TrueI; (** Uncurrying the predicate in the ordinary induction rule **) diff -r e66efbafbf1f -r 9c8909fc5865 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Sat Jul 08 12:54:32 2006 +0200 +++ b/src/ZF/Tools/primrec_package.ML Sat Jul 08 12:54:33 2006 +0200 @@ -183,8 +183,8 @@ val eqn_thms = (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])))); + Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) + (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))); val (eqn_thms', thy2) = thy1