merge

added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets

remove several redundant lemmas about floor and ceiling

merged

declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

simplify proof

simplify proof

remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used

prefer structure Keyword and Parse;

merged

merged

remove simp attribute from square_eq_1_iff

merged

make sure chained facts don't pop up in the metis proof

fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably

generate proper arity declarations for TFrees for SPASS's DFG format; and renamed a confusing function in the process

identify common SPASS error more clearly

remove simp attribute from power2_eq_1_iff

dropped old Library/Word.thy and toy example ex/Adder.thy

dropped old Library/Word.thy and toy example ex/Adder.thy

do not open Legacy by default;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;

renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;

tuned;

tuned signature;

renamed class Outer_Lex to Token and Token_Kind to Token.Kind;

centralized legacy aliases;

prefer structure Parse_Spec;

renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;

renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;

renamed structure ValueParse to Parse_Value; eliminated old-style structure alias V;

refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;

renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;

renamed Outer_Parse to Parse (in Scala);

renamed Outer_Keyword to Keyword (in Scala);

avoid open Conv;

less pervasive names from structure Thm;

less pervasive names from structure Thm;

tuned;

merged

add real_le_linear to list of legacy theorem names

make SML/NJ happy

removed unused conversions;

tuned header; tuned white space;

moved normarith.ML where it is actually used; less inaccurate dependencies;

incorporated further conversions and conversionals, after some minor tuning;

eliminated redundant runtime checks;

normalize atyp names after unconstrainT, which may rename atyps arbitrarily;

more precise dependencies for HOL-Word-SMT_Examples;

merged

merge

added Sledgehammer documentation to TOC

added some Sledgehammer news

document Nitpick changes

merge

added Sledgehammer manual; some material was recovered from the Isar material, the rest is new

renamed Sledgehammer options

renamed options

remove support for crashing beta solver HaifaSat

renamed two Sledgehammer options

merged

added listsum lemmas

Revert mixin patch due to inacceptable performance drop.

add "no_atp"s to Nitpick lemmas

query _HOME environment variables at run-time, not at build-time

move Refute dependency from Plain to Main

move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong

recognize new Kodkod error message syntax

improve precision of set constructs in Nitpick

produce more potential counterexamples for subset operator (cf. quantifiers)

improved Sledgehammer proofs

pass "full_type" argument to proof reconstruction

made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code

delect installed ATPs dynamically, _not_ at image built time

Fix syntax; apparently constant apply was introduced in an earlier changeset.

Merged.

Add mixin to base morphism, required by class package; cf ab324ffd6f3d.

Remove improper use of mixin in class package.

Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1

use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document

more precise dependencies

updated SMT certificates

layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable

integrated SMT into the HOL image

replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite

use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)

split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)

added tracing of reconstruction data

added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms

deleted SMT translation files (to be replaced by a simplified version)

move the addition of extra facts into a separate module

normalize numerals: also rewrite Numeral0 into 0

added missing rewrite rules for natural min and max

rewrite bool case expressions as if expression

simplified normalize_rule and moved it further down in the code

merged addition of rules into one function

added simplification for distinctness of small lists

moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)

added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;

conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;

the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;

avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;

raise Fail uniformly for proofterm errors, which appear to be rather low-level;

unconstrainT operations on proofs, according to krauss/schropp;

added Proofterm.get_name variants according to krauss/schropp; tuned signature;

conditional structure SingleAssignment;

merged

merged

tuned proofs and fact and class names

tuned fact collection names and some proofs

grouped local statements

tuned test problems

merged

merged

simplified proof

modernized specifications;

updated/unified some legacy warnings;

tuned;

do not emit legacy_feature warnings here -- users have no chance to disable them;

removed obsolete CVS Ids;

removed some obsolete admin stuff;

check NEWS;

removed obsolete CVS Ids;

updated some version numbers;

minor tuning;

reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only; (Spelling note: "supersede" is indeed more common in Isabelle sources, although "supercede" is also correct according to major dictionaries.)

merged

merged

modernized specifications; tuned reification

merged

added lemmas concerning last, butlast, insort

Remove RANGE_WARN

clarified NEWS entry

merged

added NEWS entry

Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'

Add rules directly to the corresponding class locales instead.

Removed usage of normalizating locales.

speed up some proofs, fixing linarith_split_limit warnings

fix some linarith_split_limit warnings

include iszero_simps in semiring_norm just once (they are already included in rel_simps)

fix duplicate simp rule warning

no more RealPow.thy (remaining lemmas moved to RealDef.thy)

merged

simplify code for emptiness check

removed lemma real_sq_order; use power2_le_imp_le instead

merged

merged

represent de-Bruin indices simply by position in list

tuned reification functions

tuned code; toward a tightended interface with generated code

fix spelling of 'superseded'

NEWS: removed theory PReal

collected NEWS updates for HOLCF

merged

move floor lemmas from RealPow.thy to RComplete.thy

add lemma tendsto_Complex

move some theorems from RealPow.thy to Transcendental.thy

add lemma power2_eq_1_iff; generalize some other lemmas

minimize imports

move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff

clarified Pretty.font_metrics;

