Re: [isabelle] extending well-founded partial orders to total well-founded orders



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






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