--- a/NEWS Fri Oct 15 12:42:51 2021 +0100
+++ b/NEWS Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/FOLP/simp.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Analysis/metric_arith.ML Mon Oct 18 11:49:01 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 NONE 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 NONE 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 NONE 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 NONE 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 NONE 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 12:42:51 2021 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Oct 18 11:49:01 2021 +0200
@@ -2427,16 +2427,16 @@
@{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 _\<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;
- 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> =
+ 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>t as Abs _\<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;
- in @{code A} (fm_of_term ps vs' p) end
+ 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);
fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
@@ -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 12:42:51 2021 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Oct 18 11:49:01 2021 +0200
@@ -24,7 +24,7 @@
simpset : simpset};
fun get_p1 th =
- funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
+ 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 NONE)
+ 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 (SOME 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 (SOME (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 12:42:51 2021 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Mon Oct 18 11:49:01 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 NONE (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 (SOME 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 (SOME (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 NONE 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/HOL.thy Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/HOL.thy Mon Oct 18 11:49:01 2021 +0200
@@ -2104,9 +2104,9 @@
method_setup eval = \<open>
let
fun eval_tac ctxt =
- let val conv = Code_Runtime.dynamic_holds_conv ctxt
+ let val conv = Code_Runtime.dynamic_holds_conv
in
- CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
+ CONVERSION (Conv.params_conv ~1 (Conv.concl_conv ~1 o conv) ctxt) THEN'
resolve_tac ctxt [TrueI]
end
in
--- a/src/HOL/HOLCF/Tools/fixrec.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Library/Pattern_Aliases.thy Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Oct 18 11:49:01 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 NONE 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 NONE (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 NONE (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 12:42:51 2021 +0100
+++ b/src/HOL/Library/cconv.ML Mon Oct 18 11:49:01 2021 +0200
@@ -124,41 +124,37 @@
Abs (x, _, _) =>
let
(* Instantiate the rule properly and apply it to the eq theorem. *)
- fun abstract_rule u v eq =
+ fun abstract_rule v eq =
let
(* Take a variable v and an equality theorem of form:
P1 \<Longrightarrow> ... \<Longrightarrow> Pn \<Longrightarrow> L v \<equiv> R v
And build a term of form:
\<And>v. (\<lambda>x. L x) v \<equiv> (\<lambda>x. R x) v *)
- fun mk_concl var eq =
+ fun mk_concl eq =
let
- val certify = Thm.cterm_of ctxt
- fun abs term = (Term.lambda var term) $ var
- fun equals_cong f t =
- Logic.dest_equals t
- |> (fn (a, b) => (f a, f b))
- |> Logic.mk_equals
+ fun abs t = lambda v t $ v
+ fun equals_cong f = Logic.dest_equals #> apply2 f #> Logic.mk_equals
in
Thm.concl_of eq
|> equals_cong abs
- |> Logic.all var |> certify
+ |> Logic.all v
+ |> Thm.cterm_of ctxt
end
val rule = abstract_rule_thm x
- val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
+ val inst = Thm.match (hd (Drule.cprems_of rule), mk_concl eq)
+ val gen = (Names.empty, Names.make_set [#1 (dest_Free v)])
in
- (Drule.instantiate_normalize inst rule OF
- [Drule.generalize (Names.empty, Names.make_set [u]) eq])
+ (Drule.instantiate_normalize inst rule OF [Drule.generalize gen eq])
|> Drule.zero_var_indexes
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 (SOME 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_cconv ct
- else abstract_rule u v eq
+ else abstract_rule (Thm.term_of v) eq
end
| _ => raise CTERM ("abs_cconv", [ct]))
@@ -173,8 +169,7 @@
then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
else cv ctxt ct
-(* TODO: This code behaves not exactly like Conv.prems_cconv does.
- Fix this! *)
+(* FIXME: This code behaves not exactly like Conv.prems_cconv does. *)
(*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
fun prems_cconv 0 cv ct = cv ct
| prems_cconv n cv ct =
--- a/src/HOL/Library/old_recdef.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Library/old_recdef.ML Mon Oct 18 11:49:01 2021 +0200
@@ -110,7 +110,7 @@
signature DCTERM =
sig
val dest_comb: cterm -> cterm * cterm
- val dest_abs: string option -> cterm -> cterm * cterm
+ val dest_abs: cterm -> cterm * cterm
val capply: cterm -> cterm -> cterm
val cabs: cterm -> cterm -> cterm
val mk_conj: cterm * cterm -> cterm
@@ -191,7 +191,7 @@
term * term list * thm * thm list -> thm -> thm * term list
val RIGHT_ASSOC: Proof.context -> thm -> thm
- val prove: Proof.context -> bool -> term * tactic -> thm
+ val prove: Proof.context -> bool -> term -> (Proof.context -> tactic) -> thm
end;
signature THRY =
@@ -221,7 +221,9 @@
val mk_induction: Proof.context ->
{fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
val postprocess: Proof.context -> bool ->
- {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
+ {wf_tac: Proof.context -> tactic,
+ terminator: Proof.context -> tactic,
+ simplifier: Proof.context -> cterm -> thm} ->
{rules: thm, induction: thm, TCs: term list list} ->
{rules: thm, induction: thm, nested_tcs: thm list}
end;
@@ -774,7 +776,7 @@
fun dest_comb t = Thm.dest_comb t
handle CTERM (msg, _) => raise ERR "dest_comb" msg;
-fun dest_abs a t = Thm.dest_abs a 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
@@ -838,7 +840,7 @@
in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
fun dest_binder expected tm =
- dest_abs NONE (dest_monop expected tm)
+ dest_abs (dest_monop expected tm)
handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
@@ -883,7 +885,7 @@
val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *)
val strip_imp = rev2swap o strip dest_imp
-val strip_abs = rev2swap o strip (dest_abs NONE)
+val strip_abs = rev2swap o strip dest_abs
val strip_forall = rev2swap o strip dest_forall
val strip_exists = rev2swap o strip dest_exists
@@ -1232,7 +1234,9 @@
fun SUBS ctxt thl =
rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
-val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
+fun rew_conv ctxt ctm =
+ Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+ (Variable.declare_term (Thm.term_of ctm) ctxt) ctm;
fun simpl_conv ctxt thl ctm =
HOLogic.mk_obj_eq (rew_conv (ctxt addsimps thl) ctm);
@@ -1590,13 +1594,13 @@
end;
-fun prove ctxt strict (t, tac) =
+fun prove ctxt strict t tac =
let
val ctxt' = Proof_Context.augment t ctxt;
in
if strict
- then Goal.prove ctxt' [] [] t (K tac)
- else Goal.prove ctxt' [] [] t (K tac)
+ then Goal.prove ctxt' [] [] t (tac o #context)
+ else Goal.prove ctxt' [] [] t (tac o #context)
handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
end;
@@ -1688,14 +1692,6 @@
val list_mk_type = Utils.end_itlist (curry (op -->));
-fun front_last [] = raise TFL_ERR "front_last" "empty list"
- | front_last [x] = ([],x)
- | front_last (h::t) =
- let val (pref,x) = front_last t
- in
- (h::pref,x)
- end;
-
(*---------------------------------------------------------------------------
* The next function is common to pattern-match translation and
@@ -2053,8 +2049,6 @@
end;
-fun givens pats = map pat_of (filter given pats);
-
fun post_definition ctxt meta_tflCongs (def, pats) =
let val thy = Proof_Context.theory_of ctxt
val tych = Thry.typecheck thy
@@ -2408,11 +2402,13 @@
(*---------------------------------------------------------------------
* Attempt to eliminate WF condition. It's the only assumption of rules
*---------------------------------------------------------------------*)
- val (rules1,induction1) =
- let val thm =
- Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
- in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
- end handle Utils.ERR _ => (rules,induction);
+ val ((rules1, induction1), ctxt') =
+ let
+ val thm =
+ Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules)))) wf_tac
+ val ctxt' = Variable.declare_thm thm ctxt
+ in ((Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction), ctxt')
+ end handle Utils.ERR _ => ((rules, induction), ctxt);
(*----------------------------------------------------------------------
* The termination condition (tc) is simplified to |- tc = tc' (there
@@ -2425,15 +2421,15 @@
fun simplify_tc tc (r,ind) =
let val tc1 = tych tc
- val _ = trace_cterm ctxt "TC before simplification: " tc1
- val tc_eq = simplifier tc1
- val _ = trace_thms ctxt "result: " [tc_eq]
+ val _ = trace_cterm ctxt' "TC before simplification: " tc1
+ val tc_eq = simplifier ctxt' tc1
+ val _ = trace_thms ctxt' "result: " [tc_eq]
in
elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind)
handle Utils.ERR _ =>
(elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
- (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
- terminator)))
+ (Rules.prove ctxt' strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)))
+ terminator))
(r,ind)
handle Utils.ERR _ =>
(Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq),
@@ -2454,14 +2450,14 @@
* 3. return |- tc = tc'
*---------------------------------------------------------------------*)
fun simplify_nested_tc tc =
- let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
+ let val tc_eq = simplifier ctxt' (tych (#2 (USyntax.strip_forall tc)))
in
- Rules.GEN_ALL ctxt
+ Rules.GEN_ALL ctxt'
(Rules.MATCH_MP @{thm tfl_eq_True} tc_eq
handle Utils.ERR _ =>
(Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
- (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
- terminator))
+ (Rules.prove ctxt' strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)))
+ terminator)
handle Utils.ERR _ => tc_eq))
end
@@ -2512,12 +2508,12 @@
*--------------------------------------------------------------------------*)
fun std_postprocessor ctxt strict wfs =
Prim.postprocess ctxt strict
- {wf_tac = REPEAT (ares_tac ctxt wfs 1),
- terminator =
- asm_simp_tac ctxt 1
- THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
- fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
- simplifier = Rules.simpl_conv ctxt []};
+ {wf_tac = fn ctxt' => REPEAT (ares_tac ctxt' wfs 1),
+ terminator = fn ctxt' =>
+ asm_simp_tac ctxt' 1
+ THEN TRY (Arith_Data.arith_tac ctxt' 1 ORELSE
+ fast_force_tac (ctxt' addSDs @{thms not0_implies_Suc}) 1),
+ simplifier = fn ctxt' => Rules.simpl_conv ctxt' []};
@@ -2581,7 +2577,8 @@
val simplified' = map (join_assums ctxt) simplified
val dummy = (Prim.trace_thms ctxt "solved =" solved;
Prim.trace_thms ctxt "simplified' =" simplified')
- val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
+ fun rewr th =
+ full_simplify (Variable.declare_thm th ctxt addsimps (solved @ simplified')) th;
val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
val induction' = rewr induction
val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
@@ -2610,6 +2607,9 @@
val spec'=
Rule_Insts.read_instantiate \<^context> [((("x", 0), Position.none), "P::'b=>bool")] [] spec;
+fun rulify_no_asm ctxt th =
+ Object_Logic.rulify_no_asm (Variable.declare_thm th ctxt) th;
+
fun simplify_defn ctxt strict congs wfs pats def0 =
let
val thy = Proof_Context.theory_of ctxt;
@@ -2624,10 +2624,9 @@
{f = f, R = R, rules = rules,
full_pats_TCs = full_pats_TCs,
TCs = TCs}
- val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
- (Rules.CONJUNCTS rules)
+ val rules' = map (Drule.export_without_context o rulify_no_asm ctxt) (Rules.CONJUNCTS rules)
in
- {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
+ {induct = meta_outer ctxt (rulify_no_asm ctxt (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
@@ -2645,7 +2644,7 @@
| solve_eq _ (_, [a], i) = [(a, i)]
| solve_eq ctxt (th, splitths, i) =
(writeln "Proving unsplit equation...";
- [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
+ [((Drule.export_without_context o rulify_no_asm ctxt)
(CaseSplit.splitto ctxt splitths th), i)])
handle ERROR s =>
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
--- a/src/HOL/Library/simps_case_conv.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Library/simps_case_conv.ML Mon Oct 18 11:49:01 2021 +0200
@@ -64,8 +64,7 @@
let
val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
- fun dest_alls (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = dest_alls t
- | dest_alls t = t
+ val dest_alls = Term.strip_qnt_body \<^const_name>\<open>All\<close>
in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
handle TERM _ => false
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Oct 18 11:49:01 2021 +0200
@@ -25,7 +25,7 @@
(put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
- (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt));
+ (Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize_conv) ctxt));
fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
@@ -131,10 +131,10 @@
let
val prop = Thm.prop_of th;
fun prove t =
- Goal.prove ctxt [] [] t (fn _ =>
- EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1,
- REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
- REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))])
+ Goal.prove ctxt [] [] t (fn {context = goal_ctxt, ...} =>
+ EVERY [cut_facts_tac [th] 1, eresolve_tac goal_ctxt [rev_mp] 1,
+ REPEAT_DETERM (FIRSTGOAL (resolve_tac goal_ctxt monos)),
+ REPEAT_DETERM (resolve_tac goal_ctxt [impI] 1 THEN (assume_tac goal_ctxt 1 ORELSE tac))])
in Option.map prove (map_term f prop (the_default prop opt)) end;
val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion;
@@ -146,23 +146,23 @@
fun first_order_mrs ths th = ths MRS
Thm.instantiate (first_order_matchs (cprems_of th) (map Thm.cprop_of ths)) th;
-fun prove_strong_ind s avoids ctxt =
+fun prove_strong_ind s avoids lthy =
let
- val thy = Proof_Context.theory_of ctxt;
+ val thy = Proof_Context.theory_of lthy;
val ({names, ...}, {raw_induct, intrs, elims, ...}) =
- Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
+ Inductive.the_inductive_global lthy (Sign.intern_const thy s);
val ind_params = Inductive.params_of raw_induct;
- val raw_induct = atomize_induct ctxt raw_induct;
- val elims = map (atomize_induct ctxt) elims;
- val monos = Inductive.get_monos ctxt;
- val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
+ val raw_induct = atomize_induct lthy raw_induct;
+ val elims = map (atomize_induct lthy) elims;
+ val monos = Inductive.get_monos lthy;
+ val eqvt_thms = NominalThmDecls.get_eqvt_thms lthy;
val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
- (Induct.lookup_inductP ctxt (hd names)))));
- val (raw_induct', ctxt') = ctxt
+ (Induct.lookup_inductP lthy (hd names)))));
+ val (raw_induct', ctxt') = lthy
|> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct);
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
@@ -275,10 +275,11 @@
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
- val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
- addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
- NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
+ fun eqvt_ss ctxt =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
+ addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
+ NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
val perm_bij = Global_Theory.get_thms thy "perm_bij";
val fs_atoms = map (fn aT => Global_Theory.get_thm thy
@@ -299,26 +300,26 @@
(HOLogic.exists_const T $ Abs ("x", T,
NominalDatatype.fresh_const T (fastype_of p) $
Bound 0 $ p)))
- (fn _ => EVERY
- [resolve_tac ctxt exists_fresh' 1,
- resolve_tac ctxt fs_atoms 1]);
+ (fn {context = goal_ctxt, ...} => EVERY
+ [resolve_tac goal_ctxt exists_fresh' 1,
+ resolve_tac goal_ctxt fs_atoms 1]);
val (([(_, cx)], ths), ctxt') = Obtain.result
- (fn ctxt' => EVERY
- [eresolve_tac ctxt' [exE] 1,
- full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1,
- full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1,
- REPEAT (eresolve_tac ctxt [conjE] 1)])
+ (fn goal_ctxt => EVERY
+ [eresolve_tac goal_ctxt [exE] 1,
+ full_simp_tac (put_simpset HOL_ss goal_ctxt addsimps (fresh_prod :: fresh_atm)) 1,
+ full_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps [@{thm id_apply}]) 1,
+ REPEAT (eresolve_tac goal_ctxt [conjE] 1)])
[ex] ctxt
in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end;
- fun mk_ind_proof ctxt' thss =
- Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
- let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
- resolve_tac context [raw_induct] 1 THEN
+ fun mk_ind_proof ctxt thss =
+ Goal.prove ctxt [] prems' concl' (fn {prems = ihyps, context = goal_ctxt} =>
+ let val th = Goal.prove goal_ctxt [] [] concl (fn {context = goal_ctxt1, ...} =>
+ resolve_tac goal_ctxt1 [raw_induct] 1 THEN
EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
- [REPEAT (resolve_tac context [allI] 1),
- simp_tac (put_simpset eqvt_ss context) 1,
- SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
+ [REPEAT (resolve_tac goal_ctxt1 [allI] 1),
+ simp_tac (eqvt_ss goal_ctxt1) 1,
+ SUBPROOF (fn {prems = gprems, params, concl, context = goal_ctxt2, ...} =>
let
val (params', (pis, z)) =
chop (length params - length atomTs - 1) (map (Thm.term_of o #2) params) ||>
@@ -329,9 +330,9 @@
val pi_bvars = map (fn (t, _) =>
fold_rev (NominalDatatype.mk_perm []) pis t) bvars';
val (P, ts) = strip_comb (HOLogic.dest_Trueprop (Thm.term_of concl));
- val (freshs1, freshs2, ctxt'') = fold
+ val (freshs1, freshs2, ctxt') = fold
(obtain_fresh_name (ts @ pi_bvars))
- (map snd bvars') ([], [], ctxt');
+ (map snd bvars') ([], [], goal_ctxt2);
val freshs2' = NominalDatatype.mk_not_sym freshs2;
val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1);
fun concat_perm pi1 pi2 =
@@ -351,7 +352,7 @@
fun mk_pi th =
Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
addsimprocs [NominalDatatype.perm_simproc])
- (Simplifier.simplify (put_simpset eqvt_ss ctxt')
+ (Simplifier.simplify (eqvt_ss ctxt')
(fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
(rev pis' @ pis) th));
val (gprems1, gprems2) = split_list
@@ -371,51 +372,54 @@
(fn t => fn u => fresh $ t $ u, lhs, rhs)
| _ $ (_ $ (_ $ lhs $ rhs)) =>
(curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs));
- val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop
+ val th'' = Goal.prove ctxt' [] [] (HOLogic.mk_Trueprop
(bop (fold_rev (NominalDatatype.mk_perm []) pis lhs)
(fold_rev (NominalDatatype.mk_perm []) pis rhs)))
- (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps
- (fresh_bij @ perm_bij)) 1 THEN resolve_tac ctxt' [th'] 1)
- in Simplifier.simplify (put_simpset eqvt_ss ctxt'' addsimps fresh_atm) th'' end)
+ (fn {context = goal_ctxt3, ...} =>
+ simp_tac (put_simpset HOL_basic_ss goal_ctxt3 addsimps
+ (fresh_bij @ perm_bij)) 1 THEN resolve_tac goal_ctxt3 [th'] 1)
+ in Simplifier.simplify (eqvt_ss ctxt' addsimps fresh_atm) th'' end)
vc_compat_ths;
val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths';
(** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **)
(** we have to pre-simplify the rewrite rules **)
- val swap_simps_simpset = put_simpset HOL_ss ctxt'' addsimps swap_simps @
- map (Simplifier.simplify (put_simpset HOL_ss ctxt'' addsimps swap_simps))
+ val swap_simps_simpset = put_simpset HOL_ss ctxt' addsimps swap_simps @
+ map (Simplifier.simplify (put_simpset HOL_ss ctxt' addsimps swap_simps))
(vc_compat_ths'' @ freshs2');
- val th = Goal.prove ctxt'' [] []
+ val th = Goal.prove ctxt' [] []
(HOLogic.mk_Trueprop (list_comb (P $ hd ts,
map (fold (NominalDatatype.mk_perm []) pis') (tl ts))))
- (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1,
- resolve_tac ctxt'' [ihyp'] 1,
+ (fn {context = goal_ctxt4, ...} =>
+ EVERY ([simp_tac (eqvt_ss goal_ctxt4) 1,
+ resolve_tac goal_ctxt4 [ihyp'] 1,
REPEAT_DETERM_N (Thm.nprems_of ihyp - length gprems)
(simp_tac swap_simps_simpset 1),
REPEAT_DETERM_N (length gprems)
- (simp_tac (put_simpset HOL_basic_ss ctxt''
+ (simp_tac (put_simpset HOL_basic_ss goal_ctxt4
addsimps [inductive_forall_def']
addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
- resolve_tac ctxt'' gprems2 1)]));
- val final = Goal.prove ctxt'' [] [] (Thm.term_of concl)
- (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
+ resolve_tac goal_ctxt4 gprems2 1)]));
+ val final = Goal.prove ctxt' [] [] (Thm.term_of concl)
+ (fn {context = goal_ctxt5, ...} =>
+ cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss goal_ctxt5
addsimps vc_compat_ths'' @ freshs2' @
perm_fresh_fresh @ fresh_atm) 1);
- val final' = Proof_Context.export ctxt'' ctxt' [final];
- in resolve_tac ctxt' final' 1 end) context 1])
+ val final' = Proof_Context.export ctxt' goal_ctxt2 [final];
+ in resolve_tac goal_ctxt2 final' 1 end) goal_ctxt1 1])
(prems ~~ thss ~~ ihyps ~~ prems'')))
in
- cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt [conjE] 1) THEN
- REPEAT (REPEAT (resolve_tac ctxt [conjI, impI] 1) THEN
- eresolve_tac ctxt [impE] 1 THEN assume_tac ctxt 1 THEN
- REPEAT (eresolve_tac ctxt @{thms allE_Nil} 1) THEN
- asm_full_simp_tac ctxt 1)
- end) |> singleton (Proof_Context.export ctxt' ctxt);
+ cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac goal_ctxt [conjE] 1) THEN
+ REPEAT (REPEAT (resolve_tac goal_ctxt [conjI, impI] 1) THEN
+ eresolve_tac goal_ctxt [impE] 1 THEN assume_tac goal_ctxt 1 THEN
+ REPEAT (eresolve_tac goal_ctxt @{thms allE_Nil} 1) THEN
+ asm_full_simp_tac goal_ctxt 1)
+ end) |> singleton (Proof_Context.export ctxt lthy);
(** strong case analysis rule **)
val cases_prems = map (fn ((name, avoids), rule) =>
let
- val ([rule'], ctxt') = Variable.import_terms false [Thm.prop_of rule] ctxt;
+ val ([rule'], ctxt') = Variable.import_terms false [Thm.prop_of rule] lthy;
val prem :: prems = Logic.strip_imp_prems rule';
val concl = Logic.strip_imp_concl rule'
in
@@ -460,18 +464,17 @@
concl))
in map mk_prem prems end) cases_prems;
- val cases_eqvt_simpset = put_simpset HOL_ss (Proof_Context.init_global thy)
- addsimps eqvt_thms @ swap_simps @ perm_pi_simp
- addsimprocs [NominalPermeq.perm_simproc_app,
- NominalPermeq.perm_simproc_fun];
+ fun cases_eqvt_simpset ctxt =
+ put_simpset HOL_ss ctxt
+ addsimps eqvt_thms @ swap_simps @ perm_pi_simp
+ addsimprocs [NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
- val simp_fresh_atm = map
- (Simplifier.simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
- addsimps fresh_atm));
+ fun simp_fresh_atm ctxt =
+ Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm);
- fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))),
+ fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt))),
prems') =
- (name, Goal.prove ctxt' [] (prem :: prems') concl
+ (name, Goal.prove ctxt [] (prem :: prems') concl
(fn {prems = hyp :: hyps, context = ctxt1} =>
EVERY (resolve_tac ctxt1 [hyp RS elim] 1 ::
map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
@@ -529,8 +532,8 @@
SUBPROOF (fn {context = ctxt5, prems = fresh_hyps, ...} =>
let
val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps;
- val case_simpset = cases_eqvt_simpset addsimps freshs2' @
- simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
+ val case_simpset = cases_eqvt_simpset ctxt5 addsimps freshs2' @
+ map (simp_fresh_atm ctxt5) (vc_compat_ths' @ fresh_hyps');
val fresh_fresh_simpset = case_simpset addsimps perm_fresh_fresh;
val hyps1' = map
(mk_pis #> Simplifier.simplify fresh_fresh_simpset) hyps1;
@@ -545,22 +548,22 @@
val final = Proof_Context.export ctxt3 ctxt2 [th]
in resolve_tac ctxt2 final 1 end) ctxt1 1)
(thss ~~ hyps ~~ prems))) |>
- singleton (Proof_Context.export ctxt' ctxt))
+ singleton (Proof_Context.export ctxt lthy))
in
ctxt'' |>
- Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
+ Proof.theorem NONE (fn thss => fn lthy1 =>
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = Rule_Cases.case_names induct_cases;
val induct_cases' = Inductive.partition_rules' raw_induct
(intrs ~~ induct_cases);
- val thss' = map (map (atomize_intr ctxt)) thss;
+ val thss' = map (map (atomize_intr lthy1)) thss;
val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
val strong_raw_induct =
- mk_ind_proof ctxt thss' |> Inductive.rulify ctxt;
- val strong_cases = map (mk_cases_proof ##> Inductive.rulify ctxt)
+ mk_ind_proof lthy1 thss' |> Inductive.rulify lthy1;
+ val strong_cases = map (mk_cases_proof ##> Inductive.rulify lthy1)
(thsss ~~ elims ~~ cases_prems ~~ cases_prems');
val strong_induct_atts =
map (Attrib.internal o K)
@@ -568,12 +571,12 @@
val strong_induct =
if length names > 1 then strong_raw_induct
else strong_raw_induct RSN (2, rev_mp);
- val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
+ val ((_, [strong_induct']), lthy2) = lthy1 |> Local_Theory.note
((rec_qualified (Binding.name "strong_induct"), strong_induct_atts), [strong_induct]);
val strong_inducts =
- Project_Rule.projects ctxt (1 upto length names) strong_induct';
+ Project_Rule.projects lthy1 (1 upto length names) strong_induct';
in
- ctxt' |>
+ lthy2 |>
Local_Theory.notes
[((rec_qualified (Binding.name "strong_inducts"), []),
strong_inducts |> map (fn th => ([th],
@@ -588,15 +591,15 @@
(map (map (rulify_term thy #> rpair [])) vc_compat)
end;
-fun prove_eqvt s xatoms ctxt = (* FIXME ctxt should be called lthy *)
+fun prove_eqvt s xatoms lthy =
let
- val thy = Proof_Context.theory_of ctxt;
+ val thy = Proof_Context.theory_of lthy;
val ({names, ...}, {raw_induct, intrs, elims, ...}) =
- Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
- val raw_induct = atomize_induct ctxt raw_induct;
- val elims = map (atomize_induct ctxt) elims;
- val intrs = map (atomize_intr ctxt) intrs;
- val monos = Inductive.get_monos ctxt;
+ Inductive.the_inductive_global lthy (Sign.intern_const thy s);
+ val raw_induct = atomize_induct lthy raw_induct;
+ val elims = map (atomize_induct lthy) elims;
+ val intrs = map (atomize_intr lthy) intrs;
+ val monos = Inductive.get_monos lthy;
val intrs' = Inductive.unpartition_rules intrs
(map (fn (((s, ths), (_, k)), th) =>
(s, ths ~~ Inductive.infer_intro_vars thy th k ths))
@@ -617,43 +620,43 @@
atoms)
end;
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
- val (([t], [pi]), ctxt') = ctxt |>
+ val (([t], [pi]), ctxt1) = lthy |>
Variable.import_terms false [Thm.concl_of raw_induct] ||>>
Variable.variant_fixes ["pi"];
- val eqvt_simpset = put_simpset HOL_basic_ss ctxt' addsimps
- (NominalThmDecls.get_eqvt_thms ctxt' @ perm_pi_simp) addsimprocs
+ fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps
+ (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
[mk_perm_bool_simproc names,
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
val ps = map (fst o HOLogic.dest_imp)
(HOLogic.dest_conj (HOLogic.dest_Trueprop t));
- fun eqvt_tac pi (intr, vs) st =
+ fun eqvt_tac ctxt pi (intr, vs) st =
let
fun eqvt_err s =
- let val ([t], ctxt'') = Variable.import_terms true [Thm.prop_of intr] ctxt'
+ let val ([t], ctxt') = Variable.import_terms true [Thm.prop_of intr] ctxt
in error ("Could not prove equivariance for introduction rule\n" ^
- Syntax.string_of_term ctxt'' t ^ "\n" ^ s)
+ Syntax.string_of_term ctxt' t ^ "\n" ^ s)
end;
- val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
+ val res = SUBPROOF (fn {context = goal_ctxt, prems, params, ...} =>
let
- val prems' = map (fn th => the_default th (map_thm ctxt''
- (split_conj (K I) names) (eresolve_tac ctxt'' [conjunct2] 1) monos NONE th)) prems;
- val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
- (mk_perm_bool ctxt'' (Thm.cterm_of ctxt'' pi) th)) prems';
- val intr' = infer_instantiate ctxt'' (map (#1 o dest_Var) vs ~~
- map (Thm.cterm_of ctxt'' o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
+ val prems' = map (fn th => the_default th (map_thm goal_ctxt
+ (split_conj (K I) names) (eresolve_tac goal_ctxt [conjunct2] 1) monos NONE th)) prems;
+ val prems'' = map (fn th => Simplifier.simplify (eqvt_simpset goal_ctxt)
+ (mk_perm_bool goal_ctxt (Thm.cterm_of goal_ctxt pi) th)) prems';
+ val intr' = infer_instantiate goal_ctxt (map (#1 o dest_Var) vs ~~
+ map (Thm.cterm_of goal_ctxt o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
intr
- in (resolve_tac ctxt'' [intr'] THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
- end) ctxt' 1 st
+ in (resolve_tac goal_ctxt [intr'] THEN_ALL_NEW (TRY o resolve_tac goal_ctxt prems'')) 1
+ end) ctxt 1 st
in
case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
NONE => eqvt_err ("Rule does not match goal\n" ^
- Syntax.string_of_term ctxt' (hd (Thm.prems_of st)))
+ Syntax.string_of_term ctxt (hd (Thm.prems_of st)))
| SOME (th, _) => Seq.single th
end;
val thss = map (fn atom =>
let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
in map (fn th => zero_var_indexes (th RS mp))
- (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
+ (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt1 [] []
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
let
val (h, ts) = strip_comb p;
@@ -662,13 +665,14 @@
HOLogic.mk_imp (p, list_comb (h, ts1 @
map (NominalDatatype.mk_perm [] pi') ts2))
end) ps)))
- (fn _ => EVERY (resolve_tac ctxt' [raw_induct] 1 :: map (fn intr_vs =>
- full_simp_tac eqvt_simpset 1 THEN
- eqvt_tac pi' intr_vs) intrs')) |>
- singleton (Proof_Context.export ctxt' ctxt)))
+ (fn {context = goal_ctxt, ...} =>
+ EVERY (resolve_tac goal_ctxt [raw_induct] 1 :: map (fn intr_vs =>
+ full_simp_tac (eqvt_simpset goal_ctxt) 1 THEN
+ eqvt_tac goal_ctxt pi' intr_vs) intrs')) |>
+ singleton (Proof_Context.export ctxt1 lthy)))
end) atoms
in
- ctxt |>
+ lthy |>
Local_Theory.notes (map (fn (name, ths) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
[Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Oct 18 11:49:01 2021 +0200
@@ -26,7 +26,7 @@
(put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
- (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt));
+ (Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize_conv) ctxt));
fun fresh_postprocess ctxt =
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps
@@ -136,10 +136,10 @@
let
val prop = Thm.prop_of th;
fun prove t =
- Goal.prove ctxt [] [] t (fn _ =>
- EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1,
- REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
- REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))])
+ Goal.prove ctxt [] [] t (fn {context = goal_ctxt, ...} =>
+ EVERY [cut_facts_tac [th] 1, eresolve_tac goal_ctxt [rev_mp] 1,
+ REPEAT_DETERM (FIRSTGOAL (resolve_tac goal_ctxt monos)),
+ REPEAT_DETERM (resolve_tac goal_ctxt [impI] 1 THEN (assume_tac goal_ctxt 1 ORELSE tac))])
in Option.map prove (map_term f prop (the_default prop opt)) end;
fun abs_params params t =
@@ -153,25 +153,25 @@
Thm.instantiate (TVars.empty, Vars.make (map (dest_Var o Envir.subst_term env) vs ~~ cts)) th
end;
-fun prove_strong_ind s alt_name avoids ctxt =
+fun prove_strong_ind s alt_name avoids lthy =
let
- val thy = Proof_Context.theory_of ctxt;
+ val thy = Proof_Context.theory_of lthy;
val ({names, ...}, {raw_induct, intrs, elims, ...}) =
- Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
+ Inductive.the_inductive_global lthy (Sign.intern_const thy s);
val ind_params = Inductive.params_of raw_induct;
- val raw_induct = atomize_induct ctxt raw_induct;
- val elims = map (atomize_induct ctxt) elims;
- val monos = Inductive.get_monos ctxt;
- val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
+ val raw_induct = atomize_induct lthy raw_induct;
+ val elims = map (atomize_induct lthy) elims;
+ val monos = Inductive.get_monos lthy;
+ val eqvt_thms = NominalThmDecls.get_eqvt_thms lthy;
val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
- (Induct.lookup_inductP ctxt (hd names)))));
+ (Induct.lookup_inductP lthy (hd names)))));
val induct_cases' = if null induct_cases then replicate (length intrs) ""
else induct_cases;
- val (raw_induct', ctxt') = ctxt
+ val (raw_induct', ctxt') = lthy
|> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct);
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
@@ -186,7 +186,7 @@
fun mk_avoids params name sets =
let
val (_, ctxt') = Proof_Context.add_fixes
- (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
+ (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) lthy;
fun mk s =
let
val t = Syntax.read_term ctxt' s;
@@ -294,10 +294,11 @@
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn a => Global_Theory.get_thm thy
("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
- val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
- addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
- NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
+ fun eqvt_ss ctxt =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
+ addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
+ NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
@@ -343,22 +344,23 @@
(Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
(f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
(pis1 @ pi :: pis2) l $ r)))
- (fn _ => cut_facts_tac [th2] 1 THEN
- full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps perm_set_forget) 1) |>
- Simplifier.simplify (put_simpset eqvt_ss ctxt')
+ (fn {context = goal_ctxt, ...} =>
+ cut_facts_tac [th2] 1 THEN
+ full_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps perm_set_forget) 1) |>
+ Simplifier.simplify (eqvt_ss ctxt')
in
(freshs @ [Thm.term_of cx],
ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt')
end;
- fun mk_ind_proof ctxt' thss =
- Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
- let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
- resolve_tac ctxt [raw_induct] 1 THEN
+ fun mk_ind_proof ctxt thss =
+ Goal.prove ctxt [] prems' concl' (fn {prems = ihyps, context = goal_ctxt} =>
+ let val th = Goal.prove goal_ctxt [] [] concl (fn {context = goal_ctxt1, ...} =>
+ resolve_tac goal_ctxt1 [raw_induct] 1 THEN
EVERY (maps (fn (((((_, sets, oprems, _),
vc_compat_ths), vc_compat_vs), ihyp), vs_ihypt) =>
- [REPEAT (resolve_tac ctxt [allI] 1), simp_tac (put_simpset eqvt_ss context) 1,
- SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
+ [REPEAT (resolve_tac goal_ctxt1 [allI] 1), simp_tac (eqvt_ss goal_ctxt1) 1,
+ SUBPROOF (fn {prems = gprems, params, concl, context = goal_ctxt2, ...} =>
let
val (cparams', (pis, z)) =
chop (length params - length atomTs - 1) (map #2 params) ||>
@@ -371,8 +373,8 @@
val gprems1 = map_filter (fn (th, t) =>
if null (preds_of ps t) then SOME th
else
- map_thm ctxt' (split_conj (K o I) names)
- (eresolve_tac ctxt' [conjunct1] 1) monos NONE th)
+ map_thm goal_ctxt2 (split_conj (K o I) names)
+ (eresolve_tac goal_ctxt2 [conjunct1] 1) monos NONE th)
(gprems ~~ oprems);
val vc_compat_ths' = map2 (fn th => fn p =>
let
@@ -380,20 +382,21 @@
val (h, ts) =
strip_comb (HOLogic.dest_Trueprop (Thm.concl_of th'))
in
- Goal.prove ctxt' [] []
+ Goal.prove goal_ctxt2 [] []
(HOLogic.mk_Trueprop (list_comb (h,
map (fold_rev (NominalDatatype.mk_perm []) pis) ts)))
- (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt' addsimps
- (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac ctxt' [th'] 1)
+ (fn {context = goal_ctxt3, ...} =>
+ simp_tac (put_simpset HOL_basic_ss goal_ctxt3 addsimps
+ (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac goal_ctxt3 [th'] 1)
end) vc_compat_ths vc_compat_vs;
val (vc_compat_ths1, vc_compat_ths2) =
chop (length vc_compat_ths - length sets) vc_compat_ths';
val vc_compat_ths1' = map
(Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
- (Simplifier.rewrite (put_simpset eqvt_ss ctxt'))))) vc_compat_ths1;
+ (Simplifier.rewrite (eqvt_ss goal_ctxt2))))) vc_compat_ths1;
val (pis', fresh_ths1, fresh_ths2, fresh_ths3, ctxt'') = fold
(obtain_fresh_name ts sets)
- (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], ctxt');
+ (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], goal_ctxt2);
fun concat_perm pi1 pi2 =
let val T = fastype_of pi1
in if T = fastype_of pi2 then
@@ -405,16 +408,17 @@
(map (fold_rev (NominalDatatype.mk_perm [])
(pis' @ pis) #> Thm.global_cterm_of thy) params' @ [Thm.global_cterm_of thy z]);
fun mk_pi th =
- Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
+ Simplifier.simplify
+ (put_simpset HOL_basic_ss ctxt'' addsimps [@{thm id_apply}]
addsimprocs [NominalDatatype.perm_simproc])
- (Simplifier.simplify (put_simpset eqvt_ss ctxt')
- (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
+ (Simplifier.simplify (eqvt_ss ctxt'')
+ (fold_rev (mk_perm_bool ctxt'' o Thm.cterm_of ctxt'')
(pis' @ pis) th));
val gprems2 = map (fn (th, t) =>
if null (preds_of ps t) then mk_pi th
else
- mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
- (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))
+ mk_pi (the (map_thm ctxt'' (inst_conj_all names ps (rev pis''))
+ (inst_conj_all_tac ctxt'' (length pis'')) monos (SOME t) th)))
(gprems ~~ oprems);
val perm_freshs_freshs' = map (fn (th, (_, T)) =>
th RS the (AList.lookup op = perm_freshs_freshs T))
@@ -422,44 +426,45 @@
val th = Goal.prove ctxt'' [] []
(HOLogic.mk_Trueprop (list_comb (P $ hd ts,
map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts))))
- (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1,
- resolve_tac ctxt'' [ihyp'] 1] @
- map (fn th => resolve_tac ctxt'' [th] 1) fresh_ths3 @
+ (fn {context = goal_ctxt4, ...} =>
+ EVERY ([simp_tac (eqvt_ss goal_ctxt4) 1,
+ resolve_tac goal_ctxt4 [ihyp'] 1] @
+ map (fn th => resolve_tac goal_ctxt4 [th] 1) fresh_ths3 @
[REPEAT_DETERM_N (length gprems)
- (simp_tac (put_simpset HOL_basic_ss ctxt''
+ (simp_tac (put_simpset HOL_basic_ss goal_ctxt4
addsimps [inductive_forall_def']
addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
- resolve_tac ctxt'' gprems2 1)]));
+ resolve_tac goal_ctxt4 gprems2 1)]));
val final = Goal.prove ctxt'' [] [] (Thm.term_of concl)
- (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
+ (fn {context = goal_ctxt5, ...} =>
+ cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss goal_ctxt5
addsimps vc_compat_ths1' @ fresh_ths1 @
perm_freshs_freshs') 1);
- val final' = Proof_Context.export ctxt'' ctxt' [final];
- in resolve_tac ctxt' final' 1 end) context 1])
+ val final' = Proof_Context.export ctxt'' goal_ctxt2 [final];
+ in resolve_tac goal_ctxt2 final' 1 end) goal_ctxt1 1])
(prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems'')))
in
- cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt' [conjE] 1) THEN
- REPEAT (REPEAT (resolve_tac ctxt' [conjI, impI] 1) THEN
- eresolve_tac ctxt' [impE] 1 THEN
- assume_tac ctxt' 1 THEN REPEAT (eresolve_tac ctxt' @{thms allE_Nil} 1) THEN
- asm_full_simp_tac ctxt 1)
+ cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac goal_ctxt [conjE] 1) THEN
+ REPEAT (REPEAT (resolve_tac goal_ctxt [conjI, impI] 1) THEN
+ eresolve_tac goal_ctxt [impE] 1 THEN
+ assume_tac goal_ctxt 1 THEN REPEAT (eresolve_tac goal_ctxt @{thms allE_Nil} 1) THEN
+ asm_full_simp_tac goal_ctxt 1)
end) |>
- fresh_postprocess ctxt' |>
- singleton (Proof_Context.export ctxt' ctxt);
-
+ fresh_postprocess ctxt |>
+ singleton (Proof_Context.export ctxt lthy);
in
ctxt'' |>
- Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
+ Proof.theorem NONE (fn thss => fn lthy1 =>
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = Rule_Cases.case_names induct_cases;
val induct_cases' = Inductive.partition_rules' raw_induct
(intrs ~~ induct_cases);
- val thss' = map (map (atomize_intr ctxt)) thss;
+ val thss' = map (map (atomize_intr lthy1)) thss;
val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
val strong_raw_induct =
- mk_ind_proof ctxt thss' |> Inductive.rulify ctxt;
+ mk_ind_proof lthy1 thss' |> Inductive.rulify lthy1;
val strong_induct_atts =
map (Attrib.internal o K)
[ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
@@ -471,12 +476,12 @@
NONE => (rec_qualified (Binding.name "strong_induct"),
rec_qualified (Binding.name "strong_inducts"))
| SOME s => (Binding.name s, Binding.name (s ^ "s"));
- val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
+ val ((_, [strong_induct']), lthy2) = lthy1 |> Local_Theory.note
((induct_name, strong_induct_atts), [strong_induct]);
val strong_inducts =
- Project_Rule.projects ctxt' (1 upto length names) strong_induct'
+ Project_Rule.projects lthy2 (1 upto length names) strong_induct'
in
- ctxt' |>
+ lthy2 |>
Local_Theory.notes [((inducts_name, []),
strong_inducts |> map (fn th => ([th],
[Attrib.internal (K ind_case_names),
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Mon Oct 18 11:49:01 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 (SOME 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 12:42:51 2021 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Oct 18 11:49:01 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_core.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Mon Oct 18 11:49:01 2021 +0200
@@ -622,8 +622,8 @@
local open Conv in
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
val sih =
- fconv_rule (Conv.binder_conv
- (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
+ fconv_rule
+ (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
end
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
--- a/src/HOL/Tools/Function/function_lib.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Oct 18 11:49:01 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 NONE 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
@@ -135,14 +135,14 @@
| _ => raise Fail "abstract: Bad term"
end;
-(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
+(* Traverse a theorem, replacing lambda-abstractions with combinators. *)
fun introduce_combinators_in_cterm ctxt ct =
if is_quasi_lambda_free (Thm.term_of ct) then
Thm.reflexive ct
else case Thm.term_of ct of
Abs _ =>
let
- val (cv, cta) = Thm.dest_abs NONE 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 NONE 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 (SOME 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Oct 18 11:49:01 2021 +0200
@@ -145,7 +145,7 @@
fun get_pmi_term t =
let val (x,eq) =
- (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE 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 NONE
+ 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 NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
- |> Thm.dest_abs NONE |> 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 NONE (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
@@ -640,7 +640,7 @@
| fm_of_term ps vs (\<^term>\<open>(=) :: bool => _ \<close> $ t1 $ t2) =
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (Const (\<^const_name>\<open>Not\<close>, _) $ t') =
- Proc.NOT (fm_of_term ps vs t')
+ Proc.Not (fm_of_term ps vs t')
| fm_of_term ps vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs abs) =
Proc.E (uncurry (fm_of_term ps) (descend vs abs))
| fm_of_term ps vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs abs) =
@@ -677,18 +677,18 @@
| term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
| term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
| term_of_fm ps vs (Proc.Iff (t1, t2)) = \<^term>\<open>(=) :: bool => _\<close> $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
- | term_of_fm ps vs (Proc.NOT t') = HOLogic.Not $ term_of_fm ps vs t'
+ | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t'
| term_of_fm ps vs (Proc.Eq t') = \<^term>\<open>(=) :: int => _ \<close> $ term_of_num vs t'$ \<^term>\<open>0::int\<close>
- | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.NOT (Proc.Eq t'))
+ | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t'))
| term_of_fm ps vs (Proc.Lt t') = \<^term>\<open>(<) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close>
| term_of_fm ps vs (Proc.Le t') = \<^term>\<open>(<=) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close>
| term_of_fm ps vs (Proc.Gt t') = \<^term>\<open>(<) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t'
| term_of_fm ps vs (Proc.Ge t') = \<^term>\<open>(<=) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t'
| term_of_fm ps vs (Proc.Dvd (i, t')) = \<^term>\<open>(dvd) :: int => _ \<close> $
HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t'
- | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.NOT (Proc.Dvd (i, t')))
+ | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t')))
| term_of_fm ps vs (Proc.Closed n) = nth ps (Proc.integer_of_nat n)
- | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.NOT (Proc.Closed n));
+ | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n));
fun procedure t =
let
@@ -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 (SOME 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 NONE 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/cooper_procedure.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Qelim/cooper_procedure.ML Mon Oct 18 11:49:01 2021 +0200
@@ -7,7 +7,7 @@
Neg of numa | Add of numa * numa | Sub of numa * numa | Mul of inta * numa
datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa |
Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa |
- NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm
+ Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm
| E of fm | A of fm | Closed of nat | NClosed of nat
val pa : fm -> fm
val nat_of_integer : int -> nat
@@ -619,7 +619,7 @@
datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa |
Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa |
- NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm |
+ Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm |
E of fm | A of fm | Closed of nat | NClosed of nat;
fun id x = (fn xa => xa) x;
@@ -643,7 +643,7 @@
| disjuncts (NEq v) = [NEq v]
| disjuncts (Dvd (v, va)) = [Dvd (v, va)]
| disjuncts (NDvd (v, va)) = [NDvd (v, va)]
- | disjuncts (NOT v) = [NOT v]
+ | disjuncts (Not v) = [Not v]
| disjuncts (And (v, va)) = [And (v, va)]
| disjuncts (Imp (v, va)) = [Imp (v, va)]
| disjuncts (Iff (v, va)) = [Iff (v, va)]
@@ -711,22 +711,22 @@
| equal_fm (Imp (x141, x142)) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (Or (x131, x132)) = false
| equal_fm (Or (x131, x132)) (And (x121, x122)) = false
- | equal_fm (NOT x11) (NClosed x19) = false
- | equal_fm (NClosed x19) (NOT x11) = false
- | equal_fm (NOT x11) (Closed x18) = false
- | equal_fm (Closed x18) (NOT x11) = false
- | equal_fm (NOT x11) (A x17) = false
- | equal_fm (A x17) (NOT x11) = false
- | equal_fm (NOT x11) (E x16) = false
- | equal_fm (E x16) (NOT x11) = false
- | equal_fm (NOT x11) (Iff (x151, x152)) = false
- | equal_fm (Iff (x151, x152)) (NOT x11) = false
- | equal_fm (NOT x11) (Imp (x141, x142)) = false
- | equal_fm (Imp (x141, x142)) (NOT x11) = false
- | equal_fm (NOT x11) (Or (x131, x132)) = false
- | equal_fm (Or (x131, x132)) (NOT x11) = false
- | equal_fm (NOT x11) (And (x121, x122)) = false
- | equal_fm (And (x121, x122)) (NOT x11) = false
+ | equal_fm (Not x11) (NClosed x19) = false
+ | equal_fm (NClosed x19) (Not x11) = false
+ | equal_fm (Not x11) (Closed x18) = false
+ | equal_fm (Closed x18) (Not x11) = false
+ | equal_fm (Not x11) (A x17) = false
+ | equal_fm (A x17) (Not x11) = false
+ | equal_fm (Not x11) (E x16) = false
+ | equal_fm (E x16) (Not x11) = false
+ | equal_fm (Not x11) (Iff (x151, x152)) = false
+ | equal_fm (Iff (x151, x152)) (Not x11) = false
+ | equal_fm (Not x11) (Imp (x141, x142)) = false
+ | equal_fm (Imp (x141, x142)) (Not x11) = false
+ | equal_fm (Not x11) (Or (x131, x132)) = false
+ | equal_fm (Or (x131, x132)) (Not x11) = false
+ | equal_fm (Not x11) (And (x121, x122)) = false
+ | equal_fm (And (x121, x122)) (Not x11) = false
| equal_fm (NDvd (x101, x102)) (NClosed x19) = false
| equal_fm (NClosed x19) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (Closed x18) = false
@@ -743,8 +743,8 @@
| equal_fm (Or (x131, x132)) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (NDvd (x101, x102)) = false
- | equal_fm (NDvd (x101, x102)) (NOT x11) = false
- | equal_fm (NOT x11) (NDvd (x101, x102)) = false
+ | equal_fm (NDvd (x101, x102)) (Not x11) = false
+ | equal_fm (Not x11) (NDvd (x101, x102)) = false
| equal_fm (Dvd (x91, x92)) (NClosed x19) = false
| equal_fm (NClosed x19) (Dvd (x91, x92)) = false
| equal_fm (Dvd (x91, x92)) (Closed x18) = false
@@ -761,8 +761,8 @@
| equal_fm (Or (x131, x132)) (Dvd (x91, x92)) = false
| equal_fm (Dvd (x91, x92)) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (Dvd (x91, x92)) = false
- | equal_fm (Dvd (x91, x92)) (NOT x11) = false
- | equal_fm (NOT x11) (Dvd (x91, x92)) = false
+ | equal_fm (Dvd (x91, x92)) (Not x11) = false
+ | equal_fm (Not x11) (Dvd (x91, x92)) = false
| equal_fm (Dvd (x91, x92)) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (Dvd (x91, x92)) = false
| equal_fm (NEq x8) (NClosed x19) = false
@@ -781,8 +781,8 @@
| equal_fm (Or (x131, x132)) (NEq x8) = false
| equal_fm (NEq x8) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (NEq x8) = false
- | equal_fm (NEq x8) (NOT x11) = false
- | equal_fm (NOT x11) (NEq x8) = false
+ | equal_fm (NEq x8) (Not x11) = false
+ | equal_fm (Not x11) (NEq x8) = false
| equal_fm (NEq x8) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (NEq x8) = false
| equal_fm (NEq x8) (Dvd (x91, x92)) = false
@@ -803,8 +803,8 @@
| equal_fm (Or (x131, x132)) (Eq x7) = false
| equal_fm (Eq x7) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (Eq x7) = false
- | equal_fm (Eq x7) (NOT x11) = false
- | equal_fm (NOT x11) (Eq x7) = false
+ | equal_fm (Eq x7) (Not x11) = false
+ | equal_fm (Not x11) (Eq x7) = false
| equal_fm (Eq x7) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (Eq x7) = false
| equal_fm (Eq x7) (Dvd (x91, x92)) = false
@@ -827,8 +827,8 @@
| equal_fm (Or (x131, x132)) (Ge x6) = false
| equal_fm (Ge x6) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (Ge x6) = false
- | equal_fm (Ge x6) (NOT x11) = false
- | equal_fm (NOT x11) (Ge x6) = false
+ | equal_fm (Ge x6) (Not x11) = false
+ | equal_fm (Not x11) (Ge x6) = false
| equal_fm (Ge x6) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (Ge x6) = false
| equal_fm (Ge x6) (Dvd (x91, x92)) = false
@@ -853,8 +853,8 @@
| equal_fm (Or (x131, x132)) (Gt x5) = false
| equal_fm (Gt x5) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (Gt x5) = false
- | equal_fm (Gt x5) (NOT x11) = false
- | equal_fm (NOT x11) (Gt x5) = false
+ | equal_fm (Gt x5) (Not x11) = false
+ | equal_fm (Not x11) (Gt x5) = false
| equal_fm (Gt x5) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (Gt x5) = false
| equal_fm (Gt x5) (Dvd (x91, x92)) = false
@@ -881,8 +881,8 @@
| equal_fm (Or (x131, x132)) (Le x4) = false
| equal_fm (Le x4) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (Le x4) = false
- | equal_fm (Le x4) (NOT x11) = false
- | equal_fm (NOT x11) (Le x4) = false
+ | equal_fm (Le x4) (Not x11) = false
+ | equal_fm (Not x11) (Le x4) = false
| equal_fm (Le x4) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (Le x4) = false
| equal_fm (Le x4) (Dvd (x91, x92)) = false
@@ -911,8 +911,8 @@
| equal_fm (Or (x131, x132)) (Lt x3) = false
| equal_fm (Lt x3) (And (x121, x122)) = false
| equal_fm (And (x121, x122)) (Lt x3) = false
- | equal_fm (Lt x3) (NOT x11) = false
- | equal_fm (NOT x11) (Lt x3) = false
+ | equal_fm (Lt x3) (Not x11) = false
+ | equal_fm (Not x11) (Lt x3) = false
| equal_fm (Lt x3) (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) (Lt x3) = false
| equal_fm (Lt x3) (Dvd (x91, x92)) = false
@@ -943,8 +943,8 @@
| equal_fm (Or (x131, x132)) F = false
| equal_fm F (And (x121, x122)) = false
| equal_fm (And (x121, x122)) F = false
- | equal_fm F (NOT x11) = false
- | equal_fm (NOT x11) F = false
+ | equal_fm F (Not x11) = false
+ | equal_fm (Not x11) F = false
| equal_fm F (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) F = false
| equal_fm F (Dvd (x91, x92)) = false
@@ -977,8 +977,8 @@
| equal_fm (Or (x131, x132)) T = false
| equal_fm T (And (x121, x122)) = false
| equal_fm (And (x121, x122)) T = false
- | equal_fm T (NOT x11) = false
- | equal_fm (NOT x11) T = false
+ | equal_fm T (Not x11) = false
+ | equal_fm (Not x11) T = false
| equal_fm T (NDvd (x101, x102)) = false
| equal_fm (NDvd (x101, x102)) T = false
| equal_fm T (Dvd (x91, x92)) = false
@@ -1009,7 +1009,7 @@
equal_fm x131 y131 andalso equal_fm x132 y132
| equal_fm (And (x121, x122)) (And (y121, y122)) =
equal_fm x121 y121 andalso equal_fm x122 y122
- | equal_fm (NOT x11) (NOT y11) = equal_fm x11 y11
+ | equal_fm (Not x11) (Not y11) = equal_fm x11 y11
| equal_fm (NDvd (x101, x102)) (NDvd (y101, y102)) =
equal_inta x101 y101 andalso equal_numa x102 y102
| equal_fm (Dvd (x91, x92)) (Dvd (y91, y92)) =
@@ -1030,7 +1030,7 @@
| Le _ => Or (f p, q) | Gt _ => Or (f p, q)
| Ge _ => Or (f p, q) | Eq _ => Or (f p, q)
| NEq _ => Or (f p, q) | Dvd (_, _) => Or (f p, q)
- | NDvd (_, _) => Or (f p, q) | NOT _ => Or (f p, q)
+ | NDvd (_, _) => Or (f p, q) | Not _ => Or (f p, q)
| And (_, _) => Or (f p, q) | Or (_, _) => Or (f p, q)
| Imp (_, _) => Or (f p, q) | Iff (_, _) => Or (f p, q)
| E _ => Or (f p, q) | A _ => Or (f p, q)
@@ -1089,7 +1089,7 @@
| minusinf (NEq (Mul (va, vb))) = NEq (Mul (va, vb))
| minusinf (Dvd (v, va)) = Dvd (v, va)
| minusinf (NDvd (v, va)) = NDvd (v, va)
- | minusinf (NOT v) = NOT v
+ | minusinf (Not v) = Not v
| minusinf (Imp (v, va)) = Imp (v, va)
| minusinf (Iff (v, va)) = Iff (v, va)
| minusinf (E v) = E v
@@ -1138,7 +1138,7 @@
| subst0 t (NEq a) = NEq (numsubst0 t a)
| subst0 t (Dvd (i, a)) = Dvd (i, numsubst0 t a)
| subst0 t (NDvd (i, a)) = NDvd (i, numsubst0 t a)
- | subst0 t (NOT p) = NOT (subst0 t p)
+ | subst0 t (Not p) = Not (subst0 t p)
| subst0 t (And (p, q)) = And (subst0 t p, subst0 t q)
| subst0 t (Or (p, q)) = Or (subst0 t p, subst0 t q)
| subst0 t (Imp (p, q)) = Imp (subst0 t p, subst0 t q)
@@ -1263,25 +1263,25 @@
else (if equal_fm p T then q
else (if equal_fm q T then p else And (p, q))));
-fun nota (NOT p) = p
+fun nota (Not p) = p
| nota T = F
| nota F = T
- | nota (Lt v) = NOT (Lt v)
- | nota (Le v) = NOT (Le v)
- | nota (Gt v) = NOT (Gt v)
- | nota (Ge v) = NOT (Ge v)
- | nota (Eq v) = NOT (Eq v)
- | nota (NEq v) = NOT (NEq v)
- | nota (Dvd (v, va)) = NOT (Dvd (v, va))
- | nota (NDvd (v, va)) = NOT (NDvd (v, va))
- | nota (And (v, va)) = NOT (And (v, va))
- | nota (Or (v, va)) = NOT (Or (v, va))
- | nota (Imp (v, va)) = NOT (Imp (v, va))
- | nota (Iff (v, va)) = NOT (Iff (v, va))
- | nota (E v) = NOT (E v)
- | nota (A v) = NOT (A v)
- | nota (Closed v) = NOT (Closed v)
- | nota (NClosed v) = NOT (NClosed v);
+ | nota (Lt v) = Not (Lt v)
+ | nota (Le v) = Not (Le v)
+ | nota (Gt v) = Not (Gt v)
+ | nota (Ge v) = Not (Ge v)
+ | nota (Eq v) = Not (Eq v)
+ | nota (NEq v) = Not (NEq v)
+ | nota (Dvd (v, va)) = Not (Dvd (v, va))
+ | nota (NDvd (v, va)) = Not (NDvd (v, va))
+ | nota (And (v, va)) = Not (And (v, va))
+ | nota (Or (v, va)) = Not (Or (v, va))
+ | nota (Imp (v, va)) = Not (Imp (v, va))
+ | nota (Iff (v, va)) = Not (Iff (v, va))
+ | nota (E v) = Not (E v)
+ | nota (A v) = Not (A v)
+ | nota (Closed v) = Not (Closed v)
+ | nota (NClosed v) = Not (NClosed v);
fun imp p q =
(if equal_fm p F orelse equal_fm q T then T
@@ -1301,7 +1301,7 @@
| simpfm (Or (p, q)) = disj (simpfm p) (simpfm q)
| simpfm (Imp (p, q)) = imp (simpfm p) (simpfm q)
| simpfm (Iff (p, q)) = iff (simpfm p) (simpfm q)
- | simpfm (NOT p) = nota (simpfm p)
+ | simpfm (Not p) = nota (simpfm p)
| simpfm (Lt a) =
let
val aa = simpnum a;
@@ -1442,7 +1442,7 @@
| a_beta (NDvd (v, Add (vb, vc))) k = NDvd (v, Add (vb, vc))
| a_beta (NDvd (v, Sub (vb, vc))) k = NDvd (v, Sub (vb, vc))
| a_beta (NDvd (v, Mul (vb, vc))) k = NDvd (v, Mul (vb, vc))
- | a_beta (NOT v) k = NOT v
+ | a_beta (Not v) k = Not v
| a_beta (Imp (v, va)) k = Imp (v, va)
| a_beta (Iff (v, va)) k = Iff (v, va)
| a_beta (E v) k = E v
@@ -1515,7 +1515,7 @@
| delta (NDvd (v, Add (vb, vc))) = one_inta
| delta (NDvd (v, Sub (vb, vc))) = one_inta
| delta (NDvd (v, Mul (vb, vc))) = one_inta
- | delta (NOT v) = one_inta
+ | delta (Not v) = one_inta
| delta (Imp (v, va)) = one_inta
| delta (Iff (v, va)) = one_inta
| delta (E v) = one_inta
@@ -1569,7 +1569,7 @@
| alpha (NEq (Mul (va, vb))) = []
| alpha (Dvd (v, va)) = []
| alpha (NDvd (v, va)) = []
- | alpha (NOT v) = []
+ | alpha (Not v) = []
| alpha (Imp (v, va)) = []
| alpha (Iff (v, va)) = []
| alpha (E v) = []
@@ -1637,7 +1637,7 @@
| zeta (NDvd (v, Add (vb, vc))) = one_inta
| zeta (NDvd (v, Sub (vb, vc))) = one_inta
| zeta (NDvd (v, Mul (vb, vc))) = one_inta
- | zeta (NOT v) = one_inta
+ | zeta (Not v) = one_inta
| zeta (Imp (v, va)) = one_inta
| zeta (Iff (v, va)) = one_inta
| zeta (E v) = one_inta
@@ -1697,7 +1697,7 @@
| beta (NEq (Mul (va, vb))) = []
| beta (Dvd (v, va)) = []
| beta (NDvd (v, va)) = []
- | beta (NOT v) = []
+ | beta (Not v) = []
| beta (Imp (v, va)) = []
| beta (Iff (v, va)) = []
| beta (E v) = []
@@ -1766,7 +1766,7 @@
| mirror (NDvd (v, Add (vb, vc))) = NDvd (v, Add (vb, vc))
| mirror (NDvd (v, Sub (vb, vc))) = NDvd (v, Sub (vb, vc))
| mirror (NDvd (v, Mul (vb, vc))) = NDvd (v, Mul (vb, vc))
- | mirror (NOT v) = NOT v
+ | mirror (Not v) = Not v
| mirror (Imp (v, va)) = Imp (v, va)
| mirror (Iff (v, va)) = Iff (v, va)
| mirror (E v) = E v
@@ -1848,9 +1848,9 @@
fun zlfm (And (p, q)) = And (zlfm p, zlfm q)
| zlfm (Or (p, q)) = Or (zlfm p, zlfm q)
- | zlfm (Imp (p, q)) = Or (zlfm (NOT p), zlfm q)
+ | zlfm (Imp (p, q)) = Or (zlfm (Not p), zlfm q)
| zlfm (Iff (p, q)) =
- Or (And (zlfm p, zlfm q), And (zlfm (NOT p), zlfm (NOT q)))
+ Or (And (zlfm p, zlfm q), And (zlfm (Not p), zlfm (Not q)))
| zlfm (Lt a) =
let
val (c, r) = zsplit0 a;
@@ -1920,28 +1920,28 @@
else NDvd (abs_int i,
CN (zero_nat, uminus_int c, Neg r))))
end)
- | zlfm (NOT (And (p, q))) = Or (zlfm (NOT p), zlfm (NOT q))
- | zlfm (NOT (Or (p, q))) = And (zlfm (NOT p), zlfm (NOT q))
- | zlfm (NOT (Imp (p, q))) = And (zlfm p, zlfm (NOT q))
- | zlfm (NOT (Iff (p, q))) =
- Or (And (zlfm p, zlfm (NOT q)), And (zlfm (NOT p), zlfm q))
- | zlfm (NOT (NOT p)) = zlfm p
- | zlfm (NOT T) = F
- | zlfm (NOT F) = T
- | zlfm (NOT (Lt a)) = zlfm (Ge a)
- | zlfm (NOT (Le a)) = zlfm (Gt a)
- | zlfm (NOT (Gt a)) = zlfm (Le a)
- | zlfm (NOT (Ge a)) = zlfm (Lt a)
- | zlfm (NOT (Eq a)) = zlfm (NEq a)
- | zlfm (NOT (NEq a)) = zlfm (Eq a)
- | zlfm (NOT (Dvd (i, a))) = zlfm (NDvd (i, a))
- | zlfm (NOT (NDvd (i, a))) = zlfm (Dvd (i, a))
- | zlfm (NOT (Closed p)) = NClosed p
- | zlfm (NOT (NClosed p)) = Closed p
+ | zlfm (Not (And (p, q))) = Or (zlfm (Not p), zlfm (Not q))
+ | zlfm (Not (Or (p, q))) = And (zlfm (Not p), zlfm (Not q))
+ | zlfm (Not (Imp (p, q))) = And (zlfm p, zlfm (Not q))
+ | zlfm (Not (Iff (p, q))) =
+ Or (And (zlfm p, zlfm (Not q)), And (zlfm (Not p), zlfm q))
+ | zlfm (Not (Not p)) = zlfm p
+ | zlfm (Not T) = F
+ | zlfm (Not F) = T
+ | zlfm (Not (Lt a)) = zlfm (Ge a)
+ | zlfm (Not (Le a)) = zlfm (Gt a)
+ | zlfm (Not (Gt a)) = zlfm (Le a)
+ | zlfm (Not (Ge a)) = zlfm (Lt a)
+ | zlfm (Not (Eq a)) = zlfm (NEq a)
+ | zlfm (Not (NEq a)) = zlfm (Eq a)
+ | zlfm (Not (Dvd (i, a))) = zlfm (NDvd (i, a))
+ | zlfm (Not (NDvd (i, a))) = zlfm (Dvd (i, a))
+ | zlfm (Not (Closed p)) = NClosed p
+ | zlfm (Not (NClosed p)) = Closed p
| zlfm T = T
| zlfm F = F
- | zlfm (NOT (E va)) = NOT (E va)
- | zlfm (NOT (A va)) = NOT (A va)
+ | zlfm (Not (E va)) = Not (E va)
+ | zlfm (Not (A va)) = Not (A va)
| zlfm (E v) = E v
| zlfm (A v) = A v
| zlfm (Closed v) = Closed v
@@ -1976,7 +1976,7 @@
| decr (NEq a) = NEq (decrnum a)
| decr (Dvd (i, a)) = Dvd (i, decrnum a)
| decr (NDvd (i, a)) = NDvd (i, decrnum a)
- | decr (NOT p) = NOT (decr p)
+ | decr (Not p) = Not (decr p)
| decr (And (p, q)) = And (decr p, decr q)
| decr (Or (p, q)) = Or (decr p, decr q)
| decr (Imp (p, q)) = Imp (decr p, decr q)
@@ -2014,8 +2014,8 @@
end;
fun qelim (E p) = (fn qe => dj qe (qelim p qe))
- | qelim (A p) = (fn qe => nota (qe (qelim (NOT p) qe)))
- | qelim (NOT p) = (fn qe => nota (qelim p qe))
+ | qelim (A p) = (fn qe => nota (qe (qelim (Not p) qe)))
+ | qelim (Not p) = (fn qe => nota (qelim p qe))
| qelim (And (p, q)) = (fn qe => conj (qelim p qe) (qelim q qe))
| qelim (Or (p, q)) = (fn qe => disj (qelim p qe) (qelim q qe))
| qelim (Imp (p, q)) = (fn qe => imp (qelim p qe) (qelim q qe))
@@ -2036,13 +2036,13 @@
fun prep (E T) = T
| prep (E F) = F
| prep (E (Or (p, q))) = Or (prep (E p), prep (E q))
- | prep (E (Imp (p, q))) = Or (prep (E (NOT p)), prep (E q))
+ | prep (E (Imp (p, q))) = Or (prep (E (Not p)), prep (E q))
| prep (E (Iff (p, q))) =
- Or (prep (E (And (p, q))), prep (E (And (NOT p, NOT q))))
- | prep (E (NOT (And (p, q)))) = Or (prep (E (NOT p)), prep (E (NOT q)))
- | prep (E (NOT (Imp (p, q)))) = prep (E (And (p, NOT q)))
- | prep (E (NOT (Iff (p, q)))) =
- Or (prep (E (And (p, NOT q))), prep (E (And (NOT p, q))))
+ Or (prep (E (And (p, q))), prep (E (And (Not p, Not q))))
+ | prep (E (Not (And (p, q)))) = Or (prep (E (Not p)), prep (E (Not q)))
+ | prep (E (Not (Imp (p, q)))) = prep (E (And (p, Not q)))
+ | prep (E (Not (Iff (p, q)))) =
+ Or (prep (E (And (p, Not q))), prep (E (And (Not p, q))))
| prep (E (Lt v)) = E (prep (Lt v))
| prep (E (Le v)) = E (prep (Le v))
| prep (E (Gt v)) = E (prep (Gt v))
@@ -2051,69 +2051,69 @@
| prep (E (NEq v)) = E (prep (NEq v))
| prep (E (Dvd (v, va))) = E (prep (Dvd (v, va)))
| prep (E (NDvd (v, va))) = E (prep (NDvd (v, va)))
- | prep (E (NOT T)) = E (prep (NOT T))
- | prep (E (NOT F)) = E (prep (NOT F))
- | prep (E (NOT (Lt va))) = E (prep (NOT (Lt va)))
- | prep (E (NOT (Le va))) = E (prep (NOT (Le va)))
- | prep (E (NOT (Gt va))) = E (prep (NOT (Gt va)))
- | prep (E (NOT (Ge va))) = E (prep (NOT (Ge va)))
- | prep (E (NOT (Eq va))) = E (prep (NOT (Eq va)))
- | prep (E (NOT (NEq va))) = E (prep (NOT (NEq va)))
- | prep (E (NOT (Dvd (va, vb)))) = E (prep (NOT (Dvd (va, vb))))
- | prep (E (NOT (NDvd (va, vb)))) = E (prep (NOT (NDvd (va, vb))))
- | prep (E (NOT (NOT va))) = E (prep (NOT (NOT va)))
- | prep (E (NOT (Or (va, vb)))) = E (prep (NOT (Or (va, vb))))
- | prep (E (NOT (E va))) = E (prep (NOT (E va)))
- | prep (E (NOT (A va))) = E (prep (NOT (A va)))
- | prep (E (NOT (Closed va))) = E (prep (NOT (Closed va)))
- | prep (E (NOT (NClosed va))) = E (prep (NOT (NClosed va)))
+ | prep (E (Not T)) = E (prep (Not T))
+ | prep (E (Not F)) = E (prep (Not F))
+ | prep (E (Not (Lt va))) = E (prep (Not (Lt va)))
+ | prep (E (Not (Le va))) = E (prep (Not (Le va)))
+ | prep (E (Not (Gt va))) = E (prep (Not (Gt va)))
+ | prep (E (Not (Ge va))) = E (prep (Not (Ge va)))
+ | prep (E (Not (Eq va))) = E (prep (Not (Eq va)))
+ | prep (E (Not (NEq va))) = E (prep (Not (NEq va)))
+ | prep (E (Not (Dvd (va, vb)))) = E (prep (Not (Dvd (va, vb))))
+ | prep (E (Not (NDvd (va, vb)))) = E (prep (Not (NDvd (va, vb))))
+ | prep (E (Not (Not va))) = E (prep (Not (Not va)))
+ | prep (E (Not (Or (va, vb)))) = E (prep (Not (Or (va, vb))))
+ | prep (E (Not (E va))) = E (prep (Not (E va)))
+ | prep (E (Not (A va))) = E (prep (Not (A va)))
+ | prep (E (Not (Closed va))) = E (prep (Not (Closed va)))
+ | prep (E (Not (NClosed va))) = E (prep (Not (NClosed va)))
| prep (E (And (v, va))) = E (prep (And (v, va)))
| prep (E (E v)) = E (prep (E v))
| prep (E (A v)) = E (prep (A v))
| prep (E (Closed v)) = E (prep (Closed v))
| prep (E (NClosed v)) = E (prep (NClosed v))
| prep (A (And (p, q))) = And (prep (A p), prep (A q))
- | prep (A T) = prep (NOT (E (NOT T)))
- | prep (A F) = prep (NOT (E (NOT F)))
- | prep (A (Lt v)) = prep (NOT (E (NOT (Lt v))))
- | prep (A (Le v)) = prep (NOT (E (NOT (Le v))))
- | prep (A (Gt v)) = prep (NOT (E (NOT (Gt v))))
- | prep (A (Ge v)) = prep (NOT (E (NOT (Ge v))))
- | prep (A (Eq v)) = prep (NOT (E (NOT (Eq v))))
- | prep (A (NEq v)) = prep (NOT (E (NOT (NEq v))))
- | prep (A (Dvd (v, va))) = prep (NOT (E (NOT (Dvd (v, va)))))
- | prep (A (NDvd (v, va))) = prep (NOT (E (NOT (NDvd (v, va)))))
- | prep (A (NOT v)) = prep (NOT (E (NOT (NOT v))))
- | prep (A (Or (v, va))) = prep (NOT (E (NOT (Or (v, va)))))
- | prep (A (Imp (v, va))) = prep (NOT (E (NOT (Imp (v, va)))))
- | prep (A (Iff (v, va))) = prep (NOT (E (NOT (Iff (v, va)))))
- | prep (A (E v)) = prep (NOT (E (NOT (E v))))
- | prep (A (A v)) = prep (NOT (E (NOT (A v))))
- | prep (A (Closed v)) = prep (NOT (E (NOT (Closed v))))
- | prep (A (NClosed v)) = prep (NOT (E (NOT (NClosed v))))
- | prep (NOT (NOT p)) = prep p
- | prep (NOT (And (p, q))) = Or (prep (NOT p), prep (NOT q))
- | prep (NOT (A p)) = prep (E (NOT p))
- | prep (NOT (Or (p, q))) = And (prep (NOT p), prep (NOT q))
- | prep (NOT (Imp (p, q))) = And (prep p, prep (NOT q))
- | prep (NOT (Iff (p, q))) = Or (prep (And (p, NOT q)), prep (And (NOT p, q)))
- | prep (NOT T) = NOT (prep T)
- | prep (NOT F) = NOT (prep F)
- | prep (NOT (Lt v)) = NOT (prep (Lt v))
- | prep (NOT (Le v)) = NOT (prep (Le v))
- | prep (NOT (Gt v)) = NOT (prep (Gt v))
- | prep (NOT (Ge v)) = NOT (prep (Ge v))
- | prep (NOT (Eq v)) = NOT (prep (Eq v))
- | prep (NOT (NEq v)) = NOT (prep (NEq v))
- | prep (NOT (Dvd (v, va))) = NOT (prep (Dvd (v, va)))
- | prep (NOT (NDvd (v, va))) = NOT (prep (NDvd (v, va)))
- | prep (NOT (E v)) = NOT (prep (E v))
- | prep (NOT (Closed v)) = NOT (prep (Closed v))
- | prep (NOT (NClosed v)) = NOT (prep (NClosed v))
+ | prep (A T) = prep (Not (E (Not T)))
+ | prep (A F) = prep (Not (E (Not F)))
+ | prep (A (Lt v)) = prep (Not (E (Not (Lt v))))
+ | prep (A (Le v)) = prep (Not (E (Not (Le v))))
+ | prep (A (Gt v)) = prep (Not (E (Not (Gt v))))
+ | prep (A (Ge v)) = prep (Not (E (Not (Ge v))))
+ | prep (A (Eq v)) = prep (Not (E (Not (Eq v))))
+ | prep (A (NEq v)) = prep (Not (E (Not (NEq v))))
+ | prep (A (Dvd (v, va))) = prep (Not (E (Not (Dvd (v, va)))))
+ | prep (A (NDvd (v, va))) = prep (Not (E (Not (NDvd (v, va)))))
+ | prep (A (Not v)) = prep (Not (E (Not (Not v))))
+ | prep (A (Or (v, va))) = prep (Not (E (Not (Or (v, va)))))
+ | prep (A (Imp (v, va))) = prep (Not (E (Not (Imp (v, va)))))
+ | prep (A (Iff (v, va))) = prep (Not (E (Not (Iff (v, va)))))
+ | prep (A (E v)) = prep (Not (E (Not (E v))))
+ | prep (A (A v)) = prep (Not (E (Not (A v))))
+ | prep (A (Closed v)) = prep (Not (E (Not (Closed v))))
+ | prep (A (NClosed v)) = prep (Not (E (Not (NClosed v))))
+ | prep (Not (Not p)) = prep p
+ | prep (Not (And (p, q))) = Or (prep (Not p), prep (Not q))
+ | prep (Not (A p)) = prep (E (Not p))
+ | prep (Not (Or (p, q))) = And (prep (Not p), prep (Not q))
+ | prep (Not (Imp (p, q))) = And (prep p, prep (Not q))
+ | prep (Not (Iff (p, q))) = Or (prep (And (p, Not q)), prep (And (Not p, q)))
+ | prep (Not T) = Not (prep T)
+ | prep (Not F) = Not (prep F)
+ | prep (Not (Lt v)) = Not (prep (Lt v))
+ | prep (Not (Le v)) = Not (prep (Le v))
+ | prep (Not (Gt v)) = Not (prep (Gt v))
+ | prep (Not (Ge v)) = Not (prep (Ge v))
+ | prep (Not (Eq v)) = Not (prep (Eq v))
+ | prep (Not (NEq v)) = Not (prep (NEq v))
+ | prep (Not (Dvd (v, va))) = Not (prep (Dvd (v, va)))
+ | prep (Not (NDvd (v, va))) = Not (prep (NDvd (v, va)))
+ | prep (Not (E v)) = Not (prep (E v))
+ | prep (Not (Closed v)) = Not (prep (Closed v))
+ | prep (Not (NClosed v)) = Not (prep (NClosed v))
| prep (Or (p, q)) = Or (prep p, prep q)
| prep (And (p, q)) = And (prep p, prep q)
- | prep (Imp (p, q)) = prep (Or (NOT p, q))
- | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (NOT p, NOT q)))
+ | prep (Imp (p, q)) = prep (Or (Not p, q))
+ | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (Not p, Not q)))
| prep T = T
| prep F = F
| prep (Lt v) = Lt v
--- a/src/HOL/Tools/Qelim/qelim.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Mon Oct 18 11:49:01 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 (SOME 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_def.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Oct 18 11:49:01 2021 +0200
@@ -86,21 +86,17 @@
(qconst_data Morphism.identity, lthy'')
end
-fun mk_readable_rsp_thm_eq tm lthy =
+fun mk_readable_rsp_thm_eq tm ctxt =
let
- val ctm = Thm.cterm_of lthy tm
+ val ctm = Thm.cterm_of ctxt tm
- fun norm_fun_eq ctm =
- let
- fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
- fun erase_quants ctm' =
- case (Thm.term_of ctm') of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
- | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
- Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
- in
- (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
- end
+ fun abs_conv2 cv = Conv.abs_conv (Conv.abs_conv (cv o #2) o #2) ctxt
+ fun erase_quants ctxt' ctm' =
+ case (Thm.term_of ctm') of
+ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
+ | _ => (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
+ Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+ val norm_fun_eq = abs_conv2 erase_quants then_conv Thm.eta_conversion
fun simp_arrows_conv ctm =
let
@@ -117,15 +113,15 @@
end
val unfold_ret_val_invs = Conv.bottom_conv
- (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
+ (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) ctxt
val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
- val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
+ val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) ctxt
val beta_conv = Thm.beta_conversion true
val eq_thm =
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
in
- Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
+ Object_Logic.rulify ctxt (eq_thm RS Drule.equal_elim_rule2)
end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Oct 18 11:49:01 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 NONE 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Mon Oct 18 11:49:01 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 (SOME 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/SMT/z3_isar.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/Tools/groebner.ML Mon Oct 18 11:49:01 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 NONE (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 (SOME (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/record.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/record.ML Mon Oct 18 11:49:01 2021 +0200
@@ -1355,7 +1355,8 @@
(Const (\<^const_name>\<open>Ex\<close>, Tex) $ Abs (s, T, eq), \<^term>\<open>True\<close>));
in
SOME (Goal.prove_sorry_global thy [] [] prop
- (fn _ => simp_tac (put_simpset (get_simpset thy) ctxt
+ (fn {context = ctxt', ...} =>
+ simp_tac (put_simpset (get_simpset thy) ctxt'
addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
end handle TERM _ => NONE)
| _ => NONE)
@@ -1602,12 +1603,12 @@
val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
simplify (put_simpset HOL_ss defs_ctxt)
(Goal.prove_sorry_global defs_thy [] [] inject_prop
- (fn {context = ctxt, ...} =>
- simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
+ (fn {context = ctxt', ...} =>
+ simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [ext_def]) 1 THEN
REPEAT_DETERM
- (resolve_tac ctxt @{thms refl_conj_eq} 1 ORELSE
- Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
- resolve_tac ctxt [refl] 1))));
+ (resolve_tac ctxt' @{thms refl_conj_eq} 1 ORELSE
+ Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE
+ resolve_tac ctxt' [refl] 1))));
(*We need a surjection property r = (| f = f r, g = g r ... |)
@@ -1634,21 +1635,21 @@
val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_meta_prop
- (fn {context = ctxt, ...} =>
+ (fn {context = ctxt', ...} =>
EVERY1
- [resolve_tac ctxt @{thms equal_intr_rule},
- Goal.norm_hhf_tac ctxt,
- eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt,
- resolve_tac ctxt [@{thm prop_subst} OF [surject]],
- REPEAT o eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt]));
+ [resolve_tac ctxt' @{thms equal_intr_rule},
+ Goal.norm_hhf_tac ctxt',
+ eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt',
+ resolve_tac ctxt' [@{thm prop_subst} OF [surject]],
+ REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt']));
val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
let val (assm, concl) = induct_prop in
Goal.prove_sorry_global defs_thy [] [assm] concl
- (fn {context = ctxt, prems, ...} =>
+ (fn {context = ctxt', prems, ...} =>
cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
- resolve_tac ctxt prems 2 THEN
- asm_simp_tac (put_simpset HOL_ss ctxt) 1)
+ resolve_tac ctxt' prems 2 THEN
+ asm_simp_tac (put_simpset HOL_ss ctxt') 1)
end);
val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_thy) =
@@ -2118,15 +2119,16 @@
(* 3rd stage: thms_thy *)
val record_ss = get_simpset defs_thy;
- val sel_upd_ctxt =
- put_simpset record_ss defs_ctxt
+ fun sel_upd_ctxt ctxt' =
+ put_simpset record_ss ctxt'
addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
val (sel_convs, upd_convs) =
timeit_msg defs_ctxt "record sel_convs/upd_convs proof:" (fn () =>
grouped 10 Par_List.map (fn prop =>
Goal.prove_sorry_global defs_thy [] [] prop
- (fn _ => ALLGOALS (asm_full_simp_tac sel_upd_ctxt)))
+ (fn {context = ctxt', ...} =>
+ ALLGOALS (asm_full_simp_tac (sel_upd_ctxt ctxt'))))
(sel_conv_props @ upd_conv_props))
|> chop (length sel_conv_props);
@@ -2141,43 +2143,43 @@
val induct_scheme = timeit_msg defs_ctxt "record induct_scheme proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop
- (fn {context = ctxt, ...} =>
+ (fn {context = ctxt', ...} =>
EVERY
- [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt rN ind 1,
- try_param_tac ctxt rN ext_induct 1,
- asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1]));
+ [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt' rN ind 1,
+ try_param_tac ctxt' rN ext_induct 1,
+ asm_simp_tac (put_simpset HOL_basic_ss ctxt') 1]));
val induct = timeit_msg defs_ctxt "record induct proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop)
- (fn {context = ctxt, prems, ...} =>
- try_param_tac ctxt rN induct_scheme 1
- THEN try_param_tac ctxt "more" @{thm unit.induct} 1
- THEN resolve_tac ctxt prems 1));
+ (fn {context = ctxt', prems, ...} =>
+ try_param_tac ctxt' rN induct_scheme 1
+ THEN try_param_tac ctxt' "more" @{thm unit.induct} 1
+ THEN resolve_tac ctxt' prems 1));
val surjective = timeit_msg defs_ctxt "record surjective proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] surjective_prop
- (fn {context = ctxt, ...} =>
+ (fn {context = ctxt', ...} =>
EVERY
- [resolve_tac ctxt [surject_assist_idE] 1,
- simp_tac (put_simpset HOL_basic_ss ctxt addsimps ext_defs) 1,
+ [resolve_tac ctxt' [surject_assist_idE] 1,
+ simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ext_defs) 1,
REPEAT
- (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
- (resolve_tac ctxt [surject_assistI] 1 THEN
- simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt
+ (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE
+ (resolve_tac ctxt' [surject_assistI] 1 THEN
+ simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt'
addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))]));
val cases_scheme = timeit_msg defs_ctxt "record cases_scheme proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
- (fn {context = ctxt, prems, ...} =>
- resolve_tac ctxt prems 1 THEN
- resolve_tac ctxt [surjective] 1));
+ (fn {context = ctxt', prems, ...} =>
+ resolve_tac ctxt' prems 1 THEN
+ resolve_tac ctxt' [surjective] 1));
val cases = timeit_msg defs_ctxt "record cases proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] cases_prop
- (fn {context = ctxt, ...} =>
- try_param_tac ctxt rN cases_scheme 1 THEN
+ (fn {context = ctxt', ...} =>
+ try_param_tac ctxt' rN cases_scheme 1 THEN
ALLGOALS (asm_full_simp_tac
- (put_simpset HOL_basic_ss ctxt addsimps @{thms unit_all_eq1}))));
+ (put_simpset HOL_basic_ss ctxt' addsimps @{thms unit_all_eq1}))));
val split_meta = timeit_msg defs_ctxt "record split_meta proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_meta_prop
@@ -2190,24 +2192,24 @@
val split_object = timeit_msg defs_ctxt "record split_object proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_object_prop
- (fn {context = ctxt, ...} =>
- resolve_tac ctxt [@{lemma "Trueprop A \<equiv> Trueprop B \<Longrightarrow> A = B" by (rule iffI) unfold}] 1 THEN
- rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
- resolve_tac ctxt [split_meta] 1));
+ (fn {context = ctxt', ...} =>
+ resolve_tac ctxt' [@{lemma "Trueprop A \<equiv> Trueprop B \<Longrightarrow> A = B" by (rule iffI) unfold}] 1 THEN
+ rewrite_goals_tac ctxt' @{thms atomize_all [symmetric]} THEN
+ resolve_tac ctxt' [split_meta] 1));
val split_ex = timeit_msg defs_ctxt "record split_ex proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_ex_prop
- (fn {context = ctxt, ...} =>
+ (fn {context = ctxt', ...} =>
simp_tac
- (put_simpset HOL_basic_ss ctxt addsimps
+ (put_simpset HOL_basic_ss ctxt' addsimps
(@{lemma "\<exists>x. P x \<equiv> \<not> (\<forall>x. \<not> P x)" by simp} ::
@{thms not_not Not_eq_iff})) 1 THEN
- resolve_tac ctxt [split_object] 1));
+ resolve_tac ctxt' [split_object] 1));
val equality = timeit_msg defs_ctxt "record equality proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] equality_prop
- (fn {context = ctxt, ...} =>
- asm_full_simp_tac (put_simpset record_ss ctxt addsimps (split_meta :: sel_convs)) 1));
+ (fn {context = ctxt', ...} =>
+ asm_full_simp_tac (put_simpset record_ss ctxt' addsimps (split_meta :: sel_convs)) 1));
val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'),
(_, fold_congs'), (_, unfold_congs'),
--- a/src/HOL/Tools/reification.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/reification.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/Pure/Tools/find_theorems.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/Pure/conv.ML Mon Oct 18 11:49:01 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 (SOME 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 12:42:51 2021 +0100
+++ b/src/Pure/logic.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/Pure/more_pattern.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/Pure/more_thm.ML Mon Oct 18 11:49:01 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 NONE (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 12:42:51 2021 +0100
+++ b/src/Pure/raw_simplifier.ML Mon Oct 18 11:49:01 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 (SOME 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 12:42:51 2021 +0100
+++ b/src/Pure/term.ML Mon Oct 18 11:49:01 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 12:42:51 2021 +0100
+++ b/src/Pure/thm.ML Mon Oct 18 11:49:01 2021 +0200
@@ -48,7 +48,8 @@
val dest_arg: cterm -> cterm
val dest_fun2: cterm -> cterm
val dest_arg1: cterm -> cterm
- val dest_abs: string option -> 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
@@ -304,12 +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 a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) =
- let val (y', t') = Term.dest_abs (the_default x a, 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 _ ct = raise CTERM ("dest_abs", [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]));
+
+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 12:42:51 2021 +0100
+++ b/src/Pure/variable.ML Mon Oct 18 11:49:01 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
@@ -313,12 +317,16 @@
(** bounds **)
-fun next_bound (a, T) ctxt =
+fun inc_bound (a, T) ctxt =
let
val b = Name.bound (#1 (#bounds (rep_data ctxt)));
val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds));
in (Free (b, T), ctxt') end;
+fun next_bound a ctxt =
+ let val (x as Free (b, _), ctxt') = inc_bound a ctxt
+ in if Name.is_declared (names_of ctxt') b then inc_bound a ctxt' else (x, ctxt') end;
+
fun revert_bounds ctxt t =
(case #2 (#bounds (rep_data ctxt)) of
[] => t
@@ -326,8 +334,10 @@
let
val names = Term.declare_term_names t (names_of ctxt);
val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names));
- fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
- in Term.subst_atomic (map2 subst bounds xs) t end);
+ fun substs (((b, T), _), x') =
+ let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U))
+ in [subst T, subst (Type_Annotation.ignore_type T)] end;
+ in Term.subst_atomic (maps substs (bounds ~~ xs)) t end);
@@ -650,6 +660,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 12:42:51 2021 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Oct 18 11:49:01 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/induct.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/Tools/induct.ML Mon Oct 18 11:49:01 2021 +0200
@@ -444,8 +444,8 @@
val equal_def' = Thm.symmetric Induct_Args.equal_def;
fun mark_constraints n ctxt = Conv.fconv_rule
- (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
- (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
+ (Conv.prems_conv ~1 (Conv.params_conv ~1 (fn ctxt' =>
+ Conv.prems_conv n (Raw_Simplifier.rewrite ctxt' false [equal_def'])) ctxt));
fun unmark_constraints ctxt =
Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
--- a/src/Tools/misc_legacy.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/Tools/misc_legacy.ML Mon Oct 18 11:49:01 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);