Theory Datatype_Selectors

theory Datatype_Selectors
imports Main

  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]