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

Hi Christian,

No, this is not what I had in mind.  Transfinite recursion does not need Zorn.  But I refrain from any further explanations, since hopefully the other route works out for you.

Andrei

--- On Tue, 2/19/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: Tuesday, February 19, 2013, 5:45 AM

Thanks Andrei,

(or the one from the blog post, for that matter) in a concrete proof.

Lets first review my setting (please let me know if any of this is
"strange" in any way). I use the following definitions (mostly from
AFP/Well_Quasi_Orders):

definition irreflp_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"irreflp_on P A = (∀a∈A. ¬ P a a)"
definition transp_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"transp_on P A = (∀x∈A. ∀y∈A. ∀z∈A. P x y ∧ P y z ⟶ P x z)"
definition po_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"po_on P A = (irreflp_on P A ∧ transp_on P A)"
definition total_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"total_on P A = (∀x∈A. ∀y∈A. x = y ∨ P x y ∨ P y x)"
definition wfp_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"wfp_on P A = (¬ (∃f. ∀i. f i ∈ A ∧ P (f (Suc i)) (f i)))"
definition wellorder_on where
"wellorder_on P A = (po_on P A ∧ wfp_on P A ∧ total_on P A)"
definition ext_on where "ext_on P Q A = (∀x∈A. ∀y∈A. Q x y ⟶ P x y)"

For "wfp_on" I derived the following induction schema:

wfp_on_induct:
wfp_on ?P ?A ⟹
?x ∈ ?A ⟹
(⋀y. y ∈ ?A ⟹ (⋀x. x ∈ ?A ⟹ ?P x y ⟹ ?Q x) ⟹ ?Q y) ⟹
?Q ?x

Moreover from Zorn.thy I derived the following variant of the well-order
theorem:

wellorder_on: "∃W. wellorder_on W A"

Let P be the given well-founded partial order on A. Then, we obtain a
well-order W on A by the well-order theorem. Using wfp_on_induct, I can
start a proof

{ fix x
assume "x ∈ A"
with `wfp_on W A`
have "wellorder_on N {y∈A. W^== x} ∧ ext_on N P {y∈A. W^== y x}"
proof (induct rule: wfp_on_induct)

for some appropriate definition of N (using worec (?)). Is that the
transfinite induction you were referring to?

Even if I would succeed with this proof, I don't see how I could derive
"wellorder_on N A & ext_on N P A" from it.

What am I doing wrong?

cheers

chris

On 02/19/2013 09:33 AM, Andrei Popescu wrote:
> 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 ofunderS 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:
> 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?
>