Re: [isabelle] Accessing split-theorems on ML-level



Yes, this is not quite what I had in mind though. In my program, I have a type (from some variable in a term) and I would like to get the split theorem directly from the type, without having to create a string representation of the name of that type.

Moa

Amine Chaieb wrote:
In ML you can access facts in the theorem databaase using thm or thms, when the result is a theorem list.

In you case , e.g.

ML> thm "list.split";
val it =
   "?P (list_case ?f1.0 ?f2.0 ?x) =
      ((?x = [] --> ?P ?f1.0) &
       (ALL a list. ?x = a # list --> ?P (?f2.0 a list)))" : Thm.thm

Amine.

Moa Johansson wrote:
Hi,
I need to get hold of theorems for splitting case-statements, given a datatype, on the ML level (eg. theorems like "list.split", "nat.split" etc). Where can I find these?

Thanks,
Moa






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.