src/Provers/hypsubst.ML
author immler
Sun, 27 Oct 2019 21:51:14 -0400
changeset 71035 6fe5a0e1fa8e
parent 69593 3dda49e08b9d
child 71401 a3ae93ed7b1b
permissions -rw-r--r--
moved theory Interval from the AFP
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
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
     2
    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
     3
    Copyright   1995  University of Cambridge
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     4
48107
6cebeee3863e Updated comment to reflect current state.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents: 46219
diff changeset
     5
Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst".
9628
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     6
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     7
Tactic to substitute using (at least) the assumption x=t in the rest
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     8
of the subgoal, and to delete (at least) that assumption.  Original
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
     9
version due to Martin Coen.
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    10
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    11
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
    12
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    13
Test data:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    15
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
    16
Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    17
Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    18
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
    19
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
    20
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
    21
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
    22
by (bound_hyp_subst_tac 1);
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    23
by (hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    24
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    25
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
    26
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
    27
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
    28
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
    29
\                 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
    30
by (blast_hyp_subst_tac true 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
signature HYPSUBST_DATA =
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    34
sig
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
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    36
  val dest_eq          : term -> term * term
20974
2a29a21825d1 slight type signature changes
haftmann
parents: 20945
diff changeset
    37
  val dest_imp         : term -> term * term
9532
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 *)
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    45
end;
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    46
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
signature HYPSUBST =
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    48
sig
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51717
diff changeset
    49
  val bound_hyp_subst_tac    : Proof.context -> int -> tactic
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
    50
  val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
57509
cca0db87b653 more uniform names;
wenzelm
parents: 57492
diff changeset
    51
  val hyp_subst_thin         : bool Config.T
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51717
diff changeset
    52
  val hyp_subst_tac          : Proof.context -> int -> tactic
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58950
diff changeset
    53
  val blast_hyp_subst_tac    : Proof.context -> bool -> int -> tactic
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
    54
  val stac                   : Proof.context -> thm -> int -> tactic
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    55
end;
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    56
42799
4e33894aec6d modernized functor names;
wenzelm
parents: 42366
diff changeset
    57
functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
exception EQ_VAR;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
16979
4d4d42ea3096 Term.is_bound;
wenzelm
parents: 15662
diff changeset
    62
(*Simplifier turns Bound variables to special Free variables:
4d4d42ea3096 Term.is_bound;
wenzelm
parents: 15662
diff changeset
    63
  change it back (any Bound variable will do)*)
60706
03a6b1792cd8 clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
wenzelm
parents: 60642
diff changeset
    64
fun inspect_contract t =
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
    65
  (case Envir.eta_contract t of
20074
b4d0b545df01 Name.is_bound;
wenzelm
parents: 18708
diff changeset
    66
    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
    67
  | t' => t');
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    68
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    69
val has_vars = Term.exists_subterm Term.is_Var;
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    70
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
    71
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    72
(*If novars then we forbid Vars in the equality.
16979
4d4d42ea3096 Term.is_bound;
wenzelm
parents: 15662
diff changeset
    73
  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
    74
  When can we safely delete the equality?
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    75
    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
    76
    Not if it resembles x=t[x], since substitution does not eliminate x.
4299
22596d62ce0b updated comment
paulson
parents: 4223
diff changeset
    77
    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
    78
    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
    79
        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
    80
  Prefer to eliminate Bound variables if possible.
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
    81
  Result:  true = use as is,  false = reorient first
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
    82
    also returns var to substitute, relevant if it is Free *)
21221
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    83
fun inspect_pair bnd novars (t, u) =
ef30d1e6f03a simplified dest_eq;
wenzelm
parents: 20974
diff changeset
    84
  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
    85
  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
    86
  else
60706
03a6b1792cd8 clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
wenzelm
parents: 60642
diff changeset
    87
    (case apply2 inspect_contract (t, u) of
42082
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    88
      (Bound i, _) =>
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    89
        if loose_bvar1 (u, i) orelse novars andalso has_vars u
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    90
        then raise Match
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
    91
        else (true, Bound i)                (*eliminates t*)
42082
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    92
    | (_, Bound i) =>
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    93
        if loose_bvar1 (t, i) orelse novars andalso has_vars t
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    94
        then raise Match
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
    95
        else (false, Bound i)               (*eliminates u*)
42082
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    96
    | (t' as Free _, _) =>
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    97
        if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
    98
        then raise Match
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
    99
        else (true, t')                (*eliminates t*)
42082
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
   100
    | (_, u' as Free _) =>
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
   101
        if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
   102
        then raise Match
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   103
        else (false, u')               (*eliminates u*)
42082
47f8bfe0f597 more direct loose_bvar1;
wenzelm
parents: 39782
diff changeset
   104
    | _ => raise Match);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   106
(*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
   107
   assumption.  Returns the number of intervening assumptions. *)
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   108
fun eq_var bnd novars check_frees t =
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   109
  let
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   110
    fun check_free ts (orient, Free f)
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   111
      = if not check_frees orelse not orient
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   112
            orelse exists (curry Logic.occs (Free f)) ts
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   113
        then (orient, true) else raise Match
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   114
      | check_free ts (orient, _) = (orient, false)
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 60706
diff changeset
   115
    fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 60706
diff changeset
   116
      | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) hs =
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   117
              ((k, check_free (B :: hs) (inspect_pair bnd novars
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   118
                    (Data.dest_eq (Data.dest_Trueprop A))))
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   119
               handle TERM _ => eq_var_aux (k+1) B (A :: hs)
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   120
                 | Match => eq_var_aux (k+1) B (A :: hs))
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   121
      | eq_var_aux k _ _ = raise EQ_VAR
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   122
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   123
  in  eq_var_aux 0 t [] end;
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   124
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   125
fun thin_free_eq_tac ctxt = SUBGOAL (fn (t, i) =>
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   126
  let
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   127
    val (k, _) = eq_var false false false t
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   128
    val ok = (eq_var false false true t |> fst) > k handle EQ_VAR => true
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   129
  in
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   130
    if ok then EVERY [rotate_tac k i, eresolve_tac ctxt [thin_rl] i, rotate_tac (~k) i]
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   131
    else no_tac
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   132
  end handle EQ_VAR => no_tac)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   134
(*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
   135
  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
   136
fun mk_eqs bnd th =
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   137
    [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   138
      then th RS Data.eq_reflection
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36543
diff changeset
   139
      else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
21227
76d6d445d69b avoid handling of arbitrary exceptions;
wenzelm
parents: 21221
diff changeset
   140
    handle TERM _ => [] | Match => [];
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   141
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   142
fun bool2s true = "true" | bool2s false = "false"
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   143
17896
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   144
local
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   145
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   146
15415
6e437e276ef5 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents: 13604
diff changeset
   147
  (*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
   148
    If bnd is true, then it replaces Bound variables only. *)
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51717
diff changeset
   149
  fun gen_hyp_subst_tac ctxt bnd =
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   150
    SUBGOAL (fn (Bi, i) =>
17896
66902148c436 functor: no Simplifier argument;
wenzelm
parents: 16979
diff changeset
   151
      let
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   152
        val (k, (orient, is_free)) = eq_var bnd true true Bi
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50035
diff changeset
   153
        val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50035
diff changeset
   154
      in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   155
        if not is_free then eresolve_tac ctxt [thin_rl] i
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   156
          else if orient then eresolve_tac ctxt [Data.rev_mp] i
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   157
          else eresolve_tac ctxt [Data.sym RS Data.rev_mp] i,
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   158
        rotate_tac (~k) i,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   159
        if is_free then resolve_tac ctxt [Data.imp_intr] i else all_tac]
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   160
      end 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
   161
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   162
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   163
45659
09539cdffcd7 avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
wenzelm
parents: 45625
diff changeset
   164
val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   165
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58950
diff changeset
   166
fun inst_subst_tac ctxt 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
   167
  case try (Logic.strip_assums_hyp #> hd #>
60706
03a6b1792cd8 clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
wenzelm
parents: 60642
diff changeset
   168
      Data.dest_Trueprop #> Data.dest_eq #> apply2 Envir.eta_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
   169
    SOME (t, t') =>
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   170
      let
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   171
        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
   172
        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
   173
        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
   174
        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
   175
        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
   176
        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
   177
          (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
   178
        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
   179
          (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
   180
        val (Ts, V) = split_last (Term.binder_types T);
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45659
diff changeset
   181
        val u =
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45659
diff changeset
   182
          fold_rev Term.abs (ps @ [("x", U)])
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45659
diff changeset
   183
            (case (if b then t else t') of
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45659
diff changeset
   184
              Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45659
diff changeset
   185
            | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
59642
929984c529d3 clarified context;
wenzelm
parents: 59621
diff changeset
   186
        val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45659
diff changeset
   187
      in
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58950
diff changeset
   188
        compose_tac ctxt (true, Drule.instantiate_normalize (instT,
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59642
diff changeset
   189
          map (apsnd (Thm.cterm_of ctxt))
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59642
diff changeset
   190
            [((ixn, Ts ---> U --> body_type T), u),
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59642
diff changeset
   191
             ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59642
diff changeset
   192
             ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   193
          Thm.nprems_of rl) i
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   194
      end
26992
4508f20818af inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
wenzelm
parents: 26833
diff changeset
   195
  | NONE => no_tac);
26833
7c3757fccf0e Added function for computing instantiation for the subst rule, which is used
berghofe
parents: 23908
diff changeset
   196
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   197
fun imp_intr_tac ctxt = resolve_tac ctxt [Data.imp_intr];
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   198
58958
114255dce178 proper context;
wenzelm
parents: 58957
diff changeset
   199
fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
114255dce178 proper context;
wenzelm
parents: 58957
diff changeset
   200
fun dup_subst ctxt = rev_dup_elim ctxt ssubst
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
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.*)
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58950
diff changeset
   207
fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) =>
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   208
      let val n = length(Logic.strip_assums_hyp Bi) - 1
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   209
          val (k, (orient, is_free)) = eq_var bnd false true Bi
58958
114255dce178 proper context;
wenzelm
parents: 58957
diff changeset
   210
          val rl = if is_free then dup_subst ctxt else ssubst
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   211
          val rl = if orient then rl else Data.sym RS rl
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   212
      in
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   213
         DETERM
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   214
           (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i),
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   215
                   rotate_tac 1 i,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   216
                   REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i),
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58950
diff changeset
   217
                   inst_subst_tac ctxt orient rl i,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   218
                   REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i)])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
      end
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   220
      handle THM _ => no_tac | EQ_VAR => no_tac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   222
(*Substitutes for Free or Bound variables,
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   223
  discarding equalities on Bound variables
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   224
  and on Free variables if thin=true*)
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   225
fun hyp_subst_tac_thin thin ctxt =
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58956
diff changeset
   226
  REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl],
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58950
diff changeset
   227
    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   228
    if thin then thin_free_eq_tac ctxt else K no_tac];
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   229
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 60706
diff changeset
   230
val hyp_subst_thin = Attrib.setup_config_bool \<^binding>\<open>hypsubst_thin\<close> (K false);
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   231
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   232
fun hyp_subst_tac ctxt =
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   233
  hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
(*Substitutes for Bound variables only -- this is always safe*)
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51717
diff changeset
   236
fun bound_hyp_subst_tac ctxt =
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 56245
diff changeset
   237
  REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58950
diff changeset
   238
    ORELSE' vars_gen_hyp_subst_tac ctxt true);
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   239
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   240
(** 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
   241
    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
   242
    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
   243
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   244
(*final re-reversal of the changed assumptions*)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   245
fun reverse_n_tac _ 0 i = all_tac
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   246
  | reverse_n_tac _ 1 i = rotate_tac ~1 i
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   247
  | reverse_n_tac ctxt n i =
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   248
      REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac ctxt [Data.rev_mp] i) THEN
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   249
      REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i);
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   250
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   251
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   252
fun all_imp_intr_tac ctxt hyps i =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   253
  let
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   254
    fun imptac (r, []) st = reverse_n_tac ctxt r i st
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   255
      | imptac (r, hyp::hyps) st =
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   256
          let
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   257
            val (hyp', _) =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   258
              Thm.term_of (Thm.cprem_of st i)
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   259
              |> Logic.strip_assums_concl
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   260
              |> Data.dest_Trueprop |> Data.dest_imp;
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   261
            val (r', tac) =
52131
366fa32ee2a3 tuned signature;
wenzelm
parents: 51798
diff changeset
   262
              if Envir.aeconv (hyp, hyp')
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   263
              then (r, imp_intr_tac ctxt i THEN rotate_tac ~1 i)
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   264
              else (*leave affected hyps at end*) (r + 1, imp_intr_tac ctxt i);
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   265
          in
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   266
            (case Seq.pull (tac st) of
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   267
              NONE => Seq.single st
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   268
            | SOME (st', _) => imptac (r', hyps) st')
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   269
          end
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42082
diff changeset
   270
  in imptac (0, rev hyps) end;
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   271
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   272
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   273
fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi, i) =>
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   274
  let
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   275
    val (k, (symopt, _)) = eq_var false false false Bi
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   276
    val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   277
    (*omit selected equality, returning other hyps*)
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   278
    val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   279
    val n = length hyps
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   280
  in
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   281
    if trace then tracing "Substituting an equality" else ();
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   282
    DETERM
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   283
      (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i),
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   284
              rotate_tac 1 i,
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   285
              REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i),
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   286
              inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i,
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   287
              all_imp_intr_tac ctxt hyps i])
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   288
  end
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   289
  handle THM _ => no_tac | EQ_VAR => no_tac);
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   290
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   291
(*apply an equality or definition ONCE;
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   292
  fails unless the substitution has an effect*)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   293
fun stac ctxt th =
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   294
  let val th' = th RS Data.rev_eq_reflection handle THM _ => th
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   295
  in CHANGED_GOAL (resolve_tac ctxt [th' RS ssubst]) end;
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   296
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   297
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   298
(* method setup *)
9628
53a62fd8b2dc added 'symmetric' attribute;
wenzelm
parents: 9592
diff changeset
   299
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   300
val _ =
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   301
  Theory.setup
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 60706
diff changeset
   302
   (Method.setup \<^binding>\<open>hypsubst\<close>
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   303
      (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   304
      "substitution using an assumption (improper)" #>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 60706
diff changeset
   305
    Method.setup \<^binding>\<open>hypsubst_thin\<close>
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   306
      (Scan.succeed (fn ctxt => SIMPLE_METHOD'
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   307
          (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   308
      "substitution using an assumption, eliminating assumptions" #>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 60706
diff changeset
   309
    Method.setup \<^binding>\<open>simplesubst\<close>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   310
      (Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (stac ctxt th)))
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 57509
diff changeset
   311
      "simple substitution");
9532
36b9bc6eb454 added rev_eq_reflection;
wenzelm
parents: 4466
diff changeset
   312
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
end;