Qcert.Basic.TypeSystem.TBrandModel

Section TBrandModel.



  Definition sub_brand_context {br:brand_relation} {ftype:foreign_type} (m1 m2:brand_context) :=
    subtype (brand_context_Rec m1) (brand_context_Rec m2).

  Section brand_model_types.
    Context {ftype:foreign_type} {br:brand_relation} {m:brand_context}.

    Definition brand_model_domain_t
      := ∀ a, In a (domain brand_relation_brands) →
                   In a (domain brand_context_types).

    Definition brand_model_subtype_weak_t :=
      ∀ a b τa,
        In (a,b) brand_relation_brands →
        In (a,τa) brand_context_types →
        ∃ (τb:rtype),
          In (b,τb) brand_context_types ∧
          subtype τa τb.

    Definition brand_model_subtype_t :=
      ∀ a b τa,
        In (a,b) brand_relation_brands →
        In (a,τa) brand_context_types →
        {τb:rtype |
         In (b,τb) brand_context_types ∧ subtype τa τb}.

    Section brand_model_types_dec.

Lemma brand_model_domain_dec :
  {brand_model_domain_t }
  + {¬ brand_model_domain_t}.

Lemma brand_model_subtype_weak_dec :
  {brand_model_subtype_weak_t}
  + {¬ brand_model_subtype_weak_t}.

    End brand_model_types_dec.

End brand_model_types.

  Context {ftype:foreign_type}.

  Class brand_model :=
    mkBrand_model {
        
        brand_model_relation :> brand_relation;
        brand_model_context :> brand_context;
        brand_model_domain_b :
         holds (brand_model_domain_dec);
            
        brand_model_subtype_weak_b :
           holds (brand_model_subtype_weak_dec)
      }.

Section brand_model_prop.
  Context {m:brand_model}.
Lemma brand_model_domain :
  brand_model_domain_t.

Lemma brand_model_subtype_weak :
  brand_model_subtype_weak_t.

Lemma brand_model_subtype :
  brand_model_subtype_t.

  End brand_model_prop.

  Lemma brand_model_ext a b pf1 pf2 pf1' pf2' :
    mkBrand_model a b pf1 pf2 = mkBrand_model a b pf1' pf2'.

  Definition make_brand_model (b:brand_relation) (m:brand_context)
             (pf:
             (is_true (brand_model_domain_dec)
            && is_true (brand_model_subtype_weak_dec)
             ) = true) : brand_model.

  Definition make_brand_model_fails (b:brand_relation) (m:brand_context) : option brand_model.

  Program Definition empty_brand_model := make_brand_model (mkBrand_relation nil _ _) (mkBrand_context nil _).

End TBrandModel.