ISAR-fied two proofs about equality for abstraction functions.

* Provers/induct: obtain pattern;

added an authors section (please let me know if somebody is left out or unhappy)

some minor tunings

added the version of nominal.thy that contains all properties about support of finite sets

cleaned up all examples so that they work with the current nominal-setting.

finished cleaning up the parts that collect lemmas (with instantiations) under some general names

Corrected treatment of non-recursive abstraction types.

tuned induct proofs;

induct: insert defs in object-logic form; export guess_instance;

tuned induct proofs;

tuned induct proofs;

consume: unfold defs in all major prems;

revert_skolem: fall back on Syntax.deskolem;

forall_conv ~1;

added dummy_pattern;

tuned names;

forall_conv: limit prefix;

fix_tac: proper treatment of major premises in goal; export atomize/rulify interface; tuned;

removed obsolete dummy paragraphs;

tuned;

code generator: case expressions, improved name resolving

added fsub.thy (poplmark challenge) to the examples directory.

Fixed problem with strong induction theorem for datatypes containing no atom types (ind_sort was the empty sort in this case).

send more information with test-takes-too-long message (which tests are still running)

fixed spelling of 'case_conclusion';

tuned induct proofs;

tuned induction proofs;

more robust revert_skolem; tuned;

tuned;

Provers/induct: definitional insts and fixing;

consume: proper treatment of defs; simplified case_conclusion;

added case_conclusion attribute;

(co)induct: taking; induct set: proper treatment of defs;

RuleCases.case_conclusion;

tuned;

added case_conclusion attribute; added coinduct method/attribute; induct method: definsts/fixing/taking; tuned;

improved failure tracking

Datatype_Universe: hide base names only;

added type cases/cases_tactic, and CASES, SUBGOAL_CASES; added consume rule; support named case conclusions; tuned interfaces;

cases_tactic;

moved multi_resolve(s) to drule.ML; cases_tactic;

find_xxxS: term instead of thm;

export map_tags; added multi_resolve(s) -- from Isar/method.ML;

make coinduct actually work; moved some generic code to Pure/Isar/rule_cases.ML; tuned;

Drule.multi_resolves;

declare coinduct rule; tuned;

added code generator syntax

added codegenerator

added code generator syntax

new treatment of polymorphic types, using Sign.const_typargs

added codegen package

added serializer

tweak

fixed some inconveniencies in website

CONJUNCTS;

tuned;

Goal.norm_hhf_protected;

added coinduct attribute; tuned;

added CONJUNCTS: treat conjunction as separate sub-goals;

simpset: added reorient field, set_reorient;

tuned norm_hhf_protected;

removed conj_mono; added conj_curry; tuned;

induct: CONJUNCTS for multiple goals; added coinduct method; tuned;

tuned induct syntax;

FOL: -p 2;

presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy

-- changed the interface of functions vampire_oracle and eprover_oracle.

-- terms are fully typed. -- only the top-level boolean terms are predicates.

-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.

-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.

-- added combinator reduction axioms (typed and untyped) for HOL goals. -- combined make_nnf functions for HOL and FOL goals. -- hypothesis of goals are now also skolemized by inference.

-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).

-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.

-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL. -- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input. -- added "check_is_fol" and "check_is_fol_term" into the signature.

tuned document;

tuned;

improved induction proof: local defs/fixes;

tuned Pattern.match/unify; tuned fold;

added deskolem;

added THEN_ALL_NEW_CASES; Syntax.deskolem;

added revert_skolem, mk_def, add_def; export: Goal.norm_hhf'; tuned;

ProofContext.mk_def;

Term.betapplys;

tuned Pattern.match/unify;

added betapplys;

tuned interfaces to support incremental match/unify (cf. versions in type.ML);

tuned;

norm_hhf: no normalization of protected props;

added protect_cong, cong_mono_thm; outer_params: Syntax.deskolem;

induct: support local definitions to be passed through the induction; deprecate open rule cases; misc cleanup;

Trueprop: use ObjectLogic.judgment etc.; uniform Const of name * typargs, removed TConst;

Term.betapply;

new version of "tryres" allowing multiple unifiers (apparently needed for Skolemization of higher-order theorems)

pgmlsymbolson: append Symbol.xsymbolsN at end!

better no -d option;

added generic transformators

removal of is_hol

added module system

added modules for code generator generation two, not operational yet

class_package - operational view on type classes

string_of_alist - convenient q'n'd printout function

support for polyml-4.2.0;

new syntax for class_package

added const_instance;

added instance;

added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;

Compatibility wrapper for Poly/ML 4.2.0.

tuned;

added a few equivariance lemmas (they need to be automated eventually)

changed the HOL_basic_ss back and selectively added simp_thms and triv_forall_equality. (Otherwise the goals would have been simplified too much)

exchanged HOL_ss for HOL_basic_ss in the simplification part. Otherwise the case where the context is instantiated with unit leads to vacuous quantifiers, such as ALL a. A

a proof step corrected due to the changement in the presburger method.

old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.

add header

tuned proofs;

moved find_free to term.ML;

