Session HOL-Proofs

Theories

• Tools.Code_Generator
  • File ‹cache_io.ML›
  • File ‹Code/code_preproc.ML›
  • File ‹Code/code_symbol.ML›
  • File ‹Code/code_thingol.ML›
  • File ‹Code/code_simp.ML›
  • File ‹Code/code_printer.ML›
  • File ‹Code/code_target.ML›
  • File ‹Code/code_namespace.ML›
  • File ‹Code/code_ml.ML›
  • File ‹Code/code_haskell.ML›
  • File ‹Code/code_scala.ML›
  • File ‹Code/code_runtime.ML›
  • File ‹nbe.ML›
• HOL.HOL
  • File ‹~~/src/Tools/misc_legacy.ML›
  • File ‹~~/src/Tools/try.ML›
  • File ‹~~/src/Tools/quickcheck.ML›
  • File ‹~~/src/Tools/solve_direct.ML›
  • File ‹~~/src/Tools/IsaPlanner/zipper.ML›
  • File ‹~~/src/Tools/IsaPlanner/isand.ML›
  • File ‹~~/src/Tools/IsaPlanner/rw_inst.ML›
  • File ‹~~/src/Provers/hypsubst.ML›
  • File ‹~~/src/Provers/splitter.ML›
  • File ‹~~/src/Provers/classical.ML›
  • File ‹~~/src/Provers/blast.ML›
  • File ‹~~/src/Provers/clasimp.ML›
  • File ‹~~/src/Tools/eqsubst.ML›
  • File ‹~~/src/Provers/quantifier1.ML›
  • File ‹~~/src/Tools/atomize_elim.ML›
  • File ‹~~/src/Tools/cong_tac.ML›
  • File ‹~~/src/Tools/intuitionistic.ML›
  • File ‹~~/src/Tools/project_rule.ML›
  • File ‹~~/src/Tools/subtyping.ML›
  • File ‹~~/src/Tools/case_product.ML›
  • File ‹Tools/hologic.ML›
  • File ‹Tools/rewrite_hol_proof.ML›
  • File ‹Tools/simpdata.ML›
  • File ‹~~/src/Tools/induct.ML›
  • File ‹~~/src/Tools/induction.ML›
  • File ‹~~/src/Tools/induct_tacs.ML›
  • File ‹~~/src/Tools/coherent.ML›
  • File ‹Tools/cnf.ML›
• HOL.Orderings
  • File ‹~~/src/Provers/order_procedure.ML›
  • File ‹~~/src/Provers/order_tac.ML›
• HOL.Groups
  • File ‹Tools/group_cancel.ML›
• HOL.Lattices
• HOL.Boolean_Algebras
  • File ‹Tools/boolean_algebra_cancel.ML›
• HOL.Set
• HOL.Typedef
  • File ‹Tools/typedef.ML›
• HOL.Fun
  • File ‹Tools/functor.ML›
• HOL.Complete_Lattices
• HOL.Ctr_Sugar
  • File ‹Tools/Ctr_Sugar/case_translation.ML›
  • File ‹Tools/Ctr_Sugar/ctr_sugar_util.ML›
  • File ‹Tools/Ctr_Sugar/ctr_sugar_tactics.ML›
  • File ‹Tools/Ctr_Sugar/ctr_sugar_code.ML›
  • File ‹Tools/Ctr_Sugar/ctr_sugar.ML›
  • File ‹Tools/coinduction.ML›
• HOL.Inductive
  • File ‹Tools/inductive.ML›
  • File ‹Tools/Old_Datatype/old_datatype_aux.ML›
  • File ‹Tools/Old_Datatype/old_datatype_prop.ML›
  • File ‹Tools/Old_Datatype/old_datatype_data.ML›
  • File ‹Tools/Old_Datatype/old_rep_datatype.ML›
  • File ‹Tools/Old_Datatype/old_datatype_codegen.ML›
  • File ‹Tools/BNF/bnf_fp_rec_sugar_util.ML›
  • File ‹Tools/Old_Datatype/old_primrec.ML›
  • File ‹Tools/BNF/bnf_lfp_rec_sugar.ML›
• HOL.Product_Type
  • File ‹Tools/split_rule.ML›
  • File ‹Tools/set_comprehension_pointfree.ML›
  • File ‹Tools/inductive_set.ML›
