Theory Datatype_Selectors

theory Datatype_Selectors
imports Main
begin

text‹
  Running Example: ‹datatype_new iptrule_match = is_Src: Src (src_range: ipt_iprange)›

  A discriminator ‹disc› tells whether a value is of a certain constructor.
    Example: ‹is_Src›

  A selector ‹sel› select the inner value.
    Example: ‹src_range›

  A constructor ‹C› constructs a value
    Example: ‹Src›


  The are well-formed if the belong together.
›
fun wf_disc_sel :: "(('a ⇒ bool) × ('a ⇒ 'b)) ⇒ ('b ⇒ 'a) ⇒ bool" where
  "wf_disc_sel (disc, sel) C ⟷ (∀a. disc a ⟶ C (sel a) = a) ∧ (∀a. ⌦‹disc (C a) ⟶› sel (C a) = a)"

(* should the following be added to the definition?
 the discriminator is true for all C independent of the a
 for example: is_Src_IP is true for all Src_IPs, independent of the numberic value of the ip.
lemma "wf_disc_sel (disc, sel) C ⟹ (∃a. disc (C a)) ⟶ (∀a. disc (C a))"
*)

declare wf_disc_sel.simps[simp del]

end