Enforced partial evaluation of mk_case_split_tac.

Enforced partial evaluation of mk_case_split_tac

Added dependencies on files in Provers

Added pretty-printing coments

*** empty log message ***

*** empty log message ***

Hoare logic

Changed Univ to Datatype in parents

Replaced rules by defs. Also got rid of tyconstU by including TyConst in the datatype's universe

Replaced rules by defs

Got rid of exvarU and constU by including ExVar and Const in various datatype universes.

Deleted constQU, exvarQU, expQU by including Const, ExpVar, Exp in Value.thy's codatatype declaration.

Replaced rules by defs

Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.

Moved declaration of ~= to a syntax section

replaced Pure by ProtoPure

fixed a bug in infer_types/exn_type_msg

new version of HOL/Integ with curried function application

new version of HOL/IMP with curried function application

new version of HOL with curried function application

added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)

added declaration of syntactic const "_abs";

Added initial /bin/csh line and comments

No longer calls maketest; instead, the Makefile writes the file test.

Uses "suffix substitution" to shorten macro definitions.

Re-organised to perform the tests independently. Now test is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to refer to the right command for running the object-logic. Uses "suffix substitution" to shorten macro definitions.

New example by Jacob Frost, tidied by lcp

New example by Jacob Frost, tidied by lcp

Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.

Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)

Redefined functions to suppress redundant leading 0s and 1s

new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;

Added the exception handler handle _ => exit 1. This will catch all errors and force an exit with error code, causing Make to fail.

intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ

Updated comment about list_subset_univ and list_into_univ.

exit: new, for use in Makefiles

Redefined arithmetic to suppress redundant leading 0s and 1s renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.

Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.

Proved zadd_left_commute and zmult_left_commute to define zadd_ac and zmult_ac. Deleted add_cong, add_kill and add_left_commute_kill as unused. Defined zadd_simps, zminus_simps, zmult_simps and added them to integ_ss.

New shell script for finding orphan .ML files (those with no .thy file)

added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)

added check "length ts > 1" before printing ambiguity warning in infer_types

Improved test for looping rewrite rules.

replaced pair_ss by prod_ss

Improved check for looping conditional rewrite rules.

ID for the file

ID for the file

'get ID update working'

CVS: CVS:

CVS:

added qed, qed_goal[w]

added specification of csh as script interpreter

simplified elimination of chain productions

binder: optional body pri now [bracketted];

improved read_xrules: patterns no longer read twice; tuned read_typ;

*** empty log message ***

instance: now automatically includes defs of current thy node as witnesses;

binder: optional body pri now [bracketted];

added documentation of pwd

renamed Sign.ambiguity_level to Syntax.ambiguity_level

moved ambiguity_level from sign.ML to Syntax/syntax.ML

moved ambiguity_level to Syntax/syntax.ML

added documentation of Sign.ambiguity_level

added reference variable ambiguity_level to control ambiguity warnings

changed due to new .bib files

added optional body priority to binder declaration

Under RS added cross reference to bind_thm

documented slow_tac, slow_best_tac, depth_tac, deepen_tac

removed mention of FOL_dup_cs

\bibliography now includes crossref.bib

updates for Isabelle94-2

simplified get_thm a bit

Replaced ordermap_z_lepoll by ordermap_z_lt, which is stronger and has a simpler proof. Modified proof of ordermap_csquare_le accordingly.

README: Now documents to Tools directory

Deleted semicolon at the end of the qed_goal line, which was preventing not_emptyE from being proved.

some cosmetic changes

added documentation of bind_thm, qed, qed_goal, get_thm, thms_of and theory_of_thm

added optional precedence for body of binder; removed call to infer_types from read_xrules

quite a lot of minor and major revisions (inspecting theories, read_axm, cert_axm, grammar generation, lexical matters, macro examples, ...);

empty_def typo

Proved comp_lam.

Corrected indexing of *datatype

prove_fun now includes equalityI. Added the rewrite rules Collect_simps and UnInt_simps.

Proved sum_bij, sum_ord_iso_cong, prod_bij, prod_ord_iso_cong,singleton_prod_bij, singleton_prod_ord_iso, prod_sum_singleton_bij, prod_sum_singleton_ord_iso. Rotated conjunctions in radd_Inl_iff, radd_Inr_iff to be more suitable for rewriting.

Proved case_cong and case_case.

Renamed single_fun to singleton_fun.

Now also depends upon equalities.thy, allowing use of the equalities in standard simpsets.

Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps and UnInt_simps to ZF_ss. Added consI1 to ZF_typechecks.