• HOL.Sum_Type
• HOL.Rings
  • File ‹Tools/arith_data.ML›
  • File ‹~~/src/Provers/Arith/cancel_div_mod.ML›
• HOL.Nat
  • File ‹Tools/nat_arith.ML›
• HOL.Fields
  • File ‹~~/src/Provers/Arith/fast_lin_arith.ML›
  • File ‹Tools/lin_arith.ML›
• HOL.Relation
• HOL.Finite_Set
• HOL.Transitive_Closure
  • File ‹~~/src/Provers/trancl.ML›
• HOL.Wellfounded
• HOL.Wfrec
• HOL.Order_Relation
• HOL.Hilbert_Choice
  • File ‹Tools/choice_specification.ML›
• HOL.Zorn
• HOL.BNF_Wellorder_Relation
• HOL.BNF_Wellorder_Embedding
• HOL.BNF_Wellorder_Constructions
• HOL.BNF_Cardinal_Order_Relation
• HOL.BNF_Cardinal_Arithmetic
• HOL.Fun_Def_Base
  • File ‹Tools/Function/function_lib.ML›
  • File ‹Tools/Function/function_common.ML›
  • File ‹Tools/Function/function_context_tree.ML›
  • File ‹Tools/Function/sum_tree.ML›
• HOL.BNF_Def
  • File ‹Tools/BNF/bnf_util.ML›
  • File ‹Tools/BNF/bnf_tactics.ML›
  • File ‹Tools/BNF/bnf_def_tactics.ML›
  • File ‹Tools/BNF/bnf_def.ML›
• HOL.BNF_Composition
  • File ‹Tools/BNF/bnf_comp_tactics.ML›
  • File ‹Tools/BNF/bnf_comp.ML›
• HOL.Basic_BNFs
• HOL.BNF_Fixpoint_Base
  • File ‹Tools/BNF/bnf_fp_util_tactics.ML›
  • File ‹Tools/BNF/bnf_fp_util.ML›
  • File ‹Tools/BNF/bnf_fp_def_sugar_tactics.ML›
  • File ‹Tools/BNF/bnf_fp_def_sugar.ML›
  • File ‹Tools/BNF/bnf_fp_n2m_tactics.ML›
  • File ‹Tools/BNF/bnf_fp_n2m.ML›
  • File ‹Tools/BNF/bnf_fp_n2m_sugar.ML›
• HOL.BNF_Least_Fixpoint
  • File ‹Tools/BNF/bnf_lfp_util.ML›
  • File ‹Tools/BNF/bnf_lfp_tactics.ML›
  • File ‹Tools/BNF/bnf_lfp.ML›
  • File ‹Tools/BNF/bnf_lfp_compat.ML›
  • File ‹Tools/BNF/bnf_lfp_rec_sugar_more.ML›
  • File ‹Tools/BNF/bnf_lfp_size.ML›
  • File ‹Tools/datatype_simprocs.ML›
• HOL.Equiv_Relations
• HOL.Basic_BNF_LFPs
  • File ‹Tools/BNF/bnf_lfp_basic_sugar.ML›
• HOL.Meson
  • File ‹Tools/Meson/meson.ML›
  • File ‹Tools/Meson/meson_clausify.ML›
  • File ‹Tools/Meson/meson_tactic.ML›
• HOL.ATP
  • File ‹Tools/ATP/atp_util.ML›
  • File ‹Tools/ATP/atp_problem.ML›
  • File ‹Tools/ATP/atp_proof.ML›
  • File ‹Tools/ATP/atp_proof_redirect.ML›
  • File ‹Tools/lambda_lifting.ML›
  • File ‹Tools/monomorph.ML›
  • File ‹Tools/ATP/atp_problem_generate.ML›
  • File ‹Tools/ATP/atp_proof_reconstruct.ML›
• HOL.Metis
  • File ‹~~/src/Tools/Metis/metis.ML›
  • File ‹Tools/Metis/metis_generate.ML›
  • File ‹Tools/Metis/metis_reconstruct.ML›
  • File ‹Tools/Metis/metis_tactic.ML›
• HOL.Transfer
  • File ‹Tools/Transfer/transfer.ML›
  • File ‹Tools/Transfer/transfer_bnf.ML›
  • File ‹Tools/BNF/bnf_fp_rec_sugar_transfer.ML›
