# HG changeset patch # User wenzelm # Date 1572809888 -3600 # Node ID c85efa2be6191bd46496a9b1c0f5fe9ecce01801 # Parent b05d78bfc67c80313b297225f8d4c897e8b7e9dc expose derivations more thoroughly, notably for locale/class reasoning; diff -r b05d78bfc67c -r c85efa2be619 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Sun Nov 03 19:43:59 2019 +0100 +++ b/src/Pure/Isar/class_declaration.ML Sun Nov 03 20:38:08 2019 +0100 @@ -84,6 +84,7 @@ in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm''])) + |> tap (Thm.expose_proof thy) end; val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class)); @@ -102,8 +103,9 @@ REPEAT (SOMEGOAL (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs) ORELSE' assume_tac ctxt)); - val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context); - + val of_class = + Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context) + |> tap (Thm.expose_proof thy); in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end; diff -r b05d78bfc67c -r c85efa2be619 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sun Nov 03 19:43:59 2019 +0100 +++ b/src/Pure/Isar/element.ML Sun Nov 03 20:38:08 2019 +0100 @@ -273,9 +273,9 @@ fun prove_witness ctxt t tac = Witness (t, - Thm.close_derivation \<^here> - (Goal.prove ctxt [] [] (mark_witness t) - (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac))); + Goal.prove ctxt [] [] (mark_witness t) + (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac) + |> Thm.expose_derivation \<^here>); local @@ -290,7 +290,7 @@ (map o map) (fn prop => (mark_witness prop, [])) wit_propss @ [map (rpair []) eq_props]; fun after_qed' thmss = - let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss); + let val (wits, eqs) = split_last ((map o map) (Thm.expose_derivation \<^here>) thmss); in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; in proof after_qed' propss #> refine_witness end; @@ -322,7 +322,9 @@ end; fun conclude_witness ctxt (Witness (_, th)) = - Thm.close_derivation \<^here> (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th)); + Goal.conclude th + |> Raw_Simplifier.norm_hhf_protect ctxt + |> Thm.expose_derivation \<^here>; fun pretty_witness ctxt witn = let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in diff -r b05d78bfc67c -r c85efa2be619 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sun Nov 03 19:43:59 2019 +0100 +++ b/src/Pure/Isar/expression.ML Sun Nov 03 20:38:08 2019 +0100 @@ -720,7 +720,8 @@ compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt (false, - Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1); + Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1) + |> tap (Thm.expose_proof defs_thy); val conjuncts = (Drule.equal_elim_rule2 OF diff -r b05d78bfc67c -r c85efa2be619 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Nov 03 19:43:59 2019 +0100 +++ b/src/Pure/thm.ML Sun Nov 03 20:38:08 2019 +0100 @@ -103,6 +103,7 @@ val proof_of: thm -> proof val consolidate: thm list -> unit val expose_proofs: theory -> thm list -> unit + val expose_proof: theory -> thm -> unit val future: thm future -> cterm -> thm val thm_deps: thm -> Proofterm.thm Ord_List.T val derivation_closed: thm -> bool @@ -112,6 +113,7 @@ val expand_name: thm -> Proofterm.thm_header -> string option val name_derivation: string * Position.T -> thm -> thm val close_derivation: Position.T -> thm -> thm + val expose_derivation: Position.T -> thm -> thm val trim_context: thm -> thm val axiom: theory -> string -> thm val all_axioms_of: theory -> (string * thm) list @@ -766,6 +768,8 @@ Proofterm.export_proof_boxes (map (proof_of o transfer thy) thms) else (); +fun expose_proof thy = expose_proofs thy o single; + (* future rule *) @@ -1040,6 +1044,10 @@ if not (null (tpairs_of thm)) orelse derivation_closed thm then thm else name_derivation ("", pos) thm); +fun expose_derivation pos thm = + close_derivation pos thm + |> tap (expose_proof (theory_of_thm thm)); + val trim_context = solve_constraints #> trim_context_thm; @@ -2245,7 +2253,7 @@ |> (map_classrels o Symreltab.update) ((c1, c2), (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |> standard_tvars - |> close_derivation \<^here> + |> expose_derivation \<^here> |> trim_context)); val proven = is_classrel thy1; @@ -2278,7 +2286,7 @@ val th1 = (th RS the_classrel thy (c, c1)) |> standard_tvars - |> close_derivation \<^here> + |> expose_derivation \<^here> |> trim_context; in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); val finished' = finished andalso null completions; @@ -2306,12 +2314,13 @@ fun add_classrel raw_th thy = let val th = strip_shyps (transfer thy raw_th); + val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context; val prop = plain_prop_of th; val (c1, c2) = Logic.dest_classrel prop; in thy |> Sign.primitive_classrel (c1, c2) - |> map_classrels (Symreltab.update ((c1, c2), th |> unconstrainT |> trim_context)) + |> map_classrels (Symreltab.update ((c1, c2), th')) |> perhaps complete_classrels |> perhaps complete_arities end; @@ -2319,9 +2328,10 @@ fun add_arity raw_th thy = let val th = strip_shyps (transfer thy raw_th); + val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context; val prop = plain_prop_of th; val (t, Ss, c) = Logic.dest_arity prop; - val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context, Context.theory_name thy, serial ())); + val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ())); in thy |> Sign.primitive_arity (t, Ss, [c])