Library LocalVarAlgebraImplem_struct


Require Export AlgebraType.




Definition gammaLocalVar1 : forall (V:Set) (PV:Lattice V),

  Gamma (PowPoset Value) PV -> 

  Gamma (PowPoset LocalVar) (funcTree_Lattice _ PV WordSize).

Proof.

intros V PV g.

refine (gamma_constr _ _

 (fun L l => forall x, (g (applyFunc _ PV _ L x) (l x))) _).

intros.

intros l H1 x.

apply (gamma_monotone g (applyFunc _ PV _ b1 x)); auto.

apply applyFunc_monotone; auto.

Defined.




Definition LocalVarAlgebra1 : forall (V:Set) (PV:Lattice V),

 LocalVar.Connect PV.

intros.

refine (LocalVar.Build_Connect

  (@gammaLocalVar1 V PV) _

  (fun x f => applyFunc _ PV _ f x) _

  (fun x f v => substFunc _ PV _ f x v) _ 

  (fun AbNull => (ArrayLattice.const _ WordSize AbNull)) _).

intros g1 g2 H1.

intros L l.

unfold gammaLocalVar1; simpl.

intros.

apply H1; auto.

intros g x L l H.

inversion_clear H.

inversion_clear H0 in H1.

apply H1.

intros g x L v l H.

inversion_clear H.

inversion_clear H0 in H1 H2.

intros p.

destruct L; simpl.

unfold substLocalVar.

case Var_dec; intros.

rewrite apply_subst1; auto.

destruct p; destruct x; simpl in e; simpl; auto.

rewrite apply_subst2.

apply (H1 p).

destruct p; destruct x; simpl in n; simpl; auto.




intros.

intros l H1 x.

unfold applyFunc.

rewrite (apply_const _ PV).

apply H; auto.

destruct x; auto.

Defined.

Implicit Arguments LocalVarAlgebra1 [V].
Index
This page has been generated by coqdoc