moved Mirabelle to HOL/Tools

moved Mirabelle to HOL/Tools

Mirabelle tool script conforming to standard Isabelle tool interface, tidied Perl script, moved ML sources to Tools subdirectory

made Mirabelle a component

A few Isar scripts

additional checkpoints avoid problems in error situations

tuned

removed atp_minimize invocation

reverted accidential corruption of superscripts introduced in a508148f7c25

merged

inserted space into message

formally stylized

formally stylized

corrected Pair to Char

merged

Fixed a bug where the simplifier would hang on lemma "f a = M { nat j |j. 0 <= j & j < f b}" pre_decomp/pre_tac no longer split terms that contain (non-locally) bound variables (e.g., "nat j" in the above example).

merged

Removal of redundant settings of unification trace and search bounds.

Demonstrations of sledgehammer in protocol proofs.

added PARALLEL_CHOICE, PARALLEL_GOALS;

merged

SOS: function to set default prover; output channel changed

interrupt handler for neos csdp client

clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;

updated generated document

dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML

proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML

merged

temporary adjustment to dubious state of eta expansion in recfun_codegen

properly merged

same_typscheme replaces ugly common_typ_eqns

moved all technical processing of code equations to code_thingol.ML

added map_transpose

merged

attempt to move desymbolization to translation

added a somehow clueless comment

repair mess produced by resolution afterwards

using certify_instantiate

merged

cleaned up variable desymbolification and argument expansion

more appropriate printing of function terms

improved handling of parameters

path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples

towards proper handling of argument order in comprehensions

cleaned up

termT and term_of_const

added bij lemmas

new lemma bij_comp

refined mac-poly64 tests;

tuned spacing of sections; reduced line length;

more platforms;

tuned header; visible text instead of source comments;

misc changes to SOS by Philipp Meyer: CSDP_EXE as central setting; separate component src/HOL/Library/Sum_Of_Squares; misc tuning and rearrangement of neos_csdp_client; more robust treatment of shell paths; debugging depends on local flag; removed unused parts;

settings for ATP_Manager component;

merged

SUBPROOF: recovered Goal.check_finished; tuned;

added Isabelle_System.components;

src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;

etc/components; isabelle makeall operates on all components with IsaMakefile;

turned object-logics into components; isabelle makeall: operate on all components with IsaMakefile, not just hardwired "logics";

spelling;

tuned "Bootstrapping the environment"; added "Additional components";

change IFS only locally -- thanks to bash arrays;

more uniform handling of ISABELLE_HOME_USER component; discontinued ISABELLE_IGNORE_USER_SETTINGS (ever used? cf. c567f9fd61a2);

options for more precise performance figures of at-poly, which happens to run on macbroy21;

removing tracing messages in predicate compiler

improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging

commented rpred compilation; tuned

added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning

tuned proof procedure; added size-limiting predicate compilation of higher order predicates; added guessing of number parameters for registrating predicates; removed debug messages

changed resolving depending predicates and fetching in the predicate compiler

refactoring predicate compiler; repaired proof procedure to handle all test cases

refactoring predicate compiler; added type synonyms and functions split_smode and split_mode

adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates

extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures

imported patch changed mode inference of predicate compiler to return infered dataflow

imported patch generic compilation of predicate compiler with different monads

exported functions for quickcheck generator; renamed type constructing functions to fit with the type name in the Predicate theory

removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis

basic support for components (which imitate the usual Isabelle directory layout);

Tuned.

the derived induction principles can be given an explicit name

updated Variable.import;

merged

merged

modernized generated example session;

added Mirabelle

Quickcheck callable from ML

future scheduler: uninterruptible cancelation;

renamed Multithreading.regular_interrupts to Multithreading.public_interrupts; renamed Multithreading.restricted_interrupts to Multithreading.private_interrupts; added Multithreading.sync_interrupts; Multithreading.sync_wait: more careful treatment of attributes; Multithreading.tracing: uninterruptible; Multithreading.system_out: signal within critical region, more careful sync_wait; eliminated redundant Thread.testInterrupt; Future.wait_timeout: uniform Multithreading.sync_wait; future scheduler: interruptible body (sync!), to improve reactivity; future_job: reject duplicate assignments -- system error; misc tuning;

recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;

tuned tracing;

ISABELLE_USEDIR_OPTIONS: -q 2 by default;

merged

merged

merged

cleaned up abstract tuple operations and named them consistently

cleaned up abstract tuple operations and named them consistently

added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;

trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;

retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);

qualified Subgoal.FOCUS;

FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;

focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed; added FOCUS_PREMS, which may serve as full replacement for OldGoals.METAHYPS;

Variable.importT/import: return full instantiations, tuned;

added certify_inst, certify_instantiate;

merged

trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);

proper Jinja-Slicing;

merged

merged

abstractions: desymbolize name hint

added numeral code postprocessor rules on type int

sos comments modified

sos documentation

Added remote-SOS changes by Philipp Meyer

Functionality for sum of squares to call a remote csdp prover

merged

updated generated document

reinserted legacy ML function

Set.UNIV and Set.empty are mere abbreviations for top and bot

