src/Provers/quantifier1.ML
changeset 58838 59203adfc33f
parent 54998 8601434fa334
child 59498 50b60f501b05
     1.1 --- a/src/Provers/quantifier1.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Provers/quantifier1.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -126,10 +126,10 @@
     1.4        yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
     1.5      val thm =
     1.6        Goal.prove ctxt' [] [] goal
     1.7 -        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
     1.8 +        (fn {context = ctxt'', ...} => resolve_tac [Data.iff_reflection] 1 THEN tac ctxt'');
     1.9    in singleton (Variable.export ctxt' ctxt) thm end;
    1.10  
    1.11 -fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
    1.12 +fun qcomm_tac qcomm qI i = REPEAT_DETERM (resolve_tac [qcomm] i THEN resolve_tac [qI] i);
    1.13  
    1.14  (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
    1.15     Better: instantiate exI
    1.16 @@ -138,9 +138,10 @@
    1.17    val excomm = Data.ex_comm RS Data.iff_trans;
    1.18  in
    1.19    val prove_one_point_ex_tac =
    1.20 -    qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
    1.21 +    qcomm_tac excomm Data.iff_exI 1 THEN resolve_tac [Data.iffI] 1 THEN
    1.22      ALLGOALS
    1.23 -      (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI,
    1.24 +      (EVERY' [eresolve_tac [Data.exE], REPEAT_DETERM o eresolve_tac [Data.conjE],
    1.25 +        resolve_tac [Data.exI],
    1.26          DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
    1.27  end;
    1.28  
    1.29 @@ -150,12 +151,17 @@
    1.30  local
    1.31    val tac =
    1.32      SELECT_GOAL
    1.33 -      (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp,
    1.34 -        REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]);
    1.35 +      (EVERY1 [REPEAT o dresolve_tac [Data.uncurry],
    1.36 +        REPEAT o resolve_tac [Data.impI],
    1.37 +        eresolve_tac [Data.mp],
    1.38 +        REPEAT o eresolve_tac [Data.conjE],
    1.39 +        REPEAT o ares_tac [Data.conjI]]);
    1.40    val allcomm = Data.all_comm RS Data.iff_trans;
    1.41  in
    1.42    val prove_one_point_all_tac =
    1.43 -    EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac];
    1.44 +    EVERY1 [qcomm_tac allcomm Data.iff_allI,
    1.45 +      resolve_tac [Data.iff_allI],
    1.46 +      resolve_tac [Data.iffI], tac, tac];
    1.47  end
    1.48  
    1.49  fun renumber l u (Bound i) =