reenable Kodkodi in Mira now that Nitpick has been ported to 'a set constructor

reenable Kodkodi in Isatest now that Nitpick has been ported to 'a set constructor

fixed bisimilarity axiom -- avoid "insert" with wrong type

tuning

updated Nitpick docs after "set" reintroduction

no abuse of notation

always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)

more robust destruction of "set Collect" idiom

handle starred predicates correctly w.r.t. "set"

handle "Id" gracefully w.r.t. "set"

reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature

handle "set" correctly in Refute -- inspired by old code from Isabelle2007

create consts with proper "set" types

tuned Refute

lower cardinality for faster testing

simplify mem Collect

tuning

ported Minipick to "set"

fixed set extensionality code

tuned import

construct correct "set" type for wf goal

fixed Nitpick's typedef handling w.r.t. "set"

fixed type annotations

rationalized output (a bit)

fixed a few more bugs in \Nitpick's new "set" support

regenerate SMT example certificates, to reflect "set" type constructor

port part of Nitpick to "set" type constructor

reintroduced failing examples now that they work again, after reintroduction of "set"

ported mono calculus to handle "set" type constructors

fixed spurious catch-all patterns

more benchmarks; tuned;

tuned

ported "Sets" example to "set" type constructor

ported a dozen of proofs to the "set" type constructor

reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow

update docs to reflect "Manual_Nits"

removed special handling for set constants in relevance filter

reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter

killed unfold_set_const option that makes no sense now that set is a type constructor again

tuned

removed unnecessary lemmas

tuned proofs

tuned var names

tuned argument order

merged

add simp rules for bitwise word operations with 1

tuned types

disabled failing sledgehammer unit test (collateral damage of 184d36538e51)

disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5)

merged

Made gen_dest_case more robust against eta contraction

merged

remove unnecessary intermediate lemmas

tuned;

eliminated old-fashioned Global_Theory.add_thms;

simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;

simplified proof;

simplified proof;

simplified proof;

more parallelism;

tuned;

merged

tuned -- afford slightly larger simpset in simp_defs_tac;

tuned -- standard proofs by default;

do not fork skipped proofs;

clarified timeit_msg;

tuned;

comments;

remove constant 'ccpo.lub', re-use constant 'Sup' instead

merged

tuned

conversions from sets to predicates and vice versa; extensionality on predicates

added implementation of pred_of_set

fundamental theorems on Set.bind

updated generated files;

qualified Finite_Set.fold

qualified Finite_Set.fold

dropped redundant setup

tuned declaration

attribute code_abbrev superseedes code_unfold_post; tuned text

attribute code_abbrev superseedes code_unfold_post; tuned names and spacing

attribute code_abbrev superseedes code_unfold_post

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat

merged

merged

restate some lemmas to respect int/bin distinction

simplify some proofs

add lemma word_eq_iff

restate lemma word_1_no in terms of Numeral1

remove recursion combinator bin_rec; define AND for type int directly with function package

simplify definition of XOR for type int; reorder some lemmas

simplify definition of OR for type int; reorder some lemmas

simplify definition of NOT for type int

add several new tests, most of which don't work yet

fix typos

remove some duplicate lemmas

simplify proof

replace 'lemmas' with explicit 'lemma'

add section headings

remove duplicate lemma lists

reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;

disable kodkodi for now to prevent isatest failure of HOL-Nitpick_Examples due to 'a set constructor; prefer explicit version information;

updated platform information;

discontinued broken macbroy5 and thus the obsolete ppc-darwin platform;

more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;

print case syntax depending on "show_cases" configuration option;

merged

redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min

remove some uses of Int.succ and Int.pred

removed unused lemmas

remove redundant syntax declaration

use 'induct arbitrary' instead of 'rule_format' attribute

declare simp rules immediately, instead of using 'declare' commands

declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin

be explicit about Finite_Set.fold

dropped fact whose names clash with corresponding facts on canonical fold

