proper code generation for discriminators/selectors

reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them

experiment

make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes

news

restrict admissibility to non-empty chains to allow more syntax-directed proof rules

merge

generate "code" theorems for incomplete definitions

updated keywords

added 'no_code' option

killed obsolete artifact

revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP

avoid user-level 'Specification.definition' for low-level definitions

repaired inconsistency introduced in transiting to 'Local_Theory.define'

docs for forgotten BNF theorems

tuning

added 'cong' attribute to 'map_cong'

avoid user-level 'Specification.definition' for internal constructions (to avoid e.g. automatic code generation behavior)

don't try to register code equations in a locale with assumptions

minor doc update

generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)

simpler code

more work towards "exhaustive"

Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>

set_comprehension_pointfree simproc causes to many surprises if enabled by default

tuned

updated docs

added Riss3g

reduce dependency (toward move to 'HOL')

cleaned up indirect dependency

tuned

prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate

prefer name-normalizing devarify over unvarifyT whenever appropriate

some documentation

command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it

remove junk

revert 4af7c82463d3 and document type class problem in Haskell

merged

no ord instance for String.literal in Haskell when list is also ordered lexicographically

implement comparisons on String.literal by target-language comparisons

instantiate linorder for String.literal by lexicographic order

setup lifting/transfer for String.literal

add predicate version of lexicographic order on lists

merge

prevent exception when equations for a function are missing; pave the way for "exhaustive"

Add Zorn to HOL-Library

made SML/NJ happier

NEWS

even more precise NEWS

mreged

Small simplifications to proofs

possibility to fold coercion inference error messages; tuned;

tweaks to the documentation

MaSH files should be ignored

eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports

adapt to 9733ab5c1df6

drop theorem duplicates

eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main

typos

tidied more proofs

cleaned up more messy proofs

merged

cleaned up some messy proofs

tuned

replaced bad example

polished some ancient proofs

merged

Simplified, tidied and generalised proofs esp of Binomial Theorem.

more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;

more accurate goal context;

tuned;

more accurate goal context; actually check assertions;

more official option;

clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;

exclude gzipped files from document model, to avoid confusion about actual file name and content;

more .hgignore;

tuned messages;

more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);

correctly account for dead variables when naming set functions

compile

rationalize imports

eliminated Sledgehammer's dependency on old-style datatypes

moved meson up the dependency chain

moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)

fixed apparent copy-paste bug

merged

actually expose errors of cumulative theory dependencies; more informative error messages;

proper concatenation of messages;

renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy

fixed spying so that the envirnoment variables are queried at run-time not at build-time

effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies

killed more needless thms

killed needless thm

mention docs

took out warning (BNF is still under development, but it is finished enough)

moved 'coinduction' proof method to 'HOL'

move registration of countable set type as BNF to its own theory file (+ renamed theory)

factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)

fixed LaTeX missing }

compile

support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)

tuning

NEWS;

merged

restrict node_required status and Theories panel to actual theories;

ranges of thy_load commands count as visible within perspective; convert ranges wrt. snapshot -- relevant for outdated situation;

tuned;

refer to thy_load command of auxiliary file;

proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;

load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;

tuned;

more explicit indication of missing files;

more uniform handling of inlined files;

tuned signature;

clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;

release file errors at runtime: Command.eval instead of Command.read;

maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;

always reparse nodes with thy_load commands, to update inlined files;

proper Thy_Load.append of auxiliary file names; inlined errors;

proper theory name vs. node name;

clarified boundary cases of Document.Node.Name;

clarified Thy_Load.node_name;

inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;

persistent value;

caching of blob; precise file content according to jEdit IO;

tuned;

maintain document model for all files, with document view for theory only, and special blob for non-theory files;

tuned

whitespace tuning

tuning

more refactoring to accommodate SMT proofs

tuning

tuning

more correct NEWS

simplified old code

refactoring

refactoring

merged

BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate

add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt

refactored

updated docs

use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'

prefix internal names as well

case_if -> case_eq_if + docs

use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package

eliminiated neg_numeral in favour of - (numeral _)

more tuning for speed

tuning

tuned proofs

killed more needless theorems

killed unused lemmas

optimized more bad apples

optimized 'bad apple' method calls

compile

no need for 3-way split with GFP for a handful of theorems

moved more theorems out of LFP

moved theorems out of LFP

moved theorems out of LFP

moved theorems out of LFP

moved theorems out of LFP

split 'Cardinal_Arithmetic' 3-way

started three-way split of 'HOL-Cardinals'

send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life

merged

show all involved subtyping constraints that cause coercion inference to fail

additional lemmas in BNF/Examples/Stream

reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798

comments by Sean Seefried

more robust example;

tuned proofs;

tuned;

tuned proofs;

explicit indication of thy_load commands;

centralized management of pending buffer edits;

merged

added functions all and exists to IArray

prefer explicit "document" flag -- eliminated stateful Present.no_document;

simplified HTML linefeed (again, see 041dc6d8d344);

simplified HTML theory presentation;

removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;

tuned;

merged

tuned proofs;

tuned signature;

tuned signature -- clarified Proof General legacy;

toplevel function "use" refers to raw ML bootstrap environment;

obsolete;

proper thy_load command 'boogie_file' -- avoid direct access to file-system;

tuned signature;

updated example;

prefer UTF8.decode_permissive;

more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;

more specific Protocol_Output: empty message.body, main content via bytes/text;

tuned imports;

tuned signature;

immutable byte vectors versus UTF8 strings;

dropped duplicate of of_bool

proper code equations for Gcd and Lcm on nat and int

tuned

fixed type variable confusion in 'datatype_new_compat'

implemented 'tptp_translate'

reintroduced (unimplemented) 'tptp_translate' tool

have MaSh support nameless facts (i.e. proofs) and use that support

made SML/NJ happy

renamed thm

explicit inclusion of data refinement theory into HOL-Library session

tuned to improve automation (for REPEAT)

separated comparision on bit operations into separate theory

prohibit locally fixed type variables in bnf definitions

tuned

standard relator for list bnf

tuned example

shortened generated property name

more explicit syntax for defining a bnf

fix document generation for HOL-Probability

fix document generation for Extended_Nat

measure of a countable union

add restrict_space measure

better support for enat and ereal conversions

enat is countable

add equalities for SUP and INF over constant functions

add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image

add acyclicI_order

stronger inc_induct and dec_induct

countability of the image of a reflexive transitive closure

support of_rat with 0 or 1 on order relations

equation when indicator function equals 0 or 1

ported part of function package to new 'Ctr_Sugar' abstraction

undid copy-paste

ported 'partial_function' to 'Ctr_Sugar' abstraction

port list comprehension simproc to 'Ctr_Sugar' abstraction

added convenience function

document idiomatic use of 'simps_of_case'

ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction

register old-style datatypes as 'Ctr_Sugar'

export useful ML function

moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

tuned headers

moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction