Derived datetime parser corollaries

theorem Cedar.Thm.Datetime.parse_eq_some_iff_isDatetimeValue (str : String) (d : Spec.Ext.Datetime) : Spec.Ext.Datetime.parse str = some d ↔ IsDatetimeValue str d.val.toInt

Exact parser characterization derived from soundness and completeness: parsing succeeds with d precisely when the declarative grammar relation assigns the input the value d.val.toInt.

theorem Cedar.Thm.Datetime.bind_parse_toString? (d : Spec.Ext.Datetime) : (toString? d).bind Spec.Ext.Datetime.parse = Option.map (fun (x : String) => d) (toString? d)

Total Option formulation of the partial serialization roundtrip.