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