summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

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";