Qcert.Basic.Data.RDataNorm

Section RDataNorm.


  Context {fdata:foreign_data}.
  Context (h:brand_relation_t).
  Fixpoint normalize_data (d:data) : data :=
    match d with
      | drec rl ⇒
        drec (rec_sort (map (fun x ⇒ (fst x, normalize_data (snd x))) rl))
      | dcoll l ⇒ dcoll (map normalize_data l)
      | dleft l ⇒ dleft (normalize_data l)
      | dright l ⇒ dright (normalize_data l)
      | dbrand b d ⇒ dbrand (canon_brands h b) (normalize_data d)
      | dforeign fd ⇒ dforeign (foreign_data_normalize fd)
      | _ ⇒ d
    end.

  Inductive data_normalized : data → Prop :=
  | dnunit :
      data_normalized dunit
  | dnnat n :
      data_normalized (dnat n)
  | dnbool b :
      data_normalized (dbool b)
  | dnstring s :
      data_normalized (dstring s)
  | dncoll dl :
      Forall (fun x ⇒ data_normalized x) dl → data_normalized (dcoll dl)
  | dnrec dl :
      Forall (fun d ⇒ data_normalized (snd d)) dl →
      (is_list_sorted ODT_lt_dec (domain dl) = true) →
      data_normalized (drec dl)
  | dnleft l :
      data_normalized l →
      data_normalized (dleft l)
  | dnright r :
      data_normalized r →
      data_normalized (dright r)
  | dnbrand b d :
      is_canon_brands h b →
      data_normalized d →
      data_normalized (dbrand b d)
  | dnforeign fd :
      foreign_data_normalized fd →
      data_normalized (dforeign fd).

  Theorem normalize_normalizes :
    ∀ (d:data), data_normalized (normalize_data d).

  Theorem normalize_normalized_eq {d}:
    data_normalized d →
    normalize_data d = d.

  Lemma map_normalize_normalized_eq c :
        Forall (fun x ⇒ data_normalized (snd x)) c →
        (map
           (fun x0 : string × data ⇒ (fst x0, normalize_data (snd x0)))
           c) = c.

  Corollary normalize_idem d :
    normalize_data (normalize_data d) = normalize_data d.

  Corollary normalize_data_eq_normalized {d} :
    normalize_data d = d → data_normalized d.

  Theorem normalized_data_dec d : {data_normalized d} + {¬ data_normalized d}.

  Lemma data_normalized_dcoll a l :
    (data_normalized a ∧ data_normalized (dcoll l)) ↔
    data_normalized (dcoll (a :: l)).

  Lemma data_normalized_rec_sort_app l1 l2 :
    data_normalized (drec l1) →
    data_normalized (drec l2) →
    data_normalized (drec (rec_sort (l1 ++ l2))).

  Lemma data_normalized_rec_concat_sort l1 l2 :
    data_normalized (drec l1) →
    data_normalized (drec l2) →
    data_normalized (drec (rec_concat_sort l1 l2)).

  Lemma data_normalized_dcoll_in x l :
    In x l →
    data_normalized (dcoll l) →
    data_normalized x.

  Lemma dnrec_nil : data_normalized (drec nil).

  Lemma dnrec_sort c :
    Forall (fun d : string × data ⇒ data_normalized (snd d)) c →
    data_normalized (drec (rec_sort c)).

End RDataNorm.