Now some functions try to avoid name clashes when introducing new free
variables.
--- a/TFL/rules.sml Fri Sep 29 16:00:04 2000 +0200
+++ b/TFL/rules.sml Fri Sep 29 18:02:24 2000 +0200
@@ -496,18 +496,18 @@
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
-fun dest_all(Const("all",_) $ (a as Abs _)) = S.dest_abs a
- | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
+fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
+ | dest_all _ _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
-val is_all = Utils.can dest_all;
+val is_all = Utils.can (dest_all []);
-fun strip_all fm =
+fun strip_all used fm =
if (is_all fm)
- then let val {Bvar,Body} = dest_all fm
- val (bvs,core) = strip_all Body
- in ((Bvar::bvs), core)
+ then let val ({Bvar, Body}, used') = dest_all used fm
+ val (bvs, core, used'') = strip_all used' Body
+ in ((Bvar::bvs), core, used'')
end
- else ([],fm);
+ else ([], fm, used);
fun break_all(Const("all",_) $ Abs (_,_,body)) = body
| break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"};
@@ -594,19 +594,18 @@
fun list_mk_aabs (vstrl,tm) =
U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
-fun dest_aabs tm =
- let val {Bvar,Body} = S.dest_abs tm
- in (Bvar,Body)
- end handle _ => let val {varstruct,body} = S.dest_pabs tm (* FIXME do not handle _ !!! *)
- in (varstruct,body)
- end;
+fun dest_aabs used tm =
+ let val ({Bvar,Body}, used') = S.dest_abs used tm
+ in (Bvar, Body, used') end handle _ => (* FIXME do not handle _ !!! *)
+ let val {varstruct, body, used} = S.dest_pabs used tm
+ in (varstruct, body, used) end;
-fun strip_aabs tm =
- let val (vstr,body) = dest_aabs tm
- val (bvs, core) = strip_aabs body
- in (vstr::bvs, core)
+fun strip_aabs used tm =
+ let val (vstr, body, used') = dest_aabs used tm
+ val (bvs, core, used'') = strip_aabs used' body
+ in (vstr::bvs, core, used'')
end
- handle _ => ([],tm); (* FIXME do not handle _ !!! *)
+ handle _ => ([], tm, used); (* FIXME do not handle _ !!! *)
fun dest_combn tm 0 = (tm,[])
| dest_combn tm n =
@@ -671,13 +670,13 @@
*
* (([x,y],N),vstr)
*---------------------------------------------------------------------------*)
-fun dest_pbeta_redex M n =
+fun dest_pbeta_redex used M n =
let val (f,args) = dest_combn M n
- val dummy = dest_aabs f
- in (strip_aabs f,args)
+ val dummy = dest_aabs used f
+ in (strip_aabs used f,args)
end;
-fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M;
+fun pbeta_redex M n = U.can (U.C (dest_pbeta_redex []) n) M;
fun dest_impl tm =
let val ants = Logic.strip_imp_prems tm
@@ -697,7 +696,7 @@
val dummy = thm_ref := []
val dummy = mss_ref := []
val cut_lemma' = cut_lemma RS eq_reflection
- fun prover mss thm =
+ fun prover used mss thm =
let fun cong_prover mss thm =
let val dummy = say "cong_prover:"
val cntxt = prems_of_mss mss
@@ -714,7 +713,7 @@
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
val mss' = add_prems(mss, map ASSUME ants)
- val lhs_eq_lhs1 = Thm.rewrite_cterm(false,true,false)mss' prover lhs
+ val lhs_eq_lhs1 = Thm.rewrite_cterm (false,true,false) mss' (prover used) lhs
handle _ => reflexive lhs (* FIXME do not handle _ !!! *)
val dummy = print_thms "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
@@ -723,7 +722,7 @@
lhs_eeq_lhs2 COMP thm
end
fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
- let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist)
+ let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
val dummy = assert (forall (op aconv)
(ListPair.zip (vlist, args)))
"assertion failed in CONTEXT_REWRITE_RULE"
@@ -736,7 +735,7 @@
val QeqQ1 = pbeta_reduce (tych Q)
val Q1 = #2(D.dest_eq(cconcl QeqQ1))
val mss' = add_prems(mss, map ASSUME ants1)
- val Q1eeqQ2 = Thm.rewrite_cterm (false,true,false) mss' prover Q1
+ val Q1eeqQ2 = Thm.rewrite_cterm (false,true,false) mss' (prover used') Q1
handle _ => reflexive Q1 (* FIXME do not handle _ !!! *)
val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
@@ -753,7 +752,7 @@
in ant_th COMP thm
end
fun q_eliminate (thm,imp,sign) =
- let val (vlist,imp_body) = strip_all imp
+ let val (vlist, imp_body, used') = strip_all used imp
val (ants,Q) = dest_impl imp_body
in if (pbeta_redex Q) (length vlist)
then pq_eliminate (thm,sign,vlist,imp_body,Q)
@@ -761,8 +760,8 @@
let val tych = cterm_of sign
val ants1 = map tych ants
val mss' = add_prems(mss, map ASSUME ants1)
- val Q_eeq_Q1 = Thm.rewrite_cterm(false,true,false) mss'
- prover (tych Q)
+ val Q_eeq_Q1 = Thm.rewrite_cterm
+ (false,true,false) mss' (prover used') (tych Q)
handle _ => reflexive (tych Q) (* FIXME do not handle _ !!! *)
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
@@ -831,9 +830,9 @@
(if (is_cong thm) then cong_prover else restrict_prover) mss thm
end
val ctm = cprop_of th
+ val names = add_term_names (term_of ctm, [])
val th1 = Thm.rewrite_cterm(false,true,false)
- (add_congs(mss_of [cut_lemma'], congs))
- prover ctm
+ (add_congs(mss_of [cut_lemma'], congs)) (prover names) ctm
val th2 = equal_elim th1 th
in
(th2, filter (not o restricted) (!tc_list))
--- a/TFL/usyntax.sml Fri Sep 29 16:00:04 2000 +0200
+++ b/TFL/usyntax.sml Fri Sep 29 18:02:24 2000 +0200
@@ -44,7 +44,7 @@
(* Destruction routines *)
val dest_const: term -> {Name : string, Ty : typ}
val dest_comb : term -> {Rator : term, Rand : term}
- val dest_abs : term -> {Bvar : term, Body : term}
+ val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list
val dest_eq : term -> {lhs : term, rhs : term}
val dest_imp : term -> {ant : term, conseq : term}
val dest_forall : term -> {Bvar : term, Body : term}
@@ -53,7 +53,7 @@
val dest_conj : term -> {conj1 : term, conj2 : term}
val dest_disj : term -> {disj1 : term, disj2 : term}
val dest_pair : term -> {fst : term, snd : term}
- val dest_pabs : term -> {varstruct : term, body : term}
+ val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list}
val lhs : term -> term
val rhs : term -> term
@@ -243,11 +243,13 @@
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
| dest_comb _ = raise USYN_ERR{func = "dest_comb", mesg = "not a comb"};
-fun dest_abs(a as Abs(s,ty,M)) =
- let val v = Free(s,ty)
- in {Bvar = v, Body = betapply (a,v)}
+fun dest_abs used (a as Abs(s, ty, M)) =
+ let
+ val s' = variant used s;
+ val v = Free(s', ty);
+ in ({Bvar = v, Body = betapply (a,v)}, s'::used)
end
- | dest_abs _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
+ | dest_abs _ _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"};
@@ -255,10 +257,10 @@
fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
| dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"};
-fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
+fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"};
-fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
+fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"};
fun dest_neg(Const("not",_) $ M) = M
@@ -284,16 +286,16 @@
local fun ucheck t = (if #Name(dest_const t) = "split" then t
else raise Match)
in
-fun dest_pabs tm =
- let val {Bvar,Body} = dest_abs tm
- in {varstruct = Bvar, body = Body}
+fun dest_pabs used tm =
+ let val ({Bvar,Body}, used') = dest_abs used tm
+ in {varstruct = Bvar, body = Body, used = used'}
end
handle (* FIXME do not handle _ !!! *)
_ => let val {Rator,Rand} = dest_comb tm
val _ = ucheck Rator
- val {varstruct = lv,body} = dest_pabs Rand
- val {varstruct = rv,body} = dest_pabs body
- in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
+ val {varstruct = lv, body, used = used'} = dest_pabs used Rand
+ val {varstruct = rv, body, used = used''} = dest_pabs used' body
+ in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
end
end;
@@ -311,7 +313,7 @@
val is_conj = can dest_conj
val is_disj = can dest_disj
val is_pair = can dest_pair
-val is_pabs = can dest_pabs
+val is_pabs = can (dest_pabs [])
(* Construction of a cterm from a list of Terms *)
@@ -335,7 +337,7 @@
end;
fun strip_abs(tm as Abs _) =
- let val {Bvar,Body} = dest_abs tm
+ let val ({Bvar,Body}, _) = dest_abs [] tm
val (bvs, core) = strip_abs Body
in (Bvar::bvs, core)
end