Removed spurious comment about eq_cs

Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML

Now depends upon Bool, so that 1 and 2 are defined

Moved theorems Ord_cases_lemma and Ord_cases here from Univ, strengthening the succ(j) case to include Ord(j). Proved trans_induct3, le_implies_UN_le_UN, Ord_1, lt_Ord2, le_Ord2.

Added constants Ord_alt, ++, **

Proved equivalence of Ord and Ord_alt. Proved ordertype_eq_imp_ord_iso, le_well_ord_Memrel, le_ordertype_Memrel, lt_oadd1, oadd_le_self, bij_0_sum, oadd_0, oadd_assoc, id_ord_iso_Memrel, ordertype_0. Now well_ord_Memrel follows from le_well_ord_Memrel and ordertype_Memrel follows from le_ordertype_Memrel. Proved simpler versions of Krzysztof's theorems Ord_oadd, ordertype_pred_subset, ordertype_pred_lt, ordertype_pred_unfold, bij_sum_0, bij_sum_succ, ordertype_sum_Memrel, lt_oadd_disj, oadd_inject. Deleted ordertype_subset: subsumed by ordertype_pred_unfold. Proved ordinal multiplication theorems Ord_omult, lt_omult, omult_oadd_lt, omult_unfold, omult_0, omult_0_left, omult_1, omult_1_left, oadd_omult_distrib, omult_succ, omult_assoc, omult_UN, omult_Limit, lt_omult1, omult_le_self, omult_le_mono1, omult_lt_mono2, omult_le_mono2, omult_le_mono, omult_lt_mono, omult_le_self2, omult_inject.

Proved ord_isoI, ord_iso_refl. Simplified proof of ord_iso_restrict_pred. Proved theorems irrefl_0, ..., well_ord_0.

Proved cadd_cmult_distrib.

Now proof of Ord_jump_cardinal uses ordertype_pred_unfold; proof of sum_0_eqpoll uses bij_0_sum; proof of sum_0_eqpoll uses sum_prod_distrib_bij; proof of sum_assoc_eqpoll uses sum_assoc_bij; proof of prod_assoc_eqpoll uses prod_assoc_bij. Proved well_ord_cadd_cmult_distrib.

Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong uses lemma sum_bij; proof of prod_eqpoll_cong uses lemma prod_bij.

pretty_gram: now sorts productions;

removed print_sign, print_axioms;

slightly changed OFCLASS syntax;

fixed minor typos;

added;

RepFun_eq_0_iff, RepFun_0: new

Moved Transset_includes_summands and Transset_sum_Int_subset here from Ordinal.ML

Re-indented declarations; declared the number 2

Added Krzysztof's theorems irrefl_converse, trans_on_converse, part_ord_converse, linear_converse, tot_ord_converse, Proved rvimage_converse, ord_iso_rvimage_eq

Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage, part_ord_rvimage, tot_ord_rvimage, irrefl_Int_iff, trans_on_Int_iff, part_ord_Int_iff, linear_Int_iff, tot_ord_Int_iff, wf_on_Int_iff, well_ord_Int_iff

singleton_iff: new

Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, succ_eqpoll_succD, cons_lepoll_cons_iff, cons_eqpoll_cons_iff. Deleted inj_succ_succD. Streamlined proof of nat_lepoll_imp_le_lemma. Added Krzysztof's theorems diff_sing_lepoll, lepoll_diff_sing, diff_sing_eqpoll, lepoll_1_is_sing, inj_not_surj_succ, lesspoll_trans, lesspoll_lepoll_lesspoll, lepoll_lesspoll_lesspoll, lepoll_imp_lesspoll_succ, lesspoll_succ_imp_lepoll, lepoll_succ_disj, lepoll_nat_imp_Finite, lepoll_Finite, Finite_imp_cons_Finite, Finite_imp_succ_Finite, nat_le_infinite_Ord, nat_wf_on_converse_Memrel, nat_well_ord_converse_Memrel, well_ord_converse, ordertype_eq_n, Finite_well_ord_converse

Added Krzysztof's constants lesspoll and Finite

Added Krzysztof's theorem pred_Memrel

Moved Transset_includes_summands and Transset_sum_Int_subset to QUniv.thy to eliminate use of merge_theories. Proved Memrel_type. Added Krzysztof's theorems Memrel_mono, Memrel_empty, lt_Ord, succ_le_imp_le

natE0: deleted, since unused

Changed succ(1) to 2 in in_VLimit, two_in_univ

