# HG changeset patch # User wenzelm # Date 1702328184 -3600 # Node ID 2b2e51cc5c700ff74b5f533553f9d15ea16f963e # Parent 6dc4fd89987f158e140bd56689075d496a409e5d# Parent 54dc0b820834dda61399f89bea986885adaa87ba merged diff -r 6dc4fd89987f -r 2b2e51cc5c70 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Mon Dec 11 17:28:21 2023 +0100 +++ b/src/Pure/General/table.ML Mon Dec 11 21:56:24 2023 +0100 @@ -41,6 +41,7 @@ val default: key * 'a -> 'a table -> 'a table val map_entry: key -> ('a -> 'a) (*exception SAME*) -> 'a table -> 'a table val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table + val make_distinct: (key * 'a) list -> 'a table val make: (key * 'a) list -> 'a table (*exception DUP*) val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a table * 'a table -> 'a table (*exception DUP*) @@ -531,6 +532,8 @@ (* simultaneous modifications *) +fun make_distinct entries = build (fold default entries); + fun make entries = build (fold update_new entries); fun join f (tab1, tab2) = diff -r 6dc4fd89987f -r 2b2e51cc5c70 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Dec 11 17:28:21 2023 +0100 +++ b/src/Pure/Proof/extraction.ML Mon Dec 11 21:56:24 2023 +0100 @@ -100,7 +100,7 @@ in get_first (fn (_, (prems, (tm1, tm2))) => let - fun ren t = the_default t (Term.rename_abs tm1 tm t); + fun ren t = perhaps (Term.rename_abs tm1 tm) t; val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty); val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems; diff -r 6dc4fd89987f -r 2b2e51cc5c70 src/Pure/more_pattern.ML --- a/src/Pure/more_pattern.ML Mon Dec 11 17:28:21 2023 +0100 +++ b/src/Pure/more_pattern.ML Mon Dec 11 21:56:24 2023 +0100 @@ -39,7 +39,7 @@ (* rewriting -- simple but fast *) fun match_rew thy tm (tm1, tm2) = - let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in + let val rtm = perhaps (Term.rename_abs tm1 tm) tm2 in SOME (Envir.subst_term (Pattern.match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm) handle Pattern.MATCH => NONE end; diff -r 6dc4fd89987f -r 2b2e51cc5c70 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Dec 11 17:28:21 2023 +0100 +++ b/src/Pure/proofterm.ML Mon Dec 11 21:56:24 2023 +0100 @@ -131,8 +131,8 @@ val lift_proof: term -> int -> term list -> proof -> proof val incr_indexes: int -> proof -> proof val assumption_proof: term list -> term -> int -> proof -> proof - val bicompose_proof: bool -> term list -> term list -> term option -> term list -> - int -> int -> proof -> proof -> proof + val bicompose_proof: Envir.env -> int -> bool -> term list -> term list -> term option -> + term list -> int -> int -> proof -> proof -> proof val reflexive_axm: proof val symmetric_axm: proof val transitive_axm: proof @@ -1079,16 +1079,25 @@ | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0))); -fun bicompose_proof flatten Bs As A oldAs n m rprf sprf = +fun bicompose_proof env smax flatten Bs As A oldAs n m rprf sprf = let + val normt = Envir.norm_term env; + val normp = norm_proof_remove_types env; + val lb = length Bs; val la = length As; + + fun proof p = + mk_AbsP (map normt (Bs @ As)) (proof_combP (sprf, + map PBound (lb + la - 1 downto la)) %% + proof_combP (p, (if n>0 then [mk_asm_prf (the A) n m] else []) @ + map (if flatten then flatten_params_proof 0 0 n else PBound o snd) + (oldAs ~~ (la - 1 downto 0)))); in - mk_AbsP (Bs @ As) (proof_combP (sprf, - map PBound (lb + la - 1 downto la)) %% - proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @ - map (if flatten then flatten_params_proof 0 0 n else PBound o snd) - (oldAs ~~ (la - 1 downto 0)))) + if Envir.is_empty env then proof rprf + else if Envir.above env smax + then proof (normp rprf) + else normp (proof rprf) end; diff -r 6dc4fd89987f -r 2b2e51cc5c70 src/Pure/term.ML --- 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 *) diff -r 6dc4fd89987f -r 2b2e51cc5c70 src/Pure/thm.ML --- 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 = "\Bs; As\ \ 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 = "\Bs; As\ \ 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 = diff -r 6dc4fd89987f -r 2b2e51cc5c70 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Mon Dec 11 17:28:21 2023 +0100 +++ b/src/Pure/zterm.ML Mon Dec 11 21:56:24 2023 +0100 @@ -203,7 +203,7 @@ term list -> int -> zproof -> zproof val permute_prems_proof: theory -> term list -> int -> int -> zproof -> zproof val incr_indexes_proof: int -> zproof -> zproof - val lift_proof: theory -> term -> int -> zterm list -> zproof -> zproof + val lift_proof: theory -> term -> int -> term list -> zproof -> zproof val assumption_proof: theory -> Envir.env -> term list -> term -> int -> zproof -> zproof end; @@ -852,7 +852,7 @@ | lift Ts bs i j _ = ZAppps (Same.commit (proof (rev Ts) 0) prf, map (fn k => (#3 (fold_rev mk_app bs (i - 1, j - 1, ZBoundp k)))) (i + k - 1 downto i)); - in ZAbsps prems (lift [] [] 0 0 gprop) end; + in ZAbsps (map zterm prems) (lift [] [] 0 0 gprop) end; (* higher-order resolution *)