src/Provers/splitter.ML
changeset 58838 59203adfc33f
parent 58826 2ed2eaabe3df
child 58956 a816aa3ff391
     1.1 --- a/src/Provers/splitter.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Provers/splitter.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4  val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
     1.5    [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
     1.6    (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
     1.7 -  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
     1.8 +  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN resolve_tac [reflexive_thm] 1)
     1.9  
    1.10  val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
    1.11  
    1.12 @@ -365,11 +365,11 @@
    1.13                     (case apsns of
    1.14                        [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
    1.15                      | p::_ => EVERY [lift_tac Ts t p,
    1.16 -                                     rtac reflexive_thm (i+1),
    1.17 +                                     resolve_tac [reflexive_thm] (i+1),
    1.18                                       lift_split_tac] state)
    1.19              end
    1.20    in COND (has_fewer_prems i) no_tac
    1.21 -          (rtac meta_iffD i THEN lift_split_tac)
    1.22 +          (resolve_tac [meta_iffD] i THEN lift_split_tac)
    1.23    end;
    1.24  
    1.25  in (split_tac, exported_split_posns) end;  (* mk_case_split_tac *)
    1.26 @@ -400,16 +400,16 @@
    1.27        (* does not work properly if the split variable is bound by a quantifier *)
    1.28                fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
    1.29                             (if first_prem_is_disj t
    1.30 -                            then EVERY[etac Data.disjE i,rotate_tac ~1 i,
    1.31 +                            then EVERY[eresolve_tac [Data.disjE] i, rotate_tac ~1 i,
    1.32                                         rotate_tac ~1  (i+1),
    1.33                                         flat_prems_tac (i+1)]
    1.34                              else all_tac)
    1.35                             THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
    1.36                             THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
    1.37            in if n<0 then  no_tac  else (DETERM (EVERY'
    1.38 -                [rotate_tac n, etac Data.contrapos2,
    1.39 +                [rotate_tac n, eresolve_tac [Data.contrapos2],
    1.40                   split_tac splits,
    1.41 -                 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
    1.42 +                 rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1,
    1.43                   flat_prems_tac] i))
    1.44            end;
    1.45    in SUBGOAL tac