src/Tools/IsaPlanner/rw_inst.ML
changeset 52240 066c2ff17f7c
parent 52239 6a6033fa507c
child 52242 2d634bfa1bbf
     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;