# HG changeset patch # User wenzelm # Date 1634574826 -7200 # Node ID 2ff001a8c9f22f0def7b15c441dd6ea75098f0a5 # Parent dc1a7c10565b489f8d505826de6299df3dc91ed1# Parent c87b403b03eb450d173491cf0e758ef3bd708cbf merged diff -r dc1a7c10565b -r 2ff001a8c9f2 NEWS --- a/NEWS Thu Oct 14 16:56:02 2021 +0200 +++ b/NEWS Mon Oct 18 18:33:46 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/FOLP/simp.ML Mon Oct 18 18:33:46 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 = diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Analysis/metric_arith.ML --- a/src/HOL/Analysis/metric_arith.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Analysis/metric_arith.ML Mon Oct 18 18:33:46 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Mon Oct 18 18:33:46 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_>\HOL.Not for t'\ = @{code Not} (fm_of_term ps vs t') - | fm_of_term ps vs \<^Const_>\Ex _ for \Abs (xn, xT, p)\\ = + | fm_of_term ps vs \<^Const_>\Ex _ for \t as Abs _\\ = 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_>\All _ for \Abs (xn, xT, p)\\ = + 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_>\All _ for \t as Abs _\\ = 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; diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Oct 18 18:33:46 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_>\less_eq _ for p q\ = @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) - | fm_of_term fs ps (\<^Const_>\Ex _\ $ 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_>\All _\ $ 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_>\Ex _ for \p as Abs _\\ = + 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_>\All _ for \p as Abs _\\ = + 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)) = diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Oct 18 18:33:46 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_>\Ex _ for \Abs(xn,xT,_)\\ => - Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn + \<^Const_>\Ex _ for \Abs (xn, _, _)\\ => + 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_>\HOL.eq \<^Type>\bool\ for _ _\ => find_args bounds tm - | \<^Const_>\Not for _\ => h bounds (Thm.dest_arg tm) - | \<^Const_>\All _ for _\ => find_body bounds (Thm.dest_arg tm) - | \<^Const_>\Ex _ for _\ => find_body bounds (Thm.dest_arg tm) - | \<^Const_>\conj for _ _\ => find_args bounds tm - | \<^Const_>\disj for _ _\ => find_args bounds tm - | \<^Const_>\implies for _ _\ => find_args bounds tm - | \<^Const_>\Pure.imp for _ _\ => find_args bounds tm - | \<^Const_>\Pure.eq _ for _ _\ => find_args bounds tm - | \<^Const_>\Pure.all _ for _\ => find_body bounds (Thm.dest_arg tm) - | \<^Const_>\Trueprop for _\ => h bounds (Thm.dest_arg tm) + \<^Const_>\HOL.eq \<^Type>\bool\ for _ _\ => find_args ctxt tm + | \<^Const_>\Not for _\ => h ctxt (Thm.dest_arg tm) + | \<^Const_>\All _ for _\ => find_body ctxt (Thm.dest_arg tm) + | \<^Const_>\Ex _ for _\ => find_body ctxt (Thm.dest_arg tm) + | \<^Const_>\conj for _ _\ => find_args ctxt tm + | \<^Const_>\disj for _ _\ => find_args ctxt tm + | \<^Const_>\implies for _ _\ => find_args ctxt tm + | \<^Const_>\Pure.imp for _ _\ => find_args ctxt tm + | \<^Const_>\Pure.eq _ for _ _\ => find_args ctxt tm + | \<^Const_>\Pure.all _ for _\ => find_body ctxt (Thm.dest_arg tm) + | \<^Const_>\Trueprop for _\ => 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Decision_Procs/langford.ML Mon Oct 18 18:33:46 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_>\Ex _ for \Abs (xn, _, _)\\ => + \<^Const_>\Ex _ for \Abs _\\ => 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>\Trueprop\ 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_>\HOL.eq \<^Type>\bool\ for _ _\ => find_args bounds tm - | \<^Const_>\Not for _\ => h bounds (Thm.dest_arg tm) - | \<^Const_>\All _ for _\ => find_body bounds (Thm.dest_arg tm) - | \<^Const_>\Pure.all _ for _\ => find_body bounds (Thm.dest_arg tm) - | \<^Const_>\Ex _ for _\ => find_body bounds (Thm.dest_arg tm) - | \<^Const_>\HOL.conj for _ _\ => find_args bounds tm - | \<^Const_>\HOL.disj for _ _\ => find_args bounds tm - | \<^Const_>\HOL.implies for _ _\ => find_args bounds tm - | \<^Const_>\Pure.imp for _ _\ => find_args bounds tm - | \<^Const_>\Pure.eq _ for _ _\ => find_args bounds tm - | \<^Const_>\Trueprop for _\ => h bounds (Thm.dest_arg tm) + \<^Const_>\HOL.eq \<^Type>\bool\ for _ _\ => find_args ctxt tm + | \<^Const_>\Not for _\ => h ctxt (Thm.dest_arg tm) + | \<^Const_>\All _ for _\ => find_body ctxt (Thm.dest_arg tm) + | \<^Const_>\Pure.all _ for _\ => find_body ctxt (Thm.dest_arg tm) + | \<^Const_>\Ex _ for _\ => find_body ctxt (Thm.dest_arg tm) + | \<^Const_>\HOL.conj for _ _\ => find_args ctxt tm + | \<^Const_>\HOL.disj for _ _\ => find_args ctxt tm + | \<^Const_>\HOL.implies for _ _\ => find_args ctxt tm + | \<^Const_>\Pure.imp for _ _\ => find_args ctxt tm + | \<^Const_>\Pure.eq _ for _ _\ => find_args ctxt tm + | \<^Const_>\Trueprop for _\ => 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) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/HOL.thy Mon Oct 18 18:33:46 2021 +0200 @@ -2104,9 +2104,9 @@ method_setup eval = \ 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Oct 18 18:33:46 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) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Library/Pattern_Aliases.thy --- a/src/HOL/Library/Pattern_Aliases.thy Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Library/Pattern_Aliases.thy Mon Oct 18 18:33:46 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) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Oct 18 18:33:46 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>\Ex\,_)$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>\All\,_)$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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Library/cconv.ML Mon Oct 18 18:33:46 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 \ ... \ Pn \ L v \ R v And build a term of form: \v. (\x. L x) v \ (\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 \ ... \ An \ B*) fun prems_cconv 0 cv ct = cv ct | prems_cconv n cv ct = diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Library/old_recdef.ML Mon Oct 18 18:33:46 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); diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Library/simps_case_conv.ML --- a/src/HOL/Library/simps_case_conv.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Library/simps_case_conv.ML Mon Oct 18 18:33:46 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>\All\, _) $ Abs (_, _, t)) = dest_alls t - | dest_alls t = t + val dest_alls = Term.strip_qnt_body \<^const_name>\All\ in forall (is_free_eq_imp o dest_alls) (get_conjs t) end handle TERM _ => false diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Mon Oct 18 18:33:46 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>\Fun.id\], - 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>\Fun.id\], + 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, [])])) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Oct 18 18:33:46 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>\Fun.id\], - 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>\Fun.id\], + 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), diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Real_Asymp/exp_log_expression.ML --- a/src/HOL/Real_Asymp/exp_log_expression.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Real_Asymp/exp_log_expression.ML Mon Oct 18 18:33:46 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Mon Oct 18 18:33:46 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' diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/TPTP/atp_problem_import.ML diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Oct 18 18:33:46 2021 +0200 @@ -451,9 +451,9 @@ make_case ctxt (if b = \<^term>\True\ 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)); diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Mon Oct 18 18:33:46 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Mon Oct 18 18:33:46 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>\Pure.all\,_) $ _)) = +fun dest_all_all \<^Const>\Pure.all _ for t\ = 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') diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Function/partial_function.ML diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Oct 18 18:33:46 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_>\All _ for \Abs abs\\ rhss = dec_sko (#2 (Term.dest_abs abs)) rhss + | dec_sko \<^Const_>\All _ for \t as Abs _\\ rhss = dec_sko (#2 (Term.dest_abs_global t)) rhss | dec_sko \<^Const_>\conj for p q\ rhss = rhss |> dec_sko p |> dec_sko q | dec_sko \<^Const_>\disj for p q\ rhss = rhss |> dec_sko p |> dec_sko q | dec_sko \<^Const_>\Trueprop for p\ 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>\Pure.all\ orelse s = \<^const_name>\All\ orelse s = \<^const_name>\Ex\ 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, _) $ _ $ _ => diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Metis/metis_tactic.ML diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Mon Oct 18 18:33:46 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>\int\); @@ -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>\(=) :: bool => _ \ $ t1 $ t2) = Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (Const (\<^const_name>\Not\, _) $ 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>\Ex\, _) $ Abs abs) = Proc.E (uncurry (fm_of_term ps) (descend vs abs)) | fm_of_term ps vs (Const (\<^const_name>\All\, _) $ 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>\(=) :: bool => _\ $ 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>\(=) :: int => _ \ $ term_of_num vs t'$ \<^term>\0::int\ - | 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>\(<) :: int => _ \ $ term_of_num vs t' $ \<^term>\0::int\ | term_of_fm ps vs (Proc.Le t') = \<^term>\(<=) :: int => _ \ $ term_of_num vs t' $ \<^term>\0::int\ | term_of_fm ps vs (Proc.Gt t') = \<^term>\(<) :: int => _ \ $ \<^term>\0::int\ $ term_of_num vs t' | term_of_fm ps vs (Proc.Ge t') = \<^term>\(<=) :: int => _ \ $ \<^term>\0::int\ $ term_of_num vs t' | term_of_fm ps vs (Proc.Dvd (i, t')) = \<^term>\(dvd) :: int => _ \ $ 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>\All\, _) $ Abs (xn,_,_) => - let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct + Const (\<^const_name>\All\, _) $ 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; diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Qelim/cooper_procedure.ML --- a/src/HOL/Tools/Qelim/cooper_procedure.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Qelim/cooper_procedure.ML Mon Oct 18 18:33:46 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Mon Oct 18 18:33:46 2021 +0200 @@ -29,10 +29,10 @@ then Conv.binop_conv (conv env) p else atcv env p | Const(\<^const_name>\Not\,_)$_ => Conv.arg_conv (conv env) p - | Const(\<^const_name>\Ex\,_)$Abs(s,_,_) => + | Const(\<^const_name>\Ex\,_)$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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Oct 18 18:33:46 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>\HOL.eq\, _) $ _ $ _ => 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>\HOL.eq\, _) $ _ $ _ => 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Oct 18 18:33:46 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Oct 18 18:33:46 2021 +0200 @@ -713,12 +713,12 @@ mk_repabs ctxt (rty, qty) (Const (\<^const_name>\Babs\, 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Oct 18 18:33:46 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) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/SMT/smt_util.ML --- a/src/HOL/Tools/SMT/smt_util.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_util.ML Mon Oct 18 18:33:46 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) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/SMT/z3_isar.ML --- a/src/HOL/Tools/SMT/z3_isar.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/SMT/z3_isar.ML Mon Oct 18 18:33:46 2021 +0200 @@ -62,10 +62,9 @@ end end -fun dest_alls (Const (\<^const_name>\Pure.all\, _) $ Abs (abs as (_, T, _))) = - let val (s', t') = Term.dest_abs abs in - dest_alls t' |>> cons (s', T) - end +fun dest_alls \<^Const_>\Pure.all _ for \t as Abs _\\ = + let val (v, t') = Term.dest_abs_global t + in dest_alls t' |>> cons v end | dest_alls t = ([], t) val reorder_foralls = diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/Transfer/transfer.ML diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/datatype_realizer.ML diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/groebner.ML Mon Oct 18 18:33:46 2021 +0200 @@ -385,8 +385,8 @@ val strip_exists = let fun h (acc, t) = case Thm.term_of t of - Const (\<^const_name>\Ex\, _) $ Abs _ => - h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc)) + \<^Const_>\Ex _ for \Abs _\\ => + 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>\HOL.eq\, T) $ _ $ _ => - if domain_type T = HOLogic.boolT then find_args bounds tm - else Thm.dest_arg tm - | Const (\<^const_name>\Not\, _) $ _ => find_term bounds (Thm.dest_arg tm) - | Const (\<^const_name>\All\, _) $ _ => find_body bounds (Thm.dest_arg tm) - | Const (\<^const_name>\Ex\, _) $ _ => find_body bounds (Thm.dest_arg tm) - | Const (\<^const_name>\HOL.conj\, _) $ _ $ _ => find_args bounds tm - | Const (\<^const_name>\HOL.disj\, _) $ _ $ _ => find_args bounds tm - | Const (\<^const_name>\HOL.implies\, _) $ _ $ _ => find_args bounds tm - | \<^term>\Pure.imp\ $_$_ => find_args bounds tm - | Const("(==)",_)$_$_ => find_args bounds tm (* FIXME proper const name *) - | \<^term>\Trueprop\$_ => 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>\Not\, _) $ _ => find_term (Thm.dest_arg tm) ctxt + | Const (\<^const_name>\All\, _) $ _ => find_body (Thm.dest_arg tm) ctxt + | Const (\<^const_name>\Ex\, _) $ _ => find_body (Thm.dest_arg tm) ctxt + | Const (\<^const_name>\HOL.conj\, _) $ _ $ _ => find_args tm ctxt + | Const (\<^const_name>\HOL.disj\, _) $ _ $ _ => find_args tm ctxt + | Const (\<^const_name>\HOL.implies\, _) $ _ $ _ => find_args tm ctxt + | \<^term>\Pure.imp\ $_$_ => find_args tm ctxt + | Const("(==)",_)$_$_ => find_args tm ctxt (* FIXME proper const name *) + | \<^term>\Trueprop\$_ => 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>\find_term form ctxt\ 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/record.ML Mon Oct 18 18:33:46 2021 +0200 @@ -1355,7 +1355,8 @@ (Const (\<^const_name>\Ex\, Tex) $ Abs (s, T, eq), \<^term>\True\)); 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 \ Trueprop B \ 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 \ Trueprop B \ 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 "\x. P x \ \ (\x. \ 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'), diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/Tools/reification.ML --- a/src/HOL/Tools/reification.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/Tools/reification.ML Mon Oct 18 18:33:46 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, diff -r dc1a7c10565b -r 2ff001a8c9f2 src/HOL/ex/Sketch_and_Explore.thy --- a/src/HOL/ex/Sketch_and_Explore.thy Thu Oct 14 16:56:02 2021 +0200 +++ b/src/HOL/ex/Sketch_and_Explore.thy Mon Oct 18 18:33:46 2021 +0200 @@ -12,7 +12,7 @@ ML \ 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; diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/Tools/find_theorems.ML Mon Oct 18 18:33:46 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; diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/conv.ML --- a/src/Pure/conv.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/conv.ML Mon Oct 18 18:33:46 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 = diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/goal.ML diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/logic.ML --- a/src/Pure/logic.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/logic.ML Mon Oct 18 18:33:46 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)); diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/more_pattern.ML --- a/src/Pure/more_pattern.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/more_pattern.ML Mon Oct 18 18:33:46 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'') diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/more_thm.ML Mon Oct 18 18:33:46 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; diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/raw_simplifier.ML Mon Oct 18 18:33:46 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 $ _ => diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/term.ML --- a/src/Pure/term.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/term.ML Mon Oct 18 18:33:46 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 *) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/thm.ML Mon Oct 18 18:33:46 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 *) diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Pure/variable.ML Mon Oct 18 18:33:46 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: \x y z. B *) val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false); diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Tools/Code/code_thingol.ML Mon Oct 18 18:33:46 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 diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Tools/induct.ML Mon Oct 18 18:33:46 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]); diff -r dc1a7c10565b -r 2ff001a8c9f2 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Thu Oct 14 16:56:02 2021 +0200 +++ b/src/Tools/misc_legacy.ML Mon Oct 18 18:33:46 2021 +0200 @@ -126,9 +126,9 @@ it replaces the bound variables by free variables. *) fun strip_context_aux (params, Hs, \<^Const_>\Pure.imp for H B\) = strip_context_aux (params, H :: Hs, B) - | strip_context_aux (params, Hs, \<^Const_>\Pure.all _ for \Abs (a, T, t)\\) = - 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_>\Pure.all _ for \t as Abs _\\) = + 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);