lemmas about addition, SUP on countable sets and infinite sums for extreal

add infinite sums and power on extreal

introduce setsum on extreal

use abs_extreal

simplified definition of open_extreal

use case_product for extrel[2,3]_cases

add Extended_Reals from AFP/Lower_Semicontinuous

add lemmas for monotone sequences

add lemmas for SUP and INF

generalize infinite sums

moved t2_spaces to HOL image

example settings for ISABELLE_GHC, ISABELLE_OCAML, ISABELLE_SWIPL;

isatest: fresh copy of settings avoids odd cumulative environment;

tuned exhaustive_generators

removing definition of cons0; hiding constants in Quickcheck_Narrowing

tuned subsubsection names in Quickcheck_Narrowing

tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)

correcting names in Narrowing_Engine and example theory for Quickcheck_Narrowing

renaming series and serial to narrowing in Quickcheck_Narrowing

eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;

tuned headers;

eliminated hard tabs;

less ambitious isatest;

modernized imports (untested!?);

files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;

explicit type SHA1.digest;

slightly more robust bash exec, which fails on empty executable;

cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; determine swipl_version at runtime;

some cleanup of old-style settings;

clarified ISABELLE_CSDP setting (formerly CSDP_EXE);

more conventional Mutabelle settings -- similar to Mirabelle;

more basic use of Path.position/File.read;

prefer qualified ISABELLE_NEOS_SERVER;

proper File.shell_path;

more conventional variable name;

Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;

fixed document;

isatest: test more external code;

tuned headers;

allow spaces in executable names; simplified generated bash scripts;

tuned;

tuned headers;

adapting example file to renaming of the quickcheck tester

renaming tester from lazy_exhaustive to narrowing

minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common

renaming example file correctly

adapting Main file generation for Quickcheck_Narrowing

adapting Quickcheck_Narrowing and example file to new names

renaming LSC_Examples theory to Quickcheck_Narrowing

renaming lazysmallcheck ML file to Quickcheck_Narrowing

renaming LSC to Quickcheck_Narrowing

adaptions in generators using the common functions

adding file quickcheck_common to carry common functions of all quickcheck generators

adapting record package to renaming of quickcheck's structures

moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better

correcting dependencies in IsaMakefile

renaming signatures and structures; correcting header

adapting Quickcheck theory after moving ML files

moving quickcheck_generators.ML to Quickcheck directory and renaming it random_generators.ML

moving exhaustive_generators.ML to Quickcheck directory

correcting dependencies after renaming

replacing naming of small by exhaustive

renaming smallvalue_generators.ML to exhaustive_generators.ML

renaming constants in Quickcheck_Exhaustive theory

renaming Smallcheck to Quickcheck_Exhaustive

only testing theory LSC_Examples when GHC is installed on the machine

increasing timeout of example for counterexample generation

adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC

adding lazysmallcheck example theory to HOL-ex session

adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies

replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype

changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent

adding an example theory for Lazysmallcheck prototype

adding Lazysmallcheck prototype to HOL-Library

adding files for prototype of lazysmallcheck

removing debug message in quickcheck's postprocessor

fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample

renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck

improving term postprocessing for counterexample presentation in quickcheck

tuned

finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)

improved formula for specialization, to prevent needless specializations -- and removed dead code

perform no arity check in debug mode so that we get to see the Kodkod problem

spark_end now joins proofs of VCs before writing *.prv file.

clarified

produce helpful mira summary for more errors

eliminated prems;

eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;

tuned proofs -- eliminated prems;

merged

merged

don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on

simplified Thy_Info.check_file -- discontinued load path;

discontinued legacy load path;

re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;

modernized imports;

observe standard header format;

removed spurious 'unused_thms' (cf. 1a65b780bd56);

isatest cygwin-poly-e: new memory management of polyml-svn could be more stable;

merged

merged

- Made sure that sort_defs is aware of constants introduced by add_type_def - add_def now compares Isabelle types rather than SPARK types to ensure that type abbreviations are taken into account

mention new Nitpick options

simplify "need" option's syntax

renamed "preconstr" option "need"

finally remove upper_bound_finite_set

separate settings for afp test

added missing spaces in output

lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on

unfold definitions in "preconstrs" option

robust handling of types occurring in "eval" and "preconstr" options but not in the goal

make "preconstr" option more robust -- shouldn't throw exceptions

merged

merged

declare ext [intro]: Extensionality now available by default

merged

removed dependency on Dense_Linear_Order

adding function Quickcheck.test_terms to provide checking a batch of terms

adding a function to compile a batch of terms for quickcheck with one code generation invocation

improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)

made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"

if "total_consts" is set, report cex's as quasi-genuine

document new "total_consts" option

added "total_consts" option

added a few lemmas by Andreas Lochbihler

Corrected HOLCF/FOCUS dependency

Added material by David Trachtenherz

corrected HOLCF dependency on Nat_Infinity

got rid of lemma upper_bound_finite_set

merged

Some cleaning up

updated generated files

fixed manual (rule no longer exists)

removed support for tail-recursion from function package (now implemented by partial_function)

reactivate time measurement (partly reverting c27b0b37041a); export pretty_theorem, to display both internal or external facts

generalize find_theorems filters to work on raw propositions, too

merged

added simp lemma nth_Cons_pos to List

Refactor find_theorems to provide a more general filter_facts method

removed dead code/unused exports/speculative generality

recdef -> fun(ction)

