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