--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed Feb 11 11:42:39 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed Feb 11 18:16:33 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 Wed Feb 11 11:42:39 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Feb 11 18:16:33 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