improve Isabelle default simplifier

[till]

Improve function isSimpRule in Isabelle.IsaProve. All non-looping conditional rewrite rules should be put in the simplifier set, while the looping ones should be excluded. For the attached example, the definition of ++ should be in the simplifier, such that associativity can be proved using

apply ((rule allI)+)
apply (induct_tac "x")
apply (auto)

Set up simpsets for minimizing or maximizing sorts, using the overloading axioms. Cf. the corresponding tactics overload_down and overload_up in HOL-CASL.

Definitions (see the isDef attribute) should not go into the simplifier.

[till]

Setup of simplifier in HOL-CASL

[maeder]

I don't understand what to do. We don't have overloading axioms.

[till]

The overloading axioms are called ga_function_monotonicity and ga_predicate_monotonicity in source:trunk/Comorphisms/CASL2PCFOL.inline.hs

[maeder]

I've added a test for a conditional rewrite rule and allowed to exclude or include generated axioms by name prefix. I don't know how to test for "non-looping" or which name prefixes exactly to include or to exclude. (see source:trunk/Isabelle/MarkSimp.hs)

[maeder]

The prove for RCCVerification does not go through with the new simplifier set. Before only declare half_gt_zero [simp] had to be deleted.

[maeder]

This needs some theory or heuristics before implementation