src/Provers/hypsubst.ML
author wenzelm
Fri, 04 Aug 2000 22:58:23 +0200
changeset 9532 36b9bc6eb454
parent 4466 305390f23734
child 9592 abbd48606a0a
permissions -rw-r--r--
added rev_eq_reflection; export stac; proof method setup: subst, hypsubst;
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
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
     6
Tactic to substitute using (at least) the assumption x=t in the rest of the
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
     7
subgoal, and to delete (at least) that assumption.
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
     8
Original version due to Martin Coen.
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     9
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    10
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
    11
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    12
Test data:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    14
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
    15
Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    16
Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    17
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
    18
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    19
by (hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    20
by (bound_hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    21
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    22
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
    23
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
    24
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    25
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
    26
\                 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
    27
by (blast_hyp_subst_tac (ref true) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
signature HYPSUBST_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    32
  structure Simplifier : SIMPLIFIER
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    33
  val dest_Trueprop    : term -> term
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    34
  val dest_eq          : term -> term*term*typ
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    35
  val dest_imp         : term -> term*term
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    36
  val eq_reflection    : thm               (* a=b ==> a==b *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    37
  val rev_eq_reflection: thm               (* a==b ==> a=b *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    38
  val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    39
  val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    40
  val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    41
  val sym              : thm               (* a=b ==> b=a *)
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
    42
  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
    43
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    45
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
signature HYPSUBST =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    48
  val bound_hyp_subst_tac    : int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    49
  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
    50
  val blast_hyp_subst_tac    : bool ref -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
    (*exported purely for debugging purposes*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    52
  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
    53
  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
    54
  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
    55
  val inspect_pair           : bool -> bool -> term * term * typ -> bool
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    56
  val mk_eqs                 : thm -> thm list
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    57
  val thin_leading_eqs_tac   : bool -> int -> int -> tactic
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    58
  val stac		     : thm -> int -> tactic
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    59
  val hypsubst_setup         : (theory -> theory) list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    62
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    63
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    64
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
exception EQ_VAR;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
2174
0829b7b632c5 Removed a call to polymorphic mem
paulson
parents: 2143
diff changeset
    69
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    71
local val odot = ord"."
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    72
in
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    73
(*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
    74
  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
    75
*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    76
fun contract t =
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    77
    case Pattern.eta_contract_atom t of
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    78
        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
    79
      | t'        => t'
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    80
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    81
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    82
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
    83
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    84
(*If novars then we forbid Vars in the equality.
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    85
  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
    86
  When can we safely delete the equality?
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    87
    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
    88
    Not if it resembles x=t[x], since substitution does not eliminate x.
4299
22596d62ce0b updated comment
paulson
parents: 4223
diff changeset
    89
    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
    90
    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
    91
        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
    92
  Prefer to eliminate Bound variables if possible.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    93
  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
    94
fun inspect_pair bnd novars (t,u,T) =
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    95
  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
    96
  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
    97
  else
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    98
  case (contract t, contract u) of
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    99
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   100
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   101
                       else true                (*eliminates t*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   102
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
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 false               (*eliminates u*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   105
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   106
                          novars andalso has_vars u
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   107
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   108
                       else true                (*eliminates t*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   109
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   110
                          novars andalso has_vars t
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   111
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   112
                       else false               (*eliminates u*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
     | _ => raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   115
(*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
   116
   assumption.  Returns the number of intervening assumptions. *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   117
fun eq_var bnd novars =
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   118
  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
   119
        | eq_var_aux k (Const("==>",_) $ A $ B) =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   120
              ((k, inspect_pair bnd novars
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   121
                    (Data.dest_eq (Data.dest_Trueprop A)))
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   122
                      (*Exception comes from inspect_pair or dest_eq*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   123
               handle _ => eq_var_aux (k+1) B)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   124
        | eq_var_aux k _ = raise EQ_VAR
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   125
  in  eq_var_aux 0  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   127
(*We do not try to delete ALL equality assumptions at once.  But
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   128
  it is easy to handle several consecutive equality assumptions in a row.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   129
  Note that we have to inspect the proof state after doing the rewriting,
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   130
  since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   131
  must NOT be deleted.  Tactic must rotate or delete m assumptions.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   132
*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   133
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   134
    let fun count []      = 0
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   135
          | count (A::Bs) = ((inspect_pair bnd true
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   136
                              (Data.dest_eq (Data.dest_Trueprop A));
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   137
                              1 + count Bs)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   138
                             handle _ => 0)
2143
093bbe6d333b Replaced min by Int.min
paulson
parents: 1011
diff changeset
   139
        val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
   140
    in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   141
    end);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   142
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   143
(*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
   144
  No vars are allowed here, as simpsets are built from meta-assumptions*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   145
fun mk_eqs th =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   146
    [ if inspect_pair false false (Data.dest_eq
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   147
                                   (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
   148
      then th RS Data.eq_reflection
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   149
      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
   150
    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
   151
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   152
local open Simplifier
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   153
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   154
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   155
  val hyp_subst_ss = empty_ss setmksimps mk_eqs
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   156
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   157
  (*Select a suitable equality assumption and substitute throughout the subgoal
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   158
    Replaces only Bound variables if bnd is true*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   159
  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   160
        let val n = length(Logic.strip_assums_hyp Bi) - 1
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   161
            val (k,_) = eq_var bnd true Bi
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   162
        in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   163
           DETERM (EVERY [rotate_tac k i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   164
                          asm_full_simp_tac hyp_subst_ss i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   165
                          etac thin_rl i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   166
                          thin_leading_eqs_tac bnd (n-k) i])
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   167
        end
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   168
        handle THM _ => no_tac | EQ_VAR => no_tac);
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   169
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   170
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   171
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   172
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
   173
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   174
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
   175
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   176
(*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
   177
  to handle equalities containing Vars.*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   178
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   179
      let val n = length(Logic.strip_assums_hyp Bi) - 1
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   180
          val (k,symopt) = eq_var bnd false Bi
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   181
      in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   182
         DETERM
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   183
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   184
                   rotate_tac 1 i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   185
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   186
                   etac (if symopt then ssubst else Data.subst) i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   187
                   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
      end
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   189
      handle THM _ => no_tac | EQ_VAR => no_tac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
(*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
   192
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
   193
        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
(*Substitutes for Bound variables only -- this is always safe*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   196
val bound_hyp_subst_tac =
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   197
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   199
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   200
(** 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
   201
    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
   202
    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
   203
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   204
(*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
   205
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
   206
  | reverse_n_tac 1 i = rotate_tac ~1 i
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   207
  | 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
   208
      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
   209
      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
   210
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   211
(*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
   212
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
   213
  let fun imptac (r, [])    st = reverse_n_tac r i st
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   214
        | imptac (r, hyp::hyps) st =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   215
           let val (hyp',_) = List.nth (prems_of st, i-1) |>
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   216
                              Logic.strip_assums_concl    |>
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   217
                              Data.dest_Trueprop          |> Data.dest_imp
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   218
               val (r',tac) = if Pattern.aeconv (hyp,hyp')
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   219
                              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   220
                              else (*leave affected hyps at end*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   221
                                   (r+1, imp_intr_tac i)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   222
           in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   223
               case Seq.pull(tac st) of
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   224
                   None       => Seq.single(st)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   225
                 | Some(st',_) => imptac (r',hyps) st'
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   226
           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
   227
  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
   228
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   229
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   230
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
   231
      let val (k,symopt) = eq_var false false Bi
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   232
          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
   233
          (*omit selected equality, returning other hyps*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   234
          val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   235
          val n = length hyps
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   236
      in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   237
         if !trace then writeln "Substituting an equality" else ();
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   238
         DETERM
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   239
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   240
                   rotate_tac 1 i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   241
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   242
                   etac (if symopt then ssubst else Data.subst) i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   243
                   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
   244
      end
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   245
      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
   246
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   247
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   248
(*apply an equality or definition ONCE;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   249
  fails unless the substitution has an effect*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   250
fun stac th =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   251
  let val th' = th RS Data.rev_eq_reflection handle THM _ => th
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   252
  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   253
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   254
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   255
(* proof method setup *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   256
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   257
val subst_meth = Method.goal_args' Attrib.local_thm stac;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   258
val hypsubst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac);
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   259
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   260
val hypsubst_setup =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   261
 [Method.add_methods
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   262
  [("hypsubst", hypsubst_meth, "substitution using an assumption (improper)"),
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   263
   ("subst", subst_meth, "substitution")]];
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   264
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
end;