# HG changeset patch # User wenzelm # Date 1423674993 -3600 # Node ID e9ffe89a20a483877f3a6bfed7b37a7797ca3e01 # Parent 82ab8168d940487d0e0d39a4cf83d511896d3a3b proper context; tuned; diff -r 82ab8168d940 -r e9ffe89a20a4 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- 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 diff -r 82ab8168d940 -r e9ffe89a20a4 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- 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