Library can_change_aop_proof

Require Import include.
Require Import memory.
Require Import memdata.
Require Import assertion.
Require Import absop.
Require Import simulation.
Require Import language.
Require Import opsem.
Require Import os_program.
Require Import os_spec.
Require Import inferules.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import baseTac.
Require Import auxdef.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import derivedrules.
Require Import hoare_conseq.
Require Import symbolic_execution.
Require Import hoare_assign.
Require Import hoare_lemmas.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Set Implicit Arguments.


Theorem can_change_aop_ptrmapsto :
  forall l t v,
    can_change_aop (PV l @ t |-> v).

Theorem can_change_aop_lvarenv :
  forall x t a,
    can_change_aop (L& x @ t == a).

Theorem can_change_aop_gvarenv :
  forall x t a,
    can_change_aop (G& x @ t == a).

Hint Resolve can_change_aop_ptrmapsto can_change_aop_lvarenv can_change_aop_gvarenv : can_change_aop.

Theorem can_change_aop_lvarmapsto :
  forall x t v,
    can_change_aop (LV x @ t |-> v).

Theorem can_change_aop_gvarmapsto :
  forall x t v,
    can_change_aop (GV x @ t |-> v).

Hint Resolve can_change_aop_lvarmapsto can_change_aop_gvarmapsto : can_change_aop.

Theorem can_change_aop_ptrarray´ :
  forall l n t vl,
    can_change_aop (Aarray´ l n t vl).

Hint Resolve can_change_aop_ptrarray´ : can_change_aop.

Theorem can_change_aop_ptrarray :
  forall l t vl,
    can_change_aop (Aarray l t vl).

Hint Resolve can_change_aop_ptrarray : can_change_aop.

Theorem can_change_aop_lvararray :
  forall x t vl,
    can_change_aop (LAarray x t vl).

Theorem can_change_aop_gvararray :
  forall x t vl,
    can_change_aop (GAarray x t vl).

Hint Resolve can_change_aop_lvararray can_change_aop_gvararray : can_change_aop.

Theorem can_change_aop_struct´ :
  forall l dls ls,
    can_change_aop (Astruct´ l dls ls).

Hint Resolve can_change_aop_struct´ : can_change_aop.

Theorem can_change_aop_struct :
  forall l t ls,
    can_change_aop (Astruct l t ls).

Hint Resolve can_change_aop_struct : can_change_aop.


Ltac can_change_aop_solver ::=
  try unfold OSInv;
  try unfold AOSEventFreeList, AOSQFreeList, AOSQFreeBlk, AECBList;
  try unfold AOSMapTbl, AOSUnMapTbl, AOSTCBPrioTbl, AOSIntNesting, AOSTCBList, AOSTCBFreeList;
  try unfold AOSRdyTblGrp, AOSRdyTbl, AOSRdyGrp, AOSTime, AGVars;
  try unfold AOSEvent, AOSEventTbl, AMsgData, AOSQCtr, AOSQBlk, node;
  unfold can_change_aop; fold can_change_aop; intuition auto 1 with can_change_aop;simpl;intros; intuition auto 1 with can_change_aop.

Theorem can_change_aop_sllseg :
  forall h tn t l next,
    can_change_aop (sllseg h tn l t next).

Hint Resolve can_change_aop_sllseg : can_change_aop.

Theorem can_change_aop_node :
  forall x v T,
    can_change_aop (node x v T).

Hint Resolve can_change_aop_node : can_change_aop.
Theorem can_change_aop_msgq :
  forall c d e f,
    can_change_aop (AMsgData c d e f).

Hint Resolve can_change_aop_msgq : can_change_aop.

Theorem can_change_aop_aevtdata:
  forall vl d , can_change_aop (AEventData vl d).

Hint Resolve can_change_aop_aevtdata : can_change_aop.

Theorem can_change_aop_msgqnode :
  forall l vl d c,
    can_change_aop (AEventNode l vl d c).

Hint Resolve can_change_aop_msgqnode : can_change_aop.

Theorem can_change_aop_msgqllseg :
  forall h tn l msgqls,
    can_change_aop (evsllseg h tn l msgqls).

Hint Resolve can_change_aop_msgqllseg : can_change_aop.

Theorem can_change_aop_sll :
  forall h l tp next,
    can_change_aop (sll h l tp next).

Hint Resolve can_change_aop_sll : can_change_aop.

Theorem can_change_aop_dllseg :
  forall h hp t tn l tp pre next,
    can_change_aop (dllseg h hp t tn l tp pre next).

Hint Resolve can_change_aop_dllseg : can_change_aop.

Theorem can_change_aop_tcbdllseg :
  forall h hp t tn l,
    can_change_aop (tcbdllseg h hp t tn l).

Hint Resolve can_change_aop_tcbdllseg : can_change_aop.

Theorem can_change_aop_ecbfsllseg :
  forall ls x y, can_change_aop (ecbf_sllseg x y ls OS_EVENT V_OSEventListPtr).

Hint Resolve can_change_aop_ecbfsllseg: can_change_aop.

Theorem can_change_aop_ecbfsll :
  forall ls x , can_change_aop (ecbf_sll x ls OS_EVENT V_OSEventListPtr).

Hint Resolve can_change_aop_ecbfsll: can_change_aop.

Theorem can_change_aop_qblkfseg :
forall x y ls, can_change_aop (qblkf_sllseg x y ls OS_Q_FREEBLK V_nextblk).

Hint Resolve can_change_aop_qblkfseg: can_change_aop.

Theorem can_change_aop_qblkf :
  forall x ls, can_change_aop (qblkf_sll x ls OS_Q_FREEBLK V_nextblk).

Hint Resolve can_change_aop_qblkf: can_change_aop.

Theorem can_change_aop_OSQInv :
  can_change_aop OSInv.