guess: Seq.hd; Term.find_free;

guess: Toplevel.proof;

added find_free (from Isar/proof_context.ML);

curried multiply;

induct method: fixes; tuned;

uncurried Consts.typargs;

renamed Thm.cgoal_of to Thm.cprem_of;

duplicate axioms in ATP linkup, and general fixes

tidying

called the induction principle "unsafe" instead of "test".

Skolemization by inference, but not quite finished

Explicit data structures for some Isar language elements.

tuned;

tvars_intr_list: natural argument order;

moved datatype elem to element.ML; removed unused imports function;

P.context_element, P.locale_element;

Element.context;

use existing exeption Empty;

avoid code redundancy; tuned comments;

tuned comments;

removed obsolete term set operations;

P.locale_element;

added fold_terms; added tfrees_of, frees_of; tvars_intr_list: natural argument order;

added Isar/element.ML;

Thm.varifyT': natural argument order;

added join function

allowing indentation of 'theory' keyword

simplified after_qed;

avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;

removed export_plain; (some_)fact_tac: Drule.incr_indexes;

renamed assert_prop to ensure_prop;

renamed goals.ML to old_goals.ML; inline Drule.impose_hyps;

export compose_hhf; removed obsolete norm_hhf_plain; tuned;

removed impose_hyps, satisfy_hyps; tuned;

const args: do not store variable names (unused);

renamed goals.ML to old_goals.ML;

(fix for accidental commit)

(codegen)

generate pattern combinators for new datatypes

reimplemented Case syntax using print/parse translations; moved as-patterns to separate section

add case syntax for type one

remove syntax for as-patterns

avoid 'as' as identifier;

avoid 'as' as identifier;

Added strong induction theorem (currently only axiomatized!).

Initial commit.

Initial commit of the theory "Weakening".

added thms perm, distinct and fresh to the simplifier. One would liket to add also inject, but this causes problems with "congruences" like Lam [a].t1 = Lam [b].t2 P (Lam [a].t1) ----------------------- P (Lam [b].t2) because the equation "Lam [a].t1 = Lam [b].t2" would simplify to "[a].t1 = [b].t2" and then the goal is not true just by simplification.

added proper fillin_mixfix

added fillin_mixfix, replace_quote

New function store_thmss_atts.

used the function Library.product for the cprod from Stefan

fixed bug with nominal induct - the bug occured in rule inductions when the goal did not use all variables from the relation over which the induction was done

added fillin_mixfix' needed by serializer

add case syntax stuff

use consts for infix syntax

add proof of Bekic's theorem: fix_cprod

simplify definitions

put iterate and fix in separate sections; added Letrec

renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM

add line breaks to Rep_CFun syntax

moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section

moved adm_chfindom from Fix.thy to Cfun.thy

cleaned up

add print translation: Abs_CFun f => LAM x. f x

Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names. Also removed some functions that are not used any more.

improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion

reimplement copy_def to use data constructor constants

cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple

generate lambda pattern syntax for new data constructors

changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF

add constant one_when; LAM pattern for ONE

add translation for wildcard pattern

change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up

make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1

cleaned up; ch2ch_Rep_CFun is a simp rule

changed iterate to a continuous type

reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less

removed ex/loeckx.ML

removed proof about Ifix, which no longer exists

cleaned up; chain_const and thelub_const are simp rules

cleaned up; removed adm_tricks in favor of compactness theorems

fix spelling

Moved atom stuff to new file nominal_atoms.ML

- completed the list of thms for supp_atm - cleaned up the way how thms are collected under single names

Added code for proving that new datatype has finite support.

removed unused modify_typargs, map_typargs, fold_typargs;

added Isar.state/exn;

Isar.loop;

moved consts declarations to consts.ML;

Consts.dest;

Polymorphic constants.

added consts.ML;

fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;

dist_eqI: the_context();

Sign.const_monomorphic;

Logic.nth_prem;

added the collection of lemmas "supp_at"

some minor tweaks in some proofs (nothing extraordinary)

tunings of some comments (nothing serious)

nth_*, fold_index refined

fold_index replacing foldln

A few new lemmas

tuned my last commit

simplified the abs_supp_approx proof and tuned some comments in nominal_permeq.ML

Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'. This means the syntax of the tactics supports_simp and perm_simp are exactly like simp, namely (supports_simp add: .... del: ...) where the add's and del's are optional.

1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")

tuned;

lthms_containing: not o valid_thms;

added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;

renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;

renamed Goal constant to prop, more general protect/unprotect interfaces;

added fact method; accomodate simplified Thm.lift_rule;

tuned ProofContext.export interfaces;

syntax for literal facts;

removed try_dest_Goal, use Logic.unprotect;

added cgoal_of; simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;

accomodate simplified Thm.lift_rule; tuned;

export cong_modifiers, simp_modifiers';

certify_term: tuned monomorphic consts;

datatype thmref: added Fact; renamed Goal constant to prop;

Logic.lift_all;

renamed Goal constant to prop, more general protect/unprotect interfaces; replaced lift_fns by lift_abs, lift_all;