Various simplifications of the Constructible theories

Fixed bug involving inductive definitions with equalities in the premises.

Fixed bug involving inductive definitions having equalities in the premises, e.g. n = Suc(m).

Documented new "asm_lr" option for simp.

added the new elim rule psubsetE

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

Added some comments on new simplifier.

Documented new "asm_lr" option for simp.

Adapted to new simplifier.

Numerous cosmetic changes, prompted by the new simplifier

Deleted superfluous dest_implies.

*** empty log message ***

Adapted to new simplifier.

Adapted to new simplifier.

Fixed bug in expand_proof which caused indexes to be incremented incorrectly.

Added check for axioms with "realizes Null A = A".

Added function elim_vars.

Completely reimplemented mutual simplification of premises.

Removed nRS again because extract_rews now takes care of preserving names.

Added syntax for "asm_lr" simplifier option.

- eliminated thin_leading_eqs_tac - gen_hyp_subst_tac now uses asm_lr_simp_tac instead of asm_full_simp_tac, in order to avoid divergence of new simplifier

Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.

- additional congruence rules for boolean operators - additional rewrite rules for exI / exE

Adapted to new simplifier.

Removed nRS again because extract_rews now takes care of preserving names.

Added elim_vars to preprocessor.

Fixed problem with induct_conj_curry: variable C should have type prop.

fixes !!-bound vars in induction statement automatically

modified induct method

Proof tidying

Isar experiments, etc.

Tidied. New Pi-theorem.

new Ring example

Isar proof

Modules theory added

New theory GroupTheory/Module.thy of modules

Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML (which is automatically loaded with Int.thy) on case-insensitive filesystems.

GroupTheory and FuncSet

new theory for Pi-sets, restrict, etc.

Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"

new document directory for GroupTheory

converted to Isar and using new "implicit structures" instead of Sigma, etc

*** empty log message ***

*** empty log message ***

*** empty log message ***

Int.thy -> int.thy

became int.ML

conversion to Isar

converted to Isar

added nat_split

converted to Isar script

shortened a proof

got rid of deepen_tac

less use of x-symbols

*** empty log message ***

drule: added nRS simplifier: trace with names

preserve names of rewrite rules when transforming them

comments + usage

Streamlined proofs of instances of Separation

Bound variable preservation in Collect_cong

renamed M_triv_axioms to M_trivial and M_axioms to M_basic

tweaks

*** empty log message ***

bug in counter example finder

conversion of ZF/Integ/{Int,Bin} to Isar scripts

added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier

tidied

deleted redundant material (quasiformula, ...) and rationalized

fixed the typesetting

*** empty log message ***

Added missing rewrite rule and some arith examples

order_less_irrefl: [simp] -> [iff]

*** empty log message ***

converted Hyperreal/Zorn to Isar format and moved to Library

removal of blast.overloaded

updated;

*** empty log message ***

tuned;

fixed a name clash

improved tell_thm_deps;

various new lemmas for Constructible

completion of the consistency proof for AC

thms_containing: allow "_" in specification;

*** empty log message ***

* Pure: disallow duplicate fact bindings within new-style theory files;

disallow duplicate fact bindings for drafts (i.e. within new-style theory files);

tuned;

avoid duplicate fact bindings;

removed IsarTut;

*** empty log message ***

avoid duplicate fact bindings;

check_file: disallow current dir (typically "");

simplified results; added hook;

simplified results;

Thm.proof_of;

check_goal: produce error instead of warning;

added proof_of;

thms/axms_of_proof: proper handling of MinProof;

result dependency output;

dup_elim: improved error reporting;

*** empty log message ***

avoid duplicate fact bindings;

* Isar: preview of problems to finish 'show' now produce an error

conversion of ZF/IntDiv to Isar script

conversion of ZF/IntDiv to Isar script

*** empty log message ***

*** empty log message ***

Added div+mod cancelling simproc

for cancelling div + mod.

updated to use locales (still some rough edges);

tweaked

tweaks

tweaks and new lemmas

new proof needed now

proof can be shortened now

new lemmas

Frederic Blanqui's new "guard" examples

tidying of Isar scripts

Various tweaks of the presentation

Relativized right up to L satisfies V=L!

Tidying up

Relativization and absoluteness for DPow!!

Finished absoluteness of "satisfies"!!

arith_tac should not produce counter example

*** empty log message ***

Counter example generation mods.

Added counter example generation.

*** empty log message ***

