src/Provers/IsaPlanner/rw_inst.ML
changeset 23171 861f63a35d31
parent 23170 94e9413bd7fc
child 23172 f1ae6a8648ef
     1.1 --- a/src/Provers/IsaPlanner/rw_inst.ML	Thu May 31 19:11:19 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,315 +0,0 @@
     1.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      Pure/IsaPlanner/rw_inst.ML
     1.6 -    ID:         $Id$
     1.7 -    Author:     Lucas Dixon, University of Edinburgh
     1.8 -                lucas.dixon@ed.ac.uk
     1.9 -    Created:    25 Aug 2004
    1.10 -*)
    1.11 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.12 -(*  DESCRIPTION:
    1.13 -
    1.14 -    rewriting using a conditional meta-equality theorem which supports 
    1.15 -    schematic variable instantiation.
    1.16 -
    1.17 -*)   
    1.18 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    1.19 -signature RW_INST =
    1.20 -sig
    1.21 -
    1.22 -  (* Rewrite: give it instantiation infromation, a rule, and the
    1.23 -  target thm, and it will return the rewritten target thm *)
    1.24 -  val rw :
    1.25 -      ((Term.indexname * (Term.sort * Term.typ)) list *  (* type var instantiations *)
    1.26 -       (Term.indexname * (Term.typ * Term.term)) list)  (* schematic var instantiations *)
    1.27 -      * (string * Term.typ) list           (* Fake named bounds + types *)
    1.28 -      * (string * Term.typ) list           (* names of bound + types *)
    1.29 -      * Term.term ->                       (* outer term for instantiation *)
    1.30 -      Thm.thm ->                           (* rule with indexies lifted *)
    1.31 -      Thm.thm ->                           (* target thm *)
    1.32 -      Thm.thm                              (* rewritten theorem possibly 
    1.33 -                                              with additional premises for 
    1.34 -                                              rule conditions *)
    1.35 -
    1.36 -  (* used tools *)
    1.37 -  val mk_abstractedrule :
    1.38 -      (string * Term.typ) list (* faked outer bound *)
    1.39 -      -> (string * Term.typ) list (* hopeful name of outer bounds *)
    1.40 -      -> Thm.thm -> Thm.cterm list * Thm.thm
    1.41 -  val mk_fixtvar_tyinsts :
    1.42 -      (Term.indexname * (Term.sort * Term.typ)) list ->
    1.43 -      Term.term list -> ((string * int) * (Term.sort * Term.typ)) list 
    1.44 -                        * (string * Term.sort) list
    1.45 -  val mk_renamings :
    1.46 -      Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
    1.47 -  val new_tfree :
    1.48 -      ((string * int) * Term.sort) *
    1.49 -      (((string * int) * (Term.sort * Term.typ)) list * string list) ->
    1.50 -      ((string * int) * (Term.sort * Term.typ)) list * string list
    1.51 -  val cross_inst : (Term.indexname * (Term.typ * Term.term)) list 
    1.52 -                   -> (Term.indexname *(Term.typ * Term.term)) list
    1.53 -  val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list 
    1.54 -                   -> (Term.indexname * (Term.sort * Term.typ)) list
    1.55 -
    1.56 -  val beta_contract : Thm.thm -> Thm.thm
    1.57 -  val beta_eta_contract : Thm.thm -> Thm.thm
    1.58 -
    1.59 -end;
    1.60 -
    1.61 -structure RWInst 
    1.62 -: RW_INST
    1.63 -= struct
    1.64 -
    1.65 -
    1.66 -(* beta contract the theorem *)
    1.67 -fun beta_contract thm = 
    1.68 -    equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
    1.69 -
    1.70 -(* beta-eta contract the theorem *)
    1.71 -fun beta_eta_contract thm = 
    1.72 -    let
    1.73 -      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    1.74 -      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    1.75 -    in thm3 end;
    1.76 -
    1.77 -
    1.78 -(* to get the free names of a theorem (including hyps and flexes) *)
    1.79 -fun usednames_of_thm th =
    1.80 -    let val rep = Thm.rep_thm th
    1.81 -      val hyps = #hyps rep
    1.82 -      val (tpairl,tpairr) = Library.split_list (#tpairs rep)
    1.83 -      val prop = #prop rep
    1.84 -    in
    1.85 -      List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    1.86 -    end;
    1.87 -
    1.88 -(* Given a list of variables that were bound, and a that has been
    1.89 -instantiated with free variable placeholders for the bound vars, it
    1.90 -creates an abstracted version of the theorem, with local bound vars as
    1.91 -lambda-params:
    1.92 -
    1.93 -Ts: 
    1.94 -("x", ty)
    1.95 -
    1.96 -rule::
    1.97 -C :x ==> P :x = Q :x
    1.98 -
    1.99 -results in:
   1.100 -("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
   1.101 -
   1.102 -note: assumes rule is instantiated
   1.103 -*)
   1.104 -(* Note, we take abstraction in the order of last abstraction first *)
   1.105 -fun mk_abstractedrule TsFake Ts rule = 
   1.106 -    let 
   1.107 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
   1.108 -
   1.109 -      (* now we change the names of temporary free vars that represent 
   1.110 -         bound vars with binders outside the redex *)
   1.111 -      val prop = Thm.prop_of rule;
   1.112 -      val names = usednames_of_thm rule;
   1.113 -      val (fromnames,tonames,names2,Ts') = 
   1.114 -          Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
   1.115 -                    let val n2 = Name.variant names n in
   1.116 -                      (ctermify (Free(faken,ty)) :: rnf,
   1.117 -                       ctermify (Free(n2,ty)) :: rnt, 
   1.118 -                       n2 :: names,
   1.119 -                       (n2,ty) :: Ts'')
   1.120 -                    end)
   1.121 -                (([],[],names, []), TsFake~~Ts);
   1.122 -
   1.123 -      (* rename conflicting free's in the rule to avoid cconflicts
   1.124 -      with introduced vars from bounds outside in redex *)
   1.125 -      val rule' = rule |> Drule.forall_intr_list fromnames
   1.126 -                       |> Drule.forall_elim_list tonames;
   1.127 -      
   1.128 -      (* make unconditional rule and prems *)
   1.129 -      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
   1.130 -                                                          rule';
   1.131 -
   1.132 -      (* using these names create lambda-abstracted version of the rule *)
   1.133 -      val abstractions = rev (Ts' ~~ tonames);
   1.134 -      val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
   1.135 -                                    Thm.abstract_rule n ct th)
   1.136 -                                (uncond_rule, abstractions);
   1.137 -    in (cprems, abstract_rule) end;
   1.138 -
   1.139 -
   1.140 -(* given names to avoid, and vars that need to be fixed, it gives
   1.141 -unique new names to the vars so that they can be fixed as free
   1.142 -variables *)
   1.143 -(* make fixed unique free variable instantiations for non-ground vars *)
   1.144 -(* Create a table of vars to be renamed after instantiation - ie
   1.145 -      other uninstantiated vars in the hyps of the rule 
   1.146 -      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   1.147 -fun mk_renamings tgt rule_inst = 
   1.148 -    let
   1.149 -      val rule_conds = Thm.prems_of rule_inst
   1.150 -      val names = foldr Term.add_term_names [] (tgt :: rule_conds);
   1.151 -      val (conds_tyvs,cond_vs) = 
   1.152 -          Library.foldl (fn ((tyvs, vs), t) => 
   1.153 -                    (Library.union
   1.154 -                       (Term.term_tvars t, tyvs),
   1.155 -                     Library.union 
   1.156 -                       (map Term.dest_Var (Term.term_vars t), vs))) 
   1.157 -                (([],[]), rule_conds);
   1.158 -      val termvars = map Term.dest_Var (Term.term_vars tgt); 
   1.159 -      val vars_to_fix = Library.union (termvars, cond_vs);
   1.160 -      val (renamings, names2) = 
   1.161 -          foldr (fn (((n,i),ty), (vs, names')) => 
   1.162 -                    let val n' = Name.variant names' n in
   1.163 -                      ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   1.164 -                    end)
   1.165 -                ([], names) vars_to_fix;
   1.166 -    in renamings end;
   1.167 -
   1.168 -(* make a new fresh typefree instantiation for the given tvar *)
   1.169 -fun new_tfree (tv as (ix,sort), (pairs,used)) =
   1.170 -      let val v = Name.variant used (string_of_indexname ix)
   1.171 -      in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   1.172 -
   1.173 -
   1.174 -(* make instantiations to fix type variables that are not 
   1.175 -   already instantiated (in ignore_ixs) from the list of terms. *)
   1.176 -fun mk_fixtvar_tyinsts ignore_insts ts = 
   1.177 -    let 
   1.178 -      val ignore_ixs = map fst ignore_insts;
   1.179 -      val (tvars, tfrees) = 
   1.180 -            foldr (fn (t, (varixs, tfrees)) => 
   1.181 -                      (Term.add_term_tvars (t,varixs),
   1.182 -                       Term.add_term_tfrees (t,tfrees)))
   1.183 -                  ([],[]) ts;
   1.184 -        val unfixed_tvars = 
   1.185 -            List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
   1.186 -        val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
   1.187 -    in (fixtyinsts, tfrees) end;
   1.188 -
   1.189 -
   1.190 -(* cross-instantiate the instantiations - ie for each instantiation
   1.191 -replace all occurances in other instantiations - no loops are possible
   1.192 -and thus only one-parsing of the instantiations is necessary. *)
   1.193 -fun cross_inst insts = 
   1.194 -    let 
   1.195 -      fun instL (ix, (ty,t)) = 
   1.196 -          map (fn (ix2,(ty2,t2)) => 
   1.197 -                  (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
   1.198 -
   1.199 -      fun cross_instL ([], l) = rev l
   1.200 -        | cross_instL ((ix, t) :: insts, l) = 
   1.201 -          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   1.202 -
   1.203 -    in cross_instL (insts, []) end;
   1.204 -
   1.205 -(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
   1.206 -fun cross_inst_typs insts = 
   1.207 -    let 
   1.208 -      fun instL (ix, (srt,ty)) = 
   1.209 -          map (fn (ix2,(srt2,ty2)) => 
   1.210 -                  (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
   1.211 -
   1.212 -      fun cross_instL ([], l) = rev l
   1.213 -        | cross_instL ((ix, t) :: insts, l) = 
   1.214 -          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   1.215 -
   1.216 -    in cross_instL (insts, []) end;
   1.217 -
   1.218 -
   1.219 -(* assume that rule and target_thm have distinct var names. THINK:
   1.220 -efficient version with tables for vars for: target vars, introduced
   1.221 -vars, and rule vars, for quicker instantiation?  The outerterm defines
   1.222 -which part of the target_thm was modified.  Note: we take Ts in the
   1.223 -upterm order, ie last abstraction first., and with an outeterm where
   1.224 -the abstracted subterm has the arguments in the revered order, ie
   1.225 -first abstraction first.  FakeTs has abstractions using the fake name
   1.226 -- ie the name distinct from all other abstractions. *)
   1.227 -
   1.228 -fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
   1.229 -    let 
   1.230 -      (* general signature info *)
   1.231 -      val target_sign = (Thm.theory_of_thm target_thm);
   1.232 -      val ctermify = Thm.cterm_of target_sign;
   1.233 -      val ctypeify = Thm.ctyp_of target_sign;
   1.234 -
   1.235 -      (* fix all non-instantiated tvars *)
   1.236 -      val (fixtyinsts, othertfrees) = 
   1.237 -          mk_fixtvar_tyinsts nonfixed_typinsts
   1.238 -                             [Thm.prop_of rule, Thm.prop_of target_thm];
   1.239 -      val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
   1.240 -                               fixtyinsts;
   1.241 -      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   1.242 -
   1.243 -      (* certified instantiations for types *)
   1.244 -      val ctyp_insts = 
   1.245 -          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
   1.246 -              typinsts;
   1.247 -
   1.248 -      (* type instantiated versions *)
   1.249 -      val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   1.250 -      val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
   1.251 -
   1.252 -      val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
   1.253 -      (* type instanitated outer term *)
   1.254 -      val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
   1.255 -
   1.256 -      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   1.257 -                              FakeTs;
   1.258 -      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   1.259 -                          Ts;
   1.260 -
   1.261 -      (* type-instantiate the var instantiations *)
   1.262 -      val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
   1.263 -                            (ix, (Term.typ_subst_TVars term_typ_inst ty, 
   1.264 -                                  Term.subst_TVars term_typ_inst t))
   1.265 -                            :: insts_tyinst)
   1.266 -                        [] unprepinsts;
   1.267 -
   1.268 -      (* cross-instantiate *)
   1.269 -      val insts_tyinst_inst = cross_inst insts_tyinst;
   1.270 -
   1.271 -      (* create certms of instantiations *)
   1.272 -      val cinsts_tyinst = 
   1.273 -          map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
   1.274 -                                  ctermify t)) insts_tyinst_inst;
   1.275 -
   1.276 -      (* The instantiated rule *)
   1.277 -      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   1.278 -
   1.279 -      (* Create a table of vars to be renamed after instantiation - ie
   1.280 -      other uninstantiated vars in the hyps the *instantiated* rule 
   1.281 -      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   1.282 -      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
   1.283 -                                   rule_inst;
   1.284 -      val cterm_renamings = 
   1.285 -          map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
   1.286 -
   1.287 -      (* Create the specific version of the rule for this target application *)
   1.288 -      val outerterm_inst = 
   1.289 -          outerterm_tyinst 
   1.290 -            |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
   1.291 -            |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
   1.292 -      val couter_inst = Thm.reflexive (ctermify outerterm_inst);
   1.293 -      val (cprems, abstract_rule_inst) = 
   1.294 -          rule_inst |> Thm.instantiate ([], cterm_renamings)
   1.295 -                    |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
   1.296 -      val specific_tgt_rule = 
   1.297 -          beta_eta_contract
   1.298 -            (Thm.combination couter_inst abstract_rule_inst);
   1.299 -
   1.300 -      (* create an instantiated version of the target thm *)
   1.301 -      val tgt_th_inst = 
   1.302 -          tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
   1.303 -                        |> Thm.instantiate ([], cterm_renamings);
   1.304 -
   1.305 -      val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   1.306 -
   1.307 -    in
   1.308 -      (beta_eta_contract tgt_th_inst)
   1.309 -        |> Thm.equal_elim specific_tgt_rule
   1.310 -        |> Drule.implies_intr_list cprems
   1.311 -        |> Drule.forall_intr_list frees_of_fixed_vars
   1.312 -        |> Drule.forall_elim_list vars
   1.313 -        |> Thm.varifyT' othertfrees
   1.314 -        |-> K Drule.zero_var_indexes
   1.315 -    end;
   1.316 -
   1.317 -
   1.318 -end; (* struct *)