• HOL.Lifting
  • File ‹Tools/Lifting/lifting_util.ML›
  • File ‹Tools/Lifting/lifting_info.ML›
  • File ‹Tools/Lifting/lifting_bnf.ML›
  • File ‹Tools/Lifting/lifting_term.ML›
  • File ‹Tools/Lifting/lifting_def.ML›
  • File ‹Tools/Lifting/lifting_setup.ML›
  • File ‹Tools/Lifting/lifting_def_code_dt.ML›
• HOL.Quotient
  • File ‹Tools/Quotient/quotient_info.ML›
  • File ‹Tools/Quotient/quotient_term.ML›
  • File ‹Tools/Quotient/quotient_type.ML›
  • File ‹Tools/Quotient/quotient_def.ML›
  • File ‹Tools/Quotient/quotient_tacs.ML›
  • File ‹Tools/BNF/bnf_lift.ML›
• HOL.Num
  • File ‹Tools/numeral.ML›
• HOL.Power
• HOL.Groups_Big
• HOL.Complete_Partial_Order
• HOL.Option
• HOL.Partial_Function
  • File ‹Tools/Function/partial_function.ML›
• HOL.Argo
  • File ‹~~/src/Tools/Argo/argo_expr.ML›
  • File ‹~~/src/Tools/Argo/argo_term.ML›
  • File ‹~~/src/Tools/Argo/argo_lit.ML›
  • File ‹~~/src/Tools/Argo/argo_proof.ML›
  • File ‹~~/src/Tools/Argo/argo_rewr.ML›
  • File ‹~~/src/Tools/Argo/argo_cls.ML›
  • File ‹~~/src/Tools/Argo/argo_common.ML›
  • File ‹~~/src/Tools/Argo/argo_cc.ML›
  • File ‹~~/src/Tools/Argo/argo_simplex.ML›
  • File ‹~~/src/Tools/Argo/argo_thy.ML›
  • File ‹~~/src/Tools/Argo/argo_heap.ML›
  • File ‹~~/src/Tools/Argo/argo_cdcl.ML›
  • File ‹~~/src/Tools/Argo/argo_core.ML›
  • File ‹~~/src/Tools/Argo/argo_clausify.ML›
  • File ‹~~/src/Tools/Argo/argo_solver.ML›
  • File ‹Tools/Argo/argo_tactic.ML›
• HOL.SAT
  • File ‹Tools/prop_logic.ML›
  • File ‹Tools/sat_solver.ML›
  • File ‹Tools/sat.ML›
  • File ‹Tools/Argo/argo_sat_solver.ML›
• HOL.Fun_Def
  • File ‹Tools/Function/function_core.ML›
  • File ‹Tools/Function/mutual.ML›
  • File ‹Tools/Function/pattern_split.ML›
  • File ‹Tools/Function/relation.ML›
  • File ‹Tools/Function/function_elims.ML›
  • File ‹Tools/Function/function.ML›
  • File ‹Tools/Function/pat_completeness.ML›
  • File ‹Tools/Function/fun.ML›
  • File ‹Tools/Function/induction_schema.ML›
  • File ‹Tools/Function/measure_functions.ML›
  • File ‹Tools/Function/lexicographic_order.ML›
  • File ‹Tools/Function/termination.ML›
  • File ‹Tools/Function/scnp_solve.ML›
  • File ‹Tools/Function/scnp_reconstruct.ML›
  • File ‹Tools/Function/fun_cases.ML›
• HOL.Int
  • File ‹Tools/int_arith.ML›
• HOL.Lattices_Big
• HOL.Euclidean_Rings
• HOL.Parity
• HOL.Numeral_Simprocs
  • File ‹~~/src/Provers/Arith/assoc_fold.ML›
  • File ‹~~/src/Provers/Arith/cancel_numerals.ML›
  • File ‹~~/src/Provers/Arith/combine_numerals.ML›
  • File ‹~~/src/Provers/Arith/cancel_numeral_factor.ML›
  • File ‹~~/src/Provers/Arith/extract_common_term.ML›
  • File ‹Tools/numeral_simprocs.ML›
  • File ‹Tools/nat_numeral_simprocs.ML›
• HOL.Semiring_Normalization
  • File ‹Tools/semiring_normalizer.ML›