format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;

tuned;

more precise pretty printing based on actual font metrics; removed obsolete relative margin;

predefined spaces;

merged

support Isabelle plugin properties with defaults; font size relative to view.textsize of jEdit; margin relative to component width and approximative font metrics;

merged

tuned proof so that no simplifier warning is printed

renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution

merged

tuned

theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct

tuned; dropped strange myassoc2

stylized COOPER exception

simplified oracle

shorten names

updated references to ML files

only one module fpr presburger method

moved int induction lemma to theory Int as int_bidirectional_induct

tuned theory text; dropped unused lemma

one structure is better than three

less complex organization of cooper source code

dropped unused bindings; avoid open (documents dependency on generated code more explicitly)

add real_mult_commute to legacy theorem names

new construction of real numbers using Cauchy sequences

add more credits to ex/Dedekind_Real.thy

put construction of reals using Dedekind cuts in HOL/ex

disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);

simple dialogs: ensure Swing thread;

font size re-adjustment according to Lobo internals;

Scala for Netbeans 6.8v1.1.0rc2;

more convenient get_font;

renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;

more convenient look-and-feel setup;

more convenient get_font;

explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;

updated to jedit 4.3.2;

ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;

adapted to scala-2.8.0.RC2;

merged

real_mult_commute -> mult_commute

avoid using real-specific versions of generic lemmas

avoid using real-specific versions of generic lemmas

remove a couple of redundant lemmas; simplify some proofs

merged

add lemmas one_less_inverse and one_le_inverse

do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings

added lemmas rel_comp_UNION_distrib(2)

made SML/NJ happy;

reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;

Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;

just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;

added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);

tuned;

removed unused "option" variants of "same" operations;

more basic replacement of newlines;

static Symbol.spaces;

proper use of var stopped;

removed junk;

tuned headers;

tuned;

merged

merged

moved normalization proof tool infrastructure to canonical algebraic classes

added lemmas

merged

renamed Normalizer to the more specific Semiring_Normalizer

delete Groebner_Basis directory -- only one file left

split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces

merged

moved lemma zdvd_period to theory Int

tuned;

discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;

tuned error message: regular Pretty.string_of instead of raw Pretty.output;

unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;

renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;

prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";

tuned signature;

added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;

back-patching of axclass proofs;

back-patching via Single_Assignment.var;

support several sidekick parsers -- very basic default parser;

sidekick: unformatted content, notably without newlines;

unformatted output;

output symbolic pretty printing markup and format in the front end;

Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version; tuned;

tuned;

strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;

use existing undefined function;

merged

removed semicolons

rule subrelI (for nice Isar proofs of relation inequalities)

merged

merged

prefix normalizing replaces class_semiring

xsymbolized

moved method syntax here

tuned proof

former free-floating field_comp_conv now in structure Normalizer

proper sublocales; no free-floating ML sections

moved some lemmas from Groebner_Basis here

revert to loose merge semantics

merged

moved generic lemmas to appropriate places

tuned

dropped duplicate comp_arith

avoid open; tuned references to theorems

avoid references to groebner bases in names which have no references to groebner bases

tuned whitespace

tuned headings

avoid open

tuned internal structure

fail on merge of conflicting normalization entries: functions are not mergable

more canonical data administration

removed former algebra presimpset entirely

removed former algebra presimpset from accessor

removed former algebra presimpset from signature

moved presimplification rules for algebraic methods into named thms functor

tuned whitespace; dropped superfluous open

dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML

moved nat_arith ot Nat_Numeral: clarified normalizer setup

dropped unused file

dropped Id

remove unused constant preal_of_rat; remove several unused lemmas about preals

respectfullness and preservation of prod_rel

ProofContext.init_global

merged

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

constant name access lattice is not in use any longer

uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;

replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;

added separate;

basic formatting of pretty trees; line-up ML vs. Scala sources;

added content_length;

slightly more general Library.chunks;

misc tuning -- accumulate body via ListBuffer;

basic support for symbolic pretty printing; tuned;

extractors for document updates; Session.handle_result: use extractors instead of raw patterns -- NB: using mixed patterns of case classes vs. extractors crashes Scala 2.8.1 RC1;

extractors for outer keyword declarations;

eliminated deprecated "--" method; use case classes with copy method for functional record update;

use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;

use SwingApplication instead of deprecated GUIApplication;

simplified via Position extractors;

some rearrangement of Scala sources;

fminus and some more theorems ported from Finite_Set.

eq_morphism is always optional: avoid trivial morphism for empty list of equations

tuned whitespace

tuned interpunctation, dropped dead comment

merged

avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)

generalize some lemmas to class t1_space

simplify definition of t1_space; generalize lemma closed_sing and related lemmas

generalize some lemmas

convert comments to 'text' blocks

generalize more lemmas about limits

repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)

merged

generalize types of LIMSEQ and LIM; generalize many lemmas

make (f -- a --> x) an abbreviation for (f ---> x) (at a)

make (X ----> L) an abbreviation for (X ---> L) sequentially

adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)

declare cont_discrete_cpo [cont2cont]

remove unneeded constant Zseq

