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