misc tuning;
authorwenzelm
Thu May 30 16:31:53 2013 +0200 (2013-05-30)
changeset 52240066c2ff17f7c
parent 52239 6a6033fa507c
child 52241 5f6e885382e9
misc tuning;
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 16:11:14 2013 +0200
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 16:31:53 2013 +0200
     1.3 @@ -7,20 +7,18 @@
     1.4  
     1.5  signature RW_INST =
     1.6  sig
     1.7 -  val rw : Proof.context ->
     1.8 -      ((indexname * (sort * typ)) list *  (* type var instantiations *)
     1.9 -       (indexname * (typ * term)) list)  (* schematic var instantiations *)
    1.10 -      * (string * typ) list           (* Fake named bounds + types *)
    1.11 -      * (string * typ) list           (* names of bound + types *)
    1.12 -      * term ->                       (* outer term for instantiation *)
    1.13 -      thm ->                           (* rule with indexies lifted *)
    1.14 -      thm ->                           (* target thm *)
    1.15 -      thm                              (* rewritten theorem possibly
    1.16 -                                          with additional premises for
    1.17 -                                          rule conditions *)
    1.18 +  val rw: Proof.context ->
    1.19 +    ((indexname * (sort * typ)) list * (* type var instantiations *)
    1.20 +     (indexname * (typ * term)) list) (* schematic var instantiations *)
    1.21 +    * (string * typ) list (* Fake named bounds + types *)
    1.22 +    * (string * typ) list (* names of bound + types *)
    1.23 +    * term -> (* outer term for instantiation *)
    1.24 +    thm -> (* rule with indexes lifted *)
    1.25 +    thm -> (* target thm *)
    1.26 +    thm  (* rewritten theorem possibly with additional premises for rule conditions *)
    1.27  end;
    1.28  
    1.29 -structure RWInst : RW_INST =
    1.30 +structure RW_Inst: RW_INST =
    1.31  struct
    1.32  
    1.33  (* Given a list of variables that were bound, and a that has been
    1.34 @@ -41,37 +39,37 @@
    1.35  *)
    1.36  (* Note, we take abstraction in the order of last abstraction first *)
    1.37  fun mk_abstractedrule ctxt TsFake Ts rule =
    1.38 -    let
    1.39 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
    1.40 +  let
    1.41 +    val cert = Thm.cterm_of (Thm.theory_of_thm rule);
    1.42  
    1.43 -      (* now we change the names of temporary free vars that represent
    1.44 -         bound vars with binders outside the redex *)
    1.45 +    (* now we change the names of temporary free vars that represent
    1.46 +       bound vars with binders outside the redex *)
    1.47  
    1.48 -      val ns =
    1.49 -        IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts);
    1.50 +    val ns =
    1.51 +      IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts);
    1.52  
    1.53 -      val (fromnames, tonames, Ts') =
    1.54 -          fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>
    1.55 -                      (ctermify (Free(faken,ty)) :: rnf,
    1.56 -                       ctermify (Free(n2,ty)) :: rnt,
    1.57 -                       (n2,ty) :: Ts''))
    1.58 -                (TsFake ~~ Ts ~~ ns) ([], [], []);
    1.59 +    val (fromnames, tonames, Ts') =
    1.60 +      fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>
    1.61 +              (cert (Free(faken,ty)) :: rnf,
    1.62 +               cert (Free(n2,ty)) :: rnt,
    1.63 +               (n2,ty) :: Ts''))
    1.64 +            (TsFake ~~ Ts ~~ ns) ([], [], []);
    1.65  
    1.66 -      (* rename conflicting free's in the rule to avoid cconflicts
    1.67 -      with introduced vars from bounds outside in redex *)
    1.68 -      val rule' = rule |> Drule.forall_intr_list fromnames
    1.69 -                       |> Drule.forall_elim_list tonames;
    1.70 +    (* rename conflicting free's in the rule to avoid cconflicts
    1.71 +    with introduced vars from bounds outside in redex *)
    1.72 +    val rule' = rule
    1.73 +      |> Drule.forall_intr_list fromnames
    1.74 +      |> Drule.forall_elim_list tonames;
    1.75  
    1.76 -      (* make unconditional rule and prems *)
    1.77 -      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
    1.78 -                                                          rule';
    1.79 +    (* make unconditional rule and prems *)
    1.80 +    val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule';
    1.81  
    1.82 -      (* using these names create lambda-abstracted version of the rule *)
    1.83 -      val abstractions = rev (Ts' ~~ tonames);
    1.84 -      val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
    1.85 -                                    Thm.abstract_rule n ct th)
    1.86 -                                (uncond_rule, abstractions);
    1.87 -    in (cprems, abstract_rule) end;
    1.88 +    (* using these names create lambda-abstracted version of the rule *)
    1.89 +    val abstractions = rev (Ts' ~~ tonames);
    1.90 +    val abstract_rule =
    1.91 +      Library.foldl (fn (th,((n,ty),ct)) => Thm.abstract_rule n ct th)
    1.92 +        (uncond_rule, abstractions);
    1.93 +  in (cprems, abstract_rule) end;
    1.94  
    1.95  
    1.96  (* given names to avoid, and vars that need to be fixed, it gives
    1.97 @@ -82,67 +80,63 @@
    1.98        other uninstantiated vars in the hyps of the rule
    1.99        ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   1.100  fun mk_renamings ctxt tgt rule_inst =
   1.101 -    let
   1.102 -      val rule_conds = Thm.prems_of rule_inst;
   1.103 -      val (_, cond_vs) =
   1.104 -          Library.foldl (fn ((tyvs, vs), t) =>
   1.105 -                    (union (op =) (Misc_Legacy.term_tvars t) tyvs,
   1.106 -                     union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
   1.107 -                (([],[]), rule_conds);
   1.108 -      val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
   1.109 -      val vars_to_fix = union (op =) termvars cond_vs;
   1.110 -      val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix);
   1.111 +  let
   1.112 +    val rule_conds = Thm.prems_of rule_inst;
   1.113 +    val (_, cond_vs) =
   1.114 +      Library.foldl (fn ((tyvs, vs), t) =>
   1.115 +                (union (op =) (Misc_Legacy.term_tvars t) tyvs,
   1.116 +                 union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
   1.117 +            (([], []), rule_conds);
   1.118 +    val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
   1.119 +    val vars_to_fix = union (op =) termvars cond_vs;
   1.120 +    val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix);
   1.121    in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end;
   1.122  
   1.123  (* make a new fresh typefree instantiation for the given tvar *)
   1.124  fun new_tfree (tv as (ix,sort), (pairs,used)) =
   1.125 -      let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   1.126 -      in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   1.127 +  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   1.128 +  in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
   1.129  
   1.130  
   1.131  (* make instantiations to fix type variables that are not
   1.132     already instantiated (in ignore_ixs) from the list of terms. *)
   1.133  fun mk_fixtvar_tyinsts ignore_insts ts =
   1.134 -    let
   1.135 -      val ignore_ixs = map fst ignore_insts;
   1.136 -      val (tvars, tfrees) =
   1.137 -            List.foldr (fn (t, (varixs, tfrees)) =>
   1.138 -                      (Misc_Legacy.add_term_tvars (t,varixs),
   1.139 -                       Misc_Legacy.add_term_tfrees (t,tfrees)))
   1.140 -                  ([],[]) ts;
   1.141 -        val unfixed_tvars =
   1.142 -            filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
   1.143 -        val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
   1.144 -    in (fixtyinsts, tfrees) end;
   1.145 +  let
   1.146 +    val ignore_ixs = map fst ignore_insts;
   1.147 +    val (tvars, tfrees) =
   1.148 +      List.foldr (fn (t, (varixs, tfrees)) =>
   1.149 +        (Misc_Legacy.add_term_tvars (t,varixs),
   1.150 +         Misc_Legacy.add_term_tfrees (t,tfrees))) ([],[]) ts;
   1.151 +    val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
   1.152 +    val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
   1.153 +  in (fixtyinsts, tfrees) end;
   1.154  
   1.155  
   1.156  (* cross-instantiate the instantiations - ie for each instantiation
   1.157  replace all occurances in other instantiations - no loops are possible
   1.158  and thus only one-parsing of the instantiations is necessary. *)
   1.159  fun cross_inst insts =
   1.160 -    let
   1.161 -      fun instL (ix, (ty,t)) =
   1.162 -          map (fn (ix2,(ty2,t2)) =>
   1.163 -                  (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
   1.164 +  let
   1.165 +    fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) =>
   1.166 +      (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
   1.167  
   1.168 -      fun cross_instL ([], l) = rev l
   1.169 -        | cross_instL ((ix, t) :: insts, l) =
   1.170 +    fun cross_instL ([], l) = rev l
   1.171 +      | cross_instL ((ix, t) :: insts, l) =
   1.172            cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   1.173  
   1.174 -    in cross_instL (insts, []) end;
   1.175 +  in cross_instL (insts, []) end;
   1.176  
   1.177  (* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
   1.178  fun cross_inst_typs insts =
   1.179 -    let
   1.180 -      fun instL (ix, (srt,ty)) =
   1.181 -          map (fn (ix2,(srt2,ty2)) =>
   1.182 -                  (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
   1.183 +  let
   1.184 +    fun instL (ix, (srt,ty)) =
   1.185 +      map (fn (ix2,(srt2,ty2)) => (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
   1.186  
   1.187 -      fun cross_instL ([], l) = rev l
   1.188 -        | cross_instL ((ix, t) :: insts, l) =
   1.189 +    fun cross_instL ([], l) = rev l
   1.190 +      | cross_instL ((ix, t) :: insts, l) =
   1.191            cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   1.192  
   1.193 -    in cross_instL (insts, []) end;
   1.194 +  in cross_instL (insts, []) end;
   1.195  
   1.196  
   1.197  (* assume that rule and target_thm have distinct var names. THINK:
   1.198 @@ -155,90 +149,83 @@
   1.199  - ie the name distinct from all other abstractions. *)
   1.200  
   1.201  fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
   1.202 -    let
   1.203 -      (* general signature info *)
   1.204 -      val target_sign = (Thm.theory_of_thm target_thm);
   1.205 -      val ctermify = Thm.cterm_of target_sign;
   1.206 -      val ctypeify = Thm.ctyp_of target_sign;
   1.207 +  let
   1.208 +    val thy = Thm.theory_of_thm target_thm;
   1.209 +    val cert = Thm.cterm_of thy;
   1.210 +    val certT = Thm.ctyp_of thy;
   1.211  
   1.212 -      (* fix all non-instantiated tvars *)
   1.213 -      val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)
   1.214 -          mk_fixtvar_tyinsts nonfixed_typinsts
   1.215 -                             [Thm.prop_of rule, Thm.prop_of target_thm];
   1.216 -      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   1.217 +    (* fix all non-instantiated tvars *)
   1.218 +    val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)
   1.219 +      mk_fixtvar_tyinsts nonfixed_typinsts
   1.220 +        [Thm.prop_of rule, Thm.prop_of target_thm];
   1.221 +    val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   1.222  
   1.223 -      (* certified instantiations for types *)
   1.224 -      val ctyp_insts =
   1.225 -          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
   1.226 -              typinsts;
   1.227 +    (* certified instantiations for types *)
   1.228 +    val ctyp_insts = map (fn (ix, (s, ty)) => (certT (TVar (ix, s)), certT ty)) typinsts;
   1.229 +
   1.230 +    (* type instantiated versions *)
   1.231 +    val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   1.232 +    val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
   1.233  
   1.234 -      (* type instantiated versions *)
   1.235 -      val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   1.236 -      val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
   1.237 +    val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
   1.238 +    (* type instanitated outer term *)
   1.239 +    val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
   1.240  
   1.241 -      val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
   1.242 -      (* type instanitated outer term *)
   1.243 -      val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
   1.244 +    val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs;
   1.245 +    val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts;
   1.246  
   1.247 -      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
   1.248 -                              FakeTs;
   1.249 -      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
   1.250 -                          Ts;
   1.251 +    (* type-instantiate the var instantiations *)
   1.252 +    val insts_tyinst =
   1.253 +      List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
   1.254 +        (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t))
   1.255 +          :: insts_tyinst)
   1.256 +        [] unprepinsts;
   1.257  
   1.258 -      (* type-instantiate the var instantiations *)
   1.259 -      val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
   1.260 -                            (ix, (Term.typ_subst_TVars term_typ_inst ty,
   1.261 -                                  Term.subst_TVars term_typ_inst t))
   1.262 -                            :: insts_tyinst)
   1.263 -                        [] unprepinsts;
   1.264 +    (* cross-instantiate *)
   1.265 +    val insts_tyinst_inst = cross_inst insts_tyinst;
   1.266  
   1.267 -      (* cross-instantiate *)
   1.268 -      val insts_tyinst_inst = cross_inst insts_tyinst;
   1.269 +    (* create certms of instantiations *)
   1.270 +    val cinsts_tyinst =
   1.271 +      map (fn (ix, (ty, t)) => (cert (Var (ix, ty)), cert t)) insts_tyinst_inst;
   1.272  
   1.273 -      (* create certms of instantiations *)
   1.274 -      val cinsts_tyinst =
   1.275 -          map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
   1.276 -                                  ctermify t)) insts_tyinst_inst;
   1.277 +    (* The instantiated rule *)
   1.278 +    val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   1.279  
   1.280 -      (* The instantiated rule *)
   1.281 -      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   1.282 -
   1.283 -      (* Create a table of vars to be renamed after instantiation - ie
   1.284 -      other uninstantiated vars in the hyps the *instantiated* rule
   1.285 -      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   1.286 -      val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst;
   1.287 -      val cterm_renamings =
   1.288 -          map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
   1.289 +    (* Create a table of vars to be renamed after instantiation - ie
   1.290 +    other uninstantiated vars in the hyps the *instantiated* rule
   1.291 +    ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   1.292 +    val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst;
   1.293 +    val cterm_renamings = map (fn (x, y) => (cert (Var x), cert y)) renamings;
   1.294  
   1.295 -      (* Create the specific version of the rule for this target application *)
   1.296 -      val outerterm_inst =
   1.297 -          outerterm_tyinst
   1.298 -            |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
   1.299 -            |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
   1.300 -      val couter_inst = Thm.reflexive (ctermify outerterm_inst);
   1.301 -      val (cprems, abstract_rule_inst) =
   1.302 -          rule_inst |> Thm.instantiate ([], cterm_renamings)
   1.303 -                    |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
   1.304 -      val specific_tgt_rule =
   1.305 -          Conv.fconv_rule Drule.beta_eta_conversion
   1.306 -            (Thm.combination couter_inst abstract_rule_inst);
   1.307 +    (* Create the specific version of the rule for this target application *)
   1.308 +    val outerterm_inst =
   1.309 +      outerterm_tyinst
   1.310 +      |> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst)
   1.311 +      |> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings);
   1.312 +    val couter_inst = Thm.reflexive (cert outerterm_inst);
   1.313 +    val (cprems, abstract_rule_inst) =
   1.314 +      rule_inst
   1.315 +      |> Thm.instantiate ([], cterm_renamings)
   1.316 +      |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
   1.317 +    val specific_tgt_rule =
   1.318 +      Conv.fconv_rule Drule.beta_eta_conversion
   1.319 +        (Thm.combination couter_inst abstract_rule_inst);
   1.320  
   1.321 -      (* create an instantiated version of the target thm *)
   1.322 -      val tgt_th_inst =
   1.323 -          tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
   1.324 -                        |> Thm.instantiate ([], cterm_renamings);
   1.325 -
   1.326 -      val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   1.327 +    (* create an instantiated version of the target thm *)
   1.328 +    val tgt_th_inst =
   1.329 +      tgt_th_tyinst
   1.330 +      |> Thm.instantiate ([], cinsts_tyinst)
   1.331 +      |> Thm.instantiate ([], cterm_renamings);
   1.332  
   1.333 -    in
   1.334 -      Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst
   1.335 -        |> Thm.equal_elim specific_tgt_rule
   1.336 -        |> Drule.implies_intr_list cprems
   1.337 -        |> Drule.forall_intr_list frees_of_fixed_vars
   1.338 -        |> Drule.forall_elim_list vars
   1.339 -        |> Thm.varifyT_global' othertfrees
   1.340 -        |-> K Drule.zero_var_indexes
   1.341 -    end;
   1.342 -
   1.343 +    val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   1.344 +  in
   1.345 +    Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst
   1.346 +    |> Thm.equal_elim specific_tgt_rule
   1.347 +    |> Drule.implies_intr_list cprems
   1.348 +    |> Drule.forall_intr_list frees_of_fixed_vars
   1.349 +    |> Drule.forall_elim_list vars
   1.350 +    |> Thm.varifyT_global' othertfrees
   1.351 +    |-> K Drule.zero_var_indexes
   1.352 +  end;
   1.353  
   1.354  end;
     2.1 --- a/src/Tools/eqsubst.ML	Thu May 30 16:11:14 2013 +0200
     2.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 16:31:53 2013 +0200
     2.3 @@ -123,7 +123,7 @@
     2.4  (* before matching we need to fake the bound vars that are missing an
     2.5     abstraction. In this function we additionally construct the
     2.6     abstraction environment, and an outer context term (with the focus
     2.7 -   abstracted out) for use in rewriting with RWInst.rw *)
     2.8 +   abstracted out) for use in rewriting with RW_Inst.rw *)
     2.9  fun prep_zipper_match z =
    2.10    let
    2.11      val t = Zipper.trm z
    2.12 @@ -245,7 +245,7 @@
    2.13  (* m is instantiation/match information *)
    2.14  (* rule is the equation for substitution *)
    2.15  fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
    2.16 -  RWInst.rw ctxt m rule conclthm
    2.17 +  RW_Inst.rw ctxt m rule conclthm
    2.18    |> IsaND.unfix_frees cfvs
    2.19    |> Conv.fconv_rule Drule.beta_eta_conversion
    2.20    |> (fn r => Tactic.rtac r i st);
    2.21 @@ -323,7 +323,7 @@
    2.22    let
    2.23      val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
    2.24      val preelimrule =
    2.25 -      RWInst.rw ctxt m rule pth
    2.26 +      RW_Inst.rw ctxt m rule pth
    2.27        |> (Seq.hd o prune_params_tac)
    2.28        |> Thm.permute_prems 0 ~1 (* put old asm first *)
    2.29        |> IsaND.unfix_frees cfvs (* unfix any global params *)