--- a/src/FOL/IFOL.thy Thu Feb 12 12:46:50 2015 +0000
+++ b/src/FOL/IFOL.thy Fri Feb 13 23:39:25 2015 +0100
@@ -208,8 +208,8 @@
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
ML {*
- fun mp_tac i = eresolve0_tac [@{thm notE}, @{thm impE}] i THEN atac i
- fun eq_mp_tac i = eresolve0_tac [@{thm notE}, @{thm impE}] i THEN eq_assume_tac i
+ fun mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i
+ fun eq_mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i
*}
@@ -304,18 +304,20 @@
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*)
ML {*
- fun iff_tac prems i =
- resolve0_tac (prems RL @{thms iffE}) i THEN
- REPEAT1 (eresolve0_tac [@{thm asm_rl}, @{thm mp}] i)
+ fun iff_tac ctxt prems i =
+ resolve_tac ctxt (prems RL @{thms iffE}) i THEN
+ REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i)
*}
+method_setup iff =
+ \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+
lemma conj_cong:
assumes "P <-> P'"
and "P' ==> Q <-> Q'"
shows "(P&Q) <-> (P'&Q')"
apply (insert assms)
- apply (assumption | rule iffI conjI | erule iffE conjE mp |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
done
(*Reversed congruence rule! Used in ZF/Order*)
@@ -324,8 +326,7 @@
and "P' ==> Q <-> Q'"
shows "(Q&P) <-> (Q'&P')"
apply (insert assms)
- apply (assumption | rule iffI conjI | erule iffE conjE mp |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
done
lemma disj_cong:
@@ -340,8 +341,7 @@
and "P' ==> Q <-> Q'"
shows "(P-->Q) <-> (P'-->Q')"
apply (insert assms)
- apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
done
lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
@@ -355,22 +355,19 @@
lemma all_cong:
assumes "!!x. P(x) <-> Q(x)"
shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
- apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
done
lemma ex_cong:
assumes "!!x. P(x) <-> Q(x)"
shows "(EX x. P(x)) <-> (EX x. Q(x))"
- apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
done
lemma ex1_cong:
assumes "!!x. P(x) <-> Q(x)"
shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
- apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
done
(*** Equality rules ***)
--- a/src/FOL/intprover.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/FOL/intprover.ML Fri Feb 13 23:39:25 2015 +0100
@@ -6,7 +6,7 @@
BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
-Completeness (for propositional logic) is proved in
+Completeness (for propositional logic) is proved in
Roy Dyckhoff.
Contraction-Free Sequent Calculi for Intuitionistic Logic.
@@ -15,7 +15,7 @@
The approach was developed independently by Roy Dyckhoff and L C Paulson.
*)
-signature INT_PROVER =
+signature INT_PROVER =
sig
val best_tac: Proof.context -> int -> tactic
val best_dup_tac: Proof.context -> int -> tactic
@@ -31,7 +31,7 @@
end;
-structure IntPr : INT_PROVER =
+structure IntPr : INT_PROVER =
struct
(*Negation is treated as a primitive symbol, with rules notI (introduction),
@@ -44,11 +44,11 @@
(false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
(true, @{thm conjE}), (true, @{thm exE}),
(false, @{thm conjI}), (true, @{thm conj_impE}),
- (true, @{thm disj_impE}), (true, @{thm disjE}),
+ (true, @{thm disj_impE}), (true, @{thm disjE}),
(false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
val haz_brls =
- [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
+ [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
(true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
(true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
@@ -65,7 +65,7 @@
fun safe_step_tac ctxt =
FIRST' [
eq_assume_tac,
- eq_mp_tac,
+ eq_mp_tac ctxt,
bimatch_tac ctxt safe0_brls,
hyp_subst_tac ctxt,
bimatch_tac ctxt safep_brls];
@@ -75,7 +75,7 @@
(*These steps could instantiate variables and are therefore unsafe.*)
fun inst_step_tac ctxt =
- assume_tac ctxt APPEND' mp_tac APPEND'
+ assume_tac ctxt APPEND' mp_tac ctxt APPEND'
biresolve_tac ctxt (safe0_brls @ safep_brls);
(*One safe or unsafe step. *)
--- a/src/FOLP/IFOLP.thy Thu Feb 12 12:46:50 2015 +0000
+++ b/src/FOLP/IFOLP.thy Fri Feb 13 23:39:25 2015 +0100
@@ -275,6 +275,7 @@
fun mp_tac ctxt i =
eresolve_tac ctxt [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac ctxt i
*}
+method_setup mp = \<open>Scan.succeed (SIMPLE_METHOD' o mp_tac)\<close>
(*Like mp_tac but instantiates no variables*)
ML {*
@@ -360,23 +361,25 @@
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*)
ML {*
-fun iff_tac prems i =
- resolve0_tac (prems RL [@{thm iffE}]) i THEN
- REPEAT1 (eresolve0_tac [asm_rl, @{thm mp}] i)
+fun iff_tac ctxt prems i =
+ resolve_tac ctxt (prems RL [@{thm iffE}]) i THEN
+ REPEAT1 (eresolve_tac ctxt [asm_rl, @{thm mp}] i)
*}
+method_setup iff =
+ \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+
schematic_lemma conj_cong:
assumes "p:P <-> P'"
and "!!x. x:P' ==> q(x):Q <-> Q'"
shows "?p:(P&Q) <-> (P'&Q')"
apply (insert assms(1))
- apply (assumption | rule iffI conjI |
- erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
+ apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
done
schematic_lemma disj_cong:
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
- apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
+ apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | mp)+
done
schematic_lemma imp_cong:
@@ -384,32 +387,29 @@
and "!!x. x:P' ==> q(x):Q <-> Q'"
shows "?p:(P-->Q) <-> (P'-->Q')"
apply (insert assms(1))
- apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac @{context} 1 *} |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (assumption | rule iffI impI | erule iffE | mp | iff assms)+
done
schematic_lemma iff_cong:
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
- apply (erule iffE | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
+ apply (erule iffE | assumption | rule iffI | mp)+
done
schematic_lemma not_cong:
"p:P <-> P' ==> ?p:~P <-> ~P'"
- apply (assumption | rule iffI notI | tactic {* mp_tac @{context} 1 *} | erule iffE notE)+
+ apply (assumption | rule iffI notI | mp | erule iffE notE)+
done
schematic_lemma all_cong:
assumes "!!x. f(x):P(x) <-> Q(x)"
shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
- apply (assumption | rule iffI allI | tactic {* mp_tac @{context} 1 *} | erule allE |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (assumption | rule iffI allI | mp | erule allE | iff assms)+
done
schematic_lemma ex_cong:
assumes "!!x. f(x):P(x) <-> Q(x)"
shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
- apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac @{context} 1 *} |
- tactic {* iff_tac @{thms assms} 1 *})+
+ apply (erule exE | assumption | rule iffI exI | mp | iff assms)+
done
(*NOT PROVED
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Feb 13 23:39:25 2015 +0100
@@ -35,24 +35,22 @@
('a * 'b) list -> ('a * 'b) list * ('a list * 'b list)
val consts_in : term -> term list
- val head_quantified_variable :
- int -> thm -> (string * typ) option
+ val head_quantified_variable : Proof.context -> int -> thm -> (string * typ) option
val push_allvar_in : string -> term -> term
val strip_top_All_var : term -> (string * typ) * term
val strip_top_All_vars : term -> (string * typ) list * term
val strip_top_all_vars :
(string * typ) list -> term -> (string * typ) list * term
- val trace_tac' :
- string ->
+ val trace_tac' : Proof.context -> string ->
('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
val try_dest_Trueprop : term -> term
val type_devar : ((indexname * sort) * typ) list -> term -> term
val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
- val batter : int -> tactic
- val break_hypotheses : int -> tactic
- val clause_breaker : int -> tactic
+ val batter_tac : Proof.context -> int -> tactic
+ val break_hypotheses_tac : Proof.context -> int -> tactic
+ val clause_breaker_tac : Proof.context -> int -> tactic
(* val dist_all_and_tac : Proof.context -> int -> tactic *)(*FIXME unused*)
val reassociate_conjs_tac : Proof.context -> int -> tactic
@@ -616,15 +614,15 @@
(** Some tactics **)
-val break_hypotheses =
- ((REPEAT_DETERM o etac @{thm conjE})
- THEN' (REPEAT_DETERM o etac @{thm disjE})
- ) #> CHANGED
+fun break_hypotheses_tac ctxt =
+ CHANGED o
+ ((REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}) THEN'
+ (REPEAT_DETERM o eresolve_tac ctxt @{thms disjE}))
(*Prove subgoals of form A ==> B1 | ... | A | ... | Bn*)
-val clause_breaker =
- (REPEAT o (resolve0_tac [@{thm "disjI1"}, @{thm "disjI2"}, @{thm "conjI"}]))
- THEN' atac
+fun clause_breaker_tac ctxt =
+ (REPEAT o resolve_tac ctxt @{thms disjI1 disjI2 conjI}) THEN'
+ assume_tac ctxt
(*
Refines a subgoal have the form:
@@ -636,9 +634,9 @@
where {A'1 .. A'm} is disjoint from {B1, ..., Aj, ..., Bi, ..., Ak, ...}
(and solves the subgoal completely if the first set is empty)
*)
-val batter =
- break_hypotheses
- THEN' K (ALLGOALS (TRY o clause_breaker))
+fun batter_tac ctxt i =
+ break_hypotheses_tac ctxt i THEN
+ ALLGOALS (TRY o clause_breaker_tac ctxt)
(*Same idiom as ex_expander_tac*)
fun dist_all_and_tac ctxt i =
@@ -669,11 +667,8 @@
D
This function returns "SOME X" if C = "! X. C'".
If C has no quantification prefix, then returns NONE.*)
-fun head_quantified_variable i = fn st =>
+fun head_quantified_variable ctxt i = fn st =>
let
- val thy = Thm.theory_of_thm st
- val ctxt = Proof_Context.init_global thy
-
val gls =
prop_of st
|> Logic.strip_horn
@@ -779,10 +774,8 @@
(** Tracing **)
(*If "tac i st" succeeds then msg is printed to "trace" channel*)
-fun trace_tac' msg tac i st =
+fun trace_tac' ctxt msg tac i st =
let
- val thy = Thm.theory_of_thm st
- val ctxt = Proof_Context.init_global thy
val result = tac i st
in
if Config.get ctxt tptp_trace_reconstruction andalso
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Feb 13 23:39:25 2015 +0100
@@ -223,7 +223,7 @@
fun instantiates param =
eres_inst_tac ctxt [(("x", 0), param)] thm
- val quantified_var = head_quantified_variable i st
+ val quantified_var = head_quantified_variable ctxt i st
in
if is_none quantified_var then no_tac st
else
@@ -1149,7 +1149,7 @@
fun closure tac =
(*batter fails if there's no toplevel disjunction in the
hypothesis, so we also try atac*)
- SOLVE o (tac THEN' (batter ORELSE' atac))
+ SOLVE o (tac THEN' (batter_tac ctxt ORELSE' assume_tac ctxt))
val search_tac =
ASAP
(rtac @{thm disjI1} APPEND' rtac @{thm disjI2})
@@ -1592,40 +1592,40 @@
fun feat_to_tac feat =
case feat of
- Close_Branch => trace_tac' "mark: closer" efq_tac
- | ConjI => trace_tac' "mark: conjI" (rtac @{thm conjI})
- | King_Cong => trace_tac' "mark: expander_animal" (expander_animal ctxt)
- | Break_Hypotheses => trace_tac' "mark: break_hypotheses" break_hypotheses
+ Close_Branch => trace_tac' ctxt "mark: closer" efq_tac
+ | ConjI => trace_tac' ctxt "mark: conjI" (rtac @{thm conjI})
+ | King_Cong => trace_tac' ctxt "mark: expander_animal" (expander_animal ctxt)
+ | Break_Hypotheses => trace_tac' ctxt "mark: break_hypotheses" (break_hypotheses_tac ctxt)
| RemoveRedundantQuantifications => K all_tac
(*
FIXME Building this into the loop instead.. maybe not the ideal choice
| RemoveRedundantQuantifications =>
- trace_tac' "mark: strip_unused_variable_hyp"
+ trace_tac' ctxt "mark: strip_unused_variable_hyp"
(REPEAT_DETERM o remove_redundant_quantification_in_lit)
*)
| Assumption => atac
(*FIXME both Existential_Free and Existential_Var run same code*)
- | Existential_Free => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
- | Existential_Var => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
- | Universal => trace_tac' "mark: forall_pos" (forall_tac ctxt feats)
- | Not_pos => trace_tac' "mark: not_pos" (dtac @{thm leo2_rules(9)})
- | Not_neg => trace_tac' "mark: not_neg" (dtac @{thm leo2_rules(10)})
- | Or_pos => trace_tac' "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
- | Or_neg => trace_tac' "mark: or_neg" (dtac @{thm leo2_rules(7)})
- | Equal_pos => trace_tac' "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
- | Equal_neg => trace_tac' "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
- | Donkey_Cong => trace_tac' "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
+ | Existential_Free => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
+ | Existential_Var => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
+ | Universal => trace_tac' ctxt "mark: forall_pos" (forall_tac ctxt feats)
+ | Not_pos => trace_tac' ctxt "mark: not_pos" (dtac @{thm leo2_rules(9)})
+ | Not_neg => trace_tac' ctxt "mark: not_neg" (dtac @{thm leo2_rules(10)})
+ | Or_pos => trace_tac' ctxt "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
+ | Or_neg => trace_tac' ctxt "mark: or_neg" (dtac @{thm leo2_rules(7)})
+ | Equal_pos => trace_tac' ctxt "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
+ | Equal_neg => trace_tac' ctxt "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
+ | Donkey_Cong => trace_tac' ctxt "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
- | Extuni_Bool2 => trace_tac' "mark: extuni_bool2" (dtac @{thm extuni_bool2})
- | Extuni_Bool1 => trace_tac' "mark: extuni_bool1" (dtac @{thm extuni_bool1})
- | Extuni_Bind => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
- | Extuni_Triv => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
- | Extuni_Dec => trace_tac' "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
- | Extuni_FlexRigid => trace_tac' "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
- | Extuni_Func => trace_tac' "mark: extuni_func" (dtac @{thm extuni_func})
- | Polarity_switch => trace_tac' "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
- | Forall_special_pos => trace_tac' "mark: dorall_special_pos" extcnf_forall_special_pos_tac
+ | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dtac @{thm extuni_bool2})
+ | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dtac @{thm extuni_bool1})
+ | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
+ | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
+ | Extuni_Dec => trace_tac' ctxt "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
+ | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
+ | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dtac @{thm extuni_func})
+ | Polarity_switch => trace_tac' ctxt "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
+ | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" extcnf_forall_special_pos_tac
val core_tac =
get_loop_feats feats
@@ -1874,7 +1874,7 @@
THEN (if have_loop_feats then
REPEAT (CHANGED
- ((ALLGOALS (TRY o clause_breaker)) (*brush away literals which don't change*)
+ ((ALLGOALS (TRY o clause_breaker_tac ctxt)) (*brush away literals which don't change*)
THEN
(*FIXME move this to a different level?*)
(if loop_can_feature [Polarity_switch] feats then
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Feb 13 23:39:25 2015 +0100
@@ -141,11 +141,6 @@
(intros'', (local_defs, thy'))
end
-(* TODO: same function occurs in inductive package *)
-fun select_disj 1 1 = []
- | select_disj _ 1 = [rtac @{thm disjI1}]
- | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1))
-
fun introrulify thy ths =
let
val ctxt = Proof_Context.init_global thy
@@ -168,7 +163,7 @@
fun prove_introrule (index, (ps, introrule)) =
let
val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
- THEN EVERY1 (select_disj (length disjuncts) (index + 1))
+ THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
THEN (EVERY (map (fn y =>
rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
--- a/src/HOL/Tools/Transfer/transfer.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/Transfer/transfer.ML Fri Feb 13 23:39:25 2015 +0100
@@ -611,13 +611,15 @@
|> Thm.instantiate (map tinst binsts, map inst binsts)
end
-fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve0_tac eq_rules)
+fun eq_rules_tac ctxt eq_rules =
+ TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules)
THEN_ALL_NEW rtac @{thm is_equality_eq}
-fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
+fun eq_tac ctxt = eq_rules_tac ctxt (get_relator_eq_raw ctxt)
-fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt))
- THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
+fun transfer_step_tac ctxt =
+ REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt)
+ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt (get_relator_eq_raw ctxt)))
fun transfer_tac equiv ctxt i =
let
@@ -635,7 +637,7 @@
THEN_ALL_NEW
(SOLVED'
(REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
- (DETERM o eq_rules_tac eq_rules))
+ (DETERM o eq_rules_tac ctxt eq_rules))
ORELSE' end_tac)) (i + 1)
handle TERM (_, ts) => raise TERM (err_msg, ts)
in
@@ -661,7 +663,7 @@
((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
THEN_ALL_NEW
(REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
- (DETERM o eq_rules_tac eq_rules))) (i + 1),
+ (DETERM o eq_rules_tac ctxt eq_rules))) (i + 1),
rtac @{thm refl} i]
end)
@@ -689,7 +691,7 @@
(rtac rule
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
- THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
+ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
val tnames = map (fst o dest_TFree o snd) instT
@@ -725,7 +727,7 @@
(rtac rule
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
- THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
+ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
val tnames = map (fst o dest_TFree o snd) instT
--- a/src/HOL/Tools/inductive.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/inductive.ML Fri Feb 13 23:39:25 2015 +0100
@@ -69,6 +69,7 @@
signature INDUCTIVE =
sig
include BASIC_INDUCTIVE
+ val select_disj_tac: Proof.context -> int -> int -> int -> tactic
type add_ind_def =
inductive_flags ->
term list -> (Attrib.binding * term) list -> thm list ->
@@ -168,9 +169,12 @@
| mk_names a 1 = [a]
| mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
-fun select_disj 1 1 = []
- | select_disj _ 1 = [resolve0_tac [disjI1]]
- | select_disj n i = resolve0_tac [disjI2] :: select_disj (n - 1) (i - 1);
+fun select_disj_tac ctxt =
+ let
+ fun tacs 1 1 = []
+ | tacs _ 1 = [resolve_tac ctxt @{thms disjI1}]
+ | tacs n i = resolve_tac ctxt @{thms disjI2} :: tacs (n - 1) (i - 1);
+ in fn n => fn i => EVERY' (tacs n i) end;
@@ -403,7 +407,7 @@
Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
[rewrite_goals_tac ctxt rec_preds_defs,
resolve_tac ctxt [unfold RS iffD2] 1,
- EVERY1 (select_disj (length intr_ts) (i + 1)),
+ select_disj_tac ctxt (length intr_ts) (i + 1) 1,
(*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 ctxt rules 1 APPEND assume_tac ctxt 1)])
@@ -495,7 +499,7 @@
else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
- EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
+ select_disj_tac ctxt'' (length c_intrs) (i + 1) 1 THEN
EVERY (replicate (length params) (resolve_tac ctxt'' @{thms exI} 1)) THEN
(if null prems then resolve_tac ctxt'' @{thms TrueI} 1
else
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/numeral_simprocs.ML Fri Feb 13 23:39:25 2015 +0100
@@ -18,7 +18,7 @@
sig
val prep_simproc: theory -> string * string list * (Proof.context -> term -> thm option)
-> simproc
- val trans_tac: thm option -> tactic
+ val trans_tac: Proof.context -> thm option -> tactic
val assoc_fold: Proof.context -> cterm -> thm option
val combine_numerals: Proof.context -> cterm -> thm option
val eq_cancel_numerals: Proof.context -> cterm -> thm option
@@ -48,8 +48,8 @@
fun prep_simproc thy (name, pats, proc) =
Simplifier.simproc_global thy name pats proc;
-fun trans_tac NONE = all_tac
- | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
+fun trans_tac _ NONE = all_tac
+ | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]);
val mk_number = Arith_Data.mk_number;
val mk_sum = Arith_Data.mk_sum;
--- a/src/Provers/Arith/cancel_numeral_factor.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Fri Feb 13 23:39:25 2015 +0100
@@ -29,7 +29,7 @@
as with < and <= but not = and div*)
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
- val trans_tac: thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: Proof.context -> tactic (*proves the initial lemma*)
val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*)
val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
@@ -72,7 +72,7 @@
in
Option.map (export o Data.simplify_meta_eq ctxt)
(Data.prove_conv
- [Data.trans_tac reshape, rtac Data.cancel 1,
+ [Data.trans_tac ctxt reshape, rtac Data.cancel 1,
Data.numeral_simp_tac ctxt] ctxt prems (t', rhs))
end
(* FIXME avoid handling of generic exceptions *)
--- a/src/Provers/Arith/cancel_numerals.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/Provers/Arith/cancel_numerals.ML Fri Feb 13 23:39:25 2015 +0100
@@ -36,7 +36,7 @@
val bal_add2: thm
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
- val trans_tac: thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: Proof.context -> tactic (*proves the initial lemma*)
val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*)
val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
@@ -92,12 +92,12 @@
Option.map (export o Data.simplify_meta_eq ctxt)
(if n2 <= n1 then
Data.prove_conv
- [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add1] 1,
+ [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add1] 1,
Data.numeral_simp_tac ctxt] ctxt prems
(t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
else
Data.prove_conv
- [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add2] 1,
+ [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add2] 1,
Data.numeral_simp_tac ctxt] ctxt prems
(t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
end
--- a/src/Provers/Arith/combine_numerals.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/Provers/Arith/combine_numerals.ML Fri Feb 13 23:39:25 2015 +0100
@@ -29,7 +29,7 @@
val left_distrib: thm
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> term * term -> thm option
- val trans_tac: thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: Proof.context -> tactic (*proves the initial lemma*)
val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*)
val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
@@ -83,7 +83,7 @@
in
Option.map (export o Data.simplify_meta_eq ctxt)
(Data.prove_conv
- [Data.trans_tac reshape, resolve_tac ctxt [Data.left_distrib] 1,
+ [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.left_distrib] 1,
Data.numeral_simp_tac ctxt] ctxt
(t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
--- a/src/ZF/arith_data.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/ZF/arith_data.ML Fri Feb 13 23:39:25 2015 +0100
@@ -9,7 +9,7 @@
(*the main outcome*)
val nat_cancel: simproc list
(*tools for use in similar applications*)
- val gen_trans_tac: thm -> thm option -> tactic
+ val gen_trans_tac: Proof.context -> thm -> thm option -> tactic
val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
(*debugging*)
@@ -50,8 +50,8 @@
| dest_sum tm = [tm];
(*Apply the given rewrite (if present) just once*)
-fun gen_trans_tac th2 NONE = all_tac
- | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve0_tac [th RS th2]);
+fun gen_trans_tac _ _ NONE = all_tac
+ | gen_trans_tac ctxt th2 (SOME th) = ALLGOALS (resolve_tac ctxt [th RS th2]);
(*Use <-> or = depending on the type of t*)
fun mk_eq_iff(t,u) =
@@ -169,7 +169,7 @@
val dest_bal = FOLogic.dest_eq
val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
- val trans_tac = gen_trans_tac @{thm iff_trans}
+ fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
end;
structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -182,7 +182,7 @@
val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
- val trans_tac = gen_trans_tac @{thm iff_trans}
+ fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
end;
structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -195,7 +195,7 @@
val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
- val trans_tac = gen_trans_tac @{thm trans}
+ fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
end;
structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
--- a/src/ZF/int_arith.ML Thu Feb 12 12:46:50 2015 +0000
+++ b/src/ZF/int_arith.ML Fri Feb 13 23:39:25 2015 +0100
@@ -151,12 +151,12 @@
structure CancelNumeralsCommon =
struct
- val mk_sum = (fn _ : typ => mk_sum)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val find_first_coeff = find_first_coeff []
- val trans_tac = ArithData.gen_trans_tac @{thm iff_trans}
+ val mk_sum = (fn _ : typ => mk_sum)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val find_first_coeff = find_first_coeff []
+ fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm iff_trans}
val norm_ss1 =
simpset_of (put_simpset ZF_ss @{context}
@@ -233,16 +233,16 @@
structure CombineNumeralsData =
struct
- type coeff = int
- val iszero = (fn x => x = 0)
- val add = op +
- val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans}
- val prove_conv = prove_conv_nohyps "int_combine_numerals"
- val trans_tac = ArithData.gen_trans_tac @{thm trans}
+ type coeff = int
+ val iszero = (fn x => x = 0)
+ val add = op +
+ val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans}
+ val prove_conv = prove_conv_nohyps "int_combine_numerals"
+ fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
val norm_ss1 =
simpset_of (put_simpset ZF_ss @{context}
@@ -281,34 +281,33 @@
structure CombineNumeralsProdData =
struct
- type coeff = int
- val iszero = (fn x => x = 0)
- val add = op *
- val mk_sum = (fn _ : typ => mk_prod)
- val dest_sum = dest_prod
- fun mk_coeff(k,t) = if t=one then mk_numeral k
- else raise TERM("mk_coeff", [])
+ type coeff = int
+ val iszero = (fn x => x = 0)
+ val add = op *
+ val mk_sum = (fn _ : typ => mk_prod)
+ val dest_sum = dest_prod
+ fun mk_coeff(k,t) =
+ if t = one then mk_numeral k
+ else raise TERM("mk_coeff", [])
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*)
- val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
- val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
- val trans_tac = ArithData.gen_trans_tac @{thm trans}
-
-
+ val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
+ val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
+ fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
-val norm_ss1 =
- simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps)
-val norm_ss2 =
- simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
- bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
-fun norm_tac ctxt =
- ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
- THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
+ val norm_ss1 =
+ simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps)
+ val norm_ss2 =
+ simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
+ bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
+ fun norm_tac ctxt =
+ ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
+ THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
-val numeral_simp_ss =
- simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys)
-fun numeral_simp_tac ctxt =
- ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
-val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s);
+ val numeral_simp_ss =
+ simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys)
+ fun numeral_simp_tac ctxt =
+ ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
+ val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s);
end;