prefer canonical fold on lists

be explicit about Finite_Set.fold

incorporated More_Set and More_List into the Main body -- to be consolidated later

moved theorem requiring multisets from More_List to Multiset

NEWS: unavoidable fact renames

dropped disfruitful `constant signatures`

moved various set operations to theory Set (resp. Product_Type)

dropped Executable_Set wrapper theory

updated certificate

NEWS: `set` is now a proper type constructor

dropped references to obsolete facts `mem_def` and `Collect_def`

dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`

adjusted to set/pred distinction by means of type constructor `set`

treatment of type constructor `set`

executable intervals

`set` is now a proper type constructor

tuned layout

reduced to a compatibility layer

added setup for executable code

moved `sublists` to theory Enum

commented out examples which choke on strict set/pred distinction

explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`

adjusted to set/pred distinction by means of type constructor `set`

dropped references to obsolete fact `mem_def`

dropped obsolete lemma member_set

dropped obsolete code equation for Id

tuned proofs

generalized type signature to permit overloading on `set`

added monad instance for `set`

enum type class instance for `set`; dropped misfitting code lemma for trancl

finite type class instance for `set`

treatment of type constructor `set`

lattice type class instances for `set`; added code lemma for Set.bind

`set` is now a proper type constructor; added operation for set monad

simplify some proofs

remove redundant lemma word_sub_def

add lemmas bin_cat_zero and bin_split_zero

more uses of 'induct arbitrary'

use 'induct arbitrary' instead of universal quantifiers

remove two conflicting simp rules for 'number_of (number_of _)' pattern

add lemma bin_nth_minus1

removed killed encoding from example

updated docs

killed "guard@?" encodings -- they were found to be unsound

extend previous optimizations to guard-based encodings

treat polymorphic constructors specially in @? encodings

tuning

no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")

added some basic documentation about method induction_schema extracted from old NEWS

adding documentation about the quickcheck_generator command in the IsarRef

extending quickcheck example

NEWS

quickcheck_generator command also creates random generators

don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers

one more SPASS identifier

tuning

merged

meaningful error message on failing merges of coercion tables

add simp rules for enat and ereal

add lemmas

add lemmas

weaken preconditions on lemmas

add lemmas

removing some debug output in quotient_definition

adding quickcheck generators in some HOL-Library theories

adding quickcheck generator for distinct lists; adding examples

added keywords

quickcheck generators for abstract types; tuned

exporting instantiation functions in quickcheck for their usage in abstract generators

generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types; adding common datatype interpretation to quickcheck_common;

tuned

tuned

ensure TPTP FOF/TFF/THF formulas are close

tuned

merged

added old chestnut

isarfied proof; add log to DERIV_intros

tendsto lemmas for ln and powr

tuned settings;

updated jedit_build component;

updated version information;

patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);

eliminated Drule.export_without_context which is not really required here;

tuned signature;

enforce short hostname on all platforms (especially macbroy2);

clarified modules that contribute to datatype package;

tuned signature;

merged

merged

improved indexed complete lattice

more elementary defs;

eliminated old-fashioned Global_Theory.add_thms(s);

prefer sorting from Scala library;

prefer Name.context operations;

tuned;

clarified modules that contribute to datatype package;

tuned signature;

merged;

tuned;

add complementary lemmas for {min,max}_least

add lemmas about limits

clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

separate rep_datatype.ML; tuned signature;

misc tuning and simplification;

more stats;

made SML/NJ happier

merged

tuned

hiding the precious name map_entry in AList_Impl

killed dead code

use new redirection algorithm in Sledgehammer

fixed parsing of TPTP atoms

tuned signature;

avoid fragile Sign.intern_const -- pass internal names directly; tuned;

tuned;

added new proof redirection code

SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite

make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)

NEWS

correcting dependencies after renaming

tuned header after renaming

moving AList theory to AList_Impl to make space for the association lists with invariant

merged