# HG changeset patch # User wenzelm # Date 1703023586 -3600 # Node ID de58e518ed61ed8870dc7554fc9ac81185115274 # Parent 963570d120b22a2d8a5a3b04b5a81036d6767a5e# Parent 3b03af5125dede3fbb4ac2548142edd35cabf8c4 merged diff -r 963570d120b2 -r de58e518ed61 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Tue Dec 19 23:00:57 2023 +0100 +++ b/src/Pure/global_theory.ML Tue Dec 19 23:06:26 2023 +0100 @@ -245,7 +245,13 @@ (* store theorems and proofs *) -fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy); +fun register_proofs thms thy = + let + val (thms', thy') = + if Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) + then fold_map Thm.store_zproof thms thy + else (thms, thy); + in (thms', Thm.register_proofs (Lazy.value thms') thy') end; fun bind_name thy b = (Sign.full_name thy b, Binding.default_pos_of b); diff -r 963570d120b2 -r de58e518ed61 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Dec 19 23:00:57 2023 +0100 +++ b/src/Pure/proofterm.ML Tue Dec 19 23:06:26 2023 +0100 @@ -2202,7 +2202,8 @@ val proofs = get_proofs_level (); val (zboxes1, zproof1) = - if zproof_enabled proofs then ZTerm.box_proof thy hyps concl (#zboxes body0, #zproof body0) + if zproof_enabled proofs + then ZTerm.add_box_proof thy hyps concl (#zboxes body0, #zproof body0) else ([], ZDummy); val proof1 = if proof_enabled proofs then fold_rev implies_intr_proof hyps (#proof body0) diff -r 963570d120b2 -r de58e518ed61 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Dec 19 23:00:57 2023 +0100 +++ b/src/Pure/thm.ML Tue Dec 19 23:06:26 2023 +0100 @@ -173,6 +173,8 @@ val varifyT_global: thm -> thm val legacy_freezeT: thm -> thm val plain_prop_of: thm -> term + val get_zproof: theory -> serial -> {prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} option + val store_zproof: thm -> theory -> thm * theory val dest_state: thm * int -> (term * term) list * term list * term * term val lift_rule: cterm -> thm -> thm val incr_indexes: int -> thm -> thm @@ -405,24 +407,25 @@ val union_constraints = Ord_List.union constraint_ord; -fun insert_constraints thy (T, S) = - let - val ignored = - S = [] orelse - (case T of - TFree (_, S') => S = S' - | TVar (_, S') => S = S' - | _ => false); - in - if ignored then I - else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} - end; +fun insert_constraints _ (_, []) = I + | insert_constraints thy (T, S) = + let + val ignored = + (case T of + TFree (_, S') => S = S' + | TVar (_, S') => S = S' + | _ => false); + in + if ignored then I + else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} + end; fun insert_constraints_env thy env = let val tyenv = Envir.type_env env; + val normT = Envir.norm_type tyenv; fun insert ([], _) = I - | insert (S, T) = insert_constraints thy (Envir.norm_type tyenv T, S); + | insert (S, T) = insert_constraints thy (normT T, S); in tyenv |> Vartab.fold (insert o #2) end; end; @@ -942,23 +945,30 @@ structure Data = Theory_Data ( type T = + {prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} Inttab.table * (*stored thms: zproof*) unit Name_Space.table * (*oracles: authentic derivation names*) classes; (*type classes within the logic*) - val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes); - fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T = - (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2)); + val empty : T = (Inttab.empty, Name_Space.empty_table Markup.oracleN, empty_classes); + fun merge ((zproofs1, oracles1, sorts1), (zproofs2, oracles2, sorts2)) : T = + (Inttab.merge (K true) (zproofs1, zproofs2), + Name_Space.merge_tables (oracles1, oracles2), + merge_classes (sorts1, sorts2)); ); -val get_oracles = #1 o Data.get; -val map_oracles = Data.map o apfst; +val get_zproofs = #1 o Data.get; +fun map_zproofs f = Data.map (fn (a, b, c) => (f a, b, c)); -val get_classes = (fn (_, Classes args) => args) o Data.get; +val get_oracles = #2 o Data.get; +fun map_oracles f = Data.map (fn (a, b, c) => (a, f b, c)); + +val get_classes = (fn (_, _, Classes args) => args) o Data.get; val get_classrels = #classrels o get_classes; val get_arities = #arities o get_classes; fun map_classes f = - (Data.map o apsnd) (fn Classes {classrels, arities} => make_classes (f (classrels, arities))); + Data.map (fn (a, b, Classes {classrels, arities}) => + (a, b, make_classes (f (classrels, arities)))); fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities)); fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities)); @@ -985,54 +995,47 @@ local -val empty_digest = ([], [], []); +fun union_digest (oracles1, thms1) (oracles2, thms2) = + (Proofterm.union_oracles oracles1 oracles2, Proofterm.union_thms thms1 thms2); -fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) = - (Proofterm.union_oracles oracles1 oracles2, - Proofterm.union_thms thms1 thms2, - ZTerm.union_zboxes zboxes1 zboxes2); - -fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, zboxes, ...}, ...}, _)) = - (oracles, thms, zboxes); +fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) = (oracles, thms); fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) = Sorts.of_sort_derivation (Sign.classes_of thy) {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 => - if c1 = c2 then empty_digest else union_digest digest (thm_digest (the_classrel thy (c1, c2))), + if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))), type_constructor = fn (a, _) => fn dom => fn c => let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c)) in (fold o fold) (union_digest o #1) dom arity_digest end, - type_variable = fn T => map (pair empty_digest) (Type.sort_of_atyp T)} + type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)} (typ, sort); +fun bad_constraint_theory cert ({theory = thy, ...}: constraint) = + if Context.eq_thy_id (Context.certificate_theory_id cert, Context.theory_id thy) + then NONE else SOME thy; + in -fun solve_constraints (thm as Thm (_, {constraints = [], ...})) = thm - | solve_constraints (thm as Thm (der, args)) = - let - val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args; +fun solve_constraints (thm as Thm (der, args)) = + let + val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args; - val thy = Context.certificate_theory cert - handle ERROR msg => raise CONTEXT (msg, [], [], [thm], NONE); - val bad_thys = - constraints |> map_filter (fn {theory = thy', ...} => - if Context.eq_thy (thy, thy') then NONE else SOME thy'); - val () = - if null bad_thys then () - else - raise THEORY ("solve_constraints: bad theories for theorem\n" ^ - Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys); + val bad_thys = map_filter (bad_constraint_theory cert) constraints; + val _ = + if null bad_thys then () + else + raise THEORY ("solve_constraints: bad theories for theorem\n" ^ + Syntax.string_of_term_global (hd bad_thys) (prop_of thm), bad_thys); - val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der; - val (oracles', thms', zboxes') = (oracles, thms, zboxes) - |> fold (fold union_digest o constraint_digest) constraints; - val body' = - PBody {oracles = oracles', thms = thms', zboxes = zboxes', zproof = zproof, proof = proof}; - in - Thm (make_deriv0 promises body', - {constraints = [], cert = cert, tags = tags, maxidx = maxidx, - shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) - end; + val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der; + val (oracles', thms') = (oracles, thms) + |> fold (fold union_digest o constraint_digest) constraints; + val zproof' = ZTerm.beta_norm_prooft zproof; + in + Thm (make_deriv promises oracles' thms' zboxes zproof' proof, + {constraints = [], cert = cert, tags = tags, maxidx = maxidx, + shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) + end; end; @@ -2003,6 +2006,24 @@ end; +(* stored thms: zproof *) + +val get_zproof = Inttab.lookup o get_zproofs; + +fun store_zproof thm thy = + let + val Thm (Deriv {promises, body = PBody body}, args as {hyps, prop, ...}) = thm; + val {oracles, thms, zboxes, zproof, proof} = body; + val _ = null promises orelse + raise THM ("store_zproof: theorem may not use promises", 0, [thm]); + + val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy hyps prop zproof; + val thy' = thy + |> map_zproofs (Inttab.update (i, {prop = zprop, zboxes = zboxes, zproof = zprf})); + val der' = make_deriv promises oracles thms [] zproof' proof; + in (Thm (der', args), thy') end; + + (*** Inference rules for tactics ***) @@ -2261,19 +2282,6 @@ if Symtab.forall (op =) vars andalso Symtab.forall (op =) bounds then NONE else let - fun zterm (ZVar ((x, i), T)) = - if i >= 0 then - let val y = perhaps (Symtab.lookup vars) x - in if x = y then raise Same.SAME else ZVar ((y, i), T) end - else raise Same.SAME - | zterm (ZAbs (x, T, t)) = - let val y = perhaps (Symtab.lookup bounds) x - in if x = y then ZAbs (x, T, zterm t) else ZAbs (y, T, Same.commit zterm t) end - | zterm (ZApp (t, u)) = - (ZApp (zterm t, Same.commit zterm u) - handle Same.SAME => ZApp (t, zterm u)) - | zterm _ = raise Same.SAME; - 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 @@ -2282,8 +2290,7 @@ 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 {zterm = zterm, term = term} end + in SOME term end end; @@ -2393,11 +2400,9 @@ let val (As1, rder') = if lifted then (case rename_bvars dpairs tpairs B As0 of - SOME {zterm, term} => - let - fun zproof p = ZTerm.map_proof Same.same zterm p; - fun proof p = Same.commit (Proofterm.map_proof_terms_same term I) p; - in (map (strip_apply (Same.commit term) B) As0, deriv_rule1 zproof proof rder) end + SOME term => + let fun proof p = Same.commit (Proofterm.map_proof_terms_same term I) p; + in (map (strip_apply (Same.commit term) B) As0, deriv_rule1 I proof rder) end | NONE => (As0, rder)) else (As0, rder); in diff -r 963570d120b2 -r de58e518ed61 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Tue Dec 19 23:00:57 2023 +0100 +++ b/src/Pure/zterm.ML Tue Dec 19 23:06:26 2023 +0100 @@ -197,7 +197,8 @@ datatype zproof_name = ZAxiom of string | ZOracle of string - | ZBox of serial; + | ZBox of serial + | ZThm of serial; datatype zproof = ZDummy (*dummy proof*) @@ -250,15 +251,22 @@ val zterm_of: theory -> term -> zterm val typ_of: ztyp -> typ val term_of: theory -> zterm -> term + val beta_norm_term_same: zterm Same.operation + val beta_norm_proof_same: zproof Same.operation + val beta_norm_prooft_same: zproof -> zproof + val beta_norm_term: zterm -> zterm + val beta_norm_proof: zproof -> zproof + val beta_norm_prooft: zproof -> zproof val norm_type: Type.tyenv -> ztyp -> ztyp val norm_term: theory -> Envir.env -> zterm -> zterm val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof - type zbox = serial * (zterm * zproof future) + type zbox = serial * (zterm * zproof) val zbox_ord: zbox ord type zboxes = zbox Ord_List.T val union_zboxes: zboxes -> zboxes -> zboxes val unions_zboxes: zboxes list -> zboxes - val box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof + val add_box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof + val thm_proof: theory -> term list -> term -> zproof -> zbox * zproof val axiom_proof: theory -> string -> term -> zproof val oracle_proof: theory -> string -> term -> zproof val assume_proof: theory -> term -> zproof @@ -573,17 +581,31 @@ in term end; -(* beta normalization wrt. environment *) +(* beta contraction *) val beta_norm_term_same = let - fun norm (ZApp (ZAbs (_, _, body), t)) = Same.commit norm (subst_term_bound t body) + fun norm (ZAbs (a, T, t)) = ZAbs (a, T, Same.commit norm t) + | norm (ZApp (ZAbs (_, _, body), t)) = Same.commit norm (subst_term_bound t body) | norm (ZApp (f, t)) = ((case norm f of ZAbs (_, _, body) => Same.commit norm (subst_term_bound t body) | nf => ZApp (nf, Same.commit norm t)) handle Same.SAME => ZApp (f, norm t)) - | norm (ZAbs (a, T, t)) = ZAbs (a, T, Same.commit norm t) + | norm _ = raise Same.SAME; + in norm end; + +val beta_norm_prooft_same = + let + val term = beta_norm_term_same; + + fun norm (ZAbst (a, T, p)) = ZAbst (a, T, norm p) + | norm (ZAppt (ZAbst (_, _, body), t)) = Same.commit norm (subst_proof_bound t body) + | norm (ZAppt (f, t)) = + ((case norm f of + ZAbst (_, _, body) => Same.commit norm (subst_proof_bound t body) + | nf => ZAppt (nf, Same.commit term t)) + handle Same.SAME => ZAppt (f, term t)) | norm _ = raise Same.SAME; in norm end; @@ -591,13 +613,17 @@ let val term = beta_norm_term_same; - fun norm (ZAppt (ZAbst (_, _, body), t)) = Same.commit norm (subst_proof_bound t body) + fun norm (ZAbst (a, T, p)) = ZAbst (a, T, norm p) + | norm (ZAbsp (a, t, p)) = + (ZAbsp (a, term t, Same.commit norm p) + handle Same.SAME => ZAbsp (a, t, norm p)) + | norm (ZAppt (ZAbst (_, _, body), t)) = Same.commit norm (subst_proof_bound t body) + | norm (ZAppp (ZAbsp (_, _, body), p)) = Same.commit norm (subst_proof_boundp p body) | norm (ZAppt (f, t)) = ((case norm f of ZAbst (_, _, body) => Same.commit norm (subst_proof_bound t body) | nf => ZAppt (nf, Same.commit term t)) handle Same.SAME => ZAppt (f, term t)) - | norm (ZAppp (ZAbsp (_, _, body), p)) = Same.commit norm (subst_proof_boundp p body) | norm (ZAppp (f, p)) = ((case norm f of ZAbsp (_, _, body) => Same.commit norm (subst_proof_boundp p body) @@ -606,6 +632,13 @@ | norm _ = raise Same.SAME; in norm end; +val beta_norm_term = Same.commit beta_norm_term_same; +val beta_norm_proof = Same.commit beta_norm_proof_same; +val beta_norm_prooft = Same.commit beta_norm_prooft_same; + + +(* normalization wrt. environment and beta contraction *) + fun norm_type_same ztyp tyenv = if Vartab.is_empty tyenv then Same.same else @@ -658,8 +691,7 @@ val norm_var = ZVar #> Same.commit (norm_term_same cache envir); in fn visible => fn prf => - if Envir.is_empty envir orelse null visible - then Same.commit beta_norm_proof_same prf + if Envir.is_empty envir orelse null visible then beta_norm_prooft prf else let fun add_tvar v tab = @@ -681,7 +713,7 @@ |> instantiate_term_same inst_typ; val norm_term = Same.compose beta_norm_term_same inst_term; - in Same.commit beta_norm_proof_same (map_proof inst_typ norm_term prf) end + in beta_norm_prooft (map_proof inst_typ norm_term prf) end end; fun norm_cache thy = @@ -723,7 +755,7 @@ (* closed proof boxes *) -type zbox = serial * (zterm * zproof future); +type zbox = serial * (zterm * zproof); val zbox_ord: zbox ord = fn ((i, _), (j, _)) => int_ord (j, i); type zboxes = zbox Ord_List.T; @@ -754,21 +786,27 @@ | proof _ _ = raise Same.SAME; in ZAbsps hyps (Same.commit (proof 0) prf) end; -in - -fun box_proof thy hyps concl (zboxes: zboxes, prf) = +fun box_proof zproof_name thy hyps concl prf = let val {zterm, ...} = zterm_cache thy; val hyps' = map zterm hyps; val concl' = zterm concl; - val prop' = close_prop hyps' concl'; - val prf' = close_proof hyps' prf; + val prop' = beta_norm_term (close_prop hyps' concl'); + val prf' = beta_norm_prooft (close_proof hyps' prf); val i = serial (); - val zboxes' = add_zboxes (i, (prop', Future.value prf')) zboxes; - val prf'' = ZAppts (ZConstp (zproof_const (ZBox i) prop'), hyps'); - in (zboxes', prf'') end; + val zbox: zbox = (i, (prop', prf')); + val zbox_prf = ZAppts (ZConstp (zproof_const (zproof_name i) prop'), hyps'); + in (zbox, zbox_prf) end; + +in + +val thm_proof = box_proof ZThm; + +fun add_box_proof thy hyps concl (zboxes, prf) = + let val (zbox, zbox_prf) = box_proof ZBox thy hyps concl prf + in (add_zboxes zbox zboxes, zbox_prf) end; end;