src/Pure/IsaPlanner/rw_inst.ML
author paulson
Tue, 01 Feb 2005 18:01:57 +0100
changeset 15481 fc075ae929e4
child 15560 c862d556fb18
permissions -rw-r--r--
the new subst tactic, by Lucas Dixon
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     2
(*  Title:      sys/rw_inst.ML
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
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     5
    Created:    25 Aug 2004
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     6
*)
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
(*  DESCRIPTION:
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     9
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    10
    rewriting using a conditional meta-equality theorem which supports 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    11
    schematic variable instantiation.
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
signature RW_INST =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    16
sig
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    17
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    18
  (* Rewrite: give it instantiation infromation, a rule, and the
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    19
  target thm, and it will return the rewritten target thm *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    20
  val rw :
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    21
      ((Term.indexname * Term.typ) list *    (* type var instantiations *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    22
       (Term.indexname * Term.term) list)    (* schematic var instantiations *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    23
       * (string * Term.typ) list *          (* bound types *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    24
      Term.term ->                           (* outer term for instantiation *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    25
      Thm.thm ->                             (* rule with indexies lifted *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    26
      Thm.thm ->                             (* target thm *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    27
      Thm.thm                                (* rewritten theorem possibly 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    28
                                                with additional premises for 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    29
                                                rule conditions *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    30
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    31
  (* used tools *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    32
  val mk_abstractedrule :
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    33
      (string * Term.typ) list -> Thm.thm -> Thm.cterm list * Thm.thm
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    34
  val mk_fixtvar_tyinsts :
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    35
      Term.indexname list ->
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    36
      Term.term list -> ((string * int) * Term.typ) list * string list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    37
  val mk_renamings :
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    38
      Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    39
  val new_tfree :
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    40
      ((string * int) * Term.sort) *
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    41
      (((string * int) * Term.typ) list * string list) ->
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    42
      ((string * int) * Term.typ) list * string list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    43
  val cross_inst : (Term.indexname * Term.term) list 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    44
                   -> (Term.indexname * Term.term) list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    45
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    46
  val beta_contract_tac : Thm.thm -> Thm.thm
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    47
  val beta_eta_contract_tac : Thm.thm -> Thm.thm
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    48
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    49
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    50
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    51
structure RWInst : RW_INST= 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    52
struct
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    53
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    54
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    55
(* beta contract the theorem *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    56
fun beta_contract_tac thm = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    57
    equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    58
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    59
(* beta-eta contract the theorem *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    60
fun beta_eta_contract_tac thm = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    61
    let
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    62
      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    63
      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    64
    in thm3 end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    65
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    66
(* Given a list of variables that were bound, and a that has been
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    67
instantiated with free variable placeholders for the bound vars, it
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    68
creates an abstracted version of the theorem, with local bound vars as
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    69
lambda-params:
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    70
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    71
Ts: 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    72
("x", ty)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    73
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    74
rule::
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    75
C :x ==> P :x = Q :x
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    76
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    77
results in:
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    78
("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    79
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    80
note: assumes rule is instantiated
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    81
*)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    82
(* Note, we take abstraction in the order of last abstraction first *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    83
fun mk_abstractedrule Ts rule = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    84
    let 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    85
      val ctermify = Thm.cterm_of (Thm.sign_of_thm rule);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    86
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    87
      (* now we change the names the temporary free vars that represent 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    88
         bound vars with binders outside the redex *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    89
      val prop = Thm.prop_of rule;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    90
      val names = Term.add_term_names (prop, []);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    91
      val (fromnames,tonames,names2) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    92
          foldl (fn ((rnf,rnt,names),(n,ty)) => 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    93
                    let val n2 = Term.variant names n in
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    94
                      (ctermify (Free(RWTools.mk_fake_bound_name n,
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    95
                                      ty)) :: rnf,
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    96
                       ctermify (Free(n2,ty)) :: rnt, 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    97
                       n2 :: names)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    98
                    end)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    99
                (([],[],names), Ts);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   100
      val rule' = rule |> Drule.forall_intr_list fromnames
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   101
                       |> Drule.forall_elim_list tonames;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   102
      
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   103
      (* make unconditional rule and prems *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   104
      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify Ts rule';
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   105
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   106
      (* using these names create lambda-abstracted version of the rule *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   107
      val abstractions = Ts ~~ (rev tonames);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   108
      val abstract_rule = foldl (fn (th,((n,ty),ct)) => 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   109
                                    Thm.abstract_rule n ct th)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   110
                                (uncond_rule, abstractions);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   111
    in (cprems, abstract_rule) end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   112
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   113
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   114
(* given names to avoid, and vars that need to be fixed, it gives
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   115
unique new names to the vars so that they can be fixed as free
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   116
variables *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   117
(* make fixed unique free variable instantiations for non-ground vars *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   118
(* Create a table of vars to be renamed after instantiation - ie
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   119
      other uninstantiated vars in the hyps of the rule 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   120
      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   121
fun mk_renamings tgt rule_inst = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   122
    let
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   123
      val rule_conds = Thm.prems_of rule_inst
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   124
      val names = foldr Term.add_term_names (tgt :: rule_conds, []);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   125
      val (conds_tyvs,cond_vs) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   126
          foldl (fn ((tyvs, vs), t) => 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   127
                    (Library.union
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   128
                       (Term.term_tvars t, tyvs),
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   129
                     Library.union 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   130
                       (map Term.dest_Var (Term.term_vars t), vs))) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   131
                (([],[]), rule_conds);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   132
      val termvars = map Term.dest_Var (Term.term_vars tgt); 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   133
      val vars_to_fix = Library.union (termvars, cond_vs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   134
      val (renamings, names2) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   135
          foldr (fn (((n,i),ty), (vs, names')) => 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   136
                    let val n' = Term.variant names' n in
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   137
                      ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   138
                    end)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   139
                (vars_to_fix, ([], names));
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   140
    in renamings end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   141
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   142
(* make a new fresh typefree instantiation for the given tvar *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   143
fun new_tfree (tv as (ix,sort), (pairs,used)) =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   144
      let val v = variant used (string_of_indexname ix)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   145
      in  ((ix,TFree(v,sort))::pairs, v::used)  end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   146
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   147
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   148
(* make instantiations to fix type variables that are not 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   149
   already instantiated (in ignore_ixs) from the list of terms. *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   150
fun mk_fixtvar_tyinsts ignore_ixs ts = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   151
    let val (tvars, tfreenames) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   152
            foldr (fn (t, (varixs, tfreenames)) => 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   153
                      (Term.add_term_tvars (t,varixs),
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   154
                       Term.add_term_tfree_names (t,tfreenames)))
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   155
                  (ts, ([],[]));
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   156
        val unfixed_tvars = filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   157
        val (fixtyinsts, _) = foldr new_tfree (unfixed_tvars, ([], tfreenames))
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   158
    in (fixtyinsts, tfreenames) end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   159
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   160
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   161
(* cross-instantiate the instantiations - ie for each instantiation
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   162
replace all occurances in other instantiations - no loops are possible
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   163
and thus only one-parsing of the instantiations is necessary. *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   164
fun cross_inst insts = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   165
    let 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   166
      fun instL (ix, t) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   167
          map (fn (ix2,t2) => (ix2, Term.subst_vars ([], [(ix, t)]) t2));
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   168
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   169
      fun cross_instL ([], l) = rev l
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   170
        | cross_instL ((ix, t) :: insts, l) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   171
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   172
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   173
    in cross_instL (insts, []) end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   174
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   175
fun cross_inst_typs insts = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   176
    let 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   177
      fun instL (ix, ty) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   178
          map (fn (ix2,ty2) => (ix2, Term.typ_subst_TVars [(ix, ty)] ty2));
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   179
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   180
      fun cross_instL ([], l) = rev l
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   181
        | cross_instL ((ix, t) :: insts, l) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   182
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   183
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   184
    in cross_instL (insts, []) end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   185
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   186
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   187
(* assume that rule and target_thm have distinct var names *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   188
(* THINK: efficient version with tables for vars for: target vars,
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   189
introduced vars, and rule vars, for quicker instantiation? *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   190
(* The outerterm defines which part of the target_thm was modified *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   191
(* Note: we take Ts in the upterm order, ie last abstraction first.,
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   192
and with an outeterm where the abstracted subterm has the arguments in
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   193
the revered order, ie first abstraction first. *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   194
fun rw ((nonfixed_typinsts, unprepinsts), Ts, outerterm) rule target_thm = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   195
    let 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   196
      (* general signature info *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   197
      val target_sign = (Thm.sign_of_thm target_thm);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   198
      val ctermify = Thm.cterm_of target_sign;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   199
      val ctypeify = Thm.ctyp_of target_sign;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   200
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   201
      (* fix all non-instantiated tvars *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   202
      val (fixtyinsts, othertfrees) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   203
          mk_fixtvar_tyinsts (map fst nonfixed_typinsts) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   204
                             [Thm.prop_of rule, Thm.prop_of target_thm];
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   205
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   206
      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   207
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   208
      (* certified instantiations for types *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   209
      val ctyp_insts = map (apsnd ctypeify) typinsts;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   210
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   211
      (* type instantiated versions *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   212
      val tgt_th_tyinst = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   213
          Thm.instantiate (ctyp_insts, []) target_thm;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   214
      val rule_tyinst = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   215
          Thm.instantiate (ctyp_insts, []) rule;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   216
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   217
      (* type instanitated outer term *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   218
      val outerterm_tyinst = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   219
          Term.subst_vars (typinsts,[]) outerterm;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   220
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   221
      (* type-instantiate the var instantiations *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   222
      val insts_tyinst = foldr (fn ((ix,t),insts_tyinst) => 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   223
                            (ix, Term.subst_vars (typinsts,[]) t)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   224
                            :: insts_tyinst)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   225
                        (unprepinsts,[]);
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
      (* cross-instantiate *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   228
      val insts_tyinst_inst = cross_inst insts_tyinst;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   229
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   230
      (* create certms of instantiations *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   231
      val cinsts_tyinst = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   232
          map (fn (ix,t) => (ctermify (Var (ix, Term.type_of t)), 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   233
                             ctermify t)) insts_tyinst_inst;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   234
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   235
      (* The instantiated rule *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   236
      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   237
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   238
      (* Create a table of vars to be renamed after instantiation - ie
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   239
      other uninstantiated vars in the hyps the *instantiated* rule 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   240
      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   241
      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   242
                                   rule_inst;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   243
      val cterm_renamings = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   244
          map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
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
      (* Create the specific version of the rule for this target application *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   247
      val outerterm_inst = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   248
          outerterm_tyinst 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   249
            |> Term.subst_vars ([], insts_tyinst_inst)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   250
            |> Term.subst_vars ([], map (fn ((ix,ty),t) => (ix,t)) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   251
                                        renamings);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   252
      val couter_inst = Thm.reflexive (ctermify outerterm_inst);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   253
      val (cprems, abstract_rule_inst) = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   254
          rule_inst |> Thm.instantiate ([], cterm_renamings)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   255
                    |> mk_abstractedrule Ts;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   256
      val specific_tgt_rule = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   257
          beta_eta_contract_tac
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   258
            (Thm.combination couter_inst abstract_rule_inst);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   259
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   260
      (* create an instantiated version of the target thm *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   261
      val tgt_th_inst = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   262
          tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   263
                        |> Thm.instantiate ([], cterm_renamings);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   264
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   265
      val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   266
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   267
    in
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   268
      (beta_eta_contract_tac tgt_th_inst)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   269
        |> Thm.equal_elim specific_tgt_rule
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   270
        |> Drule.implies_intr_list cprems
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   271
        |> Drule.forall_intr_list frees_of_fixed_vars
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   272
        |> Drule.forall_elim_list vars
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   273
        |> fst o Thm.varifyT' othertfrees
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   274
        |> Drule.zero_var_indexes
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   275
    end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   276
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   277
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   278
end; (* struct *)