1(* Title: Tools/IsaPlanner/rw_inst.ML 2 Author: Lucas Dixon, University of Edinburgh 3 4Rewriting using a conditional meta-equality theorem which supports 5schematic variable instantiation. 6*) 7 8signature RW_INST = 9sig 10 val rw: Proof.context -> 11 ((indexname * (sort * typ)) list * (* type var instantiations *) 12 (indexname * (typ * term)) list) (* schematic var instantiations *) 13 * (string * typ) list (* Fake named bounds + types *) 14 * (string * typ) list (* names of bound + types *) 15 * term -> (* outer term for instantiation *) 16 thm -> (* rule with indexes lifted *) 17 thm -> (* target thm *) 18 thm (* rewritten theorem possibly with additional premises for rule conditions *) 19end; 20 21structure RW_Inst: RW_INST = 22struct 23 24(* Given (string,type) pairs capturing the free vars that need to be 25allified in the assumption, and a theorem with assumptions possibly 26containing the free vars, then we give back the assumptions allified 27as hidden hyps. 28 29Given: x 30th: A vs ==> B vs 31Results in: "B vs" [!!x. A x] 32*) 33fun allify_conditions ctxt Ts th = 34 let 35 fun allify (x, T) t = 36 Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t)); 37 38 val cTs = map (Thm.cterm_of ctxt o Free) Ts; 39 val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th); 40 val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms; 41 in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; 42 43 44(* Given a list of variables that were bound, and a that has been 45instantiated with free variable placeholders for the bound vars, it 46creates an abstracted version of the theorem, with local bound vars as 47lambda-params: 48 49Ts: 50("x", ty) 51 52rule:: 53C :x ==> P :x = Q :x 54 55results in: 56("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) 57 58note: assumes rule is instantiated 59*) 60(* Note, we take abstraction in the order of last abstraction first *) 61fun mk_abstractedrule ctxt TsFake Ts rule = 62 let 63 (* now we change the names of temporary free vars that represent 64 bound vars with binders outside the redex *) 65 66 val ns = 67 IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts); 68 69 val (fromnames, tonames, Ts') = 70 fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') => 71 (Thm.cterm_of ctxt (Free(faken,ty)) :: rnf, 72 Thm.cterm_of ctxt (Free(n2,ty)) :: rnt, 73 (n2,ty) :: Ts'')) 74 (TsFake ~~ Ts ~~ ns) ([], [], []); 75 76 (* rename conflicting free's in the rule to avoid cconflicts 77 with introduced vars from bounds outside in redex *) 78 val rule' = rule 79 |> Drule.forall_intr_list fromnames 80 |> Drule.forall_elim_list tonames; 81 82 (* make unconditional rule and prems *) 83 val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule'; 84 85 (* using these names create lambda-abstracted version of the rule *) 86 val abstractions = rev (Ts' ~~ tonames); 87 val abstract_rule = 88 fold (fn ((n, ty), ct) => Thm.abstract_rule n ct) 89 abstractions uncond_rule; 90 in (cprems, abstract_rule) end; 91 92 93(* given names to avoid, and vars that need to be fixed, it gives 94unique new names to the vars so that they can be fixed as free 95variables *) 96(* make fixed unique free variable instantiations for non-ground vars *) 97(* Create a table of vars to be renamed after instantiation - ie 98 other uninstantiated vars in the hyps of the rule 99 ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) 100fun mk_renamings ctxt tgt rule_inst = 101 let 102 val rule_conds = Thm.prems_of rule_inst; 103 val (_, cond_vs) = 104 fold (fn t => fn (tyvs, vs) => 105 (union (op =) (Misc_Legacy.term_tvars t) tyvs, 106 union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []); 107 val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); 108 val vars_to_fix = union (op =) termvars cond_vs; 109 val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); 110 in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; 111 112(* make a new fresh typefree instantiation for the given tvar *) 113fun new_tfree (tv as (ix,sort)) (pairs, used) = 114 let val v = singleton (Name.variant_list used) (string_of_indexname ix) 115 in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; 116 117 118(* make instantiations to fix type variables that are not 119 already instantiated (in ignore_ixs) from the list of terms. *) 120fun mk_fixtvar_tyinsts ignore_insts ts = 121 let 122 val ignore_ixs = map fst ignore_insts; 123 val (tvars, tfrees) = 124 fold_rev (fn t => fn (varixs, tfrees) => 125 (Misc_Legacy.add_term_tvars (t,varixs), 126 Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []); 127 val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; 128 val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees) 129 in (fixtyinsts, tfrees) end; 130 131 132(* cross-instantiate the instantiations - ie for each instantiation 133replace all occurrences in other instantiations - no loops are possible 134and thus only one-parsing of the instantiations is necessary. *) 135fun cross_inst insts = 136 let 137 fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) => 138 (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); 139 140 fun cross_instL ([], l) = rev l 141 | cross_instL ((ix, t) :: insts, l) = 142 cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 143 144 in cross_instL (insts, []) end; 145 146(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *) 147fun cross_inst_typs insts = 148 let 149 fun instL (ix, (srt,ty)) = 150 map (fn (ix2,(srt2,ty2)) => (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); 151 152 fun cross_instL ([], l) = rev l 153 | cross_instL ((ix, t) :: insts, l) = 154 cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 155 156 in cross_instL (insts, []) end; 157 158 159(* assume that rule and target_thm have distinct var names. THINK: 160efficient version with tables for vars for: target vars, introduced 161vars, and rule vars, for quicker instantiation? The outerterm defines 162which part of the target_thm was modified. Note: we take Ts in the 163upterm order, ie last abstraction first., and with an outeterm where 164the abstracted subterm has the arguments in the revered order, ie 165first abstraction first. FakeTs has abstractions using the fake name 166- ie the name distinct from all other abstractions. *) 167 168fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 169 let 170 (* fix all non-instantiated tvars *) 171 val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) 172 mk_fixtvar_tyinsts nonfixed_typinsts 173 [Thm.prop_of rule, Thm.prop_of target_thm]; 174 val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); 175 176 (* certified instantiations for types *) 177 val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts; 178 179 (* type instantiated versions *) 180 val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; 181 val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; 182 183 val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts; 184 (* type instanitated outer term *) 185 val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; 186 187 val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs; 188 val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts; 189 190 (* type-instantiate the var instantiations *) 191 val insts_tyinst = 192 fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => 193 (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) 194 :: insts_tyinst) unprepinsts []; 195 196 (* cross-instantiate *) 197 val insts_tyinst_inst = cross_inst insts_tyinst; 198 199 (* create certms of instantiations *) 200 val cinsts_tyinst = 201 map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst; 202 203 (* The instantiated rule *) 204 val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); 205 206 (* Create a table of vars to be renamed after instantiation - ie 207 other uninstantiated vars in the hyps the *instantiated* rule 208 ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) 209 val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst; 210 val cterm_renamings = map (fn (x, y) => apply2 (Thm.cterm_of ctxt) (Var x, y)) renamings; 211 212 (* Create the specific version of the rule for this target application *) 213 val outerterm_inst = 214 outerterm_tyinst 215 |> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst) 216 |> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings); 217 val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst); 218 val (cprems, abstract_rule_inst) = 219 rule_inst 220 |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings) 221 |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; 222 val specific_tgt_rule = 223 Conv.fconv_rule Drule.beta_eta_conversion 224 (Thm.combination couter_inst abstract_rule_inst); 225 226 (* create an instantiated version of the target thm *) 227 val tgt_th_inst = 228 tgt_th_tyinst 229 |> Thm.instantiate ([], cinsts_tyinst) 230 |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings); 231 232 val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; 233 in 234 Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst 235 |> Thm.equal_elim specific_tgt_rule 236 |> Drule.implies_intr_list cprems 237 |> Drule.forall_intr_list frees_of_fixed_vars 238 |> Drule.forall_elim_list vars 239 |> Thm.varifyT_global' othertfrees 240 |-> K Drule.zero_var_indexes 241 end; 242 243end; 244