discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Simplifier and equational conversions demand a proper proof context;
--- a/NEWS Fri Oct 15 17:45:47 2021 +0200
+++ b/NEWS Fri Oct 15 19:25:31 2021 +0200
@@ -287,6 +287,38 @@
*** ML ***
+* Term operations under abstractions are now more robust (and more
+strict) by using the formal proof context in subsequent operations:
+
+ Variable.dest_abs
+ Variable.dest_abs_cterm
+ Variable.dest_all
+ Variable.dest_all_cterm
+
+This works under the assumption that terms are always properly declared
+to the proof context (e.g. via Variable.declare_term). Failure to do so,
+or working with the wrong context, will cause an error (exception Fail,
+based on Term.USED_FREE from Term.dest_abs_fresh).
+
+The Simplifier and equational conversions now use the above operations
+routinely, and thus require user-space tools to be serious about the
+proof context (notably in their use of Goal.prove, SUBPROOF etc.).
+INCOMPATIBILITY in add-on tools is to be expected occasionally: a proper
+context discipline needs to be followed.
+
+* Former operations Term.dest_abs and Logic.dest_all (without a proper
+context) have been discontinued. INCOMPATIBILITY, either use
+Variable.dest_abs etc. above, or the following operations that imitate
+the old behavior to a great extent:
+
+ Term.dest_abs_global
+ Logic.dest_all_global
+
+This works under the assumption that the given (sub-)term directly shows
+all free variables that need to be avoided when generating a fresh name.
+A violation of the assumption are variables stemming from the enclosing
+context that get involved in a proof only later.
+
* ML structures TFrees, TVars, Frees, Vars, Names provide scalable
operations to accumulate items from types and terms, using a fast
syntactic order. The original order of occurrences may be recovered as
--- a/src/FOLP/simp.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/FOLP/simp.ML Fri Oct 15 19:25:31 2021 +0200
@@ -366,7 +366,7 @@
(*Replace parameters by Free variables in P*)
fun variants_abs ([],P) = P
| variants_abs ((a,T)::aTs, P) =
- variants_abs (aTs, #2 (Term.dest_abs(a,T,P)));
+ variants_abs (aTs, #2 (Term.dest_abs_global (Abs (a,T,P))));
(*Select subgoal i from proof state; substitute parameters, for printing*)
fun prepare_goal i st =
--- a/src/HOL/Analysis/metric_arith.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML Fri Oct 15 19:25:31 2021 +0200
@@ -92,7 +92,7 @@
app_union_ct_pair find (Thm.dest_comb ct)
| Abs (_, _, _) =>
(* ensure the point doesn't contain the bound variable *)
- let val (var, bod) = Thm.dest_abs ct in
+ let val (var, bod) = Thm.dest_abs_global ct in
filter (free_in var #> not) (find bod)
end
| _ => [])
@@ -120,7 +120,7 @@
| _ $ _ =>
app_union_ct_pair find (Thm.dest_comb ct)
| Abs (_, _, _) =>
- let val (var, bod) = Thm.dest_abs ct in
+ let val (var, bod) = Thm.dest_abs_global ct in
filter (free_in var #> not) (find bod)
end
| _ => []
@@ -139,7 +139,7 @@
else app_union_ct_pair find (Thm.dest_binop ct)
| _ $ _ => app_union_ct_pair find (Thm.dest_comb ct)
| Abs (_, _, _) =>
- let val (var, bod) = Thm.dest_abs ct in
+ let val (var, bod) = Thm.dest_abs_global ct in
filter (free_in var #> not) (find bod)
end
| _ => []
@@ -255,7 +255,7 @@
let val (s, t) = Thm.dest_comb ct in
default (find_dist t) (find_dist s)
end
- | Abs (_, _, _) => find_dist (snd (Thm.dest_abs ct))
+ | Abs (_, _, _) => find_dist (snd (Thm.dest_abs_global ct))
| _ => NONE
fun find_eq ct =
case Thm.term_of ct of
@@ -269,7 +269,7 @@
let val (s, t) = Thm.dest_comb ct in
default (find_eq t) (find_eq s)
end
- | Abs (_, _, _) => find_eq (snd (Thm.dest_abs ct))
+ | Abs (_, _, _) => find_eq (snd (Thm.dest_abs_global ct))
| _ => NONE
in
case default (find_eq ct) (find_dist ct) of
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Oct 15 19:25:31 2021 +0200
@@ -2427,15 +2427,15 @@
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs \<^Const_>\<open>HOL.Not for t'\<close> =
@{code Not} (fm_of_term ps vs t')
- | fm_of_term ps vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> =
+ | fm_of_term ps vs \<^Const_>\<open>Ex _ for \<open>t as Abs (_, _, p)\<close>\<close> =
let
- val (xn', p') = Term.dest_abs (xn, xT, p);
- val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+ val (x', p') = Term.dest_abs_global t;
+ val vs' = (Free x', 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code E} (fm_of_term ps vs' p) end
- | fm_of_term ps vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> =
+ | fm_of_term ps vs \<^Const_>\<open>All _ for \<open>t as Abs (_, _, p)\<close>\<close> =
let
- val (xn', p') = Term.dest_abs (xn, xT, p);
- val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+ val (x', p') = Term.dest_abs_global t;
+ val vs' = (Free x', 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code A} (fm_of_term ps vs' p) end
| fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
@@ -2505,7 +2505,7 @@
| f $ a =>
if is_ty t orelse is_op t then term_bools (term_bools acc f) a
else insert (op aconv) t acc
- | Abs p => term_bools acc (snd (Term.dest_abs p))
+ | Abs _ => term_bools acc (snd (Term.dest_abs_global t))
| _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
end;
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Oct 15 19:25:31 2021 +0200
@@ -3974,12 +3974,12 @@
@{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
| fm_of_term fs ps \<^Const_>\<open>less_eq _ for p q\<close> =
@{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
- | fm_of_term fs ps (\<^Const_>\<open>Ex _\<close> $ Abs (abs as (_, xT, _))) =
- let val (xn', p') = Term.dest_abs abs
- in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end
- | fm_of_term fs ps (\<^Const_>\<open>All _\<close> $ Abs (abs as (_, xT, _))) =
- let val (xn', p') = Term.dest_abs abs
- in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end
+ | fm_of_term fs ps \<^Const_>\<open>Ex _ for \<open>p as Abs _\<close>\<close> =
+ let val (x', p') = Term.dest_abs_global p
+ in @{code E} (fm_of_term (Free x' :: fs) ps p') end
+ | fm_of_term fs ps \<^Const_>\<open>All _ for \<open>p as Abs _\<close>\<close> =
+ let val (x', p') = Term.dest_abs_global p
+ in @{code A} (fm_of_term (Free x' :: fs) ps p') end
| fm_of_term fs ps _ = error "fm_of_term";
fun term_of_num T ps (@{code poly.C} (a, b)) =
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Oct 15 19:25:31 2021 +0200
@@ -24,7 +24,7 @@
simpset : simpset};
fun get_p1 th =
- funpow 2 (Thm.dest_arg o snd o Thm.dest_abs)
+ funpow 2 (Thm.dest_arg o snd o Thm.dest_abs_global)
(funpow 2 Thm.dest_arg (Thm.cprop_of th)) |> Thm.dest_arg
fun ferrack_conv ctxt
@@ -55,7 +55,7 @@
in (S,th) end
val ((p1_v,p2_v),(mp1_v,mp2_v)) =
- funpow 2 (Thm.dest_arg o snd o Thm.dest_abs)
+ funpow 2 (Thm.dest_arg o snd o Thm.dest_abs_global)
(funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf)))
|> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun)
|> apply2 (apply2 (dest_Var o Thm.term_of))
@@ -78,8 +78,8 @@
fun main vs p =
let
val ((xn,ce),(x,fm)) = (case Thm.term_of p of
- \<^Const_>\<open>Ex _ for \<open>Abs(xn,xT,_)\<close>\<close> =>
- Thm.dest_comb p ||> Thm.dest_abs_name xn |>> pair xn
+ \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> =>
+ Thm.dest_comb p ||> Thm.dest_abs_global |>> pair xn
| _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
val cT = Thm.ctyp_of_cterm x
val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
@@ -174,25 +174,25 @@
val grab_atom_bop =
let
- fun h bounds tm =
+ fun h ctxt tm =
(case Thm.term_of tm of
- \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>conj for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>disj for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>implies for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
+ \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Not for _\<close> => h ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>All _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>Ex _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>conj for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>disj for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>implies for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Pure.all _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>Trueprop for _\<close> => h ctxt (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
- and find_args bounds tm =
- (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
- and find_body bounds b =
- let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
- in h (bounds + 1) b' end;
+ and find_args ctxt tm =
+ (h ctxt (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
+ and find_body ctxt b =
+ let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt
+ in h ctxt' b' end;
in h end;
fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset = ss}) tm =
@@ -213,7 +213,7 @@
in (Simplifier.rewrite (put_simpset ss ctxt) then_conv qe_conv) tm end;
fun dlo_instance ctxt tm =
- Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
+ Ferrante_Rackoff_Data.match ctxt (grab_atom_bop ctxt tm);
fun dlo_conv ctxt tm =
(case dlo_instance ctxt tm of
--- a/src/HOL/Decision_Procs/langford.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Fri Oct 15 19:25:31 2021 +0200
@@ -41,7 +41,7 @@
simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
(Thm.instantiate' [] [SOME p] stupid)
val (L, U) =
- let val (_, q) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of ths))
+ let val (_, q) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of ths))
in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
fun proveneF S =
let
@@ -128,10 +128,11 @@
fun proc ctxt ct =
(case Thm.term_of ct of
- \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> =>
+ \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
let
val e = Thm.dest_fun ct
- val (x,p) = Thm.dest_abs_name xn (Thm.dest_arg ct)
+ val (x,p) = Thm.dest_abs_global (Thm.dest_arg ct)
+ val Free (xn, _) = Thm.term_of x
val Pp = Thm.apply \<^cterm>\<open>Trueprop\<close> p
val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
in
@@ -193,29 +194,29 @@
val grab_atom_bop =
let
- fun h bounds tm =
+ fun h ctxt tm =
(case Thm.term_of tm of
- \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
- | \<^Const_>\<open>HOL.conj for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>HOL.disj for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>HOL.implies for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
- | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
+ \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Not for _\<close> => h ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>All _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>Pure.all _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>Ex _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+ | \<^Const_>\<open>HOL.conj for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>HOL.disj for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>HOL.implies for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args ctxt tm
+ | \<^Const_>\<open>Trueprop for _\<close> => h ctxt (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
- and find_args bounds tm =
- (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
- and find_body bounds b =
- let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
- in h (bounds + 1) b' end;
+ and find_args ctxt tm =
+ (h ctxt (Thm.dest_arg tm) handle CTERM _ => h ctxt (Thm.dest_arg1 tm))
+ and find_body ctxt b =
+ let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt
+ in h ctxt' b' end;
in h end;
fun dlo_instance ctxt tm =
- (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm));
+ (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop ctxt tm));
fun dlo_conv ctxt tm =
(case dlo_instance ctxt tm of
@@ -240,7 +241,7 @@
then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
| _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
- | Abs _ => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc))
+ | Abs _ => Thm.dest_abs_global t ||> h acc |> uncurry (remove (op aconvc))
| Free _ => if member (op aconvc) ats t then acc else ins t acc
| Var _ => if member (op aconvc) ats t then acc else ins t acc
| _ => acc)
--- a/src/HOL/HOLCF/Tools/fixrec.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Fri Oct 15 19:25:31 2021 +0200
@@ -251,7 +251,7 @@
^ ML_Syntax.print_term pat)
fun strip_alls t =
- (case try Logic.dest_all t of
+ (case try Logic.dest_all_global t of
SOME (_, u) => strip_alls u
| NONE => t)
--- a/src/HOL/Library/Pattern_Aliases.thy Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy Fri Oct 15 19:25:31 2021 +0200
@@ -55,7 +55,7 @@
fun as_typ a = a --> a --> a
fun strip_all t =
- case try Logic.dest_all t of
+ case try Logic.dest_all_global t of
NONE => ([], t)
| SOME (var, t) => apfst (cons var) (strip_all t)
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Fri Oct 15 19:25:31 2021 +0200
@@ -308,7 +308,7 @@
if p t then t else
case Thm.term_of t of
_$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
- | Abs (_,_,_) => find_cterm p (Thm.dest_abs t |> snd)
+ | Abs (_,_,_) => find_cterm p (Thm.dest_abs_global t |> snd)
| _ => raise CTERM ("find_cterm",[t]);
fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
@@ -496,7 +496,7 @@
fun h (acc, t) =
case Thm.term_of t of
Const(\<^const_name>\<open>Ex\<close>,_)$Abs(_,_,_) =>
- h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
+ h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -541,7 +541,7 @@
fun h (acc, t) =
case Thm.term_of t of
Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_) =>
- h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
+ h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
--- a/src/HOL/Library/cconv.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/cconv.ML Fri Oct 15 19:25:31 2021 +0200
@@ -152,8 +152,7 @@
end
(* Destruct the abstraction and apply the conversion. *)
- val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
- val (v, ct') = Thm.dest_abs_name u ct
+ val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt
val eq = cv (v, ctxt') ct'
in
if Thm.is_reflexive eq
--- a/src/HOL/Library/old_recdef.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML Fri Oct 15 19:25:31 2021 +0200
@@ -774,7 +774,7 @@
fun dest_comb t = Thm.dest_comb t
handle CTERM (msg, _) => raise ERR "dest_comb" msg;
-fun dest_abs t = Thm.dest_abs t
+fun dest_abs t = Thm.dest_abs_global t
handle CTERM (msg, _) => raise ERR "dest_abs" msg;
fun capply t u = Thm.apply t u
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Fri Oct 15 19:25:31 2021 +0200
@@ -164,8 +164,7 @@
handle Pattern.MATCH => NONE
fun rewrite_subterm prems ct (Abs (x, _, _)) =
let
- val (u, ctxt') = yield_singleton Variable.variant_fixes x ctxt;
- val (v, ct') = Thm.dest_abs_name u ct;
+ val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt;
val (thm, prems) = rewrite' ctxt' prems (x :: bounds) thms ct'
in
if Thm.is_reflexive thm then
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Oct 15 19:25:31 2021 +0200
@@ -321,7 +321,7 @@
fun strip_top_all_vars acc t =
if Logic.is_all t then
let
- val (v, t') = Logic.dest_all t
+ val (v, t') = Logic.dest_all_global t
(*bound instances in t' are replaced with free vars*)
in
strip_top_all_vars (v :: acc) t'
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Oct 15 19:25:31 2021 +0200
@@ -451,9 +451,9 @@
make_case ctxt (if b = \<^term>\<open>True\<close> then Error else Warning)
Name.context (decode_case u) (decode_cases t)
| decode_case (t $ u) = decode_case t $ decode_case u
- | decode_case (Abs (x, T, u)) =
- let val (x', u') = Term.dest_abs (x, T, u);
- in Term.absfree (x', T) (decode_case u') end
+ | decode_case (t as Abs _) =
+ let val (v, t') = Term.dest_abs_global t;
+ in Term.absfree v (decode_case t') end
| decode_case t = t;
in
map decode_case
@@ -587,9 +587,9 @@
| NONE =>
(case t of
t $ u => strip_case_full ctxt d t $ strip_case_full ctxt d u
- | Abs (x, T, u) =>
- let val (x', u') = Term.dest_abs (x, T, u);
- in Term.absfree (x', T) (strip_case_full ctxt d u') end
+ | Abs _ =>
+ let val (v, t') = Term.dest_abs_global t;
+ in Term.absfree v (strip_case_full ctxt d t') end
| _ => t));
--- a/src/HOL/Tools/Function/function_lib.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Fri Oct 15 19:25:31 2021 +0200
@@ -50,9 +50,9 @@
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
-fun dest_all_all (t as (Const (\<^const_name>\<open>Pure.all\<close>,_) $ _)) =
+fun dest_all_all \<^Const>\<open>Pure.all _ for t\<close> =
let
- val (v,b) = Logic.dest_all t |> apfst Free
+ val (v,b) = Term.dest_abs_global t |>> Free
val (vs, b') = dest_all_all b
in
(v :: vs, b')
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 19:25:31 2021 +0200
@@ -71,7 +71,7 @@
|> mk_old_skolem_term_wrapper
val comb = list_comb (rhs, args)
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
- | dec_sko \<^Const_>\<open>All _ for \<open>Abs abs\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs abs)) rhss
+ | dec_sko \<^Const_>\<open>All _ for \<open>t as Abs _\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs_global t)) rhss
| dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss
@@ -90,7 +90,7 @@
fun abstract ctxt ct =
let
val Abs (_, _, body) = Thm.term_of ct
- val (x, cbody) = Thm.dest_abs ct
+ val (x, cbody) = Thm.dest_abs_global ct
val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct)
fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K}
in
@@ -142,7 +142,7 @@
else case Thm.term_of ct of
Abs _ =>
let
- val (cv, cta) = Thm.dest_abs ct
+ val (cv, cta) = Thm.dest_abs_global ct
val (v, _) = dest_Free (Thm.term_of cv)
val u_th = introduce_combinators_in_cterm ctxt cta
val cu = Thm.rhs_of u_th
@@ -174,7 +174,7 @@
(*Given an abstraction over n variables, replace the bound variables by free
ones. Return the body, along with the list of free variables.*)
fun c_variant_abs_multi (ct0, vars) =
- let val (cv,ct) = Thm.dest_abs ct0
+ let val (cv,ct) = Thm.dest_abs_global ct0
in c_variant_abs_multi (ct, cv::vars) end
handle CTERM _ => (ct0, rev vars);
@@ -263,10 +263,10 @@
fun zap pos ct =
ct
|> (case Thm.term_of ct of
- Const (s, _) $ Abs (s', _, _) =>
+ Const (s, _) $ Abs _ =>
if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse
s = \<^const_name>\<open>Ex\<close> then
- Thm.dest_comb #> snd #> Thm.dest_abs_name s' #> snd #> zap pos
+ Thm.dest_comb #> snd #> Thm.dest_abs_global #> snd #> zap pos
else
Conv.all_conv
| Const (s, _) $ _ $ _ =>
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 19:25:31 2021 +0200
@@ -145,7 +145,7 @@
fun get_pmi_term t =
let val (x,eq) =
- (Thm.dest_abs o Thm.dest_arg o snd o Thm.dest_abs o Thm.dest_arg)
+ (Thm.dest_abs_global o Thm.dest_arg o snd o Thm.dest_abs_global o Thm.dest_arg)
(Thm.dest_arg t)
in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end;
@@ -348,7 +348,7 @@
fun unify ctxt q =
let
- val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs
+ val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs_global
val x = Thm.term_of cx
val ins = insert (op = : int * int -> bool)
fun h (acc,dacc) t =
@@ -436,8 +436,8 @@
val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
val [A_v,B_v] =
map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg
- |> Thm.dest_abs |> snd |> Thm.dest_arg1 |> Thm.dest_arg
- |> Thm.dest_abs |> snd |> Thm.dest_fun |> Thm.dest_arg
+ |> Thm.dest_abs_global |> snd |> Thm.dest_arg1 |> Thm.dest_arg
+ |> Thm.dest_abs_global |> snd |> Thm.dest_fun |> Thm.dest_arg
|> Thm.term_of |> dest_Var) [asetP, bsetP];
val D_v = (("D", 0), \<^typ>\<open>int\<close>);
@@ -446,7 +446,7 @@
let
val uth = unify ctxt q
- val (x,p) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of uth))
+ val (x,p) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of uth))
val ins = insert (op aconvc)
fun h t (bacc,aacc,dacc) =
case (whatis x t) of
@@ -599,12 +599,12 @@
else insert (op aconv) t
| f $ a => if skip orelse is_op f then add_bools a o add_bools f
else insert (op aconv) t
- | Abs p => add_bools (snd (Term.dest_abs p))
+ | Abs _ => add_bools (snd (Term.dest_abs_global t))
| _ => if skip orelse is_op t then I else insert (op aconv) t
end;
fun descend vs (abs as (_, xT, _)) =
- let val (xn', p') = Term.dest_abs abs
+ let val ((xn', _), p') = Term.dest_abs_global (Abs abs)
in ((xn', xT) :: vs, p') end;
local structure Proc = Cooper_Procedure in
@@ -716,8 +716,8 @@
fun strip_objall ct =
case Thm.term_of ct of
- Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn,_,_) =>
- let val (a,(v,t')) = (apsnd (Thm.dest_abs_name xn) o Thm.dest_comb) ct
+ Const (\<^const_name>\<open>All\<close>, _) $ Abs _ =>
+ let val (a,(v,t')) = (apsnd Thm.dest_abs_global o Thm.dest_comb) ct
in apfst (cons (a,v)) (strip_objall t')
end
| _ => ([],ct);
@@ -798,7 +798,7 @@
fun h acc t = if ty cts t then insert (op aconvc) t acc else
case Thm.term_of t of
_$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
- | Abs(_,_,_) => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc))
+ | Abs _ => Thm.dest_abs_global t ||> h acc |> uncurry (remove (op aconvc))
| _ => acc
in h [] ct end
end;
--- a/src/HOL/Tools/Qelim/qelim.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Fri Oct 15 19:25:31 2021 +0200
@@ -29,10 +29,10 @@
then Conv.binop_conv (conv env) p
else atcv env p
| Const(\<^const_name>\<open>Not\<close>,_)$_ => Conv.arg_conv (conv env) p
- | Const(\<^const_name>\<open>Ex\<close>,_)$Abs(s,_,_) =>
+ | Const(\<^const_name>\<open>Ex\<close>,_)$Abs (s, _, _) =>
let
val (e,p0) = Thm.dest_comb p
- val (x,p') = Thm.dest_abs_name s p0
+ val (x,p') = Thm.dest_abs_global p0
val env' = ins x env
val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
|> Drule.arg_cong_rule e
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Oct 15 19:25:31 2021 +0200
@@ -221,7 +221,7 @@
fun unlam t =
(case t of
- Abs a => snd (Term.dest_abs a)
+ Abs _ => snd (Term.dest_abs_global t)
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Oct 15 19:25:31 2021 +0200
@@ -713,12 +713,12 @@
mk_repabs ctxt (rty, qty) (Const (\<^const_name>\<open>Babs\<close>, T) $ r $ (inj_repabs_trm ctxt (t, t')))
end
- | (Abs (x, T, t), Abs (x', T', t')) =>
+ | (t as Abs _, t' as Abs _) =>
let
val rty = fastype_of rtrm
val qty = fastype_of qtrm
- val (y, s) = Term.dest_abs (x, T, t)
- val (_, s') = Term.dest_abs (x', T', t')
+ val ((y, T), s) = Term.dest_abs_global t
+ val (_, s') = Term.dest_abs_global t'
val yvar = Free (y, T)
val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
in
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Oct 15 19:25:31 2021 +0200
@@ -382,7 +382,7 @@
let val (cu1, cu2) = Thm.dest_comb ct
in f vs cu1 cu2 #> add_apps f vs cu1 #> add_apps f vs cu2 end
| Abs _ =>
- let val (cv, cu) = Thm.dest_abs ct
+ let val (cv, cu) = Thm.dest_abs_global ct
in add_apps f (Thm.term_of cv :: vs) cu end
| _ => I)
--- a/src/HOL/Tools/SMT/smt_util.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Fri Oct 15 19:25:31 2021 +0200
@@ -181,12 +181,7 @@
(* certified terms *)
-fun dest_cabs ct ctxt =
- (case Thm.term_of ct of
- Abs _ =>
- let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
- in (snd (Thm.dest_abs_name n ct), ctxt') end
- | _ => raise CTERM ("no abstraction", [ct]))
+fun dest_cabs ct ctxt = Variable.dest_abs_cterm ct ctxt |>> #1
val dest_all_cabs = repeat_yield (try o dest_cabs)
--- a/src/HOL/Tools/SMT/z3_isar.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_isar.ML Fri Oct 15 19:25:31 2021 +0200
@@ -62,10 +62,9 @@
end
end
-fun dest_alls (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (abs as (_, T, _))) =
- let val (s', t') = Term.dest_abs abs in
- dest_alls t' |>> cons (s', T)
- end
+fun dest_alls \<^Const_>\<open>Pure.all _ for \<open>t as Abs _\<close>\<close> =
+ let val (v, t') = Term.dest_abs_global t
+ in dest_alls t' |>> cons v end
| dest_alls t = ([], t)
val reorder_foralls =
--- a/src/HOL/Tools/groebner.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/groebner.ML Fri Oct 15 19:25:31 2021 +0200
@@ -385,8 +385,8 @@
val strip_exists =
let fun h (acc, t) =
case Thm.term_of t of
- Const (\<^const_name>\<open>Ex\<close>, _) $ Abs _ =>
- h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
+ \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
+ h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end;
@@ -885,40 +885,40 @@
end;
-fun find_term bounds tm =
+fun find_term tm ctxt =
(case Thm.term_of tm of
Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
- if domain_type T = HOLogic.boolT then find_args bounds tm
- else Thm.dest_arg tm
- | Const (\<^const_name>\<open>Not\<close>, _) $ _ => find_term bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
- | \<^term>\<open>Pure.imp\<close> $_$_ => find_args bounds tm
- | Const("(==)",_)$_$_ => find_args bounds tm (* FIXME proper const name *)
- | \<^term>\<open>Trueprop\<close>$_ => find_term bounds (Thm.dest_arg tm)
+ if domain_type T = HOLogic.boolT then find_args tm ctxt
+ else (Thm.dest_arg tm, ctxt)
+ | Const (\<^const_name>\<open>Not\<close>, _) $ _ => find_term (Thm.dest_arg tm) ctxt
+ | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
+ | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
+ | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args tm ctxt
+ | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args tm ctxt
+ | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args tm ctxt
+ | \<^term>\<open>Pure.imp\<close> $_$_ => find_args tm ctxt
+ | Const("(==)",_)$_$_ => find_args tm ctxt (* FIXME proper const name *)
+ | \<^term>\<open>Trueprop\<close>$_ => find_term (Thm.dest_arg tm) ctxt
| _ => raise TERM ("find_term", []))
-and find_args bounds tm =
+and find_args tm ctxt =
let val (t, u) = Thm.dest_binop tm
- in (find_term bounds t handle TERM _ => find_term bounds u) end
-and find_body bounds b =
- let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
- in find_term (bounds + 1) b' end;
+ in (find_term t ctxt handle TERM _ => find_term u ctxt) end
+and find_body b ctxt =
+ let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt
+ in find_term b' ctxt' end;
fun get_ring_ideal_convs ctxt form =
- case try (find_term 0) form of
+ case \<^try>\<open>find_term form ctxt\<close> of
NONE => NONE
-| SOME tm =>
- (case Semiring_Normalizer.match ctxt tm of
+| SOME (tm, ctxt') =>
+ (case Semiring_Normalizer.match ctxt' tm of
NONE => NONE
| SOME (res as (theory, {is_const = _, dest_const,
mk_const, conv = ring_eq_conv})) =>
SOME (ring_and_ideal_conv theory
- dest_const (mk_const (Thm.ctyp_of_cterm tm)) (ring_eq_conv ctxt)
- (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)))
+ dest_const (mk_const (Thm.ctyp_of_cterm tm)) (ring_eq_conv ctxt')
+ (Semiring_Normalizer.semiring_normalize_wrapper ctxt' res)))
fun presimplify ctxt add_thms del_thms =
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt
--- a/src/HOL/Tools/reification.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/reification.ML Fri Oct 15 19:25:31 2021 +0200
@@ -136,13 +136,10 @@
val thy = Proof_Context.theory_of ctxt;
fun tryabsdecomp (ct, ctxt) bds =
(case Thm.term_of ct of
- Abs (_, xT, ta) =>
+ Abs (_, xT, _) =>
let
- val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
- val (xn, ta) = Term.dest_abs (raw_xn, xT, ta);
- val x = Free (xn, xT);
- val cx = Thm.cterm_of ctxt' x;
- val cta = Thm.cterm_of ctxt' ta;
+ val ((cx, cta), ctxt') = Variable.dest_abs_cterm ct ctxt;
+ val x = Thm.term_of cx;
val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of
NONE => error "tryabsdecomp: Type not found in the Environement"
| SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT,
--- a/src/HOL/ex/Sketch_and_Explore.thy Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy Fri Oct 15 19:25:31 2021 +0200
@@ -12,7 +12,7 @@
ML \<open>
fun split_clause t =
let
- val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all t;
+ val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all_global t;
val assms = Logic.strip_imp_prems horn;
val concl = Logic.strip_imp_concl horn;
in (fixes, assms, concl) end;
--- a/src/Pure/Tools/find_theorems.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Oct 15 19:25:31 2021 +0200
@@ -231,14 +231,17 @@
fun get_names t = Term.add_const_names t (Term.add_free_names t []);
(* Does pat match a subterm of obj? *)
-fun matches_subterm thy (pat, obj) =
+fun matches_subterm ctxt (pat, obj) =
let
- fun msub bounds obj = Pattern.matches thy (pat, obj) orelse
+ val thy = Proof_Context.theory_of ctxt;
+ fun matches obj ctxt' = Pattern.matches thy (pat, obj) orelse
(case obj of
- Abs (_, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
- | t $ u => msub bounds t orelse msub bounds u
- | _ => false)
- in msub 0 obj end;
+ Abs (_, T, t) =>
+ let val ((_, t'), ctxt'') = Variable.dest_abs obj ctxt'
+ in matches t' ctxt'' end
+ | t $ u => matches t ctxt' orelse matches u ctxt'
+ | _ => false);
+ in matches obj ctxt end;
(*Including all constants and frees is only sound because matching
uses higher-order patterns. If full matching were used, then
@@ -255,7 +258,7 @@
fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
| check ((_, thm), c as SOME thm_consts) =
(if subset (op =) (pat_consts, thm_consts) andalso
- matches_subterm (Proof_Context.theory_of ctxt) (pat', Thm.full_prop_of thm)
+ matches_subterm ctxt (pat', Thm.full_prop_of thm)
then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
in check end;
--- a/src/Pure/conv.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/conv.ML Fri Oct 15 19:25:31 2021 +0200
@@ -91,12 +91,11 @@
fun abs_conv cv ctxt ct =
(case Thm.term_of ct of
- Abs (x, _, _) =>
+ Abs (a, _, _) =>
let
- val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
- val (v, ct') = Thm.dest_abs_name u ct;
+ val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt;
val eq = cv (v, ctxt') ct';
- in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
+ in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule a v eq end
| _ => raise CTERM ("abs_conv", [ct]));
fun combination_conv cv1 cv2 ct =
--- a/src/Pure/logic.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/logic.ML Fri Oct 15 19:25:31 2021 +0200
@@ -11,7 +11,7 @@
val all: term -> term -> term
val dependent_all_name: string * term -> term -> term
val is_all: term -> bool
- val dest_all: term -> (string * typ) * term
+ val dest_all_global: term -> (string * typ) * term
val list_all: (string * typ) list * term -> term
val all_constraint: (string -> typ option) -> string * string -> term -> term
val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
@@ -125,10 +125,10 @@
fun is_all (Const ("Pure.all", _) $ Abs _) = true
| is_all _ = false;
-fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) =
- let val (x, b) = Term.dest_abs abs (*potentially slow*)
- in ((x, T), b) end
- | dest_all t = raise TERM ("dest_all", [t]);
+fun dest_all_global t =
+ (case t of
+ Const ("Pure.all", _) $ (u as Abs _) => Term.dest_abs_global u
+ | _ => raise TERM ("dest_all", [t]));
fun list_all ([], t) = t
| list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
--- a/src/Pure/more_pattern.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/more_pattern.ML Fri Oct 15 19:25:31 2021 +0200
@@ -48,9 +48,11 @@
let
val skel0 = Bound 0;
- fun variant_absfree bounds (x, T, t) =
+ fun variant_absfree bounds x tm =
let
- val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
+ val ((x', T), t') =
+ Term.dest_abs_fresh (Name.bound bounds) tm
+ handle Term.USED_FREE _ => Term.dest_abs_global tm; (* FIXME proper context *)
fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
in (abs, t') end;
@@ -76,9 +78,9 @@
SOME tm2' => SOME (tm1 $ tm2')
| NONE => NONE)
end)
- | rew_sub r bounds skel (Abs body) =
+ | rew_sub r bounds skel (tm as Abs (x, _, _)) =
let
- val (abs, tm') = variant_absfree bounds body;
+ val (abs, tm') = variant_absfree bounds x tm;
val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
in case r (bounds + 1) skel' tm' of
SOME tm'' => SOME (abs tm'')
--- a/src/Pure/more_thm.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/more_thm.ML Fri Oct 15 19:25:31 2021 +0200
@@ -336,36 +336,48 @@
local
-fun dest_all ct =
+val used_frees =
+ Name.build_context o
+ Thm.fold_terms {hyps = true} Term.declare_term_frees;
+
+fun used_vars i =
+ Name.build_context o
+ (Thm.fold_terms {hyps = false} o Term.fold_aterms)
+ (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I);
+
+fun dest_all ct used =
(case Thm.term_of ct of
- Const ("Pure.all", _) $ Abs (a, _, _) =>
- let val (x, ct') = Thm.dest_abs (Thm.dest_arg ct)
- in SOME ((a, Thm.ctyp_of_cterm x), ct') end
+ Const ("Pure.all", _) $ Abs (x, _, _) =>
+ let
+ val (x', used') = Name.variant x used;
+ val (v, ct') = Thm.dest_abs_fresh x' (Thm.dest_arg ct);
+ in SOME ((x, Thm.ctyp_of_cterm v), (ct', used')) end
| _ => NONE);
-fun dest_all_list ct =
- (case dest_all ct of
- NONE => []
- | SOME (v, ct') => v :: dest_all_list ct');
+fun dest_all_list ct used =
+ (case dest_all ct used of
+ NONE => ([], used)
+ | SOME (v, (ct', used')) =>
+ let val (vs, used'') = dest_all_list ct' used'
+ in (v :: vs, used'') end);
fun forall_elim_vars_list vars i th =
let
- val used =
- (Thm.fold_terms {hyps = false} o Term.fold_aterms)
- (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th [];
- val vars' = (Name.variant_list used (map #1 vars), vars)
- |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T));
+ val (vars', _) =
+ (vars, used_vars i th) |-> fold_map (fn (x, T) => fn used =>
+ let val (x', used') = Name.variant x used
+ in (Thm.var ((x', i), T), used') end);
in fold Thm.forall_elim vars' th end;
in
fun forall_elim_vars i th =
- forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th;
+ forall_elim_vars_list (#1 (dest_all_list (Thm.cprop_of th) (used_frees th))) i th;
fun forall_elim_var i th =
let
val vars =
- (case dest_all (Thm.cprop_of th) of
+ (case dest_all (Thm.cprop_of th) (used_frees th) of
SOME (v, _) => [v]
| NONE => raise THM ("forall_elim_var", i, [th]));
in forall_elim_vars_list vars i th end;
--- a/src/Pure/raw_simplifier.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/raw_simplifier.ML Fri Oct 15 19:25:31 2021 +0200
@@ -1130,21 +1130,13 @@
and subc skel ctxt t0 =
let val Simpset (_, {congs, ...}) = simpset_of ctxt in
(case Thm.term_of t0 of
- Abs (a, T, _) =>
+ Abs (a, _, _) =>
let
- val (v, ctxt') = Variable.next_bound (a, T) ctxt;
- val b = #1 (Term.dest_Free v);
- val (v', t') = Thm.dest_abs_name b t0;
- val b' = #1 (Term.dest_Free (Thm.term_of v'));
- val _ =
- if b <> b' then
- warning ("Bad Simplifier context: renamed bound variable " ^
- quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
- else ();
- val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
+ val ((v, t'), ctxt') = Variable.dest_abs_cterm t0 ctxt;
+ val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
in
(case botc skel' ctxt' t' of
- SOME thm => SOME (Thm.abstract_rule a v' thm)
+ SOME thm => SOME (Thm.abstract_rule a v thm)
| NONE => NONE)
end
| t $ _ =>
--- a/src/Pure/term.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/term.ML Fri Oct 15 19:25:31 2021 +0200
@@ -166,7 +166,9 @@
val could_eta_contract: term -> bool
val could_beta_eta_contract: term -> bool
val used_free: string -> term -> bool
- val dest_abs: string * typ * term -> string * term
+ exception USED_FREE of string * term
+ val dest_abs_fresh: string -> term -> (string * typ) * term
+ val dest_abs_global: term -> (string * typ) * term
val dummy_pattern: typ -> term
val dummy: term
val dummy_prop: term
@@ -965,6 +967,9 @@
(* dest abstraction *)
+(*ASSUMPTION: x is fresh wrt. the current context, but the check
+ of used_free merely guards against gross mistakes*)
+
fun used_free x =
let
fun used (Free (y, _)) = (x = y)
@@ -973,11 +978,27 @@
| used _ = false;
in used end;
-fun dest_abs (x, T, b) =
- if used_free x b then
- let val (x', _) = Name.variant x (declare_term_frees b Name.context);
- in (x', subst_bound (Free (x', T), b)) end
- else (x, subst_bound (Free (x, T), b));
+exception USED_FREE of string * term;
+
+fun subst_abs v b = (v, subst_bound (Free v, b));
+
+fun dest_abs_fresh x t =
+ (case t of
+ Abs (_, T, b) =>
+ if used_free x b then raise USED_FREE (x, t)
+ else subst_abs (x, T) b
+ | _ => raise TERM ("dest_abs", [t]));
+
+fun dest_abs_global t =
+ (case t of
+ Abs (x, T, b) =>
+ if used_free x b then
+ let
+ val used = Name.build_context (declare_term_frees b);
+ val x' = #1 (Name.variant x used);
+ in subst_abs (x', T) b end
+ else subst_abs (x, T) b
+ | _ => raise TERM ("dest_abs", [t]));
(* dummy patterns *)
--- a/src/Pure/thm.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/thm.ML Fri Oct 15 19:25:31 2021 +0200
@@ -48,8 +48,8 @@
val dest_arg: cterm -> cterm
val dest_fun2: cterm -> cterm
val dest_arg1: cterm -> cterm
- val dest_abs_name: string -> cterm -> cterm * cterm
- val dest_abs: cterm -> cterm * cterm
+ val dest_abs_fresh: string -> cterm -> cterm * cterm
+ val dest_abs_global: cterm -> cterm * cterm
val rename_tvar: indexname -> ctyp -> ctyp
val var: indexname * ctyp -> cterm
val apply: cterm -> cterm -> cterm
@@ -305,15 +305,18 @@
in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
| dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
-fun dest_abs_name x (Cterm {t = Abs (_, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) =
- let val (y', t') = Term.dest_abs (x, T, t) in
- (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts},
- Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts})
- end
- | dest_abs_name _ ct = raise CTERM ("dest_abs_name", [ct]);
+fun gen_dest_abs dest ct =
+ (case ct of
+ Cterm {t = t as Abs _, T = Type ("fun", [_, U]), cert, maxidx, sorts} =>
+ let
+ val ((x', T), t') = dest t;
+ val v = Cterm {t = Free (x', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts};
+ val body = Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts};
+ in (v, body) end
+ | _ => raise CTERM ("dest_abs", [ct]));
-fun dest_abs (ct as Cterm {t = Abs (x, _, _), ...}) = dest_abs_name x ct
- | dest_abs ct = raise CTERM ("dest_abs", [ct]);
+val dest_abs_fresh = gen_dest_abs o Term.dest_abs_fresh;
+val dest_abs_global = gen_dest_abs Term.dest_abs_global;
(* constructors *)
--- a/src/Pure/variable.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/variable.ML Fri Oct 15 19:25:31 2021 +0200
@@ -81,6 +81,10 @@
val import_vars: Proof.context -> thm -> thm
val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
+ val dest_abs: term -> Proof.context -> ((string * typ) * term) * Proof.context
+ val dest_abs_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context
+ val dest_all: term -> Proof.context -> ((string * typ) * term) * Proof.context
+ val dest_all_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context
val is_bound_focus: Proof.context -> bool
val set_bound_focus: bool -> Proof.context -> Proof.context
val restore_bound_focus: Proof.context -> Proof.context -> Proof.context
@@ -650,6 +654,40 @@
val trade = gen_trade (import true) export;
+(* destruct binders *)
+
+local
+
+fun gen_dest_abs exn dest term_of arg ctxt =
+ (case term_of arg of
+ Abs (a, T, _) =>
+ let
+ val (x, ctxt') = yield_singleton bound_fixes (a, T) ctxt;
+ val res = dest x arg handle Term.USED_FREE _ =>
+ raise Fail ("Bad context: clash of fresh free for bound: " ^
+ Syntax.string_of_term ctxt (Free (x, T)) ^ " vs. " ^
+ Syntax.string_of_term ctxt' (Free (x, T)));
+ in (res, ctxt') end
+ | _ => raise exn ("dest_abs", [arg]));
+
+in
+
+val dest_abs = gen_dest_abs TERM Term.dest_abs_fresh I;
+val dest_abs_cterm = gen_dest_abs CTERM Thm.dest_abs_fresh Thm.term_of;
+
+fun dest_all t ctxt =
+ (case t of
+ Const ("Pure.all", _) $ u => dest_abs u ctxt
+ | _ => raise TERM ("dest_all", [t]));
+
+fun dest_all_cterm ct ctxt =
+ (case Thm.term_of ct of
+ Const ("Pure.all", _) $ _ => dest_abs_cterm (Thm.dest_arg ct) ctxt
+ | _ => raise CTERM ("dest_all", [ct]));
+
+end;
+
+
(* focus on outermost parameters: \<And>x y z. B *)
val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false);
--- a/src/Tools/Code/code_thingol.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Oct 15 19:25:31 2021 +0200
@@ -622,7 +622,7 @@
pair (IVar (SOME v))
| translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
let
- val (v', t') = Term.dest_abs (Name.desymbolize (SOME false) v, ty, t);
+ val ((v', _), t') = Term.dest_abs_global (Abs (Name.desymbolize (SOME false) v, ty, t));
val v'' = if Term.used_free v' t' then SOME v' else NONE
in
translate_typ ctxt algbr eqngr permissive ty
--- a/src/Tools/misc_legacy.ML Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Tools/misc_legacy.ML Fri Oct 15 19:25:31 2021 +0200
@@ -126,9 +126,9 @@
it replaces the bound variables by free variables. *)
fun strip_context_aux (params, Hs, \<^Const_>\<open>Pure.imp for H B\<close>) =
strip_context_aux (params, H :: Hs, B)
- | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>Abs (a, T, t)\<close>\<close>) =
- let val (b, u) = Term.dest_abs (a, T, t)
- in strip_context_aux ((b, T) :: params, Hs, u) end
+ | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>t as Abs _\<close>\<close>) =
+ let val (v, u) = Term.dest_abs_global t
+ in strip_context_aux (v :: params, Hs, u) end
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
fun strip_context A = strip_context_aux ([], [], A);