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