--- a/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 17:26:05 2012 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 22:00:29 2012 +0200
@@ -3,61 +3,34 @@
Rewriting using a conditional meta-equality theorem which supports
schematic variable instantiation.
-*)
+*)
signature RW_INST =
sig
+ val beta_eta_contract : thm -> thm
+
(* Rewrite: give it instantiation infromation, a rule, and the
target thm, and it will return the rewritten target thm *)
val rw :
- ((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *)
- (Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *)
- * (string * Term.typ) list (* Fake named bounds + types *)
- * (string * Term.typ) list (* names of bound + types *)
- * Term.term -> (* outer term for instantiation *)
- Thm.thm -> (* rule with indexies lifted *)
- Thm.thm -> (* target thm *)
- Thm.thm (* rewritten theorem possibly
- with additional premises for
- rule conditions *)
-
- (* used tools *)
- val mk_abstractedrule :
- (string * Term.typ) list (* faked outer bound *)
- -> (string * Term.typ) list (* hopeful name of outer bounds *)
- -> Thm.thm -> Thm.cterm list * Thm.thm
- val mk_fixtvar_tyinsts :
- (Term.indexname * (Term.sort * Term.typ)) list ->
- Term.term list -> ((string * int) * (Term.sort * Term.typ)) list
- * (string * Term.sort) list
- val mk_renamings :
- Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
- val new_tfree :
- ((string * int) * Term.sort) *
- (((string * int) * (Term.sort * Term.typ)) list * string list) ->
- ((string * int) * (Term.sort * Term.typ)) list * string list
- val cross_inst : (Term.indexname * (Term.typ * Term.term)) list
- -> (Term.indexname *(Term.typ * Term.term)) list
- val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list
- -> (Term.indexname * (Term.sort * Term.typ)) list
-
- val beta_contract : Thm.thm -> Thm.thm
- val beta_eta_contract : Thm.thm -> Thm.thm
-
+ ((indexname * (sort * typ)) list * (* type var instantiations *)
+ (indexname * (typ * term)) list) (* schematic var instantiations *)
+ * (string * typ) list (* Fake named bounds + types *)
+ * (string * typ) list (* names of bound + types *)
+ * term -> (* outer term for instantiation *)
+ thm -> (* rule with indexies lifted *)
+ thm -> (* target thm *)
+ thm (* rewritten theorem possibly
+ with additional premises for
+ rule conditions *)
end;
-structure RWInst
-: RW_INST
-= struct
+structure RWInst : RW_INST =
+struct
-(* beta contract the theorem *)
-fun beta_contract thm =
- Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
-
(* beta-eta contract the theorem *)
-fun beta_eta_contract thm =
+fun beta_eta_contract thm =
let
val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
@@ -79,7 +52,7 @@
creates an abstracted version of the theorem, with local bound vars as
lambda-params:
-Ts:
+Ts:
("x", ty)
rule::
@@ -91,19 +64,18 @@
note: assumes rule is instantiated
*)
(* Note, we take abstraction in the order of last abstraction first *)
-fun mk_abstractedrule TsFake Ts rule =
- let
+fun mk_abstractedrule TsFake Ts rule =
+ let
val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
- (* now we change the names of temporary free vars that represent
+ (* now we change the names of temporary free vars that represent
bound vars with binders outside the redex *)
- val prop = Thm.prop_of rule;
val names = usednames_of_thm rule;
- val (fromnames,tonames,names2,Ts') =
- Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
+ val (fromnames,tonames,_,Ts') =
+ Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
let val n2 = singleton (Name.variant_list names) n in
(ctermify (Free(faken,ty)) :: rnf,
- ctermify (Free(n2,ty)) :: rnt,
+ ctermify (Free(n2,ty)) :: rnt,
n2 :: names,
(n2,ty) :: Ts'')
end)
@@ -113,14 +85,14 @@
with introduced vars from bounds outside in redex *)
val rule' = rule |> Drule.forall_intr_list fromnames
|> Drule.forall_elim_list tonames;
-
+
(* make unconditional rule and prems *)
- val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
+ val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
rule';
(* using these names create lambda-abstracted version of the rule *)
val abstractions = rev (Ts' ~~ tonames);
- val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
+ val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
Thm.abstract_rule n ct th)
(uncond_rule, abstractions);
in (cprems, abstract_rule) end;
@@ -131,21 +103,21 @@
variables *)
(* make fixed unique free variable instantiations for non-ground vars *)
(* Create a table of vars to be renamed after instantiation - ie
- other uninstantiated vars in the hyps of the rule
+ other uninstantiated vars in the hyps of the rule
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
-fun mk_renamings tgt rule_inst =
+fun mk_renamings tgt rule_inst =
let
val rule_conds = Thm.prems_of rule_inst
val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
- val (conds_tyvs,cond_vs) =
- Library.foldl (fn ((tyvs, vs), t) =>
+ val (_, cond_vs) =
+ Library.foldl (fn ((tyvs, vs), t) =>
(union (op =) (Misc_Legacy.term_tvars t) tyvs,
union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
(([],[]), rule_conds);
- val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
+ val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
val vars_to_fix = union (op =) termvars cond_vs;
- val (renamings, names2) =
- List.foldr (fn (((n,i),ty), (vs, names')) =>
+ val (renamings, _) =
+ List.foldr (fn (((n,i),ty), (vs, names')) =>
let val n' = singleton (Name.variant_list names') n in
((((n,i),ty), Free (n', ty)) :: vs, n'::names')
end)
@@ -158,17 +130,17 @@
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
-(* make instantiations to fix type variables that are not
+(* make instantiations to fix type variables that are not
already instantiated (in ignore_ixs) from the list of terms. *)
-fun mk_fixtvar_tyinsts ignore_insts ts =
- let
+fun mk_fixtvar_tyinsts ignore_insts ts =
+ let
val ignore_ixs = map fst ignore_insts;
- val (tvars, tfrees) =
- List.foldr (fn (t, (varixs, tfrees)) =>
+ val (tvars, tfrees) =
+ List.foldr (fn (t, (varixs, tfrees)) =>
(Misc_Legacy.add_term_tvars (t,varixs),
Misc_Legacy.add_term_tfrees (t,tfrees)))
([],[]) ts;
- val unfixed_tvars =
+ val unfixed_tvars =
filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
in (fixtyinsts, tfrees) end;
@@ -177,27 +149,27 @@
(* cross-instantiate the instantiations - ie for each instantiation
replace all occurances in other instantiations - no loops are possible
and thus only one-parsing of the instantiations is necessary. *)
-fun cross_inst insts =
- let
- fun instL (ix, (ty,t)) =
- map (fn (ix2,(ty2,t2)) =>
+fun cross_inst insts =
+ let
+ fun instL (ix, (ty,t)) =
+ map (fn (ix2,(ty2,t2)) =>
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
fun cross_instL ([], l) = rev l
- | cross_instL ((ix, t) :: insts, l) =
+ | cross_instL ((ix, t) :: insts, l) =
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
in cross_instL (insts, []) end;
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
-fun cross_inst_typs insts =
- let
- fun instL (ix, (srt,ty)) =
- map (fn (ix2,(srt2,ty2)) =>
+fun cross_inst_typs insts =
+ let
+ fun instL (ix, (srt,ty)) =
+ map (fn (ix2,(srt2,ty2)) =>
(ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
fun cross_instL ([], l) = rev l
- | cross_instL ((ix, t) :: insts, l) =
+ | cross_instL ((ix, t) :: insts, l) =
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
in cross_instL (insts, []) end;
@@ -212,42 +184,40 @@
first abstraction first. FakeTs has abstractions using the fake name
- ie the name distinct from all other abstractions. *)
-fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
- let
+fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
+ let
(* general signature info *)
val target_sign = (Thm.theory_of_thm target_thm);
val ctermify = Thm.cterm_of target_sign;
val ctypeify = Thm.ctyp_of target_sign;
(* fix all non-instantiated tvars *)
- val (fixtyinsts, othertfrees) =
+ val (fixtyinsts, othertfrees) =
mk_fixtvar_tyinsts nonfixed_typinsts
[Thm.prop_of rule, Thm.prop_of target_thm];
- val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
- fixtyinsts;
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
(* certified instantiations for types *)
- val ctyp_insts =
- map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
+ val ctyp_insts =
+ map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
typinsts;
(* type instantiated versions *)
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule;
- val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
+ val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
(* type instanitated outer term *)
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
- val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
+ val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
FakeTs;
- val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
+ val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
Ts;
(* type-instantiate the var instantiations *)
- val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
- (ix, (Term.typ_subst_TVars term_typ_inst ty,
+ val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
+ (ix, (Term.typ_subst_TVars term_typ_inst ty,
Term.subst_TVars term_typ_inst t))
:: insts_tyinst)
[] unprepinsts;
@@ -256,36 +226,36 @@
val insts_tyinst_inst = cross_inst insts_tyinst;
(* create certms of instantiations *)
- val cinsts_tyinst =
- map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
+ val cinsts_tyinst =
+ map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
ctermify t)) insts_tyinst_inst;
(* The instantiated rule *)
val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
(* Create a table of vars to be renamed after instantiation - ie
- other uninstantiated vars in the hyps the *instantiated* rule
+ other uninstantiated vars in the hyps the *instantiated* rule
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
- val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
+ val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
rule_inst;
- val cterm_renamings =
+ val cterm_renamings =
map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
(* Create the specific version of the rule for this target application *)
- val outerterm_inst =
- outerterm_tyinst
+ val outerterm_inst =
+ outerterm_tyinst
|> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
|> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
val couter_inst = Thm.reflexive (ctermify outerterm_inst);
- val (cprems, abstract_rule_inst) =
+ val (cprems, abstract_rule_inst) =
rule_inst |> Thm.instantiate ([], cterm_renamings)
|> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
- val specific_tgt_rule =
+ val specific_tgt_rule =
beta_eta_contract
(Thm.combination couter_inst abstract_rule_inst);
(* create an instantiated version of the target thm *)
- val tgt_th_inst =
+ val tgt_th_inst =
tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
|> Thm.instantiate ([], cterm_renamings);
@@ -302,4 +272,4 @@
end;
-end; (* struct *)
+end;