Wed, 07 May 2008 10:57:19 +0200 Adapted to encoding of sets as predicates
berghofe [Wed, 07 May 2008 10:57:19 +0200] rev 26806
Adapted to encoding of sets as predicates
Wed, 07 May 2008 10:56:58 +0200 Replaced forward proofs of existential statements by backward proofs
berghofe [Wed, 07 May 2008 10:56:58 +0200] rev 26805
Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification
Wed, 07 May 2008 10:56:55 +0200 Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
berghofe [Wed, 07 May 2008 10:56:55 +0200] rev 26804
Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
Wed, 07 May 2008 10:56:52 +0200 - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe [Wed, 07 May 2008 10:56:52 +0200] rev 26803
- 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
Wed, 07 May 2008 10:56:50 +0200 Deleted instantiation "set :: (type) itself".
berghofe [Wed, 07 May 2008 10:56:50 +0200] rev 26802
Deleted instantiation "set :: (type) itself".
Wed, 07 May 2008 10:56:49 +0200 - Function dec in Trancl_Tac must eta-contract relation before calling
berghofe [Wed, 07 May 2008 10:56:49 +0200] rev 26801
- 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.
Wed, 07 May 2008 10:56:43 +0200 - Now uses Orderings as parent theory
berghofe [Wed, 07 May 2008 10:56:43 +0200] rev 26800
- 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
Wed, 07 May 2008 10:56:41 +0200 Deleted instance "set :: (type) power" and moved instance
berghofe [Wed, 07 May 2008 10:56:41 +0200] rev 26799
Deleted instance "set :: (type) power" and moved instance "fun :: (type, type) power" to the beginning of the theory
Wed, 07 May 2008 10:56:40 +0200 split_beta is now declared as monotonicity rule, to allow bounded
berghofe [Wed, 07 May 2008 10:56:40 +0200] rev 26798
split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.
Wed, 07 May 2008 10:56:39 +0200 - Added mem_def and predicate1I in some of the proofs
berghofe [Wed, 07 May 2008 10:56:39 +0200] rev 26797
- 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
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip