src/Provers/hypsubst.ML
author wenzelm
Mon, 04 Aug 2008 22:55:00 +0200
changeset 27734 dcec1c564f05
parent 27572 67cd6ed76446
child 30510 4120fc59dd85
permissions -rw-r--r--
meta_subst: xsymbols make it work with clean Pure;
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
15662
7e3bee7df06e improved comments;
wenzelm
parents: 15531
diff changeset
     6
Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst".
9628
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)";
23908
edca7f581c09 blast_hyp_subst_tac: plain bool argument;
wenzelm
parents: 21588
diff changeset
    31
by (blast_hyp_subst_tac 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 =
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    35
sig
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    36
  val dest_Trueprop    : term -> term
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    37
  val dest_eq          : term -> term * term
20974
2a29a21825d1 slight type signature changes
haftmann
parents: 20945
diff changeset
    38
  val dest_imp         : term -> term * term
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    39
  val eq_reflection    : thm               (* a=b ==> a==b *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    40
  val rev_eq_reflection: thm               (* a==b ==> a=b *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    41
  val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    42
  val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    43
  val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    44
  val sym              : thm               (* a=b ==> b=a *)
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
    45
  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
27572
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    46
  val prop_subst       : thm               (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    47
end;
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    48
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
signature HYPSUBST =
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    50
sig
27572
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    51
  val single_hyp_subst_tac   : int -> int -> tactic
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    52
  val single_hyp_meta_subst_tac : int -> int -> tactic
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    53
  val bound_hyp_subst_tac    : int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    54
  val hyp_subst_tac          : int -> tactic
23908
edca7f581c09 blast_hyp_subst_tac: plain bool argument;
wenzelm
parents: 21588
diff changeset
    55
  val blast_hyp_subst_tac    : bool -> int -> tactic
20945
1de0d565b483 fixed intendation
haftmann
parents: 20074
diff changeset
    56
  val stac                   : thm -> int -> tactic
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17896
diff changeset
    57
  val hypsubst_setup         : theory -> theory
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    58
end;
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    59
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    60
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
exception EQ_VAR;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
27734
dcec1c564f05 meta_subst: xsymbols make it work with clean Pure;
wenzelm
parents: 27572
diff changeset
    65
val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)"
27572
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    66
  by (unfold prop_def)}
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    67
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    68
(** Simple version: Just subtitute one hypothesis, specified by index k **)
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    69
fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    70
 let 
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    71
   val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    72
             |> cterm_of (theory_of_cterm csubg)
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    73
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    74
   val rule =
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    75
       Thm.lift_rule pat subst_rule (* lift just over parameters *)
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    76
       |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    77
 in
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    78
   rotate_tac k i
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    79
   THEN Thm.compose_no_flatten false (rule, 1) i
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    80
   THEN rotate_tac (~k) i
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    81
 end)
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    82
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    83
val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    84
val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 26992
diff changeset
    85
17896
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
    86
fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
16979
4d4d42ea3096 Term.is_bound;
wenzelm
parents: 15662
diff changeset
    88
(*Simplifier turns Bound variables to special Free variables:
4d4d42ea3096 Term.is_bound;
wenzelm
parents: 15662
diff changeset
    89
  change it back (any Bound variable will do)*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    90
fun contract t =
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
    91
  (case Envir.eta_contract t of
20074
b4d0b545df01 Name.is_bound;
wenzelm
parents: 18708
diff changeset
    92
    Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
16979
4d4d42ea3096 Term.is_bound;
wenzelm
parents: 15662
diff changeset
    93
  | t' => t');
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    94
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    95
val has_vars = Term.exists_subterm Term.is_Var;
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    96
val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    97
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    98
(*If novars then we forbid Vars in the equality.
16979
4d4d42ea3096 Term.is_bound;
wenzelm
parents: 15662
diff changeset
    99
  If bnd then we only look for Bound variables to eliminate.
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   100
  When can we safely delete the equality?
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   101
    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
   102
    Not if it resembles x=t[x], since substitution does not eliminate x.
4299
22596d62ce0b updated comment
paulson
parents: 4223
diff changeset
   103
    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
   104
    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
   105
        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
   106
  Prefer to eliminate Bound variables if possible.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   107
  Result:  true = use as is,  false = reorient first *)
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
   108
fun inspect_pair bnd novars (t, u) =
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
   109
  if novars andalso (has_tvars t orelse has_tvars u)
4179
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
   110
  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
   111
  else
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   112
  case (contract t, contract u) of
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   113
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
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 true                (*eliminates t*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   116
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   117
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   118
                       else false               (*eliminates u*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   119
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   120
                          novars andalso has_vars u
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   121
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   122
                       else true                (*eliminates t*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   123
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   124
                          novars andalso has_vars t
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   125
                       then raise Match
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   126
                       else false               (*eliminates u*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
     | _ => raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   129
(*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
   130
   assumption.  Returns the number of intervening assumptions. *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   131
fun eq_var bnd novars =
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   132
  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
   133
        | eq_var_aux k (Const("==>",_) $ A $ B) =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   134
              ((k, inspect_pair bnd novars
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   135
                    (Data.dest_eq (Data.dest_Trueprop A)))
21227
76d6d445d69b avoid handling of arbitrary exceptions;
wenzelm
parents: 21221
diff changeset
   136
               handle TERM _ => eq_var_aux (k+1) B
76d6d445d69b avoid handling of arbitrary exceptions;
wenzelm
parents: 21221
diff changeset
   137
                 | Match => eq_var_aux (k+1) B)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   138
        | eq_var_aux k _ = raise EQ_VAR
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   139
  in  eq_var_aux 0  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   141
(*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
   142
  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
   143
fun mk_eqs bnd th =
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   144
    [ if inspect_pair bnd false (Data.dest_eq
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   145
                                   (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
   146
      then th RS Data.eq_reflection
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   147
      else symmetric(th RS Data.eq_reflection) (*reorient*) ]
21227
76d6d445d69b avoid handling of arbitrary exceptions;
wenzelm
parents: 21221
diff changeset
   148
    handle TERM _ => [] | Match => [];
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   149
17896
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   150
local
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   151
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   152
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   153
  (*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
   154
    If bnd is true, then it replaces Bound variables only. *)
13604
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   155
  fun gen_hyp_subst_tac bnd =
17896
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   156
    let fun tac i st = SUBGOAL (fn (Bi, _) =>
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   157
      let
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   158
        val (k, _) = eq_var bnd true Bi
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   159
        val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   160
          setmksimps (mk_eqs bnd)
13604
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   161
      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
   162
        etac thin_rl i, rotate_tac (~k) i]
17896
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   163
      end handle THM _ => no_tac | EQ_VAR => no_tac) i st
13604
57bfacbbaeda - eliminated thin_leading_eqs_tac
berghofe
parents: 12377
diff changeset
   164
    in REPEAT_DETERM1 o tac end;
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   165
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   166
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   167
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   168
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
   169
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   170
fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   171
  case try (Logic.strip_assums_hyp #> hd #>
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   172
      Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   173
    SOME (t, t') =>
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   174
      let
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   175
        val Bi = Thm.term_of cBi;
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   176
        val ps = Logic.strip_params Bi;
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   177
        val U = Term.fastype_of1 (rev (map snd ps), t);
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   178
        val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   179
        val rl' = Thm.lift_rule cBi rl;
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   180
        val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   181
          (Logic.strip_assums_concl (Thm.prop_of rl')));
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   182
        val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   183
          (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   184
        val (Ts, V) = split_last (Term.binder_types T);
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   185
        val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   186
            Bound j => subst_bounds (map Bound
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   187
              ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   188
          | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   189
        val thy = Thm.theory_of_thm rl';
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   190
        val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   191
      in compose_tac (true, Drule.instantiate (instT,
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   192
        map (pairself (cterm_of thy))
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   193
          [(Var (ixn, Ts ---> U --> body_type T), u),
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   194
           (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   195
           (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   196
        nprems_of rl) i
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   197
      end
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   198
  | NONE => no_tac);
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   199
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   200
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
   201
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   202
(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   203
(* premises containing meta-implications or quantifiers                *)
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   204
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   205
(*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
   206
  to handle equalities containing Vars.*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   207
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   208
      let val n = length(Logic.strip_assums_hyp Bi) - 1
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   209
          val (k,symopt) = eq_var bnd false Bi
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   210
      in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   211
         DETERM
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   212
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   213
                   rotate_tac 1 i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   214
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   215
                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   216
                   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
      end
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   218
      handle THM _ => no_tac | EQ_VAR => no_tac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
(*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
   221
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
   222
        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
(*Substitutes for Bound variables only -- this is always safe*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   225
val bound_hyp_subst_tac =
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   226
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   228
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   229
(** 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
   230
    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
   231
    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
   232
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   233
(*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
   234
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
   235
  | reverse_n_tac 1 i = rotate_tac ~1 i
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   236
  | 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
   237
      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
   238
      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
   239
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   240
(*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
   241
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
   242
  let fun imptac (r, [])    st = reverse_n_tac r i st
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   243
        | imptac (r, hyp::hyps) st =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   244
           let val (hyp',_) = List.nth (prems_of st, i-1) |>
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   245
                              Logic.strip_assums_concl    |>
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   246
                              Data.dest_Trueprop          |> Data.dest_imp
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   247
               val (r',tac) = if Pattern.aeconv (hyp,hyp')
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   248
                              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   249
                              else (*leave affected hyps at end*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   250
                                   (r+1, imp_intr_tac i)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   251
           in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   252
               case Seq.pull(tac st) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
   253
                   NONE       => Seq.single(st)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
   254
                 | SOME(st',_) => imptac (r',hyps) st'
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
   255
           end
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   256
  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
   257
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   258
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   259
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
   260
      let val (k,symopt) = eq_var false false Bi
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   261
          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
   262
          (*omit selected equality, returning other hyps*)
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   263
          val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   264
          val n = length hyps
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   265
      in
23908
edca7f581c09 blast_hyp_subst_tac: plain bool argument;
wenzelm
parents: 21588
diff changeset
   266
         if trace then tracing "Substituting an equality" else ();
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   267
         DETERM
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   268
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   269
                   rotate_tac 1 i,
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   270
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   271
                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   272
                   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
   273
      end
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   274
      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
   275
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   276
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   277
(*apply an equality or definition ONCE;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   278
  fails unless the substitution has an effect*)
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   279
fun stac th =
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   280
  let val th' = th RS Data.rev_eq_reflection handle THM _ => th
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   281
  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   282
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   283
9628
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   284
(* theory setup *)
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   285
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   286
val hypsubst_setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17896
diff changeset
   287
  Method.add_methods
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21227
diff changeset
   288
    [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
cd0dc678a205 simplified method setup;
wenzelm
parents: 21227
diff changeset
   289
        "substitution using an assumption (improper)"),
cd0dc678a205 simplified method setup;
wenzelm
parents: 21227
diff changeset
   290
     ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")];
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   291
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
end;