--- 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;
--- 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' *)
--- 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
--- 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
--- 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
--- 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'),
--- 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
--- 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;
--- 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
--- 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 =
--- 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
--- 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;
--- 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 **)
--- 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