csquare_rel_def: renamed k to K

inj_apply_equality: new

Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE

empty_fun: generalized from -> to Pi

Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit

Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type Renamed doubleton_iff to doubleton_eq_iff

Added Krzysztof's theorem disj_imp_disj

Id: marker.

Added comments and Id: marker.

Added comments and Id: marker.

Tools description, largely taken from ../README

Moved description of tools to Tools/README

ord_iso_rvimage: new

Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, Ord_iso_implies_eq to top of file, as they do not require the other material. Simplified proof of ordertype_subset. Proved ordertype_eq: a short proof using deepen_tac! Deleted bij_ordermap_vimage and ordermap_Memrel "bij_ordermap_vimage and ordermap_Memrelf. [| f: bij(A,B); well_ord(B,r); x:A |] ==>\ \ ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)"; "\ ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";i. [| Ord(i); j:i |] ==> ordermap(i,Memrel(i)) ` j = j" because ordertype_eq serves the same purpose. Proofs of bij_ordertype_vimage and ordertype_Memrel are now trivial.

qed is a utility that makes ML files store the defined theories in Isabelle's theorem database

Simplified proof of ord_iso_image_pred using bij_inverse_ss. Replaced not_well_ord_iso_pred_lemma by much simpler well_ord_iso_subset_lemma. Simplifed proof of well_ord_iso_unique_lemma using well_ord_iso_subset_lemma.

Used bind_thm to store domain_rel_subset and range_rel_subset

removed quotes around "Datatype", and removed needless mention of [Q]Univ

removed quotes around "Inductive"

ran expandshort script

ran expandshort script

removed quotes around "Inductive"

added true theory dependencies

ran expandshort script

changed useless "qed" calls for lemmas back to uses of "result", and/or used "bind_thm" to declare the real results.

Defines ZF theory sections (inductive, datatype) at the start/ Moved theory section code here from Inductive.ML and Datatype.ML

Added Limit_csucc from CardinalArith Moved all theorems concerning FINITE functions to Univ.ML and deleted the declaration val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);

Limit_csucc: moved to InfDatatype and proved explicitly in theory InfDatatype.thy

put quotation marks around constant "and" because it is a keyword for inductive definitions!!

added thy_syntax.ML

Defines ZF theory sections (inductive, datatype) at the start/ Moved theory section code here from Inductive.ML and Datatype.ML

now also depends upon Finite.thy

converse_converse, converse_prod: renamed from converse_of_converse, converse_of_prod

moved congruence rule conj_cong2 to FOL/IFOL.ML

conj_cong2: new congruence rule

case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted own bij_inverse_ss and replaces uses by case_ss

updated comment; renamed converse_of_Un to converse_Un

qconverse_qconverse, qconverse_prod: renamed from qconverse_of_qconverse, qconverse_of_prod

well_ord_iso_predE replaces not_well_ord_iso_pred well_ord_iso_unique: eliminated a premise using well_ord_ord_iso Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred, part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso, well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans, mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map, ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset, domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy deleted bij_ss in favour of bij_inverse_ss

Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of not_well_ord_iso_pred

converse_UN, Diff_eq_0_iff: new

added constants mono_map, ord_iso_map

cardinal_UN_Ord_lt_csucc: added comment le_UN_Ord_lt_csucc: tided proof by proving the lemma inj_UN_subset

conj_commute,disj_commute: new

changed get_thm to search all parent theories if the theorem is not found in the current theory

added bind_thm for theorems defined by "standard ..."

added any, sprop to pure_types;

removed "logic1"; improved typ_to_nonterm;

removed FOL_Lemmas and IFOL_Lemmas; added qed_goal

added print_theory that prints stored thms;

minor internal changes;

improved axioms_of: returns thms as the manual says;

removed ZF_Lemmas and added qed_goal

added warning for already stored theorem to store_thm

sum_ss: moved down and added the rewrite rules for "case"

leI: added comment

lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3

sum_ss: deleted because it conflicts with the one in Sum.ML

not_well_ord_iso_pred: removed needless quantifier

UN_upper_cardinal: updated to refer to Card_le_imp_lepoll and lepoll_imp_Card_le

sum_lepoll_self, cadd_le_self, prod_lepoll_self, cmult_le_self, sum_lepoll_mono, cadd_le_mono, prod_lepoll_mono, cmult_le_mono, InfCard_cmult_eq, cmult_2: new well_ord_lepoll_imp_le: renamed to well_ord_lepoll_imp_Card_le

le_imp_lepoll: renamed to Card_le_imp_lepoll lepoll_imp_le: renamed to lepoll_imp_Card_le; updated to refer to well_ord_lepoll_imp_Card_le

Card_cardinal_le: new

changed Pure's grammar and the way types are converted to nonterminals

replaced type_syn by pure_syn in Pure signature

test_assume_tac: now tries eq_assume_tac on exceptional cases (formulae not of the form a:?A). Affects typechk_tac.

res_inst_tac: added comments

added qed and qed_goal[w]

moved first call of store_theory from thy_read.ML to created .thy.ML file

added bind_thm

added qed and qed_goal[w]

added qed_goal for meta_iffD

replaced "val ... = result()" by "qed ..."

le_UN_Ord_lt_csucc: added comment

replaced "rules" by "defs"

---------------------------------------------------------------------- Committing in HOLCF Use new translation mechanism and keyword syntax, cinfix.ML no longer needed. Optimized proofs in Cont.ML Modified Files: Cfun1.ML Cfun2.thy Cont.ML Cprod3.thy Makefile README Sprod3.thy Tr2.thy ccc1.thy ----------------------------------------------------------------------

ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any equalities, by adding setmksimps K[]. ZF/indrule/mut_ss: removed Collect_cong; it is redundant.

checks that the recursive sets are Consts before taking them apart! Bug was introduced during the translation to theory sections.

equiv_comp_eq: simplified proof

moved Cantors theorem here from ZF/ex/misc

deepen_tac: modified due to outcome of experiments. Its choice of unsafe rule to expand is still non-deterministic.

added qed_goal[w]

added blank line

tidied proofs, using fast_tac etc. as much as possible

prove_fun: new; no longer depends upon the version in simpdata.ML

data_domain,Codata_domain: removed replicate; now return one single domain

tidied proofs, using fast_tac etc. as much as possible

added comments on alternative uses of type_intrs/elims

modified for new treatment of mutual recursion

the_equality: more careful use of addSIs and addIs

cons_fun_eq: modified strange uses of classical reasoner

moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML hom_tac: removed to simplify the proof of comp_homs

moved version of Cantors theorem to ZF/Perm.ML

ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually recursive datatypes, especially with monotone operators Inductive_Fun,CoInductive_Fun: deleted as obsolete inductive_decl: now reads a SINGLE domain for the mutually recursive construction. This could be a sum, perhaps not! CONCRETE SYNTAX has changed too (but there are no examples of this to change).

ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually recursive construction. This is [q]univ(A), which is closed under sum.

updated for new deepen_tac

trivial changes

new reference to HO patterns

Pure/tctical/protect_subgoal: simplified to use Sequence.hd Pure/tctical/DEPTH_FIRST: now suppresses duplicate solutions

Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars

ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually recursive datatypes, especially with monotone operators ZF/add_ind_def/add_fp_def: deleted as obsolete ZF/add_ind_def/add_fp_def_i: now takes dom_sum instead of domts. We no longer automatically construct a sum of separate domains, but could use a sum-closed set such as univ(A).

ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!

replaced 'val ... = result();' by 'qed "...";'

ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of solving the subgoal. Entire tactic is enclosed in DETERM to prevent backtracking between subgoals.

ZF/EquivClass/congruent_commuteI: uncommented and simplified proof

ZF/ZF.ML/UN_iff, INT_iff: added to the signature

Pure/thm/norm_term_skip: new, for skipping normalization of the context Pure/thm/bicompose_aux: now computes nlift (number of lifted assumptions in new subgoals) and avoids normalizing the first nlift assumptions in the case where the proof state is not affected. Pure/thm/norm_term_skip: now normalizes types of parameters Pure/thm/THM: aligned colons

Pure/sequence: added comment explaining that memoing sequences were found to be much slower (due to overheads) than the sequences currently used.

Pure/envir/norm_term: replaced equality test for [] by null

page 157 erratum

now searches all subdirectories of object-logics whether or not they are called "ex"

Chnaged simplifier description (lhss)

added call of store_theory after thy file has been read

Updated description of valid lhss.

In ZF, type i has class term, not (just) logic

added check for newlines not enclosed by '\' inside strings

updated remarks about grammar; added section about ambiguities

exported 'cat';

Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of: new SELECT_GOAL is MUCH faster

Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations

Added month for Coens thesis

removal of FOL_dup_cs

removal of HOL_dup_cs rotation of arguments in split, nat_case, sum_case, list_case

Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.

Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST, REPEAT_DETERM_SOME: new