src/Provers/hypsubst.ML
author paulson
Tue, 01 Feb 2005 18:01:57 +0100
changeset 15481 fc075ae929e4
parent 15415 6e437e276ef5
child 15531 08c8dad8e399
permissions -rw-r--r--
the new subst tactic, by Lucas Dixon
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
     1
(*  Title:      Provers/hypsubst.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
     3
    Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     4
    Copyright   1995  University of Cambridge
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     5
9628
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     6
Basic equational reasoning: (hyp_)subst method and symmetric attribute.
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     7
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     8
Tactic to substitute using (at least) the assumption x=t in the rest
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     9
of the subgoal, and to delete (at least) that assumption.  Original
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
    10
version due to Martin Coen.
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    11
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    12
This version uses the simplifier, and requires it to be already present.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    13
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    14
Test data:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    16
Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    17
Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    18
Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    19
Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    20
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
    21
Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)";
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
    22
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
    23
by (bound_hyp_subst_tac 1);
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    24
by (hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    25
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    26
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    27
Goal "P(a) --> (EX y. a=y --> P(f(a)))";
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    28
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    29
Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    30
\                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    31
by (blast_hyp_subst_tac (ref true) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
signature HYPSUBST_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    36
  structure Simplifier : SIMPLIFIER
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    37
  val dest_Trueprop    : term -> term
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    38
  val dest_eq          : term -> term*term*typ
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    39
  val dest_imp         : term -> term*term
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    40
  val eq_reflection    : thm               (* a=b ==> a==b *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    41
  val rev_eq_reflection: thm               (* a==b ==> a=b *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    42
  val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    43
  val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    44
  val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    45
  val sym              : thm               (* a=b ==> b=a *)
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
    46
  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    47
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    49
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
signature HYPSUBST =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    52
  val bound_hyp_subst_tac    : int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    53
  val hyp_subst_tac          : int -> tactic
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    54
  val blast_hyp_subst_tac    : bool ref -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
    (*exported purely for debugging purposes*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    56
  val gen_hyp_subst_tac      : bool -> int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    57
  val vars_gen_hyp_subst_tac : bool -> int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    58
  val eq_var                 : bool -> bool -> term -> int * bool
4179
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    59
  val inspect_pair           : bool -> bool -> term * term * typ -> bool
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
    60
  val mk_eqs                 : bool -> thm -> thm list
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    61
  val stac		     : thm -> int -> tactic
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    62
  val hypsubst_setup         : (theory -> theory) list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    65
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    66
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    67
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
exception EQ_VAR;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
2174
0829b7b632c5 Removed a call to polymorphic mem
paulson
parents: 2143
diff changeset
    72
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    74
local val odot = ord"."
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    75
in
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    76
(*Simplifier turns Bound variables to dotted Free variables:
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    77
  change it back (any Bound variable will do)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    78
*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    79
fun contract t =
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    80
    case Pattern.eta_contract_atom t of
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    81
        Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    82
      | t'        => t'
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    83
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    84
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    85
fun has_vars t = maxidx_of_term t <> ~1;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    86
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    87
(*If novars then we forbid Vars in the equality.
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    88
  If bnd then we only look for Bound (or dotted Free) variables to eliminate.
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    89
  When can we safely delete the equality?
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    90
    Not if it equates two constants; consider 0=1.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    91
    Not if it resembles x=t[x], since substitution does not eliminate x.
4299
22596d62ce0b updated comment
paulson
parents: 4223
diff changeset
    92
    Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    93
    Not if it involves a variable free in the premises,
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    94
        but we can't check for this -- hence bnd and bound_hyp_subst_tac
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    95
  Prefer to eliminate Bound variables if possible.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    96
  Result:  true = use as is,  false = reorient first *)
4179
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    97
fun inspect_pair bnd novars (t,u,T) =
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    98
  if novars andalso maxidx_of_typ T <> ~1
4179
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    99
  then raise Match   (*variables in the type!*)
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
   100
  else
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   101
  case (contract t, contract u) of
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   102
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   103
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   104
                       else true                (*eliminates t*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   105
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   106
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   107
                       else false               (*eliminates u*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   108
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   109
                          novars andalso has_vars u
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   110
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   111
                       else true                (*eliminates t*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   112
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   113
                          novars andalso has_vars t
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   114
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   115
                       else false               (*eliminates u*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
     | _ => raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   118
(*Locates a substitutable variable on the left (resp. right) of an equality
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   119
   assumption.  Returns the number of intervening assumptions. *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   120
fun eq_var bnd novars =
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   121
  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   122
        | eq_var_aux k (Const("==>",_) $ A $ B) =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   123
              ((k, inspect_pair bnd novars
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   124
                    (Data.dest_eq (Data.dest_Trueprop A)))
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   125
                      (*Exception comes from inspect_pair or dest_eq*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   126
               handle _ => eq_var_aux (k+1) B)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   127
        | eq_var_aux k _ = raise EQ_VAR
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   128
  in  eq_var_aux 0  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   130
(*For the simpset.  Adds ALL suitable equalities, even if not first!
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   131
  No vars are allowed here, as simpsets are built from meta-assumptions*)
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   132
fun mk_eqs bnd th =
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   133
    [ if inspect_pair bnd false (Data.dest_eq
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   134
                                   (Data.dest_Trueprop (#prop (rep_thm th))))
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   135
      then th RS Data.eq_reflection
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   136
      else symmetric(th RS Data.eq_reflection) (*reorient*) ]
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   137
    handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   138
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   139
local open Simplifier
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   140
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   141
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   142
  (*Select a suitable equality assumption; substitute throughout the subgoal
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   143
    If bnd is true, then it replaces Bound variables only. *)
13604
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   144
  fun gen_hyp_subst_tac bnd =
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   145
    let val tac = SUBGOAL (fn (Bi, i) =>
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   146
      let val (k, _) = eq_var bnd true Bi
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   147
          val hyp_subst_ss = empty_ss setmksimps (mk_eqs bnd)
13604
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   148
      in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   149
        etac thin_rl i, rotate_tac (~k) i]
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   150
      end handle THM _ => no_tac | EQ_VAR => no_tac)
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   151
    in REPEAT_DETERM1 o tac end;
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   152
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   153
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   154
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   155
val ssubst = standard (Data.sym RS Data.subst);
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   156
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   157
val imp_intr_tac = rtac Data.imp_intr;
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   158
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   159
(*Old version of the tactic above -- slower but the only way
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   160
  to handle equalities containing Vars.*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   161
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   162
      let val n = length(Logic.strip_assums_hyp Bi) - 1
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   163
          val (k,symopt) = eq_var bnd false Bi
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   164
      in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   165
         DETERM
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   166
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   167
                   rotate_tac 1 i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   168
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   169
                   etac (if symopt then ssubst else Data.subst) i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   170
                   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
      end
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   172
      handle THM _ => no_tac | EQ_VAR => no_tac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
(*Substitutes for Free or Bound variables*)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   175
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
   176
        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
(*Substitutes for Bound variables only -- this is always safe*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   179
val bound_hyp_subst_tac =
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   180
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   182
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   183
(** Version for Blast_tac.  Hyps that are affected by the substitution are
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   184
    moved to the front.  Defect: even trivial changes are noticed, such as
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   185
    substitutions in the arguments of a function Var. **)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   186
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   187
(*final re-reversal of the changed assumptions*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   188
fun reverse_n_tac 0 i = all_tac
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   189
  | reverse_n_tac 1 i = rotate_tac ~1 i
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   190
  | reverse_n_tac n i =
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   191
      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   192
      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   193
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   194
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   195
fun all_imp_intr_tac hyps i =
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   196
  let fun imptac (r, [])    st = reverse_n_tac r i st
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   197
        | imptac (r, hyp::hyps) st =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   198
           let val (hyp',_) = List.nth (prems_of st, i-1) |>
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   199
                              Logic.strip_assums_concl    |>
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   200
                              Data.dest_Trueprop          |> Data.dest_imp
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   201
               val (r',tac) = if Pattern.aeconv (hyp,hyp')
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   202
                              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   203
                              else (*leave affected hyps at end*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   204
                                   (r+1, imp_intr_tac i)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   205
           in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   206
               case Seq.pull(tac st) of
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   207
                   None       => Seq.single(st)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   208
                 | Some(st',_) => imptac (r',hyps) st'
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   209
           end handle _ => error "?? in blast_hyp_subst_tac"
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   210
  in  imptac (0, rev hyps)  end;
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   211
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   212
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   213
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   214
      let val (k,symopt) = eq_var false false Bi
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   215
          val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   216
          (*omit selected equality, returning other hyps*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   217
          val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   218
          val n = length hyps
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   219
      in
12262
11ff5f47df6e use tracing function for trace output;
wenzelm
parents: 10821
diff changeset
   220
         if !trace then tracing "Substituting an equality" else ();
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   221
         DETERM
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   222
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   223
                   rotate_tac 1 i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   224
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   225
                   etac (if symopt then ssubst else Data.subst) i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   226
                   all_imp_intr_tac hyps i])
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   227
      end
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   228
      handle THM _ => no_tac | EQ_VAR => no_tac);
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   229
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   230
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   231
(*apply an equality or definition ONCE;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   232
  fails unless the substitution has an effect*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   233
fun stac th =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   234
  let val th' = th RS Data.rev_eq_reflection handle THM _ => th
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   235
  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   236
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   237
9628
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   238
(* proof methods *)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   239
9705
8eecca293907 Method.SIMPLE_METHOD';
wenzelm
parents: 9628
diff changeset
   240
val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
10821
dcb75538f542 CHANGED_PROP;
wenzelm
parents: 9893
diff changeset
   241
val hyp_subst_meth =
dcb75538f542 CHANGED_PROP;
wenzelm
parents: 9893
diff changeset
   242
  Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   243
9628
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   244
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   245
(* theory setup *)
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   246
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   247
val hypsubst_setup =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   248
 [Method.add_methods
9628
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   249
  [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15415
diff changeset
   250
   ("simplesubst", subst_meth, "simple substitution")]];
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   251
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
end;