--- a/src/Pure/term.ML Mon Dec 11 17:28:21 2023 +0100
+++ b/src/Pure/term.ML Mon Dec 11 21:56:24 2023 +0100
@@ -646,29 +646,31 @@
fun incr_boundvars inc = incr_bv inc 0;
-(*Scan a pair of terms; while they are similar,
- accumulate corresponding bound vars in "al"*)
-fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
- match_bvs(s, t, if x="" orelse y="" then al
- else (x,y)::al)
- | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
- | match_bvs(_,_,al) = al;
+(*Scan a pair of terms; while they are similar, accumulate corresponding bound vars*)
+fun match_bvs (Abs (x, _, s), Abs (y, _, t)) =
+ (x <> "" andalso y <> "") ? cons (x, y) #> match_bvs (s, t)
+ | match_bvs (f $ s, g $ t) = match_bvs (s, t) #> match_bvs (f, g)
+ | match_bvs _ = I;
(* strip abstractions created by parameters *)
-fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al);
+val match_bvars = apply2 strip_abs_body #> match_bvs;
-fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
- | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
- | map_abs_vars f t = t;
+fun map_abs_vars_same rename =
+ let
+ fun term (Abs (x, T, t)) =
+ let val y = rename x
+ in if x = y then Abs (x, T, term t) else Abs (y, T, Same.commit term t) end
+ | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
+ | term _ = raise Same.SAME;
+ in term end;
+
+fun map_abs_vars rename = Same.commit (map_abs_vars_same rename);
fun rename_abs pat obj t =
let
- val ren = match_bvs (pat, obj, []);
- fun ren_abs (Abs (x, T, b)) =
- Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
- | ren_abs (f $ t) = ren_abs f $ ren_abs t
- | ren_abs t = t
- in if null ren then NONE else SOME (ren_abs t) end;
+ val renaming = Symtab.make_distinct (match_bvs (pat, obj) []);
+ fun rename x = perhaps (Symtab.lookup renaming) x;
+ in if Symtab.forall (op =) renaming then NONE else Same.catch (map_abs_vars_same rename) t end;
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
(Bound 0) is loose at level 0 *)
--- a/src/Pure/thm.ML Mon Dec 11 17:28:21 2023 +0100
+++ b/src/Pure/thm.ML Mon Dec 11 21:56:24 2023 +0100
@@ -2029,12 +2029,13 @@
if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
else
let
+ val cert = join_certificate1 (goal, orule);
val prems = map lift_all As;
- fun zproof p = ZTerm.todo_proof p;
+ fun zproof p = ZTerm.lift_proof (Context.certificate_theory cert) gprop inc prems p;
fun proof p = Proofterm.lift_proof gprop inc prems p;
in
Thm (deriv_rule1 zproof proof der,
- {cert = join_certificate1 (goal, orule),
+ {cert = cert,
tags = [],
maxidx = maxidx + inc,
constraints = constraints,
@@ -2223,43 +2224,53 @@
(*Use the alist to rename all bound variables and some unknowns in a term
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex);
Preserves unknowns in tpairs and on lhs of dpairs. *)
-fun rename_bvs [] _ _ _ _ = K I
- | rename_bvs al dpairs tpairs B As =
+fun rename_bvs dpairs tpairs B As =
+ let val al = fold_rev Term.match_bvars dpairs [] in
+ if null al then {vars = Symtab.empty, bounds = Symtab.empty}
+ else
let
- val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I);
- val vids = []
- |> fold (add_var o fst) dpairs
- |> fold (add_var o fst) tpairs
- |> fold (add_var o snd) tpairs;
- val vids' = fold (add_var o strip_lifted B) As [];
+ val add_var = fold_aterms (fn Var ((x, _), _) => Symset.insert x | _ => I);
+ val unknowns =
+ Symset.build
+ (fold (add_var o fst) dpairs #>
+ fold (fn (t, u) => add_var t #> add_var u) tpairs);
+
(*unknowns appearing elsewhere be preserved!*)
- val al' = distinct ((op =) o apply2 fst)
- (filter_out (fn (x, y) =>
- not (member (op =) vids' x) orelse
- member (op =) vids x orelse member (op =) vids y) al);
- val unchanged = filter_out (AList.defined (op =) al') vids';
+ val unknowns' = Symset.build (fold (add_var o strip_lifted B) As);
+ val al' = al
+ |> filter_out (fn (x, y) =>
+ not (Symset.member unknowns' x) orelse
+ Symset.member unknowns x orelse Symset.member unknowns y)
+ |> distinct (eq_fst (op =));
+ val unchanged = Symset.restrict (not o AList.defined (op =) al') unknowns';
+
fun del_clashing clash xs _ [] qs =
if clash then del_clashing false xs xs qs [] else qs
| del_clashing clash xs ys ((p as (x, y)) :: ps) qs =
- if member (op =) ys y
- then del_clashing true (x :: xs) (x :: ys) ps qs
- else del_clashing clash xs (y :: ys) ps (p :: qs);
+ if Symset.member ys y
+ then del_clashing true (Symset.insert x xs) (Symset.insert x ys) ps qs
+ else del_clashing clash xs (Symset.insert y ys) ps (p :: qs);
val al'' = del_clashing false unchanged unchanged al' [];
- fun rename (t as Var ((x, i), T)) =
- (case AList.lookup (op =) al'' x of
- SOME y => Var ((y, i), T)
- | NONE => t)
- | rename (Abs (x, T, t)) =
- Abs (the_default x (AList.lookup (op =) al x), T, rename t)
- | rename (f $ t) = rename f $ rename t
- | rename t = t;
- fun strip_ren f Ai = f rename B Ai
- in strip_ren end;
+
+ in {vars = Symtab.make_distinct al'', bounds = Symtab.make_distinct al} end
+ end;
(*Function to rename bounds/unknowns in the argument, lifted over B*)
-fun rename_bvars dpairs =
- rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs;
-
+fun rename_bvars dpairs tpairs B As =
+ let val {vars, bounds} = rename_bvs dpairs tpairs B As in
+ if Symtab.forall (op =) vars andalso Symtab.forall (op =) bounds then NONE
+ else
+ let
+ fun term (Var ((x, i), T)) =
+ let val y = perhaps (Symtab.lookup vars) x
+ in if x = y then raise Same.SAME else Var ((y, i), T) end
+ | term (Abs (x, T, t)) =
+ let val y = perhaps (Symtab.lookup bounds) x
+ in if x = y then Abs (x, T, term t) else Abs (y, T, Same.commit term t) end
+ | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
+ | term _ = raise Same.SAME;
+ in SOME term end
+ end;
(*** RESOLUTION ***)
@@ -2310,112 +2321,112 @@
nsubgoal is the number of new subgoals (written m above).
Curried so that resolution calls dest_state only once.
*)
-local exception COMPOSE
-in
+local exception COMPOSE in
+
fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
- (eres_flg, orule, nsubgoal) =
- let val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state
- and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1,
- tpairs=rtpairs, prop=rprop,...}) = orule
- (*How many hyps to skip over during normalization*)
- and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
- val (context, cert) =
- make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule));
- (*Add new theorem with prop = "\<lbrakk>Bs; As\<rbrakk> \<Longrightarrow> C" to thq*)
- fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
- let val normt = Envir.norm_term env;
- (*perform minimal copying here by examining env*)
- val (ntpairs, normp) =
- if Envir.is_empty env then (tpairs, (Bs @ As, C))
- else
- let val ntps = map (apply2 normt) tpairs
- in if Envir.above env smax then
- (*no assignments in state; normalize the rule only*)
- if lifted
- then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
- else (ntps, (Bs @ map normt As, C))
- else if match then raise COMPOSE
- else (*normalize the new rule fully*)
- (ntps, (map normt (Bs @ As), normt C))
- end
- val thy' = Context.certificate_theory cert handle ERROR msg =>
- raise CONTEXT (msg, [], [], [state, orule], Option.map Context.Proof opt_ctxt);
- val constraints' =
- union_constraints constraints1 constraints2
- |> insert_constraints_env thy' env;
- fun zproof p q = ZTerm.todo_proof p;
- fun bicompose_proof p q =
- Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) p q;
- val proof =
- if Envir.is_empty env then bicompose_proof
- else if Envir.above env smax
- then bicompose_proof o Proofterm.norm_proof_remove_types env
- else Proofterm.norm_proof_remove_types env oo bicompose_proof;
- val th =
- Thm (deriv_rule2 zproof proof rder' sder,
- {tags = [],
- maxidx = Envir.maxidx_of env,
- constraints = constraints',
- shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2),
- hyps = union_hyps hyps1 hyps2,
- tpairs = ntpairs,
- prop = Logic.list_implies normp,
- cert = cert})
- in Seq.cons th thq end handle COMPOSE => thq;
- val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop)
- handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
- (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
- fun newAs(As0, n, dpairs, tpairs) =
- let val (As1, rder') =
- if not lifted then (As0, rder)
- else
- let
- val rename = rename_bvars dpairs tpairs B As0;
- fun proof p = Proofterm.map_proof_terms (rename K) I p;
- fun zproof p = ZTerm.todo_proof p;
- in (map (rename strip_apply) As0, deriv_rule1 zproof proof rder) end;
- in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
- handle TERM _ =>
- raise THM("bicompose: 1st premise", 0, [orule])
- end;
- val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
- val dpairs = BBi :: (rtpairs@stpairs);
+ (eres_flg, orule, nsubgoal) =
+ let
+ val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state
+ and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1,
+ tpairs = rtpairs, prop = rprop, ...}) = orule
+ (*How many hyps to skip over during normalization*)
+ and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0);
+ val (context, cert) =
+ make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule));
+ (*Add new theorem with prop = "\<lbrakk>Bs; As\<rbrakk> \<Longrightarrow> C" to thq*)
+ fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
+ let
+ val normt = Envir.norm_term env;
+ (*perform minimal copying here by examining env*)
+ val (ntpairs, normp) =
+ if Envir.is_empty env then (tpairs, (Bs @ As, C))
+ else
+ let val ntps = map (apply2 normt) tpairs in
+ if Envir.above env smax then
+ (*no assignments in state; normalize the rule only*)
+ if lifted
+ then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
+ else (ntps, (Bs @ map normt As, C))
+ else if match then raise COMPOSE
+ else (*normalize the new rule fully*)
+ (ntps, (map normt (Bs @ As), normt C))
+ end;
+ val thy' = Context.certificate_theory cert handle ERROR msg =>
+ raise CONTEXT (msg, [], [], [state, orule], Option.map Context.Proof opt_ctxt);
+ val constraints' =
+ union_constraints constraints1 constraints2
+ |> insert_constraints_env thy' env;
+ fun zproof p q = ZTerm.todo_proof p;
+ fun proof p q =
+ Proofterm.bicompose_proof env smax flatten Bs As A oldAs n (nlift + 1) p q;
+ val th =
+ Thm (deriv_rule2 zproof proof rder' sder,
+ {tags = [],
+ maxidx = Envir.maxidx_of env,
+ constraints = constraints',
+ shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2),
+ hyps = union_hyps hyps1 hyps2,
+ tpairs = ntpairs,
+ prop = Logic.list_implies normp,
+ cert = cert})
+ in Seq.cons th thq end handle COMPOSE => thq;
+ val (rAs, B) = Logic.strip_prems (nsubgoal, [], rprop)
+ handle TERM _ => raise THM("bicompose: rule", 0, [orule, state]);
+ (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
+ fun newAs (As0, n, dpairs, tpairs) =
+ let val (As1, rder') =
+ if lifted then
+ (case rename_bvars dpairs tpairs B As0 of
+ SOME f =>
+ let
+ fun proof p = Same.commit (Proofterm.map_proof_terms_same f I) p;
+ fun zproof p = ZTerm.todo_proof p;
+ in (map (strip_apply (Same.commit f) B) As0, deriv_rule1 zproof proof rder) end
+ | NONE => (As0, rder))
+ else (As0, rder);
+ in
+ (if flatten then map (Logic.flatten_params n) As1 else As1, As1, rder', n)
+ handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule])
+ end;
+ val BBi = if lifted then strip_assums2 (B, Bi) else (B, Bi);
+ val dpairs = BBi :: (rtpairs @ stpairs);
- (*elim-resolution: try each assumption in turn*)
- fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state])
- | eres env (A1 :: As) =
- let
- val A = SOME A1;
- val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1);
- val concl' = close concl;
- fun tryasms [] _ = Seq.empty
- | tryasms (asm :: rest) n =
- if Term.could_unify (asm, concl) then
- let val asm' = close asm in
- (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of
- NONE => tryasms rest (n + 1)
- | cell as SOME ((_, tpairs), _) =>
- Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
- (Seq.make (fn () => cell),
- Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
- end
- else tryasms rest (n + 1);
- in tryasms asms 1 end;
+ (*elim-resolution: try each assumption in turn*)
+ fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state])
+ | eres env (A1 :: As) =
+ let
+ val A = SOME A1;
+ val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1);
+ val concl' = close concl;
+ fun tryasms [] _ = Seq.empty
+ | tryasms (asm :: rest) n =
+ if Term.could_unify (asm, concl) then
+ let val asm' = close asm in
+ (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of
+ NONE => tryasms rest (n + 1)
+ | cell as SOME ((_, tpairs), _) =>
+ Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
+ (Seq.make (fn () => cell),
+ Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
+ end
+ else tryasms rest (n + 1);
+ in tryasms asms 1 end;
(*ordinary resolution*)
- fun res env =
- (case Seq.pull (Unify.unifiers (context, env, dpairs)) of
- NONE => Seq.empty
- | cell as SOME ((_, tpairs), _) =>
- Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
- (Seq.make (fn () => cell), Seq.empty));
+ fun res env =
+ (case Seq.pull (Unify.unifiers (context, env, dpairs)) of
+ NONE => Seq.empty
+ | cell as SOME ((_, tpairs), _) =>
+ Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
+ (Seq.make (fn () => cell), Seq.empty));
- val env0 = Envir.empty (Int.max (rmax, smax));
- in
- (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of
- NONE => Seq.empty
- | SOME env => if eres_flg then eres env (rev rAs) else res env)
- end;
+ val env0 = Envir.empty (Int.max (rmax, smax));
+ in
+ (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of
+ NONE => Seq.empty
+ | SOME env => if eres_flg then eres env (rev rAs) else res env)
+ end;
+
end;
fun bicompose opt_ctxt flags arg i state =