Library NumAlgebraImplem_top
Require Export AlgebraType.
Section Num.
Inductive AbNumTop : Set :=
| top : AbNumTop.
Inductive AbNumTopOrder : AbNumTop -> AbNumTop -> Prop :=
| top_order : forall (v:AbNumTop), (AbNumTopOrder v top).
Definition AbNumTopjoin := fun v1 v2:AbNumTop => top.
Definition AbNumTopPoset : (Poset AbNumTop).
refine (poset_constr _ (fun x y => x=y) _ _ _ (fun x y => x=y) _ _ _).
intuition.
intuition.
intuition; subst; auto.
intuition.
intuition.
intuition; subst; auto.
Defined.
Definition AbNumTopLattice : (Lattice AbNumTop).
refine (lattice_constr _ AbNumTopPoset AbNumTopjoin _ _ _ _ top _ top _ _).
unfold AbNumTopjoin; simpl; intros.
destruct x; auto.
unfold AbNumTopjoin; simpl; intros.
destruct y; auto.
destruct x; destruct y; destruct z; intuition.
intros; left.
destruct x; destruct y; intuition.
destruct x; auto.
destruct x; auto.
intros n.
constructor; intros y (H1,H2).
elim H1; destruct n; destruct y; auto.
Defined.
Definition gammaNumTop : Gamma (PowPoset nat) AbNumTopLattice.
refine (gamma_constr (PowPoset nat) AbNumTopLattice
(fun _ _ => True)
_).
intros b1 b2 H x; auto.
Defined.
Definition gammaTopNumTop : GammaTop (PowPoset nat) AbNumTopLattice.
refine (gammatop_constr gammaNumTop _).
simpl; auto.
Defined.
Definition NumTopAlgebra : Num.Connect.
refine (Num.Build_Connect
gammaTopNumTop
(fun n => top) _
(fun op n1 n2 => top) _).
intros; simpl; auto.
intros op n1 n2 x H; unfold gammaNumTop; simpl; auto.
Defined.
End Num.
Index
This page has been generated by coqdoc