substantial improvement in codegen iml

Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset. The hash table (for removing duplicate) now stores clauses as Term.term with names.

relevance_filter takes input axioms as Term.term.

Proof reconstruction now only takes names of theorems as input.

Added tptp_write_file to write all necessary ATP input clauses to one file.

tptp_write_file now takes goals and axioms as Term.term and writes them to a file.

Added functions to retrieve local and global atpset rules. cnf thms to Term.term format.

Moved the settings for ATP time limit to res_atp.ML

Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.

When ATP methods call ATPs, all input clauses from one subgoal are written to one file.

Merged res_atp_setup.ML into res_atp.ML.

SELECT_GOAL: fixed trivial case;

fixed a typo in a comment

tuned;

method: SelectGoals;

method: syntax for SelectGoals;

text: added SelectGoals;

tuned conj_curry;

added extract, retrofit;

added mk_conjunction; tuned conj_curry;

method: restriction to first n sub-goals;

minor changes

more examples

changed and retracted change of location of code lemmas.

ignore repeated vars on lhs, cleanup

improvements for nbe

reformatting

subset_refl now included using the atp attribute

moved the "use" directive

fixed the bugs itroduced by the previous commit

made some small changes to generate nicer latex-output

split the files - Iteration.thy contains the big proof of the iteration combinator - Recursion.thy derives from Iteration the recursion combinator - lam_substs.thy contains the examples (size, substitution and parallel substitution)

Added in a signature.

fixed a problem where a permutation is not analysed when the term is of the form (pi o f) x1...xn This was the case because the head of this term is the constant "nominal.perm". Now an applicability predicate decides the right behaviour of the simproc

streamlined the proof

refined representation of codegen intermediate language

some small tunings

added fresh_fun_eqvt theorem to the theorem collection

added initialisation-code for finite_guess

made some small tunings in the decision-procedure (in the order how the "small" tactics are called)

Added setup for "atpset" (a rule set for ATPs).

Added file Tools/res_atpset.ML.

Merged HOL and FOL clauses and combined some functions.

A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.

some minor tuning on the proofs

initial commit (especially 2nd half needs to be cleaned up)

removal of theory blacklist

new order for arity clauses

fixed but in freeze_spec

splitting up METAHYPS into smaller functions

typos

added a finite_guess tactic, which solves automatically finite-support goals

class package and codegen refinements

added nbe

added temp. nbe test

added nbe, updated neb_*

added nbe

Typo.

added support for arbitrary atoms in the simproc

put_thms: do_index;

rewrite_goals_rule_aux: actually use prems if present;

add_local: do_index;

replaced the lemma at_two by at_different; this lemma now proves EX b. a != b

improved the decision-procedure for permutations; now uses a simproc FIXME: the simproc still needs to be adapted for arbitrary atom types

improved codegen bootstrap

change in codegen syntax

some refinements

added more detailed data to consts

Reverted to old interface of AxClass.add_inst_arity(_i)

Adapted to Florian's recent changes to the AxClass package.

added lemmas at_two: EX a b in an atom type such that a !=b at_ds10 and a "test"-lemma at_prm_eq_compose (can probably be removed)

make SML/NJ happy;

Default type level is T_FULL now.

eprover removes tmp files too.

vampire/eprover methods can now be applied repeatedly until they fail.

removed obsolete meta_conjunction_tr';

rew: handle conjunctionI/D1/D2;

simplified Pure conjunction, based on actual const;

removed rename_indexes_wrt; added rename_indexes2; simplified Pure conjunction, based on actual const;

renamed class_axms to class_intros;

tuned proofs;

simplified Pure conjunction;

not_equal: replaced syntax translation by abbreviation; simplified Pure conjunction;

abandoned merge_alists' in favour of generic AList.merge

added Tools/nbe, fixes

added Tools/nbe

New normalization-by-evaluation package

distinct (op =); removed spurious PolyML.print;

fixed

Inclusion of subset_refl in ATP calls

Fix variable-naming bug (?) by removing a needless recursive call

slight code generator serialization improvements

moved intro_classes from AxClass to ClassPackage

fixed document

* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter) #3 in http://www.cs.ru.nl/~freek/100/

added a few lemmas to do with permutation-equivalence for the recursion combinator

* added Library/ASeries (sum of arithmetic series with instantiation to nat and int) * added Complex/ex/ASeries_Complex (instantiation of the above for reals) * added Complex/ex/HarmonicSeries (should really be in something like Complex/Library) (these are contributions by Benjamin Porter, numbers 68 and 34 of http://www.cs.ru.nl/~freek/100/)

use minimal imports

use qualified name for return

dest_def: tuned error msg;

const constraints: provide TFrees instead of TVars, actually delete constraint (allows Consts.merge caused by ProofContext.transfer after qed);

checkpoint/copy_node: reset body context;

global_qeds: transfer body context;

add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);

constrain: assert const declaration, optional type (i.e. may delete constraints);

removed Import/lazy_scan.ML;

hyperlinks in the PDF work now

replaced Symbol.explode by explode

updated mailing list archive link

use monomorphic sequences / scanners

make maybe into a real type constructor; remove monad syntax

use VectorScannerSeq instead of ListScannerSeq in xml.ML

removed lazy_scan

improved scanning

tuned;

Abstract Natural Numbers with polymorphic recursion.

new-style definitions/abbreviations;

added ex/Abstract_NAT.thy;

tuned;

tuned;