Isabelle induction tactic for generated types

spechub / Hets

The Heterogeneous Tool Set

http://hets.eu

GNU General Public License v2.0

57 stars 19 forks source link

Isabelle induction tactic for generated types #199

Open sternk opened 10 years ago

sternk commented 10 years ago

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

For non-free generated types, only a second-order induction axiom is generated (see ticket #156), no proper Isabelle datatype. Write an induction tactic for these axioms, building on the existing induction infrastructure if Isabelle as much as possible.

sternk commented 10 years ago

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

this is not a duplicate. The other ticket has been closed, but the task of the present ticket explicitly is mentioned as not implemented.