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
