Hi Michael,
Thanks very much, this saves me lots of time trying to prove something
impossible.
Regards,
Chun Tian
On 16 October 2017 at 00:59, <michael.norr...@data61.csiro.au> wrote:
> The definition is fine, but will not have the nice properties you want
> (e.g., monotonicity) if the domain type is bigger than the range. In
> particular if your domain includes \omega_1 and the range only has
> countable ordinals, then the result of c2a on \omega_1 will be
> unspecified. This is because the RHS of the limit case will be invoking
> sup on the set of all possible ordinals in the range type. Given that, you
> will not be able to prove that monotonicity holds.
>
> Michael
>
> On 15/10/17, 18:26, "Chun Tian" <binghe.l...@gmail.com> wrote:
>
> Hi,
>
> If I have the following recursive function on ordinals, simply
> converting ‘c ordinals into the “same” ‘a ordinals:
>
> (* Construct a 'c ordinal from 'a ordinal *)
> val c2a_def = new_specification (
> "c2a_def", ["c2a"],
> ord_RECURSION |> INST_TYPE [``:'a`` |-> ``:'c``]
> |> ISPEC ``0 :'a ordinal`` (* z *)
> |> Q.SPEC `\x r. ordSUC r` (* sf *)
> |> Q.SPEC `\x rs. sup rs` (* lf *)
> |> SIMP_RULE (srw_ss()) []);
>
> val it =
> |- (c2a 0o = 0) ∧ (∀α. c2a α⁺ = (c2a α)⁺) ∧
> ∀α. 0o < α ∧ islimit α ⇒ (c2a α = sup (IMAGE c2a (preds α))):
> thm
>
> Is my definition correct? (especially for the “lf” part using “sup”)
> And if so, what properties can I expect from this function? Is it at
> least monotone? i.e.
>
> ∀m n. m ≤ n ⇒ c2a m ≤ c2a n
>
> Regards,
>
> Chun Tian
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
