mapper for mapping type

mapper for fset type

mapper for dlist type

map_fun combinator in theory Fun

some updates after 2 years of Mercurial usage;

mention Sledgehammer with SMT

enabled SMT solver in Sledgehammer by default

merged

keep variables bound

remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem

merged

infer variances of user-given mapper operation; proper thm storing

code eqn for slice was missing; redefined splice with fun

move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain

merged

typedef (open) unit

add bind_bind rules for powerdomains

merged

emerging Isar command interface

fixed typo

updated keywords

ML signature interface

stub for Isar command interface

module for functorial mappers

merged

require the b2i file ending in the boogie_open command (for consistency with the theory header)

use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)

keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)

add lemmas about powerdomains

declare {upper,lower,convex}_pd_induct as default induction rules

rename 'repdef' to 'domaindef'

refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;

less parentheses, cf. Session.welcome;

avoid spam;

more robust determination of java executable;

init_component: require absolute path (when invoked by user scripts);

more explicit explanation of init_component shell function;

paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;

tuned message;

post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);

more reasonably defaults for typical laptops (2 GB RAM, 2 cores); enforce -server JVM if possible (NB: default JRE on Windows lacks that);

added forall2 predicate lifter

merged

merged

renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed

honour timeouts which are not rounded to full seconds

better error message

better error message

merged

cosmetics

interpret SMT_Failure.Solver_Crashed correctly

turn on Sledgehammer verbosity so we can track down crashes

pick up SMT solver crashes and report them to the user/Mirabelle if desired

merged

only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers

trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)

merged

ignoring the constant STR in the predicate compiler

non-executable source files;

eliminated old-style sed in favour of builtin regex matching;

more robust treatment of spaces in file names;

tuned error messages;

merged

re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)

re-generalized type of prod_rel (accident from 2989f9f3aa10)

formal dependency on b2i files

merged

check the return code of the SMT solver and raise an exception if the prover failed

updated README;

tuned;

cover 'write' as primitive proof command;

clarified interact/print state: proof commands are treated as in TTY mode to get full response;

somewhat adhoc replacement for 'thus' and 'hence'; complete words as short as 2 characters, e.g. "Un";

always print state of proof commands (notably "qed" etc.);

simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;

tuned message;

proper escape in regex;

report malformed symbols;

qualified Symbol_Pos.symbol;

total Symbol.source;

eliminated slightly odd pervasive Symbol_Pos.symbol;

treat Unicode "replacement character" (i.e. decoding error) is malformed;

simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);

tuned;

back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;

await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;

updated README;

defensive defaults for more robust experience for new users;

merged

preliminary support for newer versions of Z3

turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user

let the theory formally depend on the Boogie output

look for certificates relative to the theory

dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT

merged

update Theory.requires with new theory name

tuned signatures;

never open Unsynchronized;

merged

section headings

reorder chapters for generated document

merge Representable.thy into Domain.thy

move stuff from Domain.thy to Domain_Aux.thy

move map functions to new theory file Map_Functions; add theory file Plain_HOLCF

allow unpointed lazy arguments for definitional domain package

add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas

merged

removed unused lemma chain_mono2

rename class 'bifinite' to 'domain'

instance sum :: (predomain, predomain) predomain

configure sum type for fixrec

add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)

instance prod :: (predomain, predomain) predomain

adapt isodefl proof script to unpointed types

add 'predomain' class: unpointed version of bifinite

add bifiniteness check for domain_isomorphism command

implement map_of_typ using Pattern.rewrite_term

avoid using stale theory

implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data

add function the_sort