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;

renamed Goal.norm_hhf_rule to Goal.norm_hhf;

renamed Goal constant to prop, more general protect/unprotect interfaces; renamed norm_hhf_rule to norm_hhf; added comp_hhf, compose_hhf_tac, based on Drule.lift_all;

added add_local/add_global; index props (for add_local only); added could_unify;

added incr_indexes; added lift_all (approx. reverse of gen_all); renamed Goal constant to prop, more general protect/unprotect interfaces;

renamed Goal constant to prop;

accomodate simplified Thm.lift_rule;

Logic.unprotect;

literal facts;

* Pure/Isar: literal facts; * ML/Pure: tuned Thm.lift_rule; * ML/Pure: renamed Goal constant to prop, more general uses;

tuned;

unnecessary imports removed

fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"

Implemented proof of weak induction theorem.

Added "deepen" method.

circumvented smlnj value restriction

added extraction interface for code generator

Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc.

cleaned up nth, nth_update, nth_map and nth_string functions

Removed legacy prove_goalw_cterm command.

got rid of obsolete prove_goalw_cterm

swapped add_datatype result

removed obfuscating PStrStrTab

reachable - abandoned foldl_map in favor of fold_map

Added Tools/res_hol_clause.ML

Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.

Added "writeln_strs" to the signature

Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.

Added new functions to handle HOL goals and lemmas. Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file. Removed several functions definitions, and combined them with those in other files.

Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names. Also added function "repeat_RS" to the signature.

Added several functions to the signature. Added two new functions, which are used by res_hol_clause.ML programs.

A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.

sorted lemma lists

* HOL: alternative iff syntax;

consts: monomorphic;

removed inappropriate monomorphic test;

replaced Defs.monomorphic by Sign.monomorphic;

alternative iff syntax for equality on booleans, with print_mode 'iff';

added module Pure/General/rat.ML

tidied away duplicate thm

EVERY;

traceIt: plain term;

val legacy = ref false;

prove_raw: cterms, explicit asms; prove: Pattern.matches beta_norm;

avoid legacy goals;

legacy = ref true for the time being -- avoid volumious warnings;

tuned;

avoid OldGoals shortcuts;

* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. * Internal goals: structure Goal.

Internal goals.

renamed triv_goal to goalI, rev_triv_goal to goalD;

tuned header;

Goal.norm_hhf_rule;

export add_binds_i; invoke_case: AutoBind.no_facts; Goal.init, Goal.conclude;

load_file: setmp OldGoals.legacy true;

improved check_result; Goal.init, Goal.conclude;

Goal.prove_plain;

do not export find_thms;

use obsolete goals.ML here;

Goal.conclude;

moved SELECT_GOAL to goal.ML;

moved norm_hhf_rule, prove etc. to goal.ML; moved asm_rewrite_goal_tac to simplifier.ML;

added simplification tactics and rules (from meta_simplifier.ML);

moved various simplification tactics and rules to simplifier.ML;

warn_obsolete for goal commands -- danger of disrupting a local proof context; Goal.init, Goal.conclude, Goal.norm_hhf_rule; shortcuts no longer pervasive (cf. structure OldGoals);

renamed triv_goal to goalI, rev_triv_goal to goalD; removed mk_triv_goal (cf. Goal.init);

added goal.ML; moved use of goals.ML;

added goal.ML;

Goal.norm_hhf_rule, Goal.init;

avoid triv_goal and home-grown meta_allE;

OldGoals;

proper header; proper use of ML files;

avoid home-grown meta_allE;

Goal.prove;

avoid shortcuts from OldGoals;

added simplified settings for Poly/ML 4.x (commented out);

reverted (accidental?) change of 1.148;

abandoned rational number functions in favor of General/rat.ML

introduced functions from Pure/General/rat.ML

slight corrections

substantially improved integration of website into distribution framework

substantially improved integration of website into distribution framework

substantially improved integration of website into distribution framework

substantially improved integration of website into distribution framework

towards an improved website/makedist integration

towards an improved website/makedist integration

added default distinfo.mak

towards an improved website/makedist integration

towards an improved website/makedist integration

added rounding functions

Merged theory ResAtpOracle.thy into ResAtpMethods.thy

obsolete;

removed add_inductive_x;

removed obsolete add_datatype_x; tuned;

removed obsolete thy_syntax.ML;

removed obsolete old_symbol_source;

removed obsolete non-Isar theory format and old Isar theory headers;

removed old-style theory format; tuned;

avoid lagacy read function;

added thm(s) retrieval functions (from goals.ML);

