Re: [isabelle] Nested/Indirect Induction in Isabelle



Thank you all for your feedback. I think the old style inductor for my tree
datatype is just what I want. Thanks especially for the code segment
showing how to do it.

Best,
Mario

On Oct 8, 2017 4:43 AM, "Andreas Lochbihler" <andreas.lochbihler at inf.ethz.ch>
wrote:

> Hi Mario,
>
> I agree with Andrei that structural induction on rose trees should not
> depend on the order of the subtrees in the list, as you only have one
> inductive property. With the old datatype package, nested datatype
> recursion was mapped to mutual recursion (as shown by Jeremy below) where
> you could specify *two* inductive predicates (one for trees and one for
> lists of trees) for the induction. If this is what you want, you can have
> the datatype package generate the appropriate rule:
>
> datatype_compat tree
>
> thm compat_tree_tree_list.induct
>
> Hope this helps,
> Andreas
>
> On 08/10/17 12:59, Jeremy Dawson wrote:
>
>> Hi Mario,
>>
>> What is the induction principle you get, and what is the one you want?
>>
>> The reason I ask is because, using the old datatype package, I get
>>
>>  > set show_types ;
>> val it = true : bool
>>  > tree.induct ;
>> val it =
>>     "[| !!nat::nat. (?P1.0::tree => bool) (Node nat);
>>           !!list::tree list.
>>              (?P2.0::tree list => bool) list ==> ?P1.0 (Branch list);
>>           ?P2.0 [];
>>           !!(tree::tree) list::tree list.
>>              [| ?P1.0 tree; ?P2.0 list |] ==> ?P2.0 (tree # list) |]
>>        ==> ?P1.0 (?tree::tree) & ?P2.0 (?list::tree list)" : Thm.thm
>>
>> which doesn't use the "set" predicate at all
>>
>> Cheers,
>>
>> Jeremy
>>
>> On 08/10/17 16:57, Mario Alvarez wrote:
>>
>>> Hello Isabelle Users,
>>>
>>> I can't figure out how to get Isabelle to generate a sufficiently general
>>> induction principle for the following type:
>>>
>>> datatype tree =
>>> Node "nat"
>>> | Branch "tree list"
>>>
>>> The induction principle generated here is not general enough: it applies
>>> the "set" predicate to the list argument of Branch, but for my purposes I
>>> also care about the order of the trees in that list (i.e., applying "set"
>>> to the argument loses too much information, the order of elements)
>>>
>>> I could define a mutually inductive type to capture the tree lists in the
>>> Branch case, but this seems inelegant: I'd like to be able to use
>>> preexisting abstractions and theorems about lists when reasoning with my
>>> data structure.
>>>
>>> How do I solve this? I've poked around Google a fair bit but haven't
>>> found
>>> an answer.
>>>
>>> Thanks,
>>> Mario Alvarez
>>>
>>>
>>



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