src/Provers/hypsubst.ML
author wenzelm
Mon Mar 25 16:45:08 2019 +0100 (3 months ago)
changeset 69980 f2e3adfd916f
parent 69593 3dda49e08b9d
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Provers/hypsubst.ML
     2     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     3     Copyright   1995  University of Cambridge
     4 
     5 Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst".
     6 
     7 Tactic to substitute using (at least) the assumption x=t in the rest
     8 of the subgoal, and to delete (at least) that assumption.  Original
     9 version due to Martin Coen.
    10 
    11 This version uses the simplifier, and requires it to be already present.
    12 
    13 Test data:
    14 
    15 Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
    16 Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
    17 Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
    18 Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
    19 
    20 Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)";
    21 
    22 by (bound_hyp_subst_tac 1);
    23 by (hyp_subst_tac 1);
    24 
    25 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
    26 Goal "P(a) --> (EX y. a=y --> P(f(a)))";
    27 
    28 Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
    29 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    30 by (blast_hyp_subst_tac true 1);
    31 *)
    32 
    33 signature HYPSUBST_DATA =
    34 sig
    35   val dest_Trueprop    : term -> term
    36   val dest_eq          : term -> term * term
    37   val dest_imp         : term -> term * term
    38   val eq_reflection    : thm               (* a=b ==> a==b *)
    39   val rev_eq_reflection: thm               (* a==b ==> a=b *)
    40   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    41   val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
    42   val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
    43   val sym              : thm               (* a=b ==> b=a *)
    44   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    45 end;
    46 
    47 signature HYPSUBST =
    48 sig
    49   val bound_hyp_subst_tac    : Proof.context -> int -> tactic
    50   val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
    51   val hyp_subst_thin         : bool Config.T
    52   val hyp_subst_tac          : Proof.context -> int -> tactic
    53   val blast_hyp_subst_tac    : Proof.context -> bool -> int -> tactic
    54   val stac                   : Proof.context -> thm -> int -> tactic
    55 end;
    56 
    57 functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    58 struct
    59 
    60 exception EQ_VAR;
    61 
    62 (*Simplifier turns Bound variables to special Free variables:
    63   change it back (any Bound variable will do)*)
    64 fun inspect_contract t =
    65   (case Envir.eta_contract t of
    66     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
    67   | t' => t');
    68 
    69 val has_vars = Term.exists_subterm Term.is_Var;
    70 val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
    71 
    72 (*If novars then we forbid Vars in the equality.
    73   If bnd then we only look for Bound variables to eliminate.
    74   When can we safely delete the equality?
    75     Not if it equates two constants; consider 0=1.
    76     Not if it resembles x=t[x], since substitution does not eliminate x.
    77     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    78     Not if it involves a variable free in the premises,
    79         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    80   Prefer to eliminate Bound variables if possible.
    81   Result:  true = use as is,  false = reorient first
    82     also returns var to substitute, relevant if it is Free *)
    83 fun inspect_pair bnd novars (t, u) =
    84   if novars andalso (has_tvars t orelse has_tvars u)
    85   then raise Match   (*variables in the type!*)
    86   else
    87     (case apply2 inspect_contract (t, u) of
    88       (Bound i, _) =>
    89         if loose_bvar1 (u, i) orelse novars andalso has_vars u
    90         then raise Match
    91         else (true, Bound i)                (*eliminates t*)
    92     | (_, Bound i) =>
    93         if loose_bvar1 (t, i) orelse novars andalso has_vars t
    94         then raise Match
    95         else (false, Bound i)               (*eliminates u*)
    96     | (t' as Free _, _) =>
    97         if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
    98         then raise Match
    99         else (true, t')                (*eliminates t*)
   100     | (_, u' as Free _) =>
   101         if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
   102         then raise Match
   103         else (false, u')               (*eliminates u*)
   104     | _ => raise Match);
   105 
   106 (*Locates a substitutable variable on the left (resp. right) of an equality
   107    assumption.  Returns the number of intervening assumptions. *)
   108 fun eq_var bnd novars check_frees t =
   109   let
   110     fun check_free ts (orient, Free f)
   111       = if not check_frees orelse not orient
   112             orelse exists (curry Logic.occs (Free f)) ts
   113         then (orient, true) else raise Match
   114       | check_free ts (orient, _) = (orient, false)
   115     fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
   116       | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) hs =
   117               ((k, check_free (B :: hs) (inspect_pair bnd novars
   118                     (Data.dest_eq (Data.dest_Trueprop A))))
   119                handle TERM _ => eq_var_aux (k+1) B (A :: hs)
   120                  | Match => eq_var_aux (k+1) B (A :: hs))
   121       | eq_var_aux k _ _ = raise EQ_VAR
   122 
   123   in  eq_var_aux 0 t [] end;
   124 
   125 fun thin_free_eq_tac ctxt = SUBGOAL (fn (t, i) =>
   126   let
   127     val (k, _) = eq_var false false false t
   128     val ok = (eq_var false false true t |> fst) > k handle EQ_VAR => true
   129   in
   130     if ok then EVERY [rotate_tac k i, eresolve_tac ctxt [thin_rl] i, rotate_tac (~k) i]
   131     else no_tac
   132   end handle EQ_VAR => no_tac)
   133 
   134 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   135   No vars are allowed here, as simpsets are built from meta-assumptions*)
   136 fun mk_eqs bnd th =
   137     [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst
   138       then th RS Data.eq_reflection
   139       else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
   140     handle TERM _ => [] | Match => [];
   141 
   142 fun bool2s true = "true" | bool2s false = "false"
   143 
   144 local
   145 in
   146 
   147   (*Select a suitable equality assumption; substitute throughout the subgoal
   148     If bnd is true, then it replaces Bound variables only. *)
   149   fun gen_hyp_subst_tac ctxt bnd =
   150     SUBGOAL (fn (Bi, i) =>
   151       let
   152         val (k, (orient, is_free)) = eq_var bnd true true Bi
   153         val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
   154       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
   155         if not is_free then eresolve_tac ctxt [thin_rl] i
   156           else if orient then eresolve_tac ctxt [Data.rev_mp] i
   157           else eresolve_tac ctxt [Data.sym RS Data.rev_mp] i,
   158         rotate_tac (~k) i,
   159         if is_free then resolve_tac ctxt [Data.imp_intr] i else all_tac]
   160       end handle THM _ => no_tac | EQ_VAR => no_tac)
   161 
   162 end;
   163 
   164 val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
   165 
   166 fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) =>
   167   case try (Logic.strip_assums_hyp #> hd #>
   168       Data.dest_Trueprop #> Data.dest_eq #> apply2 Envir.eta_contract) (Thm.term_of cBi) of
   169     SOME (t, t') =>
   170       let
   171         val Bi = Thm.term_of cBi;
   172         val ps = Logic.strip_params Bi;
   173         val U = Term.fastype_of1 (rev (map snd ps), t);
   174         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
   175         val rl' = Thm.lift_rule cBi rl;
   176         val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
   177           (Logic.strip_assums_concl (Thm.prop_of rl')));
   178         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
   179           (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
   180         val (Ts, V) = split_last (Term.binder_types T);
   181         val u =
   182           fold_rev Term.abs (ps @ [("x", U)])
   183             (case (if b then t else t') of
   184               Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   185             | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   186         val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
   187       in
   188         compose_tac ctxt (true, Drule.instantiate_normalize (instT,
   189           map (apsnd (Thm.cterm_of ctxt))
   190             [((ixn, Ts ---> U --> body_type T), u),
   191              ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   192              ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
   193           Thm.nprems_of rl) i
   194       end
   195   | NONE => no_tac);
   196 
   197 fun imp_intr_tac ctxt = resolve_tac ctxt [Data.imp_intr];
   198 
   199 fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
   200 fun dup_subst ctxt = rev_dup_elim ctxt ssubst
   201 
   202 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
   203 (* premises containing meta-implications or quantifiers                *)
   204 
   205 (*Old version of the tactic above -- slower but the only way
   206   to handle equalities containing Vars.*)
   207 fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) =>
   208       let val n = length(Logic.strip_assums_hyp Bi) - 1
   209           val (k, (orient, is_free)) = eq_var bnd false true Bi
   210           val rl = if is_free then dup_subst ctxt else ssubst
   211           val rl = if orient then rl else Data.sym RS rl
   212       in
   213          DETERM
   214            (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i),
   215                    rotate_tac 1 i,
   216                    REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i),
   217                    inst_subst_tac ctxt orient rl i,
   218                    REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i)])
   219       end
   220       handle THM _ => no_tac | EQ_VAR => no_tac);
   221 
   222 (*Substitutes for Free or Bound variables,
   223   discarding equalities on Bound variables
   224   and on Free variables if thin=true*)
   225 fun hyp_subst_tac_thin thin ctxt =
   226   REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl],
   227     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
   228     if thin then thin_free_eq_tac ctxt else K no_tac];
   229 
   230 val hyp_subst_thin = Attrib.setup_config_bool \<^binding>\<open>hypsubst_thin\<close> (K false);
   231 
   232 fun hyp_subst_tac ctxt =
   233   hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
   234 
   235 (*Substitutes for Bound variables only -- this is always safe*)
   236 fun bound_hyp_subst_tac ctxt =
   237   REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
   238     ORELSE' vars_gen_hyp_subst_tac ctxt true);
   239 
   240 (** Version for Blast_tac.  Hyps that are affected by the substitution are
   241     moved to the front.  Defect: even trivial changes are noticed, such as
   242     substitutions in the arguments of a function Var. **)
   243 
   244 (*final re-reversal of the changed assumptions*)
   245 fun reverse_n_tac _ 0 i = all_tac
   246   | reverse_n_tac _ 1 i = rotate_tac ~1 i
   247   | reverse_n_tac ctxt n i =
   248       REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac ctxt [Data.rev_mp] i) THEN
   249       REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i);
   250 
   251 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   252 fun all_imp_intr_tac ctxt hyps i =
   253   let
   254     fun imptac (r, []) st = reverse_n_tac ctxt r i st
   255       | imptac (r, hyp::hyps) st =
   256           let
   257             val (hyp', _) =
   258               Thm.term_of (Thm.cprem_of st i)
   259               |> Logic.strip_assums_concl
   260               |> Data.dest_Trueprop |> Data.dest_imp;
   261             val (r', tac) =
   262               if Envir.aeconv (hyp, hyp')
   263               then (r, imp_intr_tac ctxt i THEN rotate_tac ~1 i)
   264               else (*leave affected hyps at end*) (r + 1, imp_intr_tac ctxt i);
   265           in
   266             (case Seq.pull (tac st) of
   267               NONE => Seq.single st
   268             | SOME (st', _) => imptac (r', hyps) st')
   269           end
   270   in imptac (0, rev hyps) end;
   271 
   272 
   273 fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi, i) =>
   274   let
   275     val (k, (symopt, _)) = eq_var false false false Bi
   276     val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   277     (*omit selected equality, returning other hyps*)
   278     val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   279     val n = length hyps
   280   in
   281     if trace then tracing "Substituting an equality" else ();
   282     DETERM
   283       (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i),
   284               rotate_tac 1 i,
   285               REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i),
   286               inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i,
   287               all_imp_intr_tac ctxt hyps i])
   288   end
   289   handle THM _ => no_tac | EQ_VAR => no_tac);
   290 
   291 (*apply an equality or definition ONCE;
   292   fails unless the substitution has an effect*)
   293 fun stac ctxt th =
   294   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   295   in CHANGED_GOAL (resolve_tac ctxt [th' RS ssubst]) end;
   296 
   297 
   298 (* method setup *)
   299 
   300 val _ =
   301   Theory.setup
   302    (Method.setup \<^binding>\<open>hypsubst\<close>
   303       (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   304       "substitution using an assumption (improper)" #>
   305     Method.setup \<^binding>\<open>hypsubst_thin\<close>
   306       (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   307           (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   308       "substitution using an assumption, eliminating assumptions" #>
   309     Method.setup \<^binding>\<open>simplesubst\<close>
   310       (Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (stac ctxt th)))
   311       "simple substitution");
   312 
   313 end;