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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