removed unused lemma

recdef -> fun(ction); tuned

eliminated clones of List.upto

fix non-exhaustive pattern match in find_theorems

merged

add lemma KL_divergence_vimage, mutual_information_generic

add lemma RN_deriv_vimage

use measure_preserving in ..._vimage lemmas

log is borel measurable

add name continuous_isCont to unnamed lemma

add example for case_product usage

setup case_product attribute in HOL and FOL

introduce attribute case_prod for combining case rules * * * [PATCH 1/9] Make tac independent of consumes From 1a53ef4c070f924ff8e69529b0c1b13fa2844722 Mon Sep 17 00:00:00 2001 --- case_product.ML | 11 ++++++----- 1 files changed, 6 insertions(+), 5 deletions(-) * * * [PATCH 2/9] Replace MRS by OF From da55d08ae287bfdc18dec554067b45a3e298c243 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) * * * [PATCH 3/9] Clean up tactic From d26d50caaa3526c8c0625d7395467c6914f1a8d9 Mon Sep 17 00:00:00 2001 --- case_product.ML | 13 +++++-------- 1 files changed, 5 insertions(+), 8 deletions(-) * * * [PATCH 4/9] Move out get_consumes a bit more From 6ed5415f29cc43cea30c216edb1e74ec6c0f6c33 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 +++- 1 files changed, 3 insertions(+), 1 deletions(-) * * * [PATCH 5/9] Clean up tactic From d301cfe6377e9f7db74b190fb085e0e66eeadfb5 Mon Sep 17 00:00:00 2001 --- case_product.ML | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) * * * [PATCH 6/9] Cleanup build_concl_prems From c30889e131e74a92caac5b1e6d3d816890406ca7 Mon Sep 17 00:00:00 2001 --- case_product.ML | 18 ++++++++---------- 1 files changed, 8 insertions(+), 10 deletions(-) * * * [PATCH 7/9] Split logic & annotation a bit From e065606118308c96e013fad72ab9ad89b5a4b945 Mon Sep 17 00:00:00 2001 --- case_product.ML | 26 ++++++++++++++++++-------- 1 files changed, 18 insertions(+), 8 deletions(-) * * * [PATCH 8/9] Remove dependency on consumes attribute From e2a4de044481586d6127bbabd0ef48d0e3ab57c0 Mon Sep 17 00:00:00 2001 --- case_product.ML | 46 ++++++++++++++++++++++------------------------ 1 files changed, 22 insertions(+), 24 deletions(-) * * * [PATCH 9/9] whitespace From 59f5036bd8f825da4a362970292a34ec06c0f1a2 Mon Sep 17 00:00:00 2001 --- case_product.ML | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-)

merged

remove confusing message

eliminated remdps in favor of List.remdups

recdef -> fun

recdef -> fun

updated generated file;

scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;

modernized specifications;

dropped obsolete FIXMEs

merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;

eliminated global prems

modernized specification; curried

recdef -> fun; curried

recdef -> fun; curried

strengthened polymul.induct

dropped stupid name

removed duplicate declarations

recdef -> function

tuned proofs -- eliminated prems;

merged

adjust example

document new "preconstr" option

more work on "fix_datatype_vals" optimization (renamed "preconstruct")

more work on "fix_datatype_vals"

first steps in implementing "fix_datatype_vals" optimization

better fudge factors for CVC3 and Yices based on Judgment Day

exit code 127 can mean many things -- not just (and probably not) Perl missing

modernized specifications;

rename Nitpick's (internal) auxiliary lemmas

updated docs w.r.t. "nitpick_unfold" attribute

improve optimization

updated docs

tweaked Nitpick based on C++ memory model example

renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics

always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"

give more weight to Frees than to Consts in relevance filter

don't distinguish between "fixes" and other free variables -- this confuses users

added a timeout around SMT preprocessing (notably monomorphization)

comments to find fudge factors easily

added test cases with quantifier occurring in first-order term positions

wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions

dropped redundancy

merged

added is_IAbs; tuned brackets and comments

more idiomatic printing of let cascades and type variable constraints

merged

modernized specifications;

modernized specifications;

more precise headers;

less verbose tracing;

standardized headers;

modernized specifications;

gracious timeout in "blocking" mode

make Nitpick's timeout mechanism somewhat more reliable/friendly; avoid producing warnings when invoked in "auto" mode

better fudge factors for Sledgehammer

adjust fudge factors

extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs

export more functionality of Sledgehammer to applications (for experiments)

export useful function (needed in a Sledgehammer-related experiment)

make experimental "Z3 ATP" work on Linux as well

adjusted fudge factors (based on Judgment Day runs)

generalized termination lemmas

strengthened induction rule; clarified some proofs

limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops); updated SMT certificate

more explicit errors to inform users about problems related to SMT solvers; fall back to remote SMT solver (if local version does not exist); extend the Z3 proof parser to accommodate for slight changes introduced by Z3 2.18

more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;

eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;

tuned;

more pretty set comprehension sugar

merged

adjusting HOL-Mutabelle to changes in quickcheck

quickcheck can be invoked with its internal timelimit or without

quickcheck invokes TimeLimit.timeLimit only in one separate function

added option to Mirabelle Sledgehammer

merged

reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space

tuning

fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)

fix path to etc/settings and etc/components in doc

run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user

remove pointless clutter

make minimizer verbose

tuning

automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)

renamed field

added "Z3 as an ATP" support to Sledgehammer locally