--- a/TFL/rules.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/TFL/rules.ML Wed Nov 16 17:45:30 2005 +0100
@@ -8,56 +8,56 @@
signature RULES =
sig
- val dest_thm : thm -> term list * term
+ val dest_thm: thm -> term list * term
(* Inference rules *)
- val REFL :cterm -> thm
- val ASSUME :cterm -> thm
- val MP :thm -> thm -> thm
- val MATCH_MP :thm -> thm -> thm
- val CONJUNCT1 :thm -> thm
- val CONJUNCT2 :thm -> thm
- val CONJUNCTS :thm -> thm list
- val DISCH :cterm -> thm -> thm
- val UNDISCH :thm -> thm
- val SPEC :cterm -> thm -> thm
- val ISPEC :cterm -> thm -> thm
- val ISPECL :cterm list -> thm -> thm
- val GEN :cterm -> thm -> thm
- val GENL :cterm list -> thm -> thm
- val LIST_CONJ :thm list -> thm
+ val REFL: cterm -> thm
+ val ASSUME: cterm -> thm
+ val MP: thm -> thm -> thm
+ val MATCH_MP: thm -> thm -> thm
+ val CONJUNCT1: thm -> thm
+ val CONJUNCT2: thm -> thm
+ val CONJUNCTS: thm -> thm list
+ val DISCH: cterm -> thm -> thm
+ val UNDISCH: thm -> thm
+ val SPEC: cterm -> thm -> thm
+ val ISPEC: cterm -> thm -> thm
+ val ISPECL: cterm list -> thm -> thm
+ val GEN: cterm -> thm -> thm
+ val GENL: cterm list -> thm -> thm
+ val LIST_CONJ: thm list -> thm
- val SYM : thm -> thm
- val DISCH_ALL : thm -> thm
- val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
- val SPEC_ALL : thm -> thm
- val GEN_ALL : thm -> thm
- val IMP_TRANS : thm -> thm -> thm
- val PROVE_HYP : thm -> thm -> thm
+ val SYM: thm -> thm
+ val DISCH_ALL: thm -> thm
+ val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
+ val SPEC_ALL: thm -> thm
+ val GEN_ALL: thm -> thm
+ val IMP_TRANS: thm -> thm -> thm
+ val PROVE_HYP: thm -> thm -> thm
- val CHOOSE : cterm * thm -> thm -> thm
- val EXISTS : cterm * cterm -> thm -> thm
- val EXISTL : cterm list -> thm -> thm
- val IT_EXISTS : (cterm*cterm) list -> thm -> thm
+ val CHOOSE: cterm * thm -> thm -> thm
+ val EXISTS: cterm * cterm -> thm -> thm
+ val EXISTL: cterm list -> thm -> thm
+ val IT_EXISTS: (cterm*cterm) list -> thm -> thm
- val EVEN_ORS : thm list -> thm list
- val DISJ_CASESL : thm -> thm list -> thm
+ val EVEN_ORS: thm list -> thm list
+ val DISJ_CASESL: thm -> thm list -> thm
- val list_beta_conv : cterm -> cterm list -> thm
- val SUBS : thm list -> thm -> thm
- val simpl_conv : simpset -> thm list -> cterm -> thm
+ val list_beta_conv: cterm -> cterm list -> thm
+ val SUBS: thm list -> thm -> thm
+ val simpl_conv: simpset -> thm list -> cterm -> thm
- val rbeta : thm -> thm
+ val rbeta: thm -> thm
(* For debugging my isabelle solver in the conditional rewriter *)
- val term_ref : term list ref
- val thm_ref : thm list ref
- val ss_ref : simpset list ref
- val tracing : bool ref
- val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
+ val term_ref: term list ref
+ val thm_ref: thm list ref
+ val ss_ref: simpset list ref
+ val tracing: bool ref
+ val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
-> thm -> thm * term list
- val RIGHT_ASSOC : thm -> thm
+ val RIGHT_ASSOC: thm -> thm
- val prove : bool -> cterm * tactic -> thm
+ val prove: bool -> cterm * tactic -> thm
end;
structure Rules: RULES =
@@ -308,7 +308,7 @@
let val gth = forall_intr v th
val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
- val theta = Pattern.match sign (P,P')
+ val theta = Pattern.match sign (P,P') (Vartab.empty, Vartab.empty);
val allI2 = instantiate (certify sign theta) allI
val thm = Thm.implies_elim allI2 gth
val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
@@ -353,7 +353,7 @@
val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
val redex = D.capply lam fvar
val {sign, t = t$u,...} = Thm.rep_cterm redex
- val residue = Thm.cterm_of sign (betapply (t, u))
+ val residue = Thm.cterm_of sign (Term.betapply (t, u))
in
GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
--- a/TFL/thry.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/TFL/thry.ML Wed Nov 16 17:45:30 2005 +0100
@@ -34,7 +34,7 @@
fun match_term thry pat ob =
let
- val (ty_theta, tm_theta) = Pattern.match thry (pat,ob)
+ val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
end;
--- a/src/Pure/IsaPlanner/term_lib.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/IsaPlanner/term_lib.ML Wed Nov 16 17:45:30 2005 +0100
@@ -141,7 +141,7 @@
(* Higher order matching with exception handled *)
(* returns optional instantiation *)
fun clean_match thy (a as (pat, t)) =
- let val (tyenv, tenv) = Pattern.match thy a
+ let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
in SOME (Vartab.dest tyenv, Vartab.dest tenv)
end handle Pattern.MATCH => NONE;
(* Higher order unification with exception handled, return the instantiations *)
--- a/src/Pure/Isar/find_theorems.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/Isar/find_theorems.ML Wed Nov 16 17:45:30 2005 +0100
@@ -83,7 +83,8 @@
Pattern.matches thy (if po then (pat, obj) else (obj, pat));
fun substsize pat =
- let val (_, subst) = Pattern.match thy (if po then (pat, obj) else (obj, pat))
+ let val (_, subst) =
+ Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
fun bestmatch [] = NONE
--- a/src/Pure/Proof/extraction.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Nov 16 17:45:30 2005 +0100
@@ -103,14 +103,13 @@
let
fun ren t = getOpt (Term.rename_abs tm1 tm t, t);
val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
- val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm);
+ val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
val env' = Envir.Envir
{maxidx = Library.foldl Int.max
(~1, map (Int.max o pairself maxidx_of_term) prems'),
iTs = Tenv, asol = tenv};
- val env'' = Library.foldl (fn (env, p) =>
- Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
+ val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
in SOME (Envir.norm_term env'' (inc (ren tm2)))
end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
(sort (int_ord o pairself fst)
--- a/src/Pure/Proof/reconstruct.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/Proof/reconstruct.ML Wed Nov 16 17:45:30 2005 +0100
@@ -132,7 +132,7 @@
val t' = mk_abs Ts t;
val u' = mk_abs Ts u
in
- (prop, prf, cs, Pattern.unify (sg, env, [(t', u')]), vTs)
+ (prop, prf, cs, Pattern.unify sg (t', u') env, vTs)
handle Pattern.Pattern =>
let val (env', cs') = decompose sg [] (env, (t', u'))
in (prop, prf, cs @ cs', env', vTs) end
@@ -268,8 +268,8 @@
val tn2 = Envir.norm_term bigenv t2
in
if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
- ((Pattern.unify (sg, env, [(tn1, tn2)]), ps) handle Pattern.Unif =>
- cantunify sg (tn1, tn2))
+ (Pattern.unify sg (tn1, tn2) env, ps) handle Pattern.Unif =>
+ cantunify sg (tn1, tn2)
else
let val (env', cs') = decompose sg [] (env, (tn1, tn2))
in if cs' = [(tn1, tn2)] then
--- a/src/Pure/thm.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/thm.ML Wed Nov 16 17:45:30 2005 +0100
@@ -292,7 +292,7 @@
ct2 as Cterm {t = t2, maxidx = maxidx2, sorts = sorts2, ...}) =
let
val thy_ref = merge_thys0 ct1 ct2;
- val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2);
+ val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2) (Vartab.empty, Vartab.empty);
val maxidx = Int.max (maxidx1, maxidx2);
val sorts = Sorts.union sorts1 sorts2;
fun mk_cTinst (ixn, (S, T)) =
--- a/src/Pure/unify.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/unify.ML Wed Nov 16 17:45:30 2005 +0100
@@ -588,8 +588,8 @@
val dps = map (fn(t,u)=> ([],t,u)) tus
in add_unify 1 ((env, dps), Seq.empty) end;
-fun unifiers params =
- Seq.cons ((Pattern.unify params, []), Seq.empty)
+fun unifiers (params as (thy, env, tus)) =
+ Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty)
handle Pattern.Unif => Seq.empty
| Pattern.Pattern => hounifiers params;