add lemmas eventually_nhds_metric and tendsto_mono

remove unneeded premise

add constants netmap and nhds

Merged.

Provide internal function for printing a single interpretation.

Explicitly manage export in dependencies.

fixed proof (cf. edc381bf7200);

Corrected imports; better approximation of dependencies.

Add Convex to Library build

Removed unnecessary assumption

Translating lemmas from Finite_Set to FSet.

merged

merged

Turned Sem into an inductive definition.

Corrected handling of "for" parameters.

induct_true_def and induct_false_def are already contained in induct_rulify_fallback.

added lemma about irreflexivity of pointer inequality in Imperative_HOL

added function ffilter and some lemmas from Finite_Set to the FSet theory

merged

avoid if on rhs of default simp rules

avoid exception Empty on malformed goal

locale predicates of classes carry a mandatory "class" prefix

a ring_div is a ring_1_no_zero_divisors

NEWS

merged

merged

complete_lattice instance for net type

swap ordering on nets, so x <= y means 'x is finer than y'

fixrec no longer uses global simpset internally to prove equations

move setsum lemmas to Product_plus.thy

remove duplicate lemmas

add lemmas about convergent

Cleanup information theory

Moved Convex theory to library.

Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.

proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences: * present type variables are only compared wrt. first component (the atomic type), not the duplicated sort; * extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem); * deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;

simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;

renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);

specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result; specification result: replaced Thm.legacy_freezeT by Thm.unvarify_global -- the final result appears to be a closed term that is globally exported;

UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;

replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;

renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;

minor tuning of Thm.strip_shyps -- no longer pervasive;

simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;

old NEWS on global operations;

ProofContext.init_global;

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

merged

do not generate code per default -- touches file of parent session

made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)

Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)

now if this doesn't make SML/NJ happy, nothing will

more stats;

renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;

slightly more standard induct_simp_add/del attributes; provide explicit context for internal addsimps;

map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

export Simplifier.with_context;

removed some old comments;

merged

merged

generalize lemma adjoint_unique; simplify some proofs

fix latex url

merged

define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general

remove unused function vector_power, unused lemma one_plus_of_nat_neq_0

move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy

remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead

generalize LIMSEQ_vector to tendsto_vector

generalize orthogonal_clauses

remove redundant lemma vector_dist_norm

remove redundant lemma norm_0

generalize some euclidean space lemmas

prove lemma openin_subopen without using choice

move path-related stuff into new theory file

add new Multivariate_Analysis files to IsaMakefile

move operator norm stuff to new theory file

eliminated spurious sledgehammer invocation;

merged

merged

merged

enclose case expression in brackets

catch the right exception

eliminate trivial case splits from Isar proofs

remove debugging code

merged

minor improvements

identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)

added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)

in "overlord" mode: ignore problem prefix specified in the .thy file

uncomment code

redid some Sledgehammer/Metis proofs

fix more "undeclared symbol" errors related to SPASS's DFG format

be more discriminate: some one-line Isar proofs are silly

one-step Isar proofs are not always pointless

the SPASS output syntax is more general than I thought -- such a pity that there's no documentation

redo more Metis/Sledgehammer example

fixed definition of "bad frees" so that it actually works

don't remove last line of proof

handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction

make SML/NJ happy, take 2

use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)

expand combinators in Isar proofs constructed by Sledgehammer; this requires shuffling around a couple of functions previously defined in Refute

more neg_clausify proofs that get replaced by direct proofs

redo some of the metis proofs

back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs

improve unskolemization

make sure short theorem names are preferred to composite ones in Sledgehammer; this code used to work at some point

properly extract SPASS proof

try out Vampire 11 and parse its output correctly; will revert to Vampire 9 if 11 doesn't perform as well

return updated info record after termination proof

proper context for rule_by_tactic;

conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

hgweb style: show author in filelog; full description in annotate hover

proper context for mksimps etc. -- via simpset of the running Simplifier;

read_const: disallow internal names as usual in visible Isar text;

more explicit treatment of context, although not fully localized;

removed some Emacs junk;

merged

make random engine persistent using code_reflect

repaired subtle misunderstanding: statement names are only passed for name resolution

fixed underscore typo

more coherent naming with ML serializer

dropped code_datatype antiquotation

dropped unnecessary ML code

avoid popular infixes

code_reflect: specify module name directly after keyword

NEWS: code_reflect

merged

updated generated file

modernized structure name

use code_reflect

merged

Tuning the quotient examples

clarified signature; simpler implementation in terms of function's tactic interface

return info record (relative to auxiliary context!)

default termination prover as plain tactic

function: sane interface for programmatic use

ML interface uses plain command names, following conventions from typedef

function: better separate Isar integration from actual functionality

merged

export somehow odd mapa explicitly

exported print_tuple

take into account tupled constructors

avoid code_datatype antiquotation

merged

added an example with a free function variable to the Predicate Compile examples

removed local clone in the predicate compiler

improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type

allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;

'write': actually observe the proof structure (like 'let' or 'fix');

adapted ProofContext.infer_type;

ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;

avoid clash with keyword 'write';

allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;

uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);