removed obsolete old-locales; moved thm(s) retrieval functions back to pure_thy.ML; removed atomic_goal(w) interface; removed user-level (top_sg, prin, printyp, pprint_term/typ, which tend to cause some confusion about the implicit goal (!) context being used here;

removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;

removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;

removed obsolete old-style syntax;

removed obsolete IOA/meta_theory/ioa_package.ML;

removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;

removed obsolete domain/interface.ML;

removed obsolete add_typedef_x; tuned;

removed print_exn (better let the toplevel do this);

removed obsolete add_recdef_old; tuned;

removed obsolete HOL/thy_syntax.ML;

* Theory syntax: discontinued non-Isar format and old Isar headers;

replaced commafy by existing commas; avoid obsolete Goals.prin;

updated;

isatool fixheaders;

fix headers;

added table functor instance for pairs of strings

added subgraph

added join

slight improvements for website

moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!

More functions are added to the signature of ResClause

*** empty log message ***

added 2 lemmas

Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").

simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;

tuned error msg;

renamed atomize_rule to atomize_cterm;

ObjectLogic.atomize_cterm;

use simplified Toplevel.proof etc.;

back: Toplevel.actual/skip_proof; use simplified Toplevel.proof etc.;

renamed set_context to context; data extend: reset context;

renamed set_context to context; export theory_context; clear_ss: inherit_context; rewrite_aux etc.: theory_context;

functor: no Simplifier argument; Simplifier.theory_context;

moved helper lemma to HilbertChoice.thy; use actual ObjectLogic.atomize_cterm; eliminated obsolete sign_of;

Simplifier.theory_context; replaced get_const by Sign.the_const_type; eliminated obsolete sign_of;

added lemma exE_some (from specification_package.ML);

Simplifier.theory_context;

tuned error msg; tuned;

Simplifier.context/theory_context;

updated;

new interface to make_conjecture_clauses

* Simplifier: simpset of a running simplification process contains a proof context; * Simplifier.inherit_context supercedes Simplifier.inherit_bounds; * Simplifier/Classical Reasoner: more abstract interfaces change_simpset/claset;

added type_solver (uses Simplifier.the_context); removed obsolete context_type_solver;

added pos/negDivAlg_induct declarations (from Main.thy);

moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy; change_simpset;

removed obsolete/experimental context components (superceded by Simplifier.the_context); more abstract change_simpset(_of); tuned;

added set/addloop' for simpset dependent loopers; simpset: added context field with the_context, set_context; added inherit_context (inherits bounds as well); removed obsolete inherit_bounds;

functor: no Simplifier argument; change_simpset;

change_claset(_of): more abtract interface; claset_of: init proof context; added raw get_claset;

functor: no Simplifier argument; export change_clasimpset;

tuned;

Simplifier.inherit_context instead of Simplifier.inherit_bounds;

change_claset/simpset;

change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;

Improved proof of injectivity theorems to make it work on "ordinary" function types as well.

Fixed bug in proof of support theorem (it failed on constructors with no arguments).

Implemented proofs for support and freshness theorems.

deleted leading space in the definition of fresh

Initial revision.

tuned;

tuned comment;

added ML_type, ML_struct;

more;

* antiquotations ML_type, ML_struct; * Isar 'guess' element;

added guess;

added antiquotations ML_type, ML_struct;

use perl for test/stat;

export strip_params;

note_thmss, read/cert_vars etc.: natural argument order; added string_of_thm; tuned;

goal statements: before_qed argument;

added 'guess', which derives the obtained context from the course of reasoning;

added primitive_text, succeed_text;

goal statements: accomodate before_qed argument; ProofContext.note_thmss_i: natural argument order;

goal statements: accomodate before_qed argument;

added 'guess';

tuned;

added no_facts;

tuned comments;

updated;

signature changes

added module rat.ML for rational numbers

longer time out for test (kleing)

deletion of Tools/res_types_sorts; removal of absolute numbering of clauses

deletion of Tools/res_types_sorts; removal of absolute numbering of clauses

obsolete;

counter added to SAT signature

no proof reconstruction when quick_and_dirty is set

tidying

domain package generates compactness lemmas for new constructors

add ML bindings for compactness lemmas

added compactness theorems

added compactness lemmas; cleaned up

added compactness theorems in locale iso

added several theorems in locale iso

added xsymbols syntax for pairs; cleaned up

added theorem typedef_compact

rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less

cleaned up; renamed less_fun to expand_fun_less

added hd lemma

simplifying the treatment of clausification

simplifying the treatment of nameless theorems

expand: error on undefined/empty env variable; tuned;

added assert; tuned;

tuned;

added string_of_pid;

raw symbols: allow non-ASCII chars (e.g. UTF-8); tuned comment;

moved string_of_pid to ML-Systems;

ML_SUFFIX in targets (experimental);

cleanup backup images;

small tidy-up of utility functions

updated print_tac;

add names to infix declarations

new syntax translations for continuous lambda abstraction

removed Istrictify; simplified some proofs

added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up

cleaned up

added theorem typedef_chfin

replaced foldr' with foldr1