improve Isabelle default simplifier

[sternk]

Reported by till and assigned to till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/62

view-test9.casl simplifier.sml

---

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.

[sternk]

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/62#comment:8

---

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

[sternk]

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/62#comment:9

---

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

[sternk]

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/62#comment:10

---

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 spechub/Hets:Isabelle/MarkSimp.hs)

[sternk]

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/62#comment:11

---

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

[sternk]

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/62#comment:12

---

This needs some theory or heuristics before implementation