src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 59533 e9ffe89a20a4
parent 59498 50b60f501b05
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Feb 11 11:42:39 2015 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Feb 11 18:16:33 2015 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4          fun instantiates param =
     1.5             eres_inst_tac ctxt [(("x", 0), param)] thm
     1.6  
     1.7 -        val quantified_var = head_quantified_variable i st
     1.8 +        val quantified_var = head_quantified_variable ctxt i st
     1.9        in
    1.10          if is_none quantified_var then no_tac st
    1.11          else
    1.12 @@ -1149,7 +1149,7 @@
    1.13      fun closure tac =
    1.14       (*batter fails if there's no toplevel disjunction in the
    1.15         hypothesis, so we also try atac*)
    1.16 -      SOLVE o (tac THEN' (batter ORELSE' atac))
    1.17 +      SOLVE o (tac THEN' (batter_tac ctxt ORELSE' assume_tac ctxt))
    1.18      val search_tac =
    1.19        ASAP
    1.20          (rtac @{thm disjI1} APPEND' rtac @{thm disjI2})
    1.21 @@ -1592,40 +1592,40 @@
    1.22  
    1.23          fun feat_to_tac feat =
    1.24            case feat of
    1.25 -              Close_Branch => trace_tac' "mark: closer" efq_tac
    1.26 -            | ConjI => trace_tac' "mark: conjI" (rtac @{thm conjI})
    1.27 -            | King_Cong => trace_tac' "mark: expander_animal" (expander_animal ctxt)
    1.28 -            | Break_Hypotheses => trace_tac' "mark: break_hypotheses" break_hypotheses
    1.29 +              Close_Branch => trace_tac' ctxt "mark: closer" efq_tac
    1.30 +            | ConjI => trace_tac' ctxt "mark: conjI" (rtac @{thm conjI})
    1.31 +            | King_Cong => trace_tac' ctxt "mark: expander_animal" (expander_animal ctxt)
    1.32 +            | Break_Hypotheses => trace_tac' ctxt "mark: break_hypotheses" (break_hypotheses_tac ctxt)
    1.33              | RemoveRedundantQuantifications => K all_tac
    1.34  (*
    1.35  FIXME Building this into the loop instead.. maybe not the ideal choice
    1.36              | RemoveRedundantQuantifications =>
    1.37 -                trace_tac' "mark: strip_unused_variable_hyp"
    1.38 +                trace_tac' ctxt "mark: strip_unused_variable_hyp"
    1.39                   (REPEAT_DETERM o remove_redundant_quantification_in_lit)
    1.40  *)
    1.41  
    1.42              | Assumption => atac
    1.43  (*FIXME both Existential_Free and Existential_Var run same code*)
    1.44 -            | Existential_Free => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
    1.45 -            | Existential_Var => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
    1.46 -            | Universal => trace_tac' "mark: forall_pos" (forall_tac ctxt feats)
    1.47 -            | Not_pos => trace_tac' "mark: not_pos" (dtac @{thm leo2_rules(9)})
    1.48 -            | Not_neg => trace_tac' "mark: not_neg" (dtac @{thm leo2_rules(10)})
    1.49 -            | Or_pos => trace_tac' "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
    1.50 -            | Or_neg => trace_tac' "mark: or_neg" (dtac @{thm leo2_rules(7)})
    1.51 -            | Equal_pos => trace_tac' "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
    1.52 -            | Equal_neg => trace_tac' "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
    1.53 -            | Donkey_Cong => trace_tac' "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
    1.54 +            | Existential_Free => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
    1.55 +            | Existential_Var => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
    1.56 +            | Universal => trace_tac' ctxt "mark: forall_pos" (forall_tac ctxt feats)
    1.57 +            | Not_pos => trace_tac' ctxt "mark: not_pos" (dtac @{thm leo2_rules(9)})
    1.58 +            | Not_neg => trace_tac' ctxt "mark: not_neg" (dtac @{thm leo2_rules(10)})
    1.59 +            | Or_pos => trace_tac' ctxt "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
    1.60 +            | Or_neg => trace_tac' ctxt "mark: or_neg" (dtac @{thm leo2_rules(7)})
    1.61 +            | Equal_pos => trace_tac' ctxt "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
    1.62 +            | Equal_neg => trace_tac' ctxt "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
    1.63 +            | Donkey_Cong => trace_tac' ctxt "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
    1.64  
    1.65 -            | Extuni_Bool2 => trace_tac' "mark: extuni_bool2" (dtac @{thm extuni_bool2})
    1.66 -            | Extuni_Bool1 => trace_tac' "mark: extuni_bool1" (dtac @{thm extuni_bool1})
    1.67 -            | Extuni_Bind => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
    1.68 -            | Extuni_Triv => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
    1.69 -            | Extuni_Dec => trace_tac' "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
    1.70 -            | Extuni_FlexRigid => trace_tac' "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
    1.71 -            | Extuni_Func => trace_tac' "mark: extuni_func" (dtac @{thm extuni_func})
    1.72 -            | Polarity_switch => trace_tac' "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
    1.73 -            | Forall_special_pos => trace_tac' "mark: dorall_special_pos" extcnf_forall_special_pos_tac
    1.74 +            | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dtac @{thm extuni_bool2})
    1.75 +            | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dtac @{thm extuni_bool1})
    1.76 +            | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
    1.77 +            | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
    1.78 +            | Extuni_Dec => trace_tac' ctxt "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
    1.79 +            | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
    1.80 +            | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dtac @{thm extuni_func})
    1.81 +            | Polarity_switch => trace_tac' ctxt "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
    1.82 +            | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" extcnf_forall_special_pos_tac
    1.83  
    1.84          val core_tac =
    1.85            get_loop_feats feats
    1.86 @@ -1874,7 +1874,7 @@
    1.87  
    1.88        THEN (if have_loop_feats then
    1.89                REPEAT (CHANGED
    1.90 -              ((ALLGOALS (TRY o clause_breaker)) (*brush away literals which don't change*)
    1.91 +              ((ALLGOALS (TRY o clause_breaker_tac ctxt)) (*brush away literals which don't change*)
    1.92                 THEN
    1.93                  (*FIXME move this to a different level?*)
    1.94                  (if loop_can_feature [Polarity_switch] feats then