In ZF/Constructible, moved many results from Satisfies_absolute, etc., to the new theory Internalize.thy

more robust printing of numerals;

new file Constructible/Satisfies_absolute.thy

Lots of new results concerning recursive datatypes, towards absoluteness of "satisfies"

*** empty log message ***

*** empty log message ***

Added Mi and Max on sets, hid Min and Pls on numerals.

*** empty log message ***

transform_error: pass through Interrupt;

tuned;

exception SIMPROC_FAIL: solid error reporting of simprocs;

tuned prove_conv (error reporting done within meta_simplifier.ML);

adhoc_freeze_vars;

proper instantiation of mk_left_commute;

converted;

tuned deps;

use Tactic.prove instead of prove_goalw_cterm in internal proofs!

Tactic.prove, Tactic.prove_standard;

* Pure: improved error reporting of simprocs; tuned;

tuned;

mk_left_commute: proper instantiation avoids expensive unification;

tuned;

Simplifier.simproc(_i);

Added time example at the end.

section on "Rule declarations and methods";

Removed (now unneeded) declaration of realizer for induction on datatype b.

Removed (now unneeded) declarations of realizers for induction on lists and letters.

Added file Tools/datatype_realizer.ML

Removed (now unneeded) declaration of realizers for induction on natural numbers.

Module for defining realizers for induction and case analysis theorems for datatypes.

Added calls to add_dt_realizers.

Exported function make_tnames.

Fixed two bugs

* Provers: Simplifier.simproc(_i) now provide sane interface for setting up simprocs;

sane interface for simprocs;

fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);

predefined locales "var" and "struct" (useful for sharing parameters);

* Pure: predefined locales "var" and "struct" are useful for sharing parameters (as in CASL, for example); just specify something like ``var x + var y + struct M'' as import;

protect simplifier operation against spurious exceptions from simprocs;

tuned; subsection on simple meta-theory of structures;

special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);

Removed theory NatDef.

Replaced nat_ind_tac by induct_tac.

Removed proof of Suc_le_D (already proved in Nat.thy).

Removed reference to theory NatDef.

Removed reference to simpset of NatDef.thy

Legacy ML bindings.

- Converted to new theory format - Moved NatDef stuff to theory Nat

Moved NatDef stuff to theory Nat.

updated;

added Isabelle LNCSes;

fixed long statement: P.opt_thm_name;

fixed railroads;

typedef: "open" option;

declare projected "axioms" as "elim?";

better satisfies rules for is_recfun A satisfies rule for is_wfrec!

some progress towards "satisfies"

*** empty log message ***

added mk_left_commute to HOL.thy and used it "everywhere"

separate "axioms" proofs: more flexible for locale reasoning

tweaks involving Separation

new theorem eq_commute

better sats rules for higher-order operators

removal of twos_compl.ML, which is not really needed

- changed date format for proper lexicographical ordering - send tail of log in email

changed date format for proper lexicographical ordering

tuned messages;

tuned;

eliminate open locales and special ML code;

tuned document;

make SML/NJ happy;

support for split assumptions in cases (hyps vs. prems);

tuned;

More lemmas, working towards relativization of "satisfies"

Added the assumption nth_replacement to locale M_datatypes. Moved up its proof to make it available for the instantiation of that locale.

simplified locale predicates;

removed unused locale_facts(_i); simplified locale predicates: only one level for zero imports; tuned;

tuned;

tweaks, aiming towards relativization of "satisfies"

Tuned type constraint of function merge_rules to make smlnj happy.

AC18: meta-level predicate via locale;

tuned view;

removed attribute "norm_hhf";

adapted fact names;

predicate defs via locales;

locales: predicate defs;

* Pure: locale specifications now produce predicate definitions;

Relativization and Separation for the function "nth"

Added "nocite" to avoid BibTeX error when proofs are switched off.

Added program extraction keywords.

Document for program extraction in HOL.

Examples for program extraction in HOL.

Rules for rewriting HOL proofs.

Added theory for setting up program extraction.

Added program extraction module.

*** empty log message ***

accomodate cumulative locale predicates;

support locale ``views'' (for cumulative predicates);

Towards relativization and absoluteness of formula_rec

Absoluteness of the function "nth"

A couple of new theorems for Constructible

absoluteness for "formula" and "eclose"

define cumulative predicate view; tuned;

adapted add_locale;

adapted locale syntax;

fixed inform_file_retracted: remove_thy;

ACe_axioms;

added satisfy_hyps;