• HOL.Groebner_Basis
  • File ‹Tools/groebner.ML›
• HOL.Set_Interval
• HOL.Presburger
  • File ‹Tools/Qelim/qelim.ML›
  • File ‹Tools/Qelim/cooper_procedure.ML›
  • File ‹Tools/Qelim/cooper.ML›
  • File ‹Tools/try0.ML›
• HOL.SMT
  • File ‹Tools/SMT/smt_util.ML›
  • File ‹Tools/SMT/smt_failure.ML›
  • File ‹Tools/SMT/smt_config.ML›
  • File ‹Tools/SMT/smt_builtin.ML›
  • File ‹Tools/SMT/smt_datatypes.ML›
  • File ‹Tools/SMT/smt_normalize.ML›
  • File ‹Tools/SMT/smt_translate.ML›
  • File ‹Tools/SMT/smtlib.ML›
  • File ‹Tools/SMT/smtlib_interface.ML›
  • File ‹Tools/SMT/smtlib_proof.ML›
  • File ‹Tools/SMT/smtlib_isar.ML›
  • File ‹Tools/SMT/z3_proof.ML›
  • File ‹Tools/SMT/z3_isar.ML›
  • File ‹Tools/SMT/smt_solver.ML›
  • File ‹Tools/SMT/cvc_interface.ML›
  • File ‹Tools/SMT/lethe_proof.ML›
  • File ‹Tools/SMT/lethe_isar.ML›
  • File ‹Tools/SMT/lethe_proof_parse.ML›
  • File ‹Tools/SMT/cvc_proof_parse.ML›
  • File ‹Tools/SMT/conj_disj_perm.ML›
  • File ‹Tools/SMT/smt_replay_methods.ML›
  • File ‹Tools/SMT/smt_replay.ML›
  • File ‹Tools/SMT/smt_replay_arith.ML›
  • File ‹Tools/SMT/z3_interface.ML›
  • File ‹Tools/SMT/z3_replay_rules.ML›
  • File ‹Tools/SMT/z3_replay_methods.ML›
  • File ‹Tools/SMT/z3_replay.ML›
  • File ‹Tools/SMT/lethe_replay_methods.ML›
  • File ‹Tools/SMT/cvc5_replay_methods.ML›
  • File ‹Tools/SMT/verit_replay_methods.ML›
  • File ‹Tools/SMT/verit_strategies.ML›
  • File ‹Tools/SMT/verit_replay.ML›
  • File ‹Tools/SMT/cvc5_replay.ML›
  • File ‹Tools/SMT/smt_systems.ML›
• HOL.Sledgehammer
  • File ‹Tools/ATP/system_on_tptp.ML›
  • File ‹Tools/Sledgehammer/async_manager_legacy.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_util.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_fact.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_proof_methods.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_isar_annotate.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_isar_proof.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_isar_preplay.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_isar_compress.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_isar_minimize.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_isar.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_atp_systems.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_prover.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_prover_atp.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_prover_smt.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_prover_minimize.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_mepo.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_mash.ML›
  • File ‹Tools/Sledgehammer/sledgehammer.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_commands.ML›
  • File ‹Tools/Sledgehammer/sledgehammer_tactics.ML›
• HOL.Lifting_Set
• HOL.List
• HOL.Groups_List
• HOL.Bit_Operations
• HOL.Code_Numeral
• HOL.Random
• HOL.Map
• HOL.Enum
• HOL.String
  • File ‹Tools/string_syntax.ML›
  • File ‹Tools/literal.ML›
• HOL.Typerep
• HOL.Predicate
• HOL.Lazy_Sequence
• HOL.Limited_Sequence
• HOL.Code_Evaluation
  • File ‹Tools/code_evaluation.ML›
  • File ‹Tools/value_command.ML›
  • File ‹Tools/reification.ML›
• HOL.Quickcheck_Random
  • File ‹Tools/Quickcheck/quickcheck_common.ML›
  • File ‹Tools/Quickcheck/random_generators.ML›
• HOL.Random_Pred
• HOL.Random_Sequence
• HOL.Quickcheck_Exhaustive
  • File ‹Tools/Quickcheck/exhaustive_generators.ML›
  • File ‹Tools/Quickcheck/abstract_generators.ML›
