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;
```