explicit is better than implicit

Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;

removed old global get_claset/map_claset; added local get_claset/put_claset;

eliminated METAHYPS;

Future.shutdown before loading sequentially -- workaround scheduler deadlock;

ResAxioms.neg_conjecture_clauses: proper context; let exceptions get through unhindered -- Poly/ML exception_trace will do the tracing;

neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS; external_prover: neg_conjecture_clauses should handle TVars within goals; misc tuning;

Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);

eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;

non-critical use_thy;

future result: Synchronized.var;

added unsynchronized Synchronized.peek;

group status: Synchronized.var;

tuned;

Task_Queue.dequeue: explicit thread;

more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;

interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);

misc tuning;

tuned

moved obsolete same_fst to Recdef.thy

adapted doc to type of "op O"

merged

merged

merged

merged

added proof of Kleene_Algebra.star_decomp

added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)

some lemmas about maps (contributed by Peter Lammich)

"more standard" argument order of relation composition (op O)

added rail antiquotation environment, which coexists with old-style content markup;

proper header; proper structure; tuned white space;

proper context for SAT tactics; eliminated METAHYPS; tuned signatures;

moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);

interruptible: Thread.testInterrupt before changing thread attributes;

wait: absorb spurious interrupts; replaced wait_timeout by explicit wait_interruptible;

scheduler: shutdown spontaneously (after some delay) if queue is empty; scheduler_check: critical, only performed after fork/enqueue; shutdown: passively wait for termination;

join_next: do not yield, even if overloaded, to minimize "running" tasks;

tuned tracing;

cancel: improved reactivity due to more careful broadcasting; internal broadcast_all;

dequeue_towards: always return active tasks; join_work: imitate worker more closely, keep active if queue appears to be blocked for the moment -- it may become free again after some worker_finished event;

merged

removed unused low-level interrupts;

tuned signature;

tuned;

more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads; more specific signal vs. broadcast; execute/finish: more careful notification based on minimal/maximal status; tuned shutdown;

enqueue/finish: return minimal/maximal state of this task;

NEWS

tacticals FOCUS and FOCUS_PARAMS;

replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);

replaced old METAHYPS by FOCUS;

added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;

replaced old METAHYPS by FOCUS;

tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);

retrofit: actually handle schematic variables -- need to export into original context;

merged

adapted to changed prefixes

merged

improved handling of parameter import; tuned

explicit is better than implicit

localized interpretation of min/max-lattice

adapted to localized interpretation of min/max-lattice

SUBPROOF/Obtain.result: named params;

updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;

advanced retrofit, which allows new subgoals and variables; added FOCUS -- does not require closed proof;

Variable.focus: named parameters;

lambda/cabs/all: named variants;

Goal.finish: explicit context for printing;

fixed Method.Basic;

eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;

Method.Basic: no position;

basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context; Method.Basic: no position;

dequeue_towards: need to try imm_preds as well;

internal session timing;

enqueue: maintain transitive closure, which simplifies dequeue_towards;

ML_Context.the_generic_context;

eliminated redundant Library.multiply;

renamed structure Display_Goal to Goal_Display;

tuned tracing;

added Multithreading.real_time;

simplified/unified Multithreading.tracing_time; tuned;

get_name: cover only PThm, not PAxm;

eliminated OldGoals.read_term;

more antiquotations instead of adhoc ML stuff;

ML_Context.the_local_context;

eliminated the_context;

do not open OldGoals;

renamed functor SplitterFun to Splitter, require explicit theory;

renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;

eliminated OldGoals.prove_goal;

explicit OldGoals;

structure OldGoals: no pervasive names;

renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;

renamed functor InductFun to Induct;

tuned;

renamed Pure/tctical.ML to Pure/tactical.ML;

eliminated print_goals_without_context -- proper pretty printing;

Display_Goal.pretty_goals: always Markup.subgoal, clarified options;

removed Formal_Power_Series_Examples (cf. adea7a729c7a);

make: keep going by default;

merged

merged

fixed proof --- fact_setprod removed for fact_altdef_nat

merged

Vandermonde vs Pochhammer; Hypergeometric series - very basic facts

More theorems about pochhammer

Moved theorem binomial_symmetric from Formal_Power_Series to here

Moved important theorems from FPS_Examples to FPS --- they are not really examples but useful theorems that are being reproved since unnoticed.

removed obsolete ML proof tools;

more @{theory} antiquotations;

eliminated adhoc ML code;

misc modernization: proper method setup instead of adhoc ML proofs;

global_claset_of;

Proper context for simpset_of, claset_of, clasimpset_of.

local simpset_of;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

merged

paramify_vars: Term_Subst.map_atypsT_same recovered coding conventions of this module;

clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;

use regular Display.string_of_thm_global;

tuned ML_OPTIONS;

fixed doc

Purely functional type inference.

merged

moved complete_lattice &c. into separate theory

merged

tuned proofs and added some lemmas

merged

set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice

set intersection and union now named inter and union

spurious proof failure

original rail implementation by Michael Kerscher;

merged, resolving trivial conflict;

News

explicit antiquotation