src/Provers/eqsubst.ML
author dixon
Sat, 19 Feb 2005 18:44:34 +0100
changeset 15538 d8edf54cc28c
parent 15486 06a32fe35ec3
child 15550 806214035275
permissions -rw-r--r--
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
     2
(*  Title:      Provers/eqsubst.ML
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     3
    Author:     Lucas Dixon, University of Edinburgh
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     4
                lucas.dixon@ed.ac.uk
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
     5
    Modified:   18 Feb 2005 - Lucas - 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     6
    Created:    29 Jan 2005
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     7
*)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     8
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     9
(*  DESCRIPTION:
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    10
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    11
    A Tactic to perform a substiution using an equation.
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    12
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    13
*)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    14
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    15
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    16
(* Logic specific data stub *)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    17
signature EQRULE_DATA =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    18
sig
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    19
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    20
  (* to make a meta equality theorem in the current logic *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    21
  val prep_meta_eq : thm -> thm list
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    22
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    23
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    24
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    25
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    26
(* the signature of an instance of the SQSUBST tactic *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    27
signature EQSUBST_TAC = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    28
sig
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    29
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    30
  val prep_subst_in_asm :
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    31
      (Sign.sg (* sign for matching *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    32
       -> int (* maxidx *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    33
       -> 'a (* input object kind *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    34
       -> BasicIsaFTerm.FcTerm (* focusterm to search under *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    35
       -> 'b) (* result type *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    36
      -> int (* subgoal to subst in *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    37
      -> Thm.thm (* target theorem with subgoals *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    38
      -> int (* premise to subst in *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    39
      -> (Thm.cterm list (* certified free var placeholders for vars *) 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    40
          * int (* premice no. to subst *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    41
          * int (* number of assumptions of premice *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    42
          * Thm.thm) (* premice as a new theorem for forward reasoning *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    43
         * ('a -> 'b) (* matchf *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    44
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    45
  val prep_subst_in_asms :
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    46
      (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    47
      -> int (* subgoal to subst in *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    48
      -> Thm.thm (* target theorem with subgoals *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    49
      -> ((Thm.cterm list (* certified free var placeholders for vars *) 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    50
          * int (* premice no. to subst *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    51
          * int (* number of assumptions of premice *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    52
          * Thm.thm) (* premice as a new theorem for forward reasoning *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    53
         * ('a -> 'b)) (* matchf *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    54
                       Seq.seq
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    55
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    56
  val apply_subst_in_asm :
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    57
      int (* subgoal *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    58
      -> Thm.thm (* overall theorem *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    59
      -> (Thm.cterm list (* certified free var placeholders for vars *) 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    60
          * int (* assump no being subst *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    61
          * int (* num of premises of asm *) 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    62
          * Thm.thm) (* premthm *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    63
      -> Thm.thm (* rule *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    64
      -> (((Term.indexname * Term.typ) list (* type instantiations *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    65
          * (Term.indexname * Term.term) list) (* term instantiations *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    66
         * (string * Term.typ) list (* type abs env *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    67
         * Term.term) (* outer term *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    68
      -> Thm.thm Seq.seq
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    69
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    70
  val prep_concl_subst :
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    71
      (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) (* searchf *) 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    72
      -> int (* subgoal *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    73
      -> Thm.thm (* overall goal theorem *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    74
      -> (Thm.cterm list * Thm.thm) * ('a -> 'b) (* (cvfs, conclthm), matchf *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    75
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    76
  val apply_subst_in_concl :
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    77
        int (* subgoal *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    78
        -> Thm.thm (* thm with all goals *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    79
        -> Thm.cterm list (* certified free var placeholders for vars *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    80
           * Thm.thm  (* trivial thm of goal concl *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    81
            (* possible matches/unifiers *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    82
        -> Thm.thm (* rule *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    83
        -> (((Term.indexname * Term.typ) list (* type instantiations *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    84
              * (Term.indexname * Term.term) list ) (* term instantiations *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    85
             * (string * Term.typ) list (* Type abs env *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    86
             * Term.term) (* outer term *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    87
        -> Thm.thm Seq.seq (* substituted goal *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    88
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    89
  val eqsubst_asm_meth : Thm.thm list -> Proof.method
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    90
  val eqsubst_asm_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    91
  val eqsubst_asm_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    92
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    93
  val eqsubst_meth : Thm.thm list -> Proof.method
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    94
  val eqsubst_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    95
  val eqsubst_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
    96
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    97
  val meth : bool * Thm.thm list -> Proof.context -> Proof.method
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    98
  val setup : (Theory.theory -> Theory.theory) list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    99
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   100
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   101
functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   102
  : EQSUBST_TAC
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   103
= struct
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   104
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   105
(* FOR DEBUGGING...
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   106
type trace_subst_errT = int (* subgoal *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   107
        * Thm.thm (* thm with all goals *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   108
        * (Thm.cterm list (* certified free var placeholders for vars *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   109
           * Thm.thm)  (* trivial thm of goal concl *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   110
            (* possible matches/unifiers *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   111
        * Thm.thm (* rule *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   112
        * (((Term.indexname * Term.typ) list (* type instantiations *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   113
              * (Term.indexname * Term.term) list ) (* term instantiations *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   114
             * (string * Term.typ) list (* Type abs env *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   115
             * Term.term) (* outer term *);
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   116
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   117
val trace_subst_err = (ref NONE : trace_subst_errT option ref);
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   118
val trace_subst_search = ref false;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   119
exception trace_subst_exp of trace_subst_errT;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   120
 *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   121
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   122
(* also defined in /HOL/Tools/inductive_codegen.ML, 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   123
   maybe move this to seq.ML ? *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   124
infix 5 :->;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   125
fun s :-> f = Seq.flat (Seq.map f s);
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   126
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   127
(* search from the top to bottom, left to right *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   128
fun search_lr_f f ft = 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   129
    let
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   130
      fun maux ft = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   131
          let val t' = (IsaFTerm.focus_of_fcterm ft) 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   132
            (* val _ = 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   133
                if !trace_subst_search then 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   134
                  (writeln ("Examining: " ^ (TermLib.string_of_term t'));
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   135
                   TermLib.writeterm t'; ())
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   136
                else (); *)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   137
          in 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   138
          (case t' of 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   139
            (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   140
                       Seq.append(f ft, 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   141
                                  maux (IsaFTerm.focus_right ft)))
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   142
          | (Abs _) => Seq.append (f ft, maux (IsaFTerm.focus_abs ft))
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   143
          | leaf => f ft) end
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   144
    in maux ft end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   145
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   146
fun search_for_match sgn maxidx lhs  = 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   147
    IsaFTerm.find_fcterm_matches 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   148
      search_lr_f 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   149
      (IsaFTerm.clean_unify_ft sgn maxidx lhs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   150
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   151
(* apply a substitution in the conclusion of the theorem th *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   152
(* cfvs are certified free var placeholders for goal params *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   153
(* conclthm is a theorem of for just the conclusion *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   154
(* m is instantiation/match information *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   155
(* rule is the equation for substitution *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   156
fun apply_subst_in_concl i th (cfvs, conclthm) rule m = 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   157
    (RWInst.rw m rule conclthm)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   158
      |> IsaND.schemify_frees_to_vars cfvs
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   159
      |> RWInst.beta_eta_contract_tac
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   160
      |> (fn r => Tactic.rtac r i th);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   161
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   162
(*
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   163
? is the following equivalent to rtac ? 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   164
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   165
 |> Thm.lift_rule (th, i)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   166
 |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   167
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   168
*)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   169
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   170
(* substitute within the conclusion of goal i of gth, using a meta
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   171
equation rule. Note that we assume rule has var indicies zero'd *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   172
fun prep_concl_subst searchf i gth = 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   173
    let 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   174
      val th = Thm.incr_indexes 1 gth;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   175
      val tgt_term = Thm.prop_of th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   176
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   177
      val sgn = Thm.sign_of_thm th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   178
      val ctermify = Thm.cterm_of sgn;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   179
      val trivify = Thm.trivial o ctermify;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   180
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   181
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   182
      val cfvs = rev (map ctermify fvs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   183
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   184
      val conclterm = Logic.strip_imp_concl fixedbody;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   185
      val conclthm = trivify conclterm;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   186
      val maxidx = Term.maxidx_of_term conclterm;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   187
    in
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   188
      ((cfvs, conclthm), 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   189
       (fn lhs => searchf sgn maxidx lhs 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   190
                          ((IsaFTerm.focus_right  
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   191
                            o IsaFTerm.focus_left
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   192
                            o IsaFTerm.fcterm_of_term 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   193
                            o Thm.prop_of) conclthm)))
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   194
    end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   195
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   196
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   197
(* substitute using an object or meta level equality *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   198
fun eqsubst_tac' instepthm i th = 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   199
    let 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   200
      val (cvfsconclthm, findmatchf) = 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   201
          prep_concl_subst search_for_match i th;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   202
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   203
      val stepthms = 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   204
          Seq.map Drule.zero_var_indexes 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   205
                  (Seq.of_list (EqRuleData.prep_meta_eq instepthm));
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   206
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   207
      fun rewrite_with_thm r =
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   208
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   209
          in (findmatchf lhs)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   210
             :-> (apply_subst_in_concl i th cvfsconclthm r) end;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   211
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   212
    in (stepthms :-> rewrite_with_thm) end;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   213
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   214
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   215
(* substitute using one of the given theorems *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   216
fun eqsubst_tac instepthms i th = 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   217
    if Thm.nprems_of th < i then Seq.empty else
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   218
    (Seq.of_list instepthms) :-> (fn r => eqsubst_tac' r i th);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   219
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   220
(* inthms are the given arguments in Isar, and treated as eqstep with
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   221
   the first one, then the second etc *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   222
fun eqsubst_meth inthms =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   223
    Method.METHOD 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   224
      (fn facts =>
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   225
          HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac inthms ));
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   226
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   227
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   228
fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   229
    (RWInst.rw m rule pth)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   230
      |> Thm.permute_prems 0 ~1
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   231
      |> IsaND.schemify_frees_to_vars cfvs
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   232
      |> RWInst.beta_eta_contract_tac
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   233
      |> (fn r => Tactic.dtac r i th);
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   234
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   235
(*
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   236
? should I be using bicompose what if we match more than one
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   237
assumption, even after instantiation ? (back will work, but it would
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   238
be nice to avoid the redudent search)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   239
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   240
something like... 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   241
 |> Thm.lift_rule (th, i)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   242
 |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r - nprems) i th)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   243
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   244
*)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   245
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   246
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   247
(* prepare to substitute within the j'th premise of subgoal i of gth,
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   248
using a meta-level equation. Note that we assume rule has var indicies
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   249
zero'd. Note that we also assume that premt is the j'th premice of
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   250
subgoal i of gth. Note the repetition of work done for each
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   251
assumption, i.e. this can be made more efficient for search over
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   252
multiple assumptions.  *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   253
fun prep_subst_in_asm searchf i gth j = 
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   254
    let 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   255
      val th = Thm.incr_indexes 1 gth;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   256
      val tgt_term = Thm.prop_of th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   257
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   258
      val sgn = Thm.sign_of_thm th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   259
      val ctermify = Thm.cterm_of sgn;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   260
      val trivify = Thm.trivial o ctermify;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   261
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   262
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   263
      val cfvs = rev (map ctermify fvs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   264
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   265
      val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody));
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   266
      val asm_nprems = length (Logic.strip_imp_prems asmt);
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   267
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   268
      val pth = trivify asmt;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   269
      val maxidx = Term.maxidx_of_term asmt;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   270
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   271
    in
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   272
      ((cfvs, j, asm_nprems, pth), 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   273
       (fn lhs => (searchf sgn maxidx lhs
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   274
                           ((IsaFTerm.focus_right 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   275
                             o IsaFTerm.fcterm_of_term 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   276
                             o Thm.prop_of) pth))))
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   277
    end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   278
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   279
(* prepare subst in every possible assumption *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   280
fun prep_subst_in_asms searchf i gth = 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   281
    Seq.map 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   282
      (prep_subst_in_asm searchf i gth)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   283
      (Seq.of_list (IsaPLib.mk_num_list
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   284
                      (length (Logic.prems_of_goal (Thm.prop_of gth) i))));
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   285
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   286
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   287
(* substitute in an assumption using an object or meta level equality *)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   288
fun eqsubst_asm_tac' instepthm i th = 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   289
    let 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   290
      val asmpreps = prep_subst_in_asms search_for_match i th;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   291
      val stepthms = 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   292
          Seq.map Drule.zero_var_indexes 
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   293
                  (Seq.of_list (EqRuleData.prep_meta_eq instepthm))
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   294
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   295
      fun rewrite_with_thm (asminfo, findmatchf) r =
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   296
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   297
          in (findmatchf lhs)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   298
             :-> (apply_subst_in_asm i th asminfo r) end;
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   299
    in
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   300
      (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a))
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   301
    end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   302
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   303
(* substitute using one of the given theorems *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   304
fun eqsubst_asm_tac instepthms i th = 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   305
    if Thm.nprems_of th < i then Seq.empty else
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   306
    (Seq.of_list instepthms) :-> (fn r => eqsubst_asm_tac' r i th);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   307
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   308
(* inthms are the given arguments in Isar, and treated as eqstep with
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   309
   the first one, then the second etc *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   310
fun eqsubst_asm_meth inthms =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   311
    Method.METHOD 
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   312
      (fn facts =>
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   313
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms ));
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   314
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   315
(* combination method that takes a flag (true indicates that subst
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   316
should be done to an assumption, false = apply to the conclusion of
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   317
the goal) as well as the theorems to use *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   318
fun meth (asmflag, inthms) ctxt = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   319
    if asmflag then eqsubst_asm_meth inthms else eqsubst_meth inthms;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   320
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   321
(* syntax for options, given "(asm)" will give back true, without
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   322
   gives back false *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   323
val options_syntax =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   324
    (Args.parens (Args.$$$ "asm") >> (K true)) ||
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   325
     (Scan.succeed false);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   326
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   327
(* method syntax, first take options, then theorems *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   328
fun meth_syntax meth src ctxt =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   329
    meth (snd (Method.syntax ((Scan.lift options_syntax) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   330
                                -- Attrib.local_thms) src ctxt)) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   331
         ctxt;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   332
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   333
(* setup function for adding method to theory. *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   334
val setup = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   335
    [Method.add_method ("subst", meth_syntax meth, "Substiution with an equation. Use \"(asm)\" option to substitute in an assumption.")];
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   336
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   337
end;