• HOL.Predicate_Compile
  • File ‹Tools/Predicate_Compile/predicate_compile_aux.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile_compilations.ML›
  • File ‹Tools/Predicate_Compile/core_data.ML›
  • File ‹Tools/Predicate_Compile/mode_inference.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile_proof.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile_core.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile_data.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile_fun.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile_pred.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile_specialisation.ML›
  • File ‹Tools/Predicate_Compile/predicate_compile.ML›
• HOL.Quickcheck_Narrowing
  • File ‹Tools/Quickcheck/Narrowing_Engine.hs›
  • File ‹Tools/Quickcheck/PNF_Narrowing_Engine.hs›
  • File ‹Tools/Quickcheck/narrowing_generators.ML›
  • File ‹Tools/Quickcheck/find_unused_assms.ML›
• HOL.Mirabelle
  • File ‹Tools/Mirabelle/mirabelle_util.ML›
  • File ‹Tools/Mirabelle/mirabelle.ML›
  • File ‹Tools/Mirabelle/mirabelle_arith.ML›
  • File ‹Tools/Mirabelle/mirabelle_order.ML›
  • File ‹Tools/Mirabelle/mirabelle_metis.ML›
  • File ‹Tools/Mirabelle/mirabelle_presburger.ML›
  • File ‹Tools/Mirabelle/mirabelle_quickcheck.ML›
  • File ‹Tools/Mirabelle/mirabelle_sledgehammer_filter.ML›
  • File ‹Tools/Mirabelle/mirabelle_sledgehammer.ML›
  • File ‹Tools/Mirabelle/mirabelle_try0.ML›
• HOL.Extraction
• HOL.Record
  • File ‹Tools/record.ML›
• HOL.GCD
• HOL.Nitpick
  • File ‹Tools/Nitpick/kodkod.ML›
  • File ‹Tools/Nitpick/kodkod_sat.ML›
  • File ‹Tools/Nitpick/nitpick_util.ML›
  • File ‹Tools/Nitpick/nitpick_hol.ML›
  • File ‹Tools/Nitpick/nitpick_mono.ML›
  • File ‹Tools/Nitpick/nitpick_preproc.ML›
  • File ‹Tools/Nitpick/nitpick_scope.ML›
  • File ‹Tools/Nitpick/nitpick_peephole.ML›
  • File ‹Tools/Nitpick/nitpick_rep.ML›
  • File ‹Tools/Nitpick/nitpick_nut.ML›
  • File ‹Tools/Nitpick/nitpick_kodkod.ML›
  • File ‹Tools/Nitpick/nitpick_model.ML›
  • File ‹Tools/Nitpick/nitpick.ML›
  • File ‹Tools/Nitpick/nitpick_commands.ML›
  • File ‹Tools/Nitpick/nitpick_tests.ML›
• HOL.Nunchaku
  • File ‹Tools/Nunchaku/nunchaku_util.ML›
  • File ‹Tools/Nunchaku/nunchaku_collect.ML›
  • File ‹Tools/Nunchaku/nunchaku_problem.ML›
  • File ‹Tools/Nunchaku/nunchaku_translate.ML›
  • File ‹Tools/Nunchaku/nunchaku_model.ML›
  • File ‹Tools/Nunchaku/nunchaku_reconstruct.ML›
  • File ‹Tools/Nunchaku/nunchaku_display.ML›
  • File ‹Tools/Nunchaku/nunchaku_tool.ML›
  • File ‹Tools/Nunchaku/nunchaku.ML›
  • File ‹Tools/Nunchaku/nunchaku_commands.ML›
• HOL.BNF_Greatest_Fixpoint
  • File ‹Tools/BNF/bnf_gfp_util.ML›
  • File ‹Tools/BNF/bnf_gfp_tactics.ML›
  • File ‹Tools/BNF/bnf_gfp.ML›
  • File ‹Tools/BNF/bnf_gfp_rec_sugar_tactics.ML›
  • File ‹Tools/BNF/bnf_gfp_rec_sugar.ML›
• HOL.Filter
• HOL.Conditionally_Complete_Lattices
• HOL.Factorial
• HOL.Binomial
• HOL.Divides
• Main
• HOL-Library.Realizers
  • File ‹~~/src/HOL/Tools/datatype_realizer.ML›
  • File ‹~~/src/HOL/Tools/inductive_realizer.ML›