diff --git a/src/HOL/Proofs/ex/XML_Data.thy b/src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy +++ b/src/HOL/Proofs/ex/XML_Data.thy @@ -1,58 +1,58 @@ (* Title: HOL/Proofs/ex/XML_Data.thy Author: Makarius Author: Stefan Berghofer XML data representation of proof terms. *) theory XML_Data imports "HOL-Isar_Examples.Drinker" begin subsection \Export and re-import of global proof terms\ ML \ fun export_proof thy thm = thm - |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} + |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm} |> Proofterm.encode (Sign.consts_of thy); fun import_proof thy xml = let val prf = Proofterm.decode (Sign.consts_of thy) xml; val (prf', _) = Proofterm.freeze_thaw_prf prf; in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end; \ subsection \Examples\ ML \val thy1 = \<^theory>\ lemma ex: "A \ A" .. ML_val \ val xml = export_proof thy1 @{thm ex}; val thm = import_proof thy1 xml; \ ML_val \ val xml = export_proof thy1 @{thm de_Morgan}; val thm = import_proof thy1 xml; \ ML_val \ val xml = export_proof thy1 @{thm Drinker's_Principle}; val thm = import_proof thy1 xml; \ text \Some fairly large proof:\ ML_val \ val xml = export_proof thy1 @{thm abs_less_iff}; val thm = import_proof thy1 xml; val xml_size = size (YXML.string_of_body xml); \<^assert> (xml_size > 400000); \ end diff --git a/src/Pure/Proof/proof_syntax.ML b/src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML +++ b/src/Pure/Proof/proof_syntax.ML @@ -1,283 +1,297 @@ (* Title: Pure/Proof/proof_syntax.ML Author: Stefan Berghofer, TU Muenchen Function for parsing and printing proof terms. *) signature PROOF_SYNTAX = sig val add_proof_syntax: theory -> theory val term_of_proof: proof -> term val proof_of_term: theory -> bool -> term -> Proofterm.proof val read_term: theory -> bool -> typ -> string -> term val read_proof: theory -> bool -> bool -> string -> Proofterm.proof val proof_syntax: Proofterm.proof -> theory -> theory val proof_of: bool -> thm -> Proofterm.proof val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T - val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T val pretty_proof_boxes_of: Proof.context -> {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T + val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} -> + thm -> Proofterm.proof + val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T end; structure Proof_Syntax : PROOF_SYNTAX = struct (**** add special syntax for embedding proof terms ****) val proofT = Type ("Pure.proof", []); local val paramT = Type ("param", []); val paramsT = Type ("params", []); val idtT = Type ("idt", []); val aT = Term.aT []; fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); in fun add_proof_syntax thy = thy |> Sign.root_path |> Sign.set_defsort [] |> Sign.add_nonterminals_global [Binding.make ("param", \<^here>), Binding.make ("params", \<^here>)] |> Sign.add_syntax Syntax.mode_default [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)), ("", paramT --> paramT, Mixfix.mixfix "'(_')"), ("", idtT --> paramsT, Mixfix.mixfix "_"), ("", paramT --> paramsT, Mixfix.mixfix "_"), (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \/ _)", [4, 5], 4)), (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \/ _)", [4, 5], 4)), (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "\<^bold>?")] |> Sign.add_trrules (map Syntax.Parse_Print_Rule [(Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam0") [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"], Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "l", Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]), (Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam1") [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"], Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A", (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"], Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst")) [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); end; (** constants for theorems and axioms **) fun add_proof_atom_consts names thy = thy |> Sign.root_path |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); (** proof terms as pure terms **) (* term_of_proof *) local val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT); val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT); val Hypt = Const ("Pure.Hyp", propT --> proofT); val Oraclet = Const ("Pure.Oracle", propT --> proofT); val MinProoft = Const ("Pure.MinProof", proofT); fun AppT T prf = Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T; fun OfClasst (T, c) = let val U = Term.itselfT T --> propT in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) = fold AppT (these Ts) (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT)) | term_of _ (PAxm (name, _, Ts)) = fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT)) | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c)) | term_of _ (PBound i) = Bound i | term_of Ts (Abst (s, opT, prf)) = let val T = the_default dummyT opT in Const ("Pure.Abst", (T --> proofT) --> proofT) $ Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf)) end | term_of Ts (AbsP (s, t, prf)) = AbsPt $ the_default Term.dummy_prop t $ Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf)) | term_of Ts (prf1 %% prf2) = AppPt $ term_of Ts prf1 $ term_of Ts prf2 | term_of Ts (prf % opt) = let val t = the_default Term.dummy opt; val T = fastype_of1 (Ts, t) handle TERM _ => dummyT; in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end | term_of _ (Hyp t) = Hypt $ t | term_of _ (Oracle (_, t, _)) = Oraclet $ t | term_of _ MinProof = MinProoft; in val term_of_proof = term_of []; end; (* proof_of_term *) fun proof_of_term thy ty = let val thms = Global_Theory.all_thms_of thy true; val axms = Theory.all_axioms_of thy; fun mk_term t = (if ty then I else map_types (K dummyT)) (Term.no_dummy_patterns t); fun prf_of [] (Bound i) = PBound i | prf_of Ts (Const (s, Type ("Pure.proof", _))) = Proofterm.change_types (if ty then SOME Ts else NONE) (case Long_Name.explode s of "axm" :: xs => let val name = Long_Name.implode xs; val prop = (case AList.lookup (op =) axms name of SOME prop => prop | NONE => error ("Unknown axiom " ^ quote name)) in PAxm (name, prop, NONE) end | "thm" :: xs => let val name = Long_Name.implode xs; in (case AList.lookup (op =) thms name of SOME thm => fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm)))) | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) = (case try Logic.class_of_const c_class of SOME c => Proofterm.change_types (if ty then SOME Ts else NONE) (OfClass (TVar ((Name.aT, 0), []), c)) | NONE => error ("Bad class constant: " ^ quote c_class)) | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop | prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v | prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) = if T = proofT then error ("Term variable abstraction may not bind proof variable " ^ quote s) else Abst (s, if ty then SOME T else NONE, Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) | prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) = AbsP (s, case t of Const ("Pure.dummy_pattern", _) => NONE | _ $ Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t), Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) = prf_of [] prf1 %% prf_of [] prf2 | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type ("itself", [T]))) = prf_of (T::Ts) prf | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf % (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) | prf_of _ t = error ("Not a proof term:\n" ^ Syntax.string_of_term_global thy t) in prf_of [] end; fun read_term thy topsort = let val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true)); val axm_names = map fst (Theory.all_axioms_of thy); val ctxt = thy |> add_proof_syntax |> add_proof_atom_consts (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |> Proof_Context.init_global |> Proof_Context.allow_dummies |> Proof_Context.set_mode Proof_Context.mode_schematic |> topsort ? (Proof_Context.set_defsort [] #> Config.put Type_Infer.object_logic false #> Config.put Type_Infer_Context.const_sorts false); in fn ty => fn s => (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |> Type.constraint ty |> Syntax.check_term ctxt end; fun read_proof thy topsort = let val rd = read_term thy topsort proofT in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; fun proof_syntax prf = let val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true (fn PThm ({name, ...}, _) => if name <> "" then Symtab.update (name, ()) else I | _ => I) [prf] Symtab.empty); val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); in add_proof_syntax #> add_proof_atom_consts (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) end; fun proof_of full thm = let val thy = Thm.theory_of_thm thm; val prop = Thm.full_prop_of thm; val prf = Thm.proof_of thm; in (case fst (Proofterm.strip_combt (fst (Proofterm.strip_combP prf))) of PThm ({prop = prop', ...}, thm_body) => if prop = prop' then Proofterm.thm_body_proof_raw thm_body else prf | _ => prf) |> full ? Proofterm.reconstruct_proof thy prop end; fun pretty_proof ctxt prf = Proof_Context.pretty_term_abbrev (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) (term_of_proof prf); -fun pretty_standard_proof_of ctxt full thm = - pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); - fun pretty_proof_boxes_of ctxt {full, preproc} thm = let val thy = Proof_Context.theory_of ctxt; val selection = {included = Proofterm.this_id (Thm.derivation_id thm), excluded = is_some o Global_Theory.lookup_thm_id thy} in Proofterm.proof_boxes selection [Thm.proof_of thm] |> map (fn ({serial = i, pos, prop, ...}, proof) => let val proof' = proof |> Proofterm.reconstruct_proof thy prop |> preproc thy |> not full ? Proofterm.shrink_proof |> Proofterm.forall_intr_variables prop; val prop' = prop |> Proofterm.forall_intr_variables_term; val name = Long_Name.append "thm" (string_of_int i); in Pretty.item [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1, Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof'] end) |> Pretty.chunks end; + +(* standardized proofs *) + +fun standard_proof_of {full, expand_name} thm = + let val thy = Thm.theory_of_thm thm in + Thm.reconstruct_proof_of thm + |> Proofterm.expand_proof thy expand_name + |> Proofterm.rew_proof thy + |> Proofterm.no_thm_proofs + |> not full ? Proofterm.shrink_proof + end; + +fun pretty_standard_proof_of ctxt full thm = + pretty_proof ctxt (standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); + end; diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,355 +1,355 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "System/distribution.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash_syntax.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "context_position.ML"; ML_file "System/options.ML"; ML_file "config.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "ML/ml_statistics.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/standard_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/html.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; ML_file "Isar/bundle.ML"; ML_file "Isar/experiment.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) +ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; -ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/thy_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/invoke_scala.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" diff --git a/src/Pure/Thy/export_theory.ML b/src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML +++ b/src/Pure/Thy/export_theory.ML @@ -1,406 +1,407 @@ (* Title: Pure/Thy/export_theory.ML Author: Makarius Export foundational theory content and locale/class structure. *) signature EXPORT_THEORY = sig val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit val export_body: theory -> string -> XML.body -> unit end; structure Export_Theory: EXPORT_THEORY = struct (* approximative syntax *) val get_syntax = Syntax.get_approx o Proof_Context.syn_of; fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type; fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const; fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed; fun get_syntax_param ctxt loc x = let val thy = Proof_Context.theory_of ctxt in if Class.is_class thy loc then (case AList.lookup (op =) (Class.these_params thy [loc]) x of NONE => NONE | SOME (_, (c, _)) => get_syntax_const ctxt c) else get_syntax_fixed ctxt x end; val encode_syntax = XML.Encode.variant [fn NONE => ([], []), fn SOME (Syntax.Prefix delim) => ([delim], []), fn SOME (Syntax.Infix {assoc, delim, pri}) => let val ass = (case assoc of Printer.No_Assoc => 0 | Printer.Left_Assoc => 1 | Printer.Right_Assoc => 2); open XML.Encode Term_XML.Encode; in ([], triple int string int (ass, delim, pri)) end]; (* free variables: not declared in the context *) val is_free = not oo Name.is_declared; fun add_frees used = fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I); fun add_tfrees used = (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I); (* spec rules *) fun primrec_types ctxt const = Spec_Rules.retrieve ctxt (Const const) |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false) | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true) | _ => NONE) |> the_default ([], false); (* locales content *) fun locale_content thy loc = let val ctxt = Locale.init loc thy; val args = Locale.params_of thy loc |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x)); val axioms = let val (asm, defs) = Locale.specification_of thy loc; val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs); val (intro1, intro2) = Locale.intros_of thy loc; val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) []; val res = Goal.init (Conjunction.mk_conjunction_balanced cprops) |> (ALLGOALS Goal.conjunction_tac THEN intros_tac) |> try Seq.hd; in (case res of SOME goal => Thm.prems_of goal | NONE => raise Fail ("Cannot unfold locale " ^ quote loc)) end; val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []); in {typargs = typargs, args = args, axioms = axioms} end; fun get_locales thy = Locale.get_locales thy |> map_filter (fn loc => if Experiment.is_experiment thy loc then NONE else SOME (loc, ())); fun get_dependencies prev_thys thy = Locale.dest_dependencies prev_thys thy |> map_filter (fn dep => if Experiment.is_experiment thy (#source dep) orelse Experiment.is_experiment thy (#target dep) then NONE else let val (type_params, params) = Locale.parameters_of thy (#source dep); val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params; val substT = typargs |> map_filter (fn v => let val T = TFree v; val T' = Morphism.typ (#morphism dep) T; in if T = T' then NONE else SOME (v, T') end); val subst = params |> map_filter (fn (v, _) => let val t = Free v; val t' = Morphism.term (#morphism dep) t; in if t aconv t' then NONE else SOME (v, t') end); in SOME (dep, (substT, subst)) end); (* general setup *) fun setup_presentation f = Theory.setup (Thy_Info.add_presentation (fn context => fn thy => if Options.bool (#options context) "export_theory" then f context thy else ())); fun export_body thy name body = if XML.is_empty_body body then () else Export.export thy (Path.binding0 (Path.make ["theory", name])) body; (* presentation *) val _ = setup_presentation (fn {adjust_pos, ...} => fn thy => let val parents = Theory.parents_of thy; val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); val thy_ctxt = Proof_Context.init_global thy; (* entities *) fun make_entity_markup name xname pos serial = let val props = Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos @ Markup.serial_properties serial; in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end; fun entity_markup space name = let val xname = Name_Space.extern_shortest thy_ctxt space name; val {serial, pos, ...} = Name_Space.the_entry space name; in make_entity_markup name xname pos serial end; fun export_entities export_name export get_space decls = let val parent_spaces = map get_space parents; val space = get_space thy; in (decls, []) |-> fold (fn (name, decl) => if exists (fn space => Name_Space.declared space name) parent_spaces then I else (case export name decl of NONE => I | SOME body => cons (#serial (Name_Space.the_entry space name), XML.Elem (entity_markup space name, body)))) |> sort (int_ord o apply2 #1) |> map #2 |> export_body thy export_name end; (* types *) val encode_type = let open XML.Encode Term_XML.Encode in triple encode_syntax (list string) (option typ) end; fun export_type c (Type.LogicalType n) = SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE)) | export_type c (Type.Abbreviation (args, U, false)) = SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U)) | export_type _ _ = NONE; val _ = export_entities "types" export_type Sign.type_space (Name_Space.dest_table (#types rep_tsig)); (* consts *) val consts = Sign.consts_of thy; val encode_term = Term_XML.Encode.term consts; val encode_const = let open XML.Encode Term_XML.Encode in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) (pair bool (pair (list string) bool))))) end; fun export_const c (T, abbrev) = let val syntax = get_syntax_const thy_ctxt c; val U = Logic.unvarifyT_global T; val U0 = Type.strip_sorts U; val recursion = primrec_types thy_ctxt (c, U); val abbrev' = abbrev |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts); val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0)); val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end; val _ = export_entities "consts" (SOME oo export_const) Sign.const_space (#constants (Consts.dest consts)); (* axioms *) fun standard_prop used extra_shyps raw_prop raw_proof = let val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof); val args = rev (add_frees used prop []); val typargs = rev (add_tfrees used prop []); val used_typargs = fold (Name.declare o #1) typargs used; val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps; in ((sorts @ typargs, args, prop), proof) end; val encode_prop = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair string typ)) encode_term end; fun encode_axiom used prop = encode_prop (#1 (standard_prop used [] prop NONE)); val _ = export_entities "axioms" (K (SOME o encode_axiom Name.context)) Theory.axiom_space (Theory.all_axioms_of thy); (* theorems and proof terms *) val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; val lookup_thm_id = Global_Theory.lookup_thm_id thy; fun expand_name thm_id (header: Proofterm.thm_header) = if #serial header = #serial thm_id then "" else (case lookup_thm_id (Proofterm.thm_header_id header) of NONE => "" | SOME thm_name => Thm_Name.print thm_name); fun entity_markup_thm (serial, (name, i)) = let val space = Facts.space_of (Global_Theory.facts_of thy); val xname = Name_Space.extern_shortest thy_ctxt space name; val {pos, ...} = Name_Space.the_entry space name; in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; fun encode_thm thm_id raw_thm = let val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = clean_thm (Thm.unconstrainT raw_thm); val proof0 = if Proofterm.export_standard_enabled () then - Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm + Proof_Syntax.standard_proof_of + {full = true, expand_name = SOME o expand_name thm_id} thm else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof; val (prop, SOME proof) = standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); val _ = Thm.expose_proofs thy [thm]; in (prop, deps, proof) |> let open XML.Encode Term_XML.Encode; val encode_proof = Proofterm.encode_standard_proof consts; in triple encode_prop (list string) encode_proof end end; fun export_thm (thm_id, thm_name) = let val markup = entity_markup_thm (#serial thm_id, thm_name); val thm = Global_Theory.get_thm_name thy (thm_name, Position.none); in XML.Elem (markup, encode_thm thm_id thm) end; val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy)); (* type classes *) val encode_class = let open XML.Encode Term_XML.Encode in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; fun export_class name = (case try (Axclass.get_info thy) name of NONE => ([], []) | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) |> encode_class |> SOME; val _ = export_entities "classes" (fn name => fn () => export_class name) Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))); (* sort algebra *) local val prop = encode_axiom Name.context o Logic.varify_global; val encode_classrel = let open XML.Encode in list (pair prop (pair string string)) end; val encode_arities = let open XML.Encode Term_XML.Encode in list (pair prop (triple string (list sort) string)) end; in val export_classrel = maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel; val export_arities = map (`Logic.mk_arity) #> encode_arities; val {classrel, arities} = Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) (#2 (#classes rep_tsig)); end; val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel); val _ = if null arities then () else export_body thy "arities" (export_arities arities); (* locales *) fun encode_locale used = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) (list (encode_axiom used)) end; fun export_locale loc = let val {typargs, args, axioms} = locale_content thy loc; val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; in encode_locale used (typargs, args, axioms) end handle ERROR msg => cat_error msg ("The error(s) above occurred in locale " ^ quote (Locale.markup_name thy_ctxt loc)); val _ = export_entities "locales" (fn loc => fn () => SOME (export_locale loc)) Locale.locale_space (get_locales thy); (* locale dependencies *) fun encode_locale_dependency (dep: Locale.locale_dependency, subst) = (#source dep, (#target dep, (#prefix dep, subst))) |> let open XML.Encode Term_XML.Encode; val encode_subst = pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts))); in pair string (pair string (pair (list (pair string bool)) encode_subst)) end; val _ = get_dependencies parents thy |> map_index (fn (i, dep) => let val xname = string_of_int (i + 1); val name = Long_Name.implode [Context.theory_name thy, xname]; val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); val body = encode_locale_dependency dep; in XML.Elem (markup, body) end) |> export_body thy "locale_dependencies"; (* constdefs *) val constdefs = Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy) |> sort_by #1; val encode_constdefs = let open XML.Encode in list (pair string string) end; val _ = if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs); (* parents *) val _ = Export.export thy \<^path_binding>\theory/parents\ (XML.Encode.string (cat_lines (map Context.theory_long_name parents))); in () end); end; diff --git a/src/Pure/more_thm.ML b/src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML +++ b/src/Pure/more_thm.ML @@ -1,755 +1,736 @@ (* Title: Pure/more_thm.ML Author: Makarius Further operations on type ctyp/cterm/thm, outside the inference kernel. *) infix aconvc; signature BASIC_THM = sig include BASIC_THM val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool type attribute = Context.generic * thm -> Context.generic option * thm option end; signature THM = sig include THM structure Ctermtab: TABLE structure Thmtab: TABLE val eq_ctyp: ctyp * ctyp -> bool val aconvc: cterm * cterm -> bool val add_tvars: thm -> ctyp list -> ctyp list val add_frees: thm -> cterm list -> cterm list val add_vars: thm -> cterm list -> cterm list val dest_funT: ctyp -> ctyp * ctyp val strip_type: ctyp -> ctyp list * ctyp val all_name: Proof.context -> string * cterm -> cterm -> cterm val all: Proof.context -> cterm -> cterm -> cterm val mk_binop: cterm -> cterm -> cterm -> cterm val dest_binop: cterm -> cterm * cterm val dest_implies: cterm -> cterm * cterm val dest_equals: cterm -> cterm * cterm val dest_equals_lhs: cterm -> cterm val dest_equals_rhs: cterm -> cterm val lhs_of: thm -> cterm val rhs_of: thm -> cterm val fast_term_ord: cterm ord val term_ord: cterm ord val thm_ord: thm ord val cterm_cache: (cterm -> 'a) -> cterm -> 'a val thm_cache: (thm -> 'a) -> thm -> 'a val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val eq_thm_strict: thm * thm -> bool val equiv_thm: theory -> thm * thm -> bool val class_triv: theory -> class -> thm val of_sort: ctyp * sort -> thm list val is_dummy: thm -> bool val add_thm: thm -> thm list -> thm list val del_thm: thm -> thm list -> thm list val merge_thms: thm list * thm list -> thm list val full_rules: thm Item_Net.T val intro_rules: thm Item_Net.T val elim_rules: thm Item_Net.T val declare_hyps: cterm -> Proof.context -> Proof.context val assume_hyps: cterm -> Proof.context -> thm * Proof.context val unchecked_hyps: Proof.context -> Proof.context val restore_hyps: Proof.context -> Proof.context -> Proof.context val undeclared_hyps: Context.generic -> thm -> term list val check_hyps: Context.generic -> thm -> thm val declare_term_sorts: term -> Proof.context -> Proof.context val extra_shyps': Proof.context -> thm -> sort list val check_shyps: Proof.context -> thm -> thm val weaken_sorts': Proof.context -> cterm -> cterm val elim_implies: thm -> thm -> thm val forall_intr_name: string * cterm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm val forall_intr_frees: thm -> thm val unvarify_global: theory -> thm -> thm val unvarify_axiom: theory -> string -> thm val rename_params_rule: string list * int -> thm -> thm val rename_boundvars: term -> term -> thm -> thm val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory val add_axiom_global: binding * term -> theory -> (string * thm) * theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory type attribute = Context.generic * thm -> Context.generic option * thm option type binding = binding * attribute list val tag_rule: string * string -> thm -> thm val untag_rule: string -> thm -> thm val is_free_dummy: thm -> bool val tag_free_dummy: thm -> thm val def_name: string -> string val def_name_optional: string -> string -> string val def_binding: Binding.binding -> Binding.binding val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding val make_def_binding: bool -> Binding.binding -> Binding.binding val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm val theoremK: string val legacy_get_kind: thm -> string val kind_rule: string -> thm -> thm val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic val theory_attributes: attribute list -> thm -> theory -> thm * theory val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag: string * string -> attribute val untag: string -> attribute val kind: string -> attribute - val reconstruct_proof_of: thm -> Proofterm.proof - val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} -> - thm -> Proofterm.proof val register_proofs: thm list lazy -> theory -> theory val consolidate_theory: theory -> unit val expose_theory: theory -> unit val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_item: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string val string_of_thm_global: theory -> thm -> string end; structure Thm: THM = struct (** basic operations **) (* collecting ctyps and cterms *) val eq_ctyp = op = o apply2 Thm.typ_of; val op aconvc = op aconv o apply2 Thm.term_of; val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); (* ctyp operations *) fun dest_funT cT = (case Thm.typ_of cT of Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end | T => raise TYPE ("dest_funT", [T], [])); (* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) fun strip_type cT = (case Thm.typ_of cT of Type ("fun", _) => let val (cT1, cT2) = dest_funT cT; val (cTs, cT') = strip_type cT2 in (cT1 :: cTs, cT') end | _ => ([], cT)); (* cterm operations *) fun all_name ctxt (x, t) A = let val T = Thm.typ_of_cterm t; val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); in Thm.apply all_const (Thm.lambda_name (x, t) A) end; fun all ctxt t A = all_name ctxt ("", t) A; fun mk_binop c a b = Thm.apply (Thm.apply c a) b; fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); fun dest_implies ct = (case Thm.term_of ct of Const ("Pure.imp", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_implies", [Thm.term_of ct])); fun dest_equals ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_equals", [Thm.term_of ct])); fun dest_equals_lhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); fun dest_equals_rhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); val lhs_of = dest_equals_lhs o Thm.cprop_of; val rhs_of = dest_equals_rhs o Thm.cprop_of; (* certified term order *) val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of; val term_ord = Term_Ord.term_ord o apply2 Thm.term_of; (* thm order: ignores theory context! *) val thm_ord = Term_Ord.fast_term_ord o apply2 Thm.prop_of <<< list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of <<< list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of <<< list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of; (* tables and caches *) structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); structure Thmtab = Table(type key = thm val ord = thm_ord); fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; (* equality *) fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) handle TERM _ => false; val eq_thm = is_equal o thm_ord; val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; fun eq_thm_strict ths = eq_thm ths andalso Context.eq_thy_id (apply2 Thm.theory_id ths) andalso op = (apply2 Thm.maxidx_of ths) andalso op = (apply2 Thm.get_tags ths); (* pattern equivalence *) fun equiv_thm thy ths = Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); (* type classes and sorts *) fun class_triv thy c = Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; (* misc operations *) fun is_dummy thm = (case try Logic.dest_term (Thm.concl_of thm) of NONE => false | SOME t => Term.is_dummy_pattern (Term.head_of t)); (* collections of theorems in canonical order *) val add_thm = update eq_thm_prop; val del_thm = remove eq_thm_prop; val merge_thms = merge eq_thm_prop; val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of); val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); (** declared hyps and sort hyps **) structure Hyps = Proof_Data ( type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; ); fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); (* hyps *) fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; in (checked_hyps, hyps', shyps) end); fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); fun restore_hyps ctxt = map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); fun undeclared_hyps context th = Thm.hyps_of th |> filter_out (case context of Context.Theory _ => K false | Context.Proof ctxt => (case Hyps.get ctxt of {checked_hyps = false, ...} => K true | {hyps, ...} => Termtab.defined hyps)); fun check_hyps context th = (case undeclared_hyps context th of [] => th | undeclared => error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); (* shyps *) fun declare_term_sorts t = map_hyps (fn (checked_hyps, hyps, shyps) => (checked_hyps, hyps, Sorts.insert_term t shyps)); fun extra_shyps' ctxt th = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); fun check_shyps ctxt raw_th = let val th = Thm.strip_shyps raw_th; val extra_shyps = extra_shyps' ctxt th; in if null extra_shyps then th else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) end; val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; (** basic derived rules **) (*Elimination of implication A A \ B ------------ B *) fun elim_implies thA thAB = Thm.implies_elim thAB thA; (* forall_intr_name *) fun forall_intr_name (a, x) th = let val th' = Thm.forall_intr x th; val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); in Thm.renamed_prop prop' th' end; (* forall_elim_var(s) *) local fun dest_all ct = (case Thm.term_of ct of Const ("Pure.all", _) $ Abs (a, _, _) => let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct) in SOME ((a, Thm.ctyp_of_cterm x), ct') end | _ => NONE); fun dest_all_list ct = (case dest_all ct of NONE => [] | SOME (v, ct') => v :: dest_all_list ct'); fun forall_elim_vars_list vars i th = let val used = (Thm.fold_terms o Term.fold_aterms) (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th []; val vars' = (Name.variant_list used (map #1 vars), vars) |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T)); in fold Thm.forall_elim vars' th end; in fun forall_elim_vars i th = forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th; fun forall_elim_var i th = let val vars = (case dest_all (Thm.cprop_of th) of SOME (v, _) => [v] | NONE => raise THM ("forall_elim_var", i, [th])); in forall_elim_vars_list vars i th end; end; (* instantiate frees *) fun instantiate_frees ([], []) th = th | instantiate_frees (instT, inst) th = let val idx = Thm.maxidx_of th + 1; fun index ((a, A), b) = (((a, idx), A), b); val insts = (map index instT, map index inst); val frees = (map (#1 o #1) instT, map (#1 o #1) inst); val hyps = Thm.chyps_of th; val inst_cterm = Thm.generalize_cterm frees idx #> Thm.instantiate_cterm insts; in th |> fold_rev Thm.implies_intr hyps |> Thm.generalize frees idx |> Thm.instantiate insts |> fold (elim_implies o Thm.assume o inst_cterm) hyps end; (* instantiate by left-to-right occurrence of variables *) fun instantiate' cTs cts thm = let fun err msg = raise TYPE ("instantiate': " ^ msg, map_filter (Option.map Thm.typ_of) cTs, map_filter (Option.map Thm.term_of) cts); fun zip_vars xs ys = zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; val thm' = Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; val thm'' = Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; in thm'' end; (* forall_intr_frees: generalization over all suitable Free variables *) fun forall_intr_frees th = let val fixed = fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) []; val frees = Thm.fold_atomic_cterms (fn a => (case Thm.term_of a of Free v => not (member (op =) fixed v) ? insert (op aconvc) a | _ => I)) th []; in fold Thm.forall_intr frees th end; (* unvarify_global: global schematic variables *) fun unvarify_global thy th = let val prop = Thm.full_prop_of th; val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) handle TERM (msg, _) => raise THM (msg, 0, [th]); val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => let val T' = Term_Subst.instantiateT instT T in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end; fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; (* user renaming of parameters in a subgoal *) (*The names, if distinct, are used for the innermost parameters of subgoal i; preceding parameters may be renamed to make all parameters distinct.*) fun rename_params_rule (names, i) st = let val (_, Bs, Bi, C) = Thm.dest_state (st, i); val params = map #1 (Logic.strip_params Bi); val short = length params - length names; val names' = if short < 0 then error "More names than parameters in subgoal!" else Name.variant_list names (take short params) @ names; val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; val Bi' = Logic.list_rename_params names' Bi; in (case duplicates (op =) names of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) | [] => (case inter (op =) names free_names of a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) end; (* preservation of bound variable names *) fun rename_boundvars pat obj th = (case Term.rename_abs pat obj (Thm.prop_of th) of NONE => th | SOME prop' => Thm.renamed_prop prop' th); (** specification primitives **) (* rules *) fun stripped_sorts thy t = let val tfrees = rev (Term.add_tfrees t []); val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); val recover = map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) tfrees' tfrees; val strip = map (apply2 TFree) (tfrees ~~ tfrees'); val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; fun add_axiom ctxt (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val (strip, recover, prop') = stripped_sorts thy prop; val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; val thy' = thy |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (recover, []) axm' |> unvarify_global thy' |> fold elim_implies of_sorts; in ((axm_name, thm), thy') end; fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (recover, []) axm' |> unvarify_global thy' |> fold_rev Thm.implies_intr prems; in ((axm_name, thm), thy') end; fun add_def_global unchecked overloaded arg thy = add_def (Defs.global_context thy) unchecked overloaded arg thy; (** theorem tags **) (* add / delete tags *) fun tag_rule tg = Thm.map_tags (insert (op =) tg); fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); (* free dummy thm -- for abstract closure *) val free_dummyN = "free_dummy"; fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; val tag_free_dummy = tag_rule (free_dummyN, ""); (* def_name *) fun def_name c = c ^ "_def"; fun def_name_optional c "" = def_name c | def_name_optional _ name = name; val def_binding = Binding.map_name def_name #> Binding.reset_pos; fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; fun make_def_binding cond b = if cond then def_binding b else Binding.empty; (* unofficial theorem names *) fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); (* theorem kinds *) val theoremK = "theorem"; fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; (** attributes **) (*attributes subsume any kind of rules or context modifiers*) type attribute = Context.generic * thm -> Context.generic option * thm option; type binding = binding * attribute list; fun rule_attribute ths f (x, th) = (NONE, (case find_first is_free_dummy (th :: ths) of SOME th' => SOME th' | NONE => SOME (f x th))); fun declaration_attribute f (x, th) = (if is_free_dummy th then NONE else SOME (f th x), NONE); fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; fun apply_attribute (att: attribute) th x = let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) in (the_default th th', the_default x x') end; fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let fun app [] th x = (th, x) | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory; val proof_attributes = apply_attributes Context.Proof Context.the_proof; fun no_attributes x = (x, []); fun simple_fact x = [(x, [])]; fun tag tg = rule_attribute [] (K (tag_rule tg)); fun untag s = rule_attribute [] (K (untag_rule s)); fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); -(** proof terms **) - -fun reconstruct_proof_of thm = - Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); - -fun standard_proof_of {full, expand_name} thm = - let val thy = Thm.theory_of_thm thm in - reconstruct_proof_of thm - |> Proofterm.expand_proof thy expand_name - |> Proofterm.rew_proof thy - |> Proofterm.no_thm_proofs - |> not full ? Proofterm.shrink_proof - end; - - - (** forked proofs **) structure Proofs = Theory_Data ( type T = thm list lazy list; val empty = []; fun extend _ = empty; fun merge _ = empty; ); fun register_proofs ths = (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths); fun force_proofs thy = rev (Proofs.get thy) |> maps (map (Thm.transfer thy) o Lazy.force); val consolidate_theory = Thm.consolidate o force_proofs; fun expose_theory thy = if Proofterm.export_enabled () then Thm.expose_proofs thy (force_proofs thy) else (); (** print theorems **) (* options *) val show_consts = Config.declare_option_bool ("show_consts", \<^here>); val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); (* pretty_thm etc. *) fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = let val show_tags = Config.get ctxt show_tags; val show_hyps = Config.get ctxt show_hyps; val th = raw_th |> perhaps (try (Thm.transfer' ctxt)) |> perhaps (try Thm.strip_shyps); val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; val extra_shyps = extra_shyps' ctxt th; val tags = Thm.get_tags th; val tpairs = Thm.tpairs_of th; val q = if quote then Pretty.quote else I; val prt_term = q o Syntax.pretty_term ctxt; val hlen = length extra_shyps + length hyps + length tpairs; val hsymbs = if hlen = 0 then [] else if show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ map (Syntax.pretty_sort ctxt) extra_shyps)] else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; val tsymbs = if null tags orelse not show_tags then [] else [Pretty.brk 1, pretty_tags tags]; in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; fun pretty_thm_global thy = pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; val string_of_thm = Pretty.string_of oo pretty_thm; val string_of_thm_global = Pretty.string_of oo pretty_thm_global; open Thm; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm; diff --git a/src/Pure/thm.ML b/src/Pure/thm.ML --- a/src/Pure/thm.ML +++ b/src/Pure/thm.ML @@ -1,2341 +1,2345 @@ (* Title: Pure/thm.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Makarius The very core of Isabelle's Meta Logic: certified types and terms, derivations, theorems, inference rules (including lifting and resolution), oracles. *) infix 0 RS RSN; signature BASIC_THM = sig type ctyp type cterm exception CTERM of string * cterm list type thm type conv = cterm -> thm exception THM of string * int * thm list val RSN: thm * (int * thm) -> thm val RS: thm * thm -> thm end; signature THM = sig include BASIC_THM (*certified types*) val typ_of: ctyp -> typ val global_ctyp_of: theory -> typ -> ctyp val ctyp_of: Proof.context -> typ -> ctyp val dest_ctyp: ctyp -> ctyp list val dest_ctypN: int -> ctyp -> ctyp val dest_ctyp0: ctyp -> ctyp val dest_ctyp1: ctyp -> ctyp val make_ctyp: ctyp -> ctyp list -> ctyp (*certified terms*) val term_of: cterm -> term val typ_of_cterm: cterm -> typ val ctyp_of_cterm: cterm -> ctyp val maxidx_of_cterm: cterm -> int val global_cterm_of: theory -> term -> cterm val cterm_of: Proof.context -> term -> cterm val renamed_term: term -> cterm -> cterm val dest_comb: cterm -> cterm * cterm val dest_fun: cterm -> cterm val dest_arg: cterm -> cterm val dest_fun2: cterm -> cterm val dest_arg1: cterm -> cterm val dest_abs: string option -> cterm -> cterm * cterm val rename_tvar: indexname -> ctyp -> ctyp val var: indexname * ctyp -> cterm val apply: cterm -> cterm -> cterm val lambda_name: string * cterm -> cterm -> cterm val lambda: cterm -> cterm -> cterm val adjust_maxidx_cterm: int -> cterm -> cterm val incr_indexes_cterm: int -> cterm -> cterm val match: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val first_order_match: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list (*theorems*) val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val theory_id: thm -> Context.theory_id val theory_name: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val shyps_of: thm -> sort Ord_List.T val hyps_of: thm -> term list val prop_of: thm -> term val tpairs_of: thm -> (term * term) list val concl_of: thm -> term val prems_of: thm -> term list val nprems_of: thm -> int val no_prems: thm -> bool val major_prem_of: thm -> term val cprop_of: thm -> cterm val cprem_of: thm -> int -> cterm val cconcl_of: thm -> cterm val cprems_of: thm -> cterm list val chyps_of: thm -> cterm list exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option val theory_of_cterm: cterm -> theory val theory_of_thm: thm -> theory val trim_context_ctyp: ctyp -> ctyp val trim_context_cterm: cterm -> cterm val transfer_ctyp: theory -> ctyp -> ctyp val transfer_cterm: theory -> cterm -> cterm val transfer: theory -> thm -> thm val transfer': Proof.context -> thm -> thm val transfer'': Context.generic -> thm -> thm val join_transfer: theory -> thm -> thm val join_transfer_context: Proof.context * thm -> Proof.context * thm val renamed_prop: term -> thm -> thm val weaken: cterm -> thm -> thm val weaken_sorts: sort list -> cterm -> cterm val extra_shyps: thm -> sort list val proof_bodies_of: thm list -> proof_body list val proof_body_of: thm -> proof_body val proof_of: thm -> proof + val reconstruct_proof_of: thm -> Proofterm.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 val derivation_name: thm -> string val derivation_id: thm -> Proofterm.thm_id option val raw_derivation_name: thm -> string 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 trim_context: thm -> thm val axiom: theory -> string -> thm val all_axioms_of: theory -> (string * thm) list val get_tags: thm -> Properties.T val map_tags: (Properties.T -> Properties.T) -> thm -> thm val norm_proof: thm -> thm val adjust_maxidx_thm: int -> thm -> thm (*type classes*) val the_classrel: theory -> class * class -> thm val the_arity: theory -> string * sort list * class -> thm val classrel_proof: theory -> class * class -> proof val arity_proof: theory -> string * sort list * class -> proof (*oracles*) val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory val oracle_space: theory -> Name_Space.T val pretty_oracle: Proof.context -> string -> Pretty.T val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list val check_oracle: Proof.context -> xstring * Position.T -> string (*inference rules*) val assume: cterm -> thm val implies_intr: cterm -> thm -> thm val implies_elim: thm -> thm -> thm val forall_intr: cterm -> thm -> thm val forall_elim: cterm -> thm -> thm val reflexive: cterm -> thm val symmetric: thm -> thm val transitive: thm -> thm -> thm val beta_conversion: bool -> conv val eta_conversion: conv val eta_long_conversion: conv val abstract_rule: string -> cterm -> thm -> thm val combination: thm -> thm -> thm val equal_intr: thm -> thm -> thm val equal_elim: thm -> thm -> thm val solve_constraints: thm -> thm val flexflex_rule: Proof.context option -> thm -> thm Seq.seq val generalize: string list * string list -> int -> thm -> thm val generalize_cterm: string list * string list -> int -> cterm -> cterm val generalize_ctyp: string list -> int -> ctyp -> ctyp val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val strip_shyps: thm -> thm val unconstrainT: thm -> thm val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm val varifyT_global: thm -> thm val legacy_freezeT: thm -> thm val plain_prop_of: thm -> term val dest_state: thm * int -> (term * term) list * term list * term * term val lift_rule: cterm -> thm -> thm val incr_indexes: int -> thm -> thm val assumption: Proof.context option -> int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm val rotate_rule: int -> int -> thm -> thm val permute_prems: int -> int -> thm -> thm val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} -> bool * thm * int -> int -> thm -> thm Seq.seq val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq val thynames_of_arity: theory -> string * class -> string list val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory end; structure Thm: THM = struct (*** Certified terms and types ***) (** certified types **) datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T}; fun typ_of (Ctyp {T, ...}) = T; fun global_ctyp_of thy raw_T = let val T = Sign.certify_typ thy raw_T; val maxidx = Term.maxidx_of_typ T; val sorts = Sorts.insert_typ T []; in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end; val ctyp_of = global_ctyp_of o Proof_Context.theory_of; fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) = map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) = let fun err () = raise TYPE ("dest_ctypN", [T], []) in (case T of Type (_, Ts) => Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (), maxidx = maxidx, sorts = sorts} | _ => err ()) end; val dest_ctyp0 = dest_ctypN 0; val dest_ctyp1 = dest_ctypN 1; fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert); fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts; fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx); fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs = let val As = map typ_of cargs; fun err () = raise TYPE ("make_ctyp", T :: As, []); in (case T of Type (a, args) => Ctyp { cert = fold join_certificate_ctyp cargs cert, maxidx = fold maxidx_ctyp cargs ~1, sorts = fold union_sorts_ctyp cargs [], T = if length args = length cargs then Type (a, As) else err ()} | _ => err ()) end; (** certified terms **) (*certified terms with checked typ, maxidx, and sorts*) datatype cterm = Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}; exception CTERM of string * cterm list; fun term_of (Cterm {t, ...}) = t; fun typ_of_cterm (Cterm {T, ...}) = T; fun ctyp_of_cterm (Cterm {cert, T, maxidx, sorts, ...}) = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}; fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx; fun global_cterm_of thy tm = let val (t, T, maxidx) = Sign.certify_term thy tm; val sorts = Sorts.insert_term t []; in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; val cterm_of = global_cterm_of o Proof_Context.theory_of; fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) = Context.join_certificate (cert1, cert2); fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) = if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts} else raise TERM ("renamed_term: terms disagree", [t, t']); (* destructors *) fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in (Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts}, Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts}) end | dest_comb ct = raise CTERM ("dest_comb", [ct]); fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_fun ct = raise CTERM ("dest_fun", [ct]); fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_arg ct = raise CTERM ("dest_arg", [ct]); fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0; val B = Term.argument_type_of c 1; in Cterm {t = c, T = A --> B --> T, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) = let val (y', t') = Term.dest_abs (the_default x a, T, t) in (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}, Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}) end | dest_abs _ ct = raise CTERM ("dest_abs", [ct]); (* constructors *) fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = let val S = (case T of TFree (_, S) => S | TVar (_, S) => S | _ => raise TYPE ("rename_tvar: no variable", [T], [])); val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else (); in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end; fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) = if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)]) else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts}; fun apply (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = if T = dty then Cterm {cert = join_certificate0 (cf, cx), t = f $ x, T = rty, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} else raise CTERM ("apply: types don't agree", [cf, cx]) | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]); fun lambda_name (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = let val t = Term.lambda_name (x, t1) t2 in Cterm {cert = join_certificate0 (ct1, ct2), t = t, T = T1 --> T2, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} end; fun lambda t u = lambda_name ("", t) u; (* indexes *) fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if maxidx = i then ct else if maxidx < i then Cterm {maxidx = i, cert = cert, t = t, T = T, sorts = sorts} else Cterm {maxidx = Int.max (maxidx_of_term t, i), cert = cert, t = t, T = T, sorts = sorts}; fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if i < 0 then raise CTERM ("negative increment", [ct]) else if i = 0 then ct else Cterm {cert = cert, t = Logic.incr_indexes ([], [], i) t, T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; (*** Derivations and Theorems ***) (* sort constraints *) type constraint = {theory: theory, typ: typ, sort: sort}; local val constraint_ord : constraint ord = Context.theory_id_ord o apply2 (Context.theory_id o #theory) <<< Term_Ord.typ_ord o apply2 #typ <<< Term_Ord.sort_ord o apply2 #sort; val smash_atyps = map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T); in 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_env thy env = let val tyenv = Envir.type_env env; fun insert ([], _) = I | insert (S, T) = insert_constraints thy (Envir.norm_type tyenv T, S); in tyenv |> Vartab.fold (insert o #2) end; end; (* datatype thm *) datatype thm = Thm of deriv * (*derivation*) {cert: Context.certificate, (*background theory certificate*) tags: Properties.T, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) constraints: constraint Ord_List.T, (*implicit proof obligations for sort constraints*) shyps: sort Ord_List.T, (*sort hypotheses*) hyps: term Ord_List.T, (*hypotheses*) tpairs: (term * term) list, (*flex-flex pairs*) prop: term} (*conclusion*) and deriv = Deriv of {promises: (serial * thm future) Ord_List.T, body: Proofterm.proof_body}; type conv = cterm -> thm; (*errors involving theorems*) exception THM of string * int * thm list; fun rep_thm (Thm (_, args)) = args; fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) = fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps; fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end; fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in (fold_terms o fold_aterms) (fn t as Const (_, T) => f (cterm t T) | t as Free (_, T) => f (cterm t T) | t as Var (_, T) => f (cterm t T) | _ => I) th end; fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs []; fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u'; fun union_tpairs ts us = Library.merge eq_tpairs (ts, us); val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u); fun attach_tpairs tpairs prop = Logic.list_implies (map Logic.mk_equals tpairs, prop); fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop; val union_hyps = Ord_List.union Term_Ord.fast_term_ord; val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) = Context.join_certificate (cert1, cert2); fun join_certificate2 (Thm (_, {cert = cert1, ...}), Thm (_, {cert = cert2, ...})) = Context.join_certificate (cert1, cert2); (* basic components *) val cert_of = #cert o rep_thm; val theory_id = Context.certificate_theory_id o cert_of; val theory_name = Context.theory_id_name o theory_id; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val shyps_of = #shyps o rep_thm; val hyps_of = #hyps o rep_thm; val prop_of = #prop o rep_thm; val tpairs_of = #tpairs o rep_thm; val concl_of = Logic.strip_imp_concl o prop_of; val prems_of = Logic.strip_imp_prems o prop_of; val nprems_of = Logic.count_prems o prop_of; fun no_prems th = nprems_of th = 0; fun major_prem_of th = (case prems_of th of prem :: _ => Logic.strip_assums_concl prem | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) = Cterm {cert = cert, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i = Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) = Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th}; fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t}) (prems_of th); fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps; (* implicit theory context *) exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option; fun theory_of_cterm (ct as Cterm {cert, ...}) = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); fun theory_of_thm th = Context.certificate_theory (cert_of th) handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE); fun trim_context_ctyp cT = (case cT of Ctyp {cert = Context.Certificate_Id _, ...} => cT | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} => Ctyp {cert = Context.Certificate_Id (Context.theory_id thy), T = T, maxidx = maxidx, sorts = sorts}); fun trim_context_cterm ct = (case ct of Cterm {cert = Context.Certificate_Id _, ...} => ct | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} => Cterm {cert = Context.Certificate_Id (Context.theory_id thy), t = t, T = T, maxidx = maxidx, sorts = sorts}); fun trim_context_thm th = (case th of Thm (_, {constraints = _ :: _, ...}) => raise THM ("trim_context: pending sort constraints", 0, [th]) | Thm (_, {cert = Context.Certificate_Id _, ...}) => th | Thm (der, {cert = Context.Certificate thy, tags, maxidx, constraints = [], shyps, hyps, tpairs, prop}) => Thm (der, {cert = Context.Certificate_Id (Context.theory_id thy), tags = tags, maxidx = maxidx, constraints = [], shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})); fun transfer_ctyp thy' cT = let val Ctyp {cert, T, maxidx, sorts} = cT; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then cT else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts} end; fun transfer_cterm thy' ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then ct else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts} end; fun transfer thy' th = let val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then th else Thm (der, {cert = cert', tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) end; val transfer' = transfer o Proof_Context.theory_of; val transfer'' = transfer o Context.theory_of; fun join_transfer thy th = if Context.subthy_id (Context.theory_id thy, theory_id th) then th else transfer thy th; fun join_transfer_context (ctxt, th) = if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then (Context.raw_transfer (theory_of_thm th) ctxt, th) else (ctxt, transfer' ctxt th); (* matching *) local fun gen_match match (ct1 as Cterm {t = t1, sorts = sorts1, ...}, ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = let val cert = join_certificate0 (ct1, ct2); val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE); val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = (((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (U, t)) = let val T = Envir.subst_type Tinsts U in (((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; in val match = gen_match Pattern.match; val first_order_match = gen_match Pattern.first_order_match; end; (*implicit alpha-conversion*) fun renamed_prop prop' (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = if prop aconv prop' then Thm (der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop'}) else raise TERM ("renamed_prop: props disagree", [prop, prop']); fun make_context ths NONE cert = (Context.Theory (Context.certificate_theory cert) handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE)) | make_context ths (SOME ctxt) cert = let val thy_id = Context.certificate_theory_id cert; val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt); in if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt else raise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt)) end; fun make_context_certificate ths opt_ctxt cert = let val context = make_context ths opt_ctxt cert; val cert' = Context.Certificate (Context.theory_of context); in (context, cert') end; (*explicit weakening: maps |- B to A |- B*) fun weaken raw_ct th = let val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; val Thm (der, {tags, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; in if T <> propT then raise THM ("weaken: assumptions must have type prop", 0, []) else if maxidxA <> ~1 then raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) else Thm (der, {cert = join_certificate1 (ct, th), tags = tags, maxidx = maxidx, constraints = constraints, shyps = Sorts.union sorts shyps, hyps = insert_hyps A hyps, tpairs = tpairs, prop = prop}) end; fun weaken_sorts raw_sorts ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val thy = theory_of_cterm ct; val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); val sorts' = Sorts.union sorts more_sorts; in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; (*dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) = Sorts.subtract (fold_terms Sorts.insert_term th []) shyps; (** derivations and promised proofs **) fun make_deriv promises oracles thms proof = Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}}; val empty_deriv = make_deriv [] [] [] MinProof; (* inference rules *) val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i); fun bad_proofs i = error ("Illegal level of detail for proof objects: " ^ string_of_int i); fun deriv_rule2 f (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}}) (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) = let val ps = Ord_List.union promise_ord ps1 ps2; val oracles = Proofterm.unions_oracles [oracles1, oracles2]; val thms = Proofterm.unions_thms [thms1, thms2]; val prf = (case ! Proofterm.proofs of 2 => f prf1 prf2 | 1 => MinProof | 0 => MinProof | i => bad_proofs i); in make_deriv ps oracles thms prf end; fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; fun deriv_rule0 make_prf = if ! Proofterm.proofs <= 1 then empty_deriv else deriv_rule1 I (make_deriv [] [] [] (make_prf ())); fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) = make_deriv promises oracles thms (f proof); (* fulfilled proofs *) fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises; fun join_promises [] = () | join_promises promises = join_promises_of (Future.joins (map snd promises)) and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); fun fulfill_body (th as Thm (Deriv {promises, body}, _)) = let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises)) in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end; fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms); val proof_body_of = singleton proof_bodies_of; val proof_of = Proofterm.proof_of o proof_body_of; +fun reconstruct_proof_of thm = + Proofterm.reconstruct_proof (theory_of_thm thm) (prop_of thm) (proof_of thm); + val consolidate = ignore o proof_bodies_of; fun expose_proofs thy thms = if Proofterm.export_proof_boxes_required thy then Proofterm.export_proof_boxes (proof_bodies_of (map (transfer thy) thms)) else (); fun expose_proof thy = expose_proofs thy o single; (* future rule *) fun future_result i orig_cert orig_shyps orig_prop thm = let fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]); val Thm (Deriv {promises, ...}, {cert, constraints, shyps, hyps, tpairs, prop, ...}) = thm; val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory"; val _ = prop aconv orig_prop orelse err "bad prop"; val _ = null constraints orelse err "bad sort constraints"; val _ = null tpairs orelse err "bad flex-flex constraints"; val _ = null hyps orelse err "bad hyps"; val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps"; val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies"; val _ = join_promises promises; in thm end; fun future future_thm ct = let val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct; val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val _ = if Proofterm.proofs_enabled () then raise CTERM ("future: proof terms enabled", [ct]) else (); val i = serial (); val future = future_thm |> Future.map (future_result i cert sorts prop); in Thm (make_deriv [(i, future)] [] [] MinProof, {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) end; (** Axioms **) fun axiom thy name = (case Name_Space.lookup (Theory.axiom_table thy) name of SOME prop => let val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); val cert = Context.Certificate thy; val maxidx = maxidx_of_term prop; val shyps = Sorts.insert_term prop []; in Thm (der, {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) end | NONE => raise THEORY ("No axiom " ^ quote name, [thy])); fun all_axioms_of thy = map (fn (name, _) => (name, axiom thy name)) (Theory.all_axioms_of thy); (* tags *) val get_tags = #tags o rep_thm; fun map_tags f (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = Thm (der, {cert = cert, tags = f tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (* technical adjustments *) fun norm_proof (th as Thm (der, args)) = Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args); fun adjust_maxidx_thm i (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = if maxidx = i then th else if maxidx < i then Thm (der, {maxidx = i, cert = cert, tags = tags, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) else Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), cert = cert, tags = tags, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (*** Theory data ***) (* type classes *) structure Aritytab = Table( type key = string * sort list * class; val ord = fast_string_ord o apply2 #1 <<< fast_string_ord o apply2 #3 <<< list_ord Term_Ord.sort_ord o apply2 #2; ); datatype classes = Classes of {classrels: thm Symreltab.table, arities: (thm * string * serial) Aritytab.table}; fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities}; val empty_classes = make_classes (Symreltab.empty, Aritytab.empty); (*see Theory.at_begin hook for transitive closure of classrels and arity completion*) fun merge_classes (Classes {classrels = classrels1, arities = arities1}, Classes {classrels = classrels2, arities = arities2}) = let val classrels' = Symreltab.merge (K true) (classrels1, classrels2); val arities' = Aritytab.merge (K true) (arities1, arities2); in make_classes (classrels', arities') end; (* data *) structure Data = Theory_Data ( type T = unit Name_Space.table * (*oracles: authentic derivation names*) classes; (*type classes within the logic*) val empty : T = (Name_Space.empty_table "oracle", empty_classes); val extend = I; fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T = (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_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))); fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities)); fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities)); (* type classes *) fun the_classrel thy (c1, c2) = (case Symreltab.lookup (get_classrels thy) (c1, c2) of SOME thm => transfer thy thm | NONE => error ("Unproven class relation " ^ Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2])); fun the_arity thy (a, Ss, c) = (case Aritytab.lookup (get_arities thy) (a, Ss, c) of SOME (thm, _, _) => transfer thy thm | NONE => error ("Unproven type arity " ^ Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); val classrel_proof = proof_of oo the_classrel; val arity_proof = proof_of oo the_arity; (* solve sort constraints by pro-forma proof *) local fun union_digest (oracles1, thms1) (oracles2, thms2) = (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]); 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 ([], []) 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 ([], [])) (Type.sort_of_atyp T)} (typ, sort); 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; val thy = Context.certificate_theory cert; 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 Deriv {promises, body = PBody {oracles, thms, proof}} = der; val (oracles', thms') = (oracles, thms) |> fold (fold union_digest o constraint_digest) constraints; val body' = PBody {oracles = oracles', thms = thms', proof = proof}; in Thm (Deriv {promises = promises, body = body'}, {constraints = [], cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) end; end; (*** Closed theorems with official name ***) (*non-deterministic, depends on unknown promises*) fun derivation_closed (Thm (Deriv {body, ...}, _)) = Proofterm.compact_proof (Proofterm.proof_of body); (*non-deterministic, depends on unknown promises*) fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body); fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = let val self_id = (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of NONE => K false | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE; in expand end; (*deterministic name of finished proof*) fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) = Proofterm.get_approximative_name shyps hyps prop (proof_of thm); (*identified PThm node*) fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) = Proofterm.get_id shyps hyps prop (proof_of thm); (*dependencies of PThm node*) fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) = (case (derivation_id thm, thms) of (SOME {serial = i, ...}, [(j, thm_node)]) => if i = j then Proofterm.thm_node_thms thm_node else thms | _ => thms) | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]); fun name_derivation name_pos = solve_constraints #> (fn thm as Thm (der, args) => let val thy = theory_of_thm thm; val Deriv {promises, body} = der; val {shyps, hyps, prop, tpairs, ...} = args; val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]); val ps = map (apsnd (Future.map fulfill_body)) promises; val (pthm, proof) = Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) name_pos shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; in Thm (der', args) end); fun close_derivation pos = solve_constraints #> (fn thm => if not (null (tpairs_of thm)) orelse derivation_closed thm then thm else name_derivation ("", pos) thm); val trim_context = solve_constraints #> trim_context_thm; (*** Oracles ***) fun add_oracle (b, oracle_fn) thy = let val (name, oracles') = Name_Space.define (Context.Theory thy) true (b, ()) (get_oracles thy); val thy' = map_oracles (K oracles') thy; fun invoke_oracle arg = let val Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else let val (oracle, prf) = (case ! Proofterm.proofs of 2 => ((name, SOME prop), Proofterm.oracle_proof name prop) | 1 => ((name, SOME prop), MinProof) | 0 => ((name, NONE), MinProof) | i => bad_proofs i); in Thm (make_deriv [] [oracle] [] prf, {cert = Context.join_certificate (Context.Certificate thy', cert2), tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) end end; in ((name, invoke_oracle), thy') end; val oracle_space = Name_Space.space_of_table o get_oracles; fun pretty_oracle ctxt = Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt)); fun extern_oracles verbose ctxt = map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt))); fun check_oracle ctxt = Name_Space.check (Context.Proof ctxt) (get_oracles (Proof_Context.theory_of ctxt)) #> #1; (*** Meta rules ***) (** primitive rules **) (*The assumption rule A |- A*) fun assume raw_ct = let val Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in if T <> propT then raise THM ("assume: prop", 0, []) else if maxidx <> ~1 then raise THM ("assume: variables", maxidx, []) else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop), {cert = cert, tags = [], maxidx = ~1, constraints = [], shyps = sorts, hyps = [prop], tpairs = [], prop = prop}) end; (*Implication introduction [A] : B ------- A \ B *) fun implies_intr (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...})) = if T <> propT then raise THM ("implies_intr: assumptions must have type prop", 0, [th]) else Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = remove_hyps A hyps, tpairs = tpairs, prop = Logic.mk_implies (A, prop)}); (*Implication elimination A \ B A ------------ B *) fun implies_elim thAB thA = let val Thm (derA, {maxidx = maxidx1, hyps = hypsA, constraints = constraintsA, shyps = shypsA, tpairs = tpairsA, prop = propA, ...}) = thA and Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...}) = thAB; fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); in (case prop of Const ("Pure.imp", _) $ A $ B => if A aconv propA then Thm (deriv_rule2 (curry Proofterm.%%) der derA, {cert = join_certificate2 (thAB, thA), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraintsA constraints, shyps = Sorts.union shypsA shyps, hyps = union_hyps hypsA hyps, tpairs = union_tpairs tpairsA tpairs, prop = B}) else err () | _ => err ()) end; (*Forall introduction. The Free or Var x must not be free in the hypotheses. [x] : A ------ \x. A *) fun forall_intr (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = let fun result a = Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))}); fun check_occs a x ts = if exists (fn t => Logic.occs (x, t)) ts then raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) | _ => raise THM ("forall_intr: not a variable", 0, [th])) end; (*Forall elimination \x. A ------ A[t/x] *) fun forall_elim (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = (case prop of Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => if T <> qary then raise THM ("forall_elim: type mismatch", 0, [th]) else Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Term.betapply (A, t)}) | _ => raise THM ("forall_elim: not quantified", 0, [th])); (* Equality *) (*Reflexivity t \ t *) fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, t)}); (*Symmetry t \ u ------ u \ t *) fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = (case prop of (eq as Const ("Pure.eq", _)) $ t $ u => Thm (deriv_rule1 Proofterm.symmetric_proof der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = eq $ u $ t}) | _ => raise THM ("symmetric", 0, [th])); (*Transitivity t1 \ u u \ t2 ------------------ t1 \ t2 *) fun transitive th1 th2 = let val Thm (der1, {maxidx = maxidx1, hyps = hyps1, constraints = constraints1, shyps = shyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, hyps = hyps2, constraints = constraints2, shyps = shyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); in case (prop1, prop2) of ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) => if not (u aconv u') then err "middle term" else Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = eq $ t1 $ t2}) | _ => err "premises" end; (*Beta-conversion (\x. t) u \ t[u/x] fully beta-reduces the term if full = true *) fun beta_conversion full (Cterm {cert, t, T = _, maxidx, sorts}) = let val t' = if full then Envir.beta_norm t else (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) | _ => raise THM ("beta_conversion: not a redex", 0, [])); in Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, t')}) end; fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, Envir.eta_contract t)}); fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, Envir.eta_long [] t)}); (*The abstraction rule. The Free or Var x must not be free in the hypotheses. The bound variable will be named "a" (since x will be something like x320) t \ u -------------- \x. t \ \x. u *) fun abstract_rule a (Cterm {t = x, T, sorts, ...}) (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) = let val (t, u) = Logic.dest_equals prop handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); val result = Thm (deriv_rule1 (Proofterm.abstract_rule_proof (a, x)) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.mk_equals (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}); fun check_occs a x ts = if exists (fn t => Logic.occs (x, t)) ts then raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) | _ => raise THM ("abstract_rule: not a variable", 0, [th])) end; (*The combination rule f \ g t \ u ------------- f t \ g u *) fun combination th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun chktypes fT tT = (case fT of Type ("fun", [T1, _]) => if T1 <> tT then raise THM ("combination: types", 0, [th1, th2]) else () | _ => raise THM ("combination: not function type", 0, [th1, th2])); in (case (prop1, prop2) of (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => (chktypes fT tT; Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (f $ t, g $ u)})) | _ => raise THM ("combination: premises", 0, [th1, th2])) end; (*Equality introduction A \ B B \ A ---------------- A \ B *) fun equal_intr th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); in (case (prop1, prop2) of (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') => if A aconv A' andalso B aconv B' then Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (A, B)}) else err "not equal" | _ => err "premises") end; (*The equal propositions rule A \ B A --------- B *) fun equal_elim th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); in (case prop1 of Const ("Pure.eq", _) $ A $ B => if prop2 aconv A then Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = B}) else err "not equal" | _ => err "major premise") end; (**** Derived rules ****) (*Smash unifies the list of term pairs leaving no flex-flex pairs. Instantiates the theorem and deletes trivial tpairs. Resulting sequence may contain multiple elements if the tpairs are not all flex-flex.*) fun flexflex_rule opt_ctxt = solve_constraints #> (fn th => let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val (context, cert') = make_context_certificate [th] opt_ctxt cert; in Unify.smash_unifiers context tpairs (Envir.empty maxidx) |> Seq.map (fn env => if Envir.is_empty env then th else let val tpairs' = tpairs |> map (apply2 (Envir.norm_term env)) (*remove trivial tpairs, of the form t \ t*) |> filter_out (op aconv); val der' = deriv_rule1 (Proofterm.norm_proof' env) der; val constraints' = insert_constraints_env (Context.certificate_theory cert') env constraints; val prop' = Envir.norm_term env prop; val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); val shyps = Envir.insert_sorts env shyps; in Thm (der', {cert = cert', tags = [], maxidx = maxidx, constraints = constraints', shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) end) end); (*Generalization of fixed variables A -------------------- A[?'a/'a, ?x/x, ...] *) fun generalize ([], []) _ th = th | generalize (tfrees, frees) idx th = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); val bad_type = if null tfrees then K false else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false); fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x | bad_term (Var (_, T)) = bad_type T | bad_term (Const (_, T)) = bad_type T | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t | bad_term (t $ u) = bad_term t orelse bad_term u | bad_term (Bound _) = false; val _ = exists bad_term hyps andalso raise THM ("generalize: variable free in assumptions", 0, [th]); val generalize = Term_Subst.generalize (tfrees, frees) idx; val prop' = generalize prop; val tpairs' = map (apply2 generalize) tpairs; val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); in Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, {cert = cert, tags = [], maxidx = maxidx', constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) end; fun generalize_cterm ([], []) _ ct = ct | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) else Cterm {cert = cert, sorts = sorts, T = Term_Subst.generalizeT tfrees idx T, t = Term_Subst.generalize (tfrees, frees) idx t, maxidx = Int.max (maxidx, idx)}; fun generalize_ctyp [] _ cT = cT | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) = if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) else Ctyp {cert = cert, sorts = sorts, T = Term_Subst.generalizeT tfrees idx T, maxidx = Int.max (maxidx, idx)}; (*Instantiation of schematic variables A -------------------- A[t1/v1, ..., tn/vn] *) local fun pretty_typing thy t T = Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; fun add_inst (v as (_, T), cu) (cert, sorts) = let val Cterm {t = u, T = U, cert = cert2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; val cert' = Context.join_certificate (cert, cert2); val sorts' = Sorts.union sorts_u sorts; in if T = U then ((v, (u, maxidx_u)), (cert', sorts')) else let val msg = (case cert' of Context.Certificate thy' => Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", Pretty.fbrk, pretty_typing thy' (Var v) T, Pretty.fbrk, pretty_typing thy' u U]) | Context.Certificate_Id _ => "instantiate: type conflict"); in raise TYPE (msg, [T, U], [Var v, u]) end end; fun add_instT (v as (_, S), cU) (cert, sorts) = let val Ctyp {T = U, cert = cert2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; val cert' = Context.join_certificate (cert, cert2); val thy' = Context.certificate_theory cert' handle ERROR msg => raise CONTEXT (msg, [cU], [], [], NONE); val sorts' = Sorts.union sorts_U sorts; in if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (cert', sorts')) else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) end; in (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...]. Instantiates distinct Vars by terms of same type. Does NOT normalize the resulting theorem!*) fun instantiate ([], []) th = th | instantiate (instT, inst) th = let val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th; val (inst', (instT', (cert', shyps'))) = (cert, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT handle CONTEXT (msg, cTs, cts, ths, context) => raise CONTEXT (msg, cTs, cts, th :: ths, context); val subst = Term_Subst.instantiate_maxidx (instT', inst'); val (prop', maxidx1) = subst prop ~1; val (tpairs', maxidx') = fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; val thy' = Context.certificate_theory cert'; val constraints' = fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints; in Thm (deriv_rule1 (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, {cert = cert', tags = [], maxidx = maxidx', constraints = constraints', shyps = shyps', hyps = hyps, tpairs = tpairs', prop = prop'}) |> solve_constraints end handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); fun instantiate_cterm ([], []) ct = ct | instantiate_cterm (instT, inst) ct = let val Cterm {cert, t, T, sorts, ...} = ct; val (inst', (instT', (cert', sorts'))) = (cert, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT; val subst = Term_Subst.instantiate_maxidx (instT', inst'); val substT = Term_Subst.instantiateT_maxidx instT'; val (t', maxidx1) = subst t ~1; val (T', maxidx') = substT T maxidx1; in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); end; (*The trivial implication A \ A, justified by assume and forall rules. A can contain Vars, not so for assume!*) fun trivial (Cterm {cert, t = A, T, maxidx, sorts}) = if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else Thm (deriv_rule0 (fn () => Proofterm.trivial_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_implies (A, A)}); (*Axiom-scheme reflecting signature contents T :: c ------------------- OFCLASS(T, c_class) *) fun of_class (cT, raw_c) = let val Ctyp {cert, T, ...} = cT; val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE); val c = Sign.certify_class thy raw_c; val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c)); in if Sign.of_sort thy (T, [c]) then Thm (deriv_rule0 (fn () => Proofterm.OfClass (T, c)), {cert = cert, tags = [], maxidx = maxidx, constraints = insert_constraints thy (T, [c]) [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, []) end |> solve_constraints; (*Remove extra sorts that are witnessed by type signature information*) fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm | strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = let val thy = theory_of_thm thm; val algebra = Sign.classes_of thy; val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; val extra = fold (Sorts.remove_sort o #2) present shyps; val witnessed = Sign.witness_sorts thy present extra; val extra' = fold (Sorts.remove_sort o #2) witnessed extra |> Sorts.minimal_sorts algebra; val shyps' = fold (Sorts.insert_sort o #2) present extra'; in Thm (deriv_rule_unconditional (Proofterm.strip_shyps_proof algebra present witnessed extra') der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) end; (*Internalize sort constraints of type variables*) val unconstrainT = solve_constraints #> (fn thm as Thm (der, args) => let val Deriv {promises, body} = der; val {cert, shyps, hyps, tpairs, prop, ...} = args; val thy = theory_of_thm thm; fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); val _ = null hyps orelse err "bad hyps"; val _ = null tpairs orelse err "bad flex-flex constraints"; val tfrees = rev (Term.add_tfree_names prop []); val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); val ps = map (apsnd (Future.map fulfill_body)) promises; val (pthm, proof) = Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) shyps prop ps body; val der' = make_deriv [] [] [pthm] proof; val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der', {cert = cert, tags = [], maxidx = maxidx_of_term prop', constraints = [], shyps = [[]], (*potentially redundant*) hyps = [], tpairs = [], prop = prop'}) end); (*Replace all TFrees not fixed or in the hyps by new TVars*) fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = let val tfrees = fold Term.add_tfrees hyps fixed; val prop1 = attach_tpairs tpairs prop; val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, {cert = cert, tags = [], maxidx = Int.max (0, maxidx), constraints = constraints, shyps = shyps, hyps = hyps, tpairs = rev (map Logic.dest_equals ts), prop = prop3})) end; val varifyT_global = #2 o varifyT_global' []; (*Replace all TVars by TFrees that are often new*) fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) = let val prop1 = attach_tpairs tpairs prop; val prop2 = Type.legacy_freeze prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der, {cert = cert, tags = [], maxidx = maxidx_of_term prop2, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = rev (map Logic.dest_equals ts), prop = prop3}) end; fun plain_prop_of raw_thm = let val thm = strip_shyps raw_thm; fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); in if not (null (hyps_of thm)) then err "theorem may not contain hypotheses" else if not (null (extra_shyps thm)) then err "theorem may not contain sort hypotheses" else if not (null (tpairs_of thm)) then err "theorem may not contain flex-flex pairs" else prop_of thm end; (*** Inference rules for tactics ***) (*Destruct proof state into constraints, other goals, goal(i), rest *) fun dest_state (state as Thm (_, {prop,tpairs,...}), i) = (case Logic.strip_prems(i, [], prop) of (B::rBs, C) => (tpairs, rev rBs, B, C) | _ => raise THM("dest_state", i, [state])) handle TERM _ => raise THM("dest_state", i, [state]); (*Prepare orule for resolution by lifting it over the parameters and assumptions of goal.*) fun lift_rule goal orule = let val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal; val inc = gmax + 1; val lift_abs = Logic.lift_abs inc gprop; val lift_all = Logic.lift_all inc gprop; val Thm (der, {maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = orule; val (As, B) = Logic.strip_horn prop; in if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) else Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der, {cert = join_certificate1 (goal, orule), tags = [], maxidx = maxidx + inc, constraints = constraints, shyps = Sorts.union shyps sorts, (*sic!*) hyps = hyps, tpairs = map (apply2 lift_abs) tpairs, prop = Logic.list_implies (map lift_all As, lift_all B)}) end; fun incr_indexes i (thm as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else Thm (deriv_rule1 (Proofterm.incr_indexes i) der, {cert = cert, tags = [], maxidx = maxidx + i, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs, prop = Logic.incr_indexes ([], [], i) prop}); (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption opt_ctxt i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (context, cert') = make_context_certificate [state] opt_ctxt cert; val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env, tpairs) = let val normt = Envir.norm_term env; fun assumption_proof prf = Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf; in Thm (deriv_rule1 (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der, {tags = [], maxidx = Envir.maxidx_of env, constraints = insert_constraints_env (Context.certificate_theory cert') env constraints, shyps = Envir.insert_sorts env shyps, hyps = hyps, tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs, prop = if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*) else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*), cert = cert'}) end; val (close, asms, concl) = Logic.assum_problems (~1, Bi); val concl' = close concl; fun addprfs [] _ = Seq.empty | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull (Seq.mapp (newth n) (if Term.could_unify (asm, concl) then (Unify.unifiers (context, Envir.empty maxidx, (close asm, concl') :: tpairs)) else Seq.empty) (addprfs rest (n + 1)))) in addprfs asms 1 end; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*) fun eq_assumption i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val (_, asms, concl) = Logic.assum_problems (~1, Bi); in (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of ~1 => raise THM ("eq_assumption", 0, [state]) | n => Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = Logic.list_implies (Bs, C)})) end; (*For rotate_tac: fast rotation of assumptions of subgoal i*) fun rotate_rule k i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val params = Term.strip_all_vars Bi; val rest = Term.strip_all_body Bi; val asms = Logic.strip_imp_prems rest val concl = Logic.strip_imp_concl rest; val n = length asms; val m = if k < 0 then n + k else k; val Bi' = if 0 = m orelse m = n then Bi else if 0 < m andalso m < n then let val (ps, qs) = chop m asms in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end else raise THM ("rotate_rule", k, [state]); in Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = Logic.list_implies (Bs @ [Bi'], C)}) end; (*Rotates a rule's premises to the left by k, leaving the first j premises unchanged. Does nothing if k=0 or if k equals n-j, where n is the number of premises. Useful with eresolve_tac and underlies defer_tac*) fun permute_prems j k rl = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = rl; val prems = Logic.strip_imp_prems prop and concl = Logic.strip_imp_concl prop; val moved_prems = List.drop (prems, j) and fixed_prems = List.take (prems, j) handle General.Subscript => raise THM ("permute_prems: j", j, [rl]); val n_j = length moved_prems; val m = if k < 0 then n_j + k else k; val (prems', prop') = if 0 = m orelse m = n_j then (prems, prop) else if 0 < m andalso m < n_j then let val (ps, qs) = chop m moved_prems; val prems' = fixed_prems @ qs @ ps; in (prems', Logic.list_implies (prems', concl)) end else raise THM ("permute_prems: k", k, [rl]); in Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop'}) end; (* strip_apply f B A strips off all assumptions/parameters from A introduced by lifting over B, and applies f to remaining part of A*) fun strip_apply f = let fun strip (Const ("Pure.imp", _) $ _ $ B1) (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2) | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1)) ( Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2) | strip _ A = f A in strip end; fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1) (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2 | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1)) (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2 | strip_lifted _ A = A; (*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 = 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 []; (*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'; 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); 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; (*Function to rename bounds/unknowns in the argument, lifted over B*) fun rename_bvars dpairs = rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs; (*** RESOLUTION ***) (** Lifting optimizations **) (*strip off pairs of assumptions/parameters in parallel -- they are identical because of lifting*) fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1, Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2) | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1), Const("Pure.all",_)$Abs(_,_,t2)) = let val (B1,B2) = strip_assums2 (t1,t2) in (Abs(a,T,B1), Abs(a,T,B2)) end | strip_assums2 BB = BB; (*Faster normalization: skip assumptions that were lifted over*) fun norm_term_skip env 0 t = Envir.norm_term env t | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) = let val T' = Envir.norm_type (Envir.type_env env) T (*Must instantiate types of parameters because they are flattened; this could be a NEW parameter*) in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) = Logic.mk_implies (A, norm_term_skip env (n - 1) B) | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??"; (*unify types of schematic variables (non-lifted case)*) fun unify_var_types context (th1, th2) env = let fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types context (T, U)) Us | unify_vars _ = I; val add_vars = full_prop_of #> fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I); val vars = Vartab.empty |> add_vars th1 |> add_vars th2; in SOME (Vartab.fold (unify_vars o #2) vars env) end handle Pattern.Unif => NONE; (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) Unifies B with Bi, replacing subgoal i (1 <= i <= n) If match then forbid instantiations in proof state If lifted then shorten the dpair using strip_assums2. If eres_flg then simultaneously proves A1 by assumption. nsubgoal is the number of new subgoals (written m above). Curried so that resolution calls dest_state only once. *) 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 constraints' = union_constraints constraints1 constraints2 |> insert_constraints_env (Context.certificate_theory cert) env; fun bicompose_proof prf1 prf2 = Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) prf1 prf2 val th = Thm (deriv_rule2 (if Envir.is_empty env then bicompose_proof else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env else Proofterm.norm_proof' env oo bicompose_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 in (map (rename strip_apply) As0, deriv_rule1 (Proofterm.map_proof_terms (rename K) I) 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); (*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)); 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 = bicompose_aux opt_ctxt flags (state, dest_state (state,i), false) arg; (*Quick test whether rule is resolvable with the subgoal with hyps Hs and conclusion B. If eres_flg then checks 1st premise of rule also*) fun could_bires (Hs, B, eres_flg, rule) = let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs | could_reshyp [] = false; (*no premise -- illegal*) in Term.could_unify(concl_of rule, B) andalso (not eres_flg orelse could_reshyp (prems_of rule)) end; (*Bi-resolution of a state with a list of (flag,rule) pairs. Puts the rule above: rule/state. Renames vars in the rules. *) fun biresolution opt_ctxt match brules i state = let val (stpairs, Bs, Bi, C) = dest_state(state,i); val lift = lift_rule (cprem_of state i); val B = Logic.strip_assums_concl Bi; val Hs = Logic.strip_assums_hyp Bi; val compose = bicompose_aux opt_ctxt {flatten = true, match = match, incremented = true} (state, (stpairs, Bs, Bi, C), true); fun res [] = Seq.empty | res ((eres_flg, rule)::brules) = if Config.get_generic (make_context [state] opt_ctxt (cert_of state)) Pattern.unify_trace_failure orelse could_bires (Hs, B, eres_flg, rule) then Seq.make (*delay processing remainder till needed*) (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule), res brules)) else res brules in Seq.flat (res brules) end; (*Resolution: exactly one resolvent must be produced*) fun tha RSN (i, thb) = (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of ([th], _) => solve_constraints th | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb]) | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb])); (*Resolution: P \ Q, Q \ R gives P \ R*) fun tha RS thb = tha RSN (1,thb); (**** Type classes ****) fun standard_tvars thm = let val thy = theory_of_thm thm; val tvars = rev (Term.add_tvars (prop_of thm) []); val names = Name.invent Name.context Name.aT (length tvars); val tinst = map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names; in instantiate (tinst, []) thm end (* class relations *) val is_classrel = Symreltab.defined o get_classrels; fun complete_classrels thy = let fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) = let fun compl c1 c2 (finished2, thy2) = if is_classrel thy2 (c1, c2) then (finished2, thy2) else (false, thy2 |> (map_classrels o Symreltab.update) ((c1, c2), (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |> standard_tvars |> close_derivation \<^here> |> tap (expose_proof thy2) |> trim_context)); val proven = is_classrel thy1; val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; in fold_product compl preds succs (finished1, thy1) end; in (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of (true, _) => NONE | (_, thy') => SOME thy') end; (* type arities *) fun thynames_of_arity thy (a, c) = (get_arities thy, []) |-> Aritytab.fold (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)) |> sort (int_ord o apply2 #2) |> map #1; fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) = let val completions = Sign.super_classes thy c |> map_filter (fn c1 => if Aritytab.defined arities (t, Ss, c1) then NONE else let val th1 = (th RS the_classrel thy (c, c1)) |> standard_tvars |> close_derivation \<^here> |> tap (expose_proof thy) |> trim_context; in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); val finished' = finished andalso null completions; val arities' = fold Aritytab.update completions arities; in (finished', arities') end; fun complete_arities thy = let val arities = get_arities thy; val (finished, arities') = Aritytab.fold (insert_arity_completions thy) arities (true, get_arities thy); in if finished then NONE else SOME (map_arities (K arities') thy) end; val _ = Theory.setup (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities); (* primitive rules *) 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')) |> perhaps complete_classrels |> perhaps complete_arities end; 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', Context.theory_name thy, serial ())); in thy |> Sign.primitive_arity (t, Ss, [c]) |> map_arities (Aritytab.update ar #> curry (insert_arity_completions thy ar) true #> #2) end; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm;