Library ucos_correctaux

Require Import include.
Require Export os_program.
Require Export os_spec.
Require Export toptheorem.
Require Export assertion.
Require Export etraceref.
Require Export Classical.
Require Export LibTactics.
Require Export absop.
Require Export inferules.
Require Export soundness.
Require Export tst_prop.
Require Export lemmasfortoptheo.
Require Export auxdef.
Require Export language.
Require Export opsem.
Require Export simulation.
Require Export memory.
Require Export inv_prop.
Require Export os_code_defs.
Require Export ucert.
Require Export List.

Definition Spec:= OSQ_spec.

Definition ucos_init S O:=
  (forall o tid, (projS S tid) = Some o ->
                 forall ab, sat ((pair o O),ab) (init_asrt I)) /\ eqdomSO S O.

Lemma api_internal_fun_nsame:
  no_fun_same os_api os_internal.

Lemma os_no_call_api:
  no_call_api_os os_api os_internal os_interrupt.

Lemma good_fun_api:
  forall (f : fid) (t : type) (d1 d2 : decllist) (s : stmts),
    os_api f = Some (t, d1, d2, s) ->
    good_decllist (revlcons d1 d2) = true /\ GoodStmt´ s.

Lemma good_fun_internal:
  forall (f : fid) (t : type) (d1 d2 : decllist) (s : stmts),
    os_internal f = Some (t, d1, d2, s) ->
    good_decllist (revlcons d1 d2) = true /\ GoodStmt´ s.

Lemma good_i: GoodI I GetHPrio.

Lemma eqdomos_p: eqdomOS (os_api, os_internal, os_interrupt) (api_spec, int_spec, GetHPrio).

Lemma eqdom_internal_lh: EqDom os_internal Spec.