Rephrased forward proofs to avoid problems with HO unification

Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification

Locally deleted some definitions that were applied too eagerly because of eta-expansion

- Instantiated parts_insert_substD to avoid problems with HO unification - Replaced auto by fastsimp in proof of parts_invKey, since auto looped because of the new encoding of sets

Instantiated parts_insert_substD to avoid problems with HO unification

Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.

Adapted to encoding of sets as predicates

Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification

Adapted functions mk_setT and dest_setT to encoding of sets as predicates.

- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set and to_pred attributes, because it is no longer applied automatically - Manually applied predicate1I in proof of accp_subset, because it is no longer part of the claset - Replaced psubset_def by less_le

Deleted instantiation "set :: (type) itself".

- Function dec in Trancl_Tac must eta-contract relation before calling decr, since it is now a function and could therefore be in eta-expanded form - The trancl prover now does more eta-contraction itself, so eta-contraction is no longer necessary in Tranclp_tac.

- Now uses Orderings as parent theory - "'a set" is now just a type abbreviation for "'a => bool" - The instantiation "set :: (type) ord" and the definition of (p)subset is no longer needed, since it is subsumed by the order on functions and booleans. The derived theorems (p)subset_eq can be used as a replacement. - mem_Collect_eq and Collect_mem_eq can now be derived from the definitions of mem and Collect. - Replaced the instantiation "set :: (type) minus" by the two instantiations "fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq can be used as a replacement for the definition set_diff_def - Replaced the instantiation "set :: (type) uminus" by the two instantiations "fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq can be used as a replacement for the definition Compl_def. - Variable P in rule split_if must be instantiated manually in proof of split_if_mem2 due to problems with HO unification - Moved definition of dense linear orders and proofs about LEAST from Orderings to Set - Deleted code setup for sets

Deleted instance "set :: (type) power" and moved instance "fun :: (type, type) power" to the beginning of the theory

split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.

- Added mem_def and predicate1I in some of the proofs - pred_equals_eq and pred_subset_eq are no longer used in the conversion between sets and predicates, because sets and predicates can no longer be distinguished

- Now imports Code_Setup, rather than Set and Fun, since the theorems about orderings are already needed in Set - Moved "Dense orders" section to Set, since it requires set notation. - The "Order on sets" section is no longer necessary, since it is subsumed by the order on functions and booleans. - Moved proofs of Least_mono and Least_equality to Set, since they require set notation. - In proof of "instance fun :: (type, order) order", use ext instead of expand_fun_eq, since the latter is not yet available. - predicate1I is no longer declared as introduction rule, since it interferes with subsetI

- Explicitely applied predicate1I in a few proofs, because it is no longer part of the claset - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set attribute, because it is no longer applied automatically

- Now imports Fun rather than Orderings - Moved "Set as lattice" section behind "Fun as lattice" section, since sets are just functions. - The instantiations instantiation set :: (type) distrib_lattice instantiation set :: (type) complete_lattice are no longer needed, and the former definitions inf_set_eq, sup_set_eq, Inf_set_def, and Sup_set_def can now be derived from abstract properties of sup, inf, etc.

Instantiated some rules to avoid problems with HO unification.

- Deleted code setup for finite and card - Deleted proof of "instance set :: (finite) finite" and modified proof of "instance fun :: (finite, finite) finite", which now uses some ideas from the instance proof for sets - Instantiated arg_cong rule to avoid problems with HO unification

Instantiated subst rule to avoid problems with HO unification.

converted "General logic setup";

misc fixes and tuning;

updated generated file;

proper scoping of railaliases;

moved some railaliases here -- for proper scoping;

element: isakeyword markup;

removed isasymIN -- already defined in isar.sty;

added isasymIN/STRUCTURE;

converted generic.tex to Thy/Generic.thy;

removed isasymIMPORTS/BEGIN -- already defined in isar.sty;

tuned syntax: props and facts;

converted refcard.tex to Thy/Quick_Reference.thy;

added \isasymdash;

misc tuning;

updated generated file;

use underscore for underscore;

output_entity: added \mbox{} to prevent hyphenation;

added more infrastructure for fresh_star

added mising lemma

Added documentation

moved begin and imports to ../isar.sty;

added begin and imports;

clean_string: handle { };

converted pure.tex to Thy/pure.thy;

polished the proof for atm_prm_fresh and more lemmas for fresh_star

unfold_locales part of default method.

extended to be a library of general facts about the lambda calculus

tuned some proofs and comments

added lemma antiquotation

proper input abbreviations in class

replaced various macros by antiquotations; misc tuning;

more ref macros;

session based on HOL;

thms Max_ge, Min_le: dropped superfluous premise

proper command/keyword markup;

added AND, IS, WHERE symbols;

converted syntax.tex to Thy/syntax.thy;

dropping return in imperative monad bindings

corrected ML semantics

added setup for Isar entities; tuned;

fixed recdef, broken by my previous commit

* New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size

Merged theories about wellfoundedness into one: Wellfounded.thy

moved 'trivial classes' to foundation of code generator

tuned index commands;

more abstract index commands;

added \indexoutersyntax; removed permuted index;

fixed proof

misc cleanup;

converted intro.tex to Thy/intro.thy;

more general evaluation combinators

different handling of eq class for nbe

basic setup for generated document (cf. ../IsarImplementation);

dropped theory PreList

added explicit check phase after reading of specification

added theory Sublist_Order

dropped some metis calls

tuned proofs

constant HOL.eq now qualified

exported is_abbrev mode discriminator

proper abbreviations in class

dropped theory PreList

added entries

move some at/a64 tests to intel mac hardware (running Linux)

updated generated file;

updated generated file;

NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;

removed dead code;

print_cases: proper context for revert_skolem;

tuned;

modernized specifications and proofs;

improved definition of upd

* Context-dependent token translations.

revert_skolem: do not change non-reversible names; default token translations: revert_skolem; removed obsolete revert_skolems;