Added variants of instantiation functions that operate on pairs of type
(indexname * string) instead of (string * string).
--- a/src/Pure/drule.ML Mon Jan 17 17:45:03 2005 +0100
+++ b/src/Pure/drule.ML Tue Jan 18 14:34:24 2005 +0100
@@ -20,7 +20,7 @@
val read_insts :
Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
-> (indexname -> typ option) * (indexname -> sort option)
- -> string list -> (string*string)list
+ -> string list -> (indexname * string) list
-> (indexname*ctyp)list * (cterm*cterm)list
val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
val strip_shyps_warning : thm -> thm
@@ -218,14 +218,11 @@
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
let
- fun split([],tvs,vs) = (tvs,vs)
- | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of
- "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs)
- | cs => split(l,tvs,(Syntax.indexname cs,st)::vs));
- val (tvs,vs) = split(insts,[],[]);
- fun readT((a,i),st) =
- let val ixn = ("'" ^ a,i);
- val S = case rsorts ixn of Some S => S | None => absent ixn;
+ fun is_tv ((a, _), _) =
+ (case Symbol.explode a of "'" :: _ => true | _ => false);
+ val (tvs, vs) = partition is_tv insts;
+ fun readT (ixn, st) =
+ let val S = case rsorts ixn of Some S => S | None => absent ixn;
val T = Sign.read_typ (sign,sorts) st;
in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
else inst_failure ixn
@@ -789,7 +786,8 @@
fun read_instantiate_sg sg sinsts th =
let val ts = types_sorts th;
val used = add_term_tvarnames (prop_of th, []);
- in instantiate (read_insts sg ts ts used sinsts) th end;
+ val sinsts' = map (apfst Syntax.indexname) sinsts
+ in instantiate (read_insts sg ts ts used sinsts') th end;
(*Instantiate theorem th, reading instantiations under theory of th*)
fun read_instantiate sinsts th =
--- a/src/Pure/tactic.ML Mon Jan 17 17:45:03 2005 +0100
+++ b/src/Pure/tactic.ML Tue Jan 18 14:34:24 2005 +0100
@@ -111,6 +111,10 @@
val conjunction_tac: tactic
val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
val prove_standard: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
+ val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
+ int -> tactic
+ val lift_inst_rule' : thm * int * (indexname * string) list * thm -> thm
+ val res_inst_tac' : (indexname * string) list -> thm -> int -> tactic
end;
structure Tactic: TACTIC =
@@ -212,7 +216,7 @@
in rename_wrt_term Bi (Logic.strip_params Bi) end;
(*Lift and instantiate a rule wrt the given state and subgoal number *)
-fun lift_inst_rule (st, i, sinsts, rule) =
+fun lift_inst_rule' (st, i, sinsts, rule) =
let val {maxidx,sign,...} = rep_thm st
val (_, _, Bi, _) = dest_state(st,i)
val params = Logic.strip_params Bi (*params of subgoal i*)
@@ -238,6 +242,9 @@
(lift_rule (st,i) rule)
end;
+fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
+ (st, i, map (apfst Syntax.indexname) sinsts, rule);
+
(*
Like lift_inst_rule but takes terms, not strings, where the terms may contain
Bounds referring to parameters of the subgoal.
@@ -271,13 +278,16 @@
subgoal. Fails if "i" is out of range. ***)
(*compose version: arguments are as for bicompose.*)
-fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st =
+fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
if i > nprems_of st then no_tac st
else st |>
- (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
+ (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
handle TERM (msg,_) => (warning msg; no_tac)
| THM (msg,_,_) => (warning msg; no_tac));
+val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
+val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
+
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the
terms that are substituted contain (term or type) unknowns from the
goal, because it is unable to instantiate goal unknowns at the same time.
@@ -290,6 +300,9 @@
fun res_inst_tac sinsts rule i =
compose_inst_tac sinsts (false, rule, nprems_of rule) i;
+fun res_inst_tac' sinsts rule i =
+ compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
+
(*eresolve elimination version*)
fun eres_inst_tac sinsts rule i =
compose_inst_tac sinsts (true, rule, nprems_of rule) i;