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