*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Mon, 18 Feb 2013 16:33:21 -0800 (PST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5121CAFB.3040205@gmail.com>

Hi Christian, >> I guess since Isabelle2013 this is now "~~/src/HOL/Cardinals/", right? Right. >> Could you elaborate on the mentioned finite recursion combinator and how it is used? The worec combinator, worec :: "(('a => 'b) => 'a => 'b) => 'a => 'b" (defined in the context of a fixed wellorder r on 'a) is just a slightly more convenient version of wfrec. It is used to define a function f :: 'a => 'b by specifying, for each x :: 'a, the value of f on x in terms of the values of f on all elements less than x w.r.t. r, i.e., in my notation, all elements of underS x. This would ideally employ an operator of type Prod x : 'a. (underS x => 'b) => 'b In HOL, the same is achieved by an "admissible" operator of a less informative type. The only relevant facts are below: definition adm_wo :: "(('a => 'b) => 'a => 'b) => bool" where "adm_wo H ≡ ∀f g x. (∀y ∈ underS x. f y = g y) --> H f x = H g x" lemma worec_fixpoint: assumes "adm_wo H" shows "worec H = H (worec H)" Cheers, Andrei --- On Mon, 2/18/13, Christian Sternagel <c.sternagel at gmail.com> wrote: From: Christian Sternagel <c.sternagel at gmail.com> Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders To: "Andrei Popescu" <uuomul at yahoo.com> Cc: cl-isabelle-users at lists.cam.ac.uk Date: Monday, February 18, 2013, 8:32 AM Dear Andrei, finally deadlines are over for the time being and I found your email again ;) On 01/19/2013 12:22 AM, Andrei Popescu wrote: > My AFP formalization ordinals > > http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml I guess since Isabelle2013 this is now "~~/src/HOL/Cardinals/", right? > (hopefully) provides the necessary ingredients: Initial segments in > Wellorder_Embedding, ordinal sum in theory Constructions_on_Wellorders, > and a transfinite recursion combinator (a small adaptation of the > wellfounded combinator) in theory Wellorder_Relation. Could you elaborate on the mentioned finite recursion combinator and how it is used? thanks in advance, chris

**Follow-Ups**:**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

**References**:**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

- Previous by Date: [isabelle] Conf. Intelligent Computer Mathematics (CICM 2013), July 8-12, 2013, Bath, UK
- Next by Date: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Previous by Thread: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Next by Thread: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Cl-isabelle-users February 2013 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