# HG changeset patch # User wenzelm # Date 1702060145 -3600 # Node ID 61af3e917597597d290899ec01bd2b78bf97d258 # Parent 0d8f0201485c57ce78b2d837ffdd80aa959762e0 more operations; more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term; diff -r 0d8f0201485c -r 61af3e917597 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Fri Dec 08 19:00:46 2023 +0100 +++ b/src/Pure/zterm.ML Fri Dec 08 19:29:05 2023 +0100 @@ -162,6 +162,8 @@ val ZAbsps: zterm list -> zproof -> zproof val ZAppts: zproof * zterm list -> zproof val ZAppps: zproof * zproof list -> zproof + val fold_proof_terms: (zterm -> 'a -> 'a) -> zproof -> 'a -> 'a + val exists_proof_terms: (zterm -> bool) -> zproof -> bool val incr_bv_same: int -> int -> zterm Same.operation val incr_bv: int -> int -> zterm -> zterm val incr_boundvars: int -> zterm -> zterm @@ -172,6 +174,7 @@ val typ_of: ztyp -> typ val term_of_consts: Consts.T -> zterm -> term val term_of: theory -> zterm -> term + val could_beta_contract: zterm -> bool val norm_type: Type.tyenv -> ztyp -> ztyp val norm_term: theory -> Envir.env -> zterm -> zterm val norm_proof: theory -> Envir.env -> zproof -> zproof @@ -231,6 +234,28 @@ val ZAppps = Library.foldl ZAppp; +(* fold *) + +fun fold_proof_terms f = + let + fun proof (ZConstp (_, _, _, inst)) = ZVars.fold (f o #2) inst + | proof (ZHyp t) = f t + | proof (ZAbst (_, _, p)) = proof p + | proof (ZAbsp (_, t, p)) = f t #> proof p + | proof (ZAppt (p, t)) = proof p #> f t + | proof (ZAppp (p, q)) = proof p #> proof q + | proof _ = I; + in proof end; + +local exception Found in + +fun exists_proof_terms P prf = + (fold_proof_terms (fn t => fn () => if P t then raise Found else ()) prf (); true) + handle Found => true; + +end; + + (* substitution of bound variables *) fun incr_bv_same inc = @@ -417,6 +442,11 @@ (* beta normalization wrt. environment *) +fun could_beta_contract (ZApp (ZAbs _, _)) = true + | could_beta_contract (ZApp (t, u)) = could_beta_contract t orelse could_beta_contract u + | could_beta_contract (ZAbs (_, _, b)) = could_beta_contract b + | could_beta_contract _ = false; + fun norm_type_same ztyp tyenv = if Vartab.is_empty tyenv then Same.same else @@ -435,8 +465,8 @@ | norm (ZType (a, Ts)) = ZType (a, Same.map norm Ts); in norm end; -fun norm_term_same {ztyp, zterm, typ} (envir as Envir.Envir {tyenv, tenv, ...}) = - if Envir.is_empty envir then Same.same +fun norm_term_same {ztyp, zterm, typ} (envir as Envir.Envir {tyenv, tenv, ...}) tm = + if Envir.is_empty envir andalso not (could_beta_contract tm) then raise Same.SAME else let val lookup = @@ -463,11 +493,12 @@ | nf => ZApp (nf, Same.commit norm t)) handle Same.SAME => ZApp (f, norm t)) | norm _ = raise Same.SAME; - in norm end; + in norm tm end; -fun norm_proof_same (cache as {ztyp, ...}) (envir as Envir.Envir {tyenv, ...}) = - if Envir.is_empty envir then Same.same - else map_proof_same (norm_type_same ztyp tyenv) (norm_term_same cache envir); +fun norm_proof_same (cache as {ztyp, ...}) (envir as Envir.Envir {tyenv, ...}) prf = + if Envir.is_empty envir andalso not (exists_proof_terms could_beta_contract prf) then + raise Same.SAME + else map_proof_same (norm_type_same ztyp tyenv) (norm_term_same cache envir) prf; fun norm_cache thy = let @@ -475,17 +506,9 @@ val typ = typ_cache (); in {ztyp = ztyp, zterm = zterm, typ = typ} end; -fun norm_type tyenv = - if Vartab.is_empty tyenv then I - else Same.commit (norm_type_same (ztyp_cache ()) tyenv); - -fun norm_term thy envir = - if Envir.is_empty envir then I - else Same.commit (norm_term_same (norm_cache thy) envir); - -fun norm_proof thy (envir as Envir.Envir {tyenv, ...}) = - if Envir.is_empty envir then I - else Same.commit (norm_proof_same (norm_cache thy) envir); +fun norm_type tyenv = Same.commit (norm_type_same (ztyp_cache ()) tyenv); +fun norm_term thy envir = Same.commit (norm_term_same (norm_cache thy) envir); +fun norm_proof thy envir = Same.commit (norm_proof_same (norm_cache thy) envir);