*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Termination for ordinal-like datatypes*From*: Eddy Westbrook <westbrook at kestrel.edu>*Date*: Tue, 15 Jul 2014 10:13:24 -0700*In-reply-to*: <53C4D534.1090405@in.tum.de>*References*: <8C5FE629-350B-4522-ADB4-623352324731@kestrel.edu> <53C4D534.1090405@in.tum.de>

Thanks so much for the replies; both were very helpful! -Eddy On Jul 15, 2014, at 12:16 AM, Dmitriy Traytel <traytel at in.tum.de> wrote: > Hi Eddy, > > as René said, I also would use primrec wherever possible. However, if you are bound to function you can prove termination by defining a subterm relation and prove that it is wellfounded: > > definition "sub ≡ {(x, Succ x) | x. True} ∪ {(f n, Limit f) | n f. True}" > > lemma subI[intro]: > "(x, Succ x) ∈ sub" > "(f n, Limit f) ∈ sub" > unfolding sub_def by blast+ > > lemma wf_sub[simp]: "wf sub" > proof (rule wfUNIVI) > fix P x > assume "∀x. (∀y. (y, x) ∈ sub ⟶ P y) ⟶ P x" > then show "P x" unfolding sub_def by (induct x) blast+ > qed > > Both of your functions can be then proved terminating via > > termination by (relation "sub <*lex*> sub") auto > > Dmitriy > > On 15.07.2014 03:08, Eddy Westbrook wrote: >> Hi, >> >> I was wondering if someone could help me figure out an easy way to prove termination for functions over ordinal-like datatypes. What I mean by this is datatypes T where one of the constructors for T takes a function that returns type T. The classic one is the ordinals: >> >> datatype ord >> = Zero >> | Succ ord >> | Limit "(nat => ord)” >> >> My question is, what is the easiest and best way to write termination proofs for recursive functions over the type ord? Are there some mechanisms already available, or do I have to define my own inductive proposition or something similar? It looks like all the default mechanisms for proving termination rely on types that satisfy “size”, which ord does not because of the Limit constructor. >> >> For example, I want to define functions like these, which should be terminating: >> >> function ord_plus :: "ord => ord => ord" >> where >> "ord_plus x Zero = x" >> | "ord_plus x (Succ y) = Succ (ord_plus x y)" >> | "ord_plus x (Limit f) = Limit (\<lambda> n . ord_plus x (f n))" >> by pat_completeness auto >> >> function ord_leq :: "ord ⇒ ord ⇒ bool" >> where >> "ord_leq Zero x = True" >> | "ord_leq (Succ x) Zero = False" >> | "ord_leq (Succ x) (Succ y) = ord_leq x y" >> | "ord_leq (Succ x) (Limit f) = (\<exists> n. ord_leq (Succ x) (f n))" >> | "ord_leq (Limit f) y = (\<forall>n . ord_leq (f n) y)" >> by pat_completeness auto >> >> Thanks very much for any help or suggestions. >> -Eddy >

**References**:**[isabelle] Termination for ordinal-like datatypes***From:*Eddy Westbrook

**Re: [isabelle] Termination for ordinal-like datatypes***From:*Dmitriy Traytel

- Previous by Date: [isabelle] newbie questions: theory for sums and Isar syntax
- Next by Date: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Previous by Thread: Re: [isabelle] Termination for ordinal-like datatypes
- Next by Thread: [isabelle] newbie questions: theory for sums and Isar syntax
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list