Reasoning about explicit specification logic

Reasoning

[View seq.thm]

Click on a command or tactic to see a detailed view of its use.

Kind   nat, tm, ty       type.
Kind   atm, atmlist      type.

Type   z                 nat.
Type   s                 nat -> nat.
Type   app               tm -> tm -> tm.
Type   abs               (tm -> tm) -> tm.
Type   arrow             ty -> ty -> ty.
Type   nl                atmlist.
Type   cons              atm -> atmlist -> atmlist.

Type   eval              tm -> tm -> atm.
Type   of                tm -> ty -> atm.

Type   tt                o.
Type   atom              atm -> o.
Type   or, and           o -> o -> o.
Type   imp               atm -> o -> o.
Type   all               (tm -> o) -> o.
Type   ex                (tm -> o) -> o.

Close nat, tm, ty.


Define nat : nat -> prop by
  nat z ;
  nat (s N) := nat N.

Define lt : nat -> nat -> prop by
  lt z (s N) ;
  lt (s M) (s N) := lt M N.

Define prog : atm -> o -> prop by
  prog (eval (abs R) (abs R)) tt ;
  prog (eval (app P Q) V)
       (and (atom (eval P (abs R)))
            (atom (eval (R Q) V))) ;

  prog (of (abs R) (arrow A B))
       (all x\ imp (of x A) (atom (of (R x) B))) ;
  prog (of (app P Q) B)
       (and (atom (of P (arrow A B)))
            (atom (of Q A))).

Define mem : atm -> atmlist -> prop by
  mem A (cons A L) ;
  mem A (cons B L) := mem A L.

Define seq : nat -> atmlist -> o -> prop by
  seq (s N) L tt ;
  seq (s N) L (atom A) := mem A L ;
  seq (s N) L (or A B) := seq N L A ;
  seq (s N) L (or A B) := seq N L B ;
  seq (s N) L (and A B) := seq N L A /\ seq N L B ;
  seq (s N) L (imp A B) := seq N (cons A L) B ;
  seq (s N) L (all G) := nabla x, seq N L (G x) ;
  seq (s N) L (ex G) := exists X, seq N L (G X) ;
  seq (s N) L (atom A) := exists B, prog A B /\ seq N L B.

Theorem seq_subset : forall L1 L2 G N,
  seq N L1 G -> (forall X, mem X L1 -> mem X L2) -> seq N L2 G.

Theorem seq_lt : forall L G N M,
  lt M N -> seq M L G -> seq N L G.

Theorem nat_lt : forall A B,
  nat A -> nat B -> lt A B \/ A = B \/ lt B A.

Theorem seq_cut : forall K L G N M,
  nat N -> seq N (cons K L) G -> nat M -> seq M L (atom K) ->
    exists P, nat P /\ seq P L G.

%% Another important result is that nabla variablts can be treated as
%% universally quantified inside of seq. That is, we can always
%% instantiate them. Furthermore, this instantiation does not increase
%% the proof height.

Theorem mem_inst : forall L A T, nabla (x:tm),
  mem (A x) (L x) -> mem (A T) (L T).

Theorem prog_inst : forall A B T, nabla (x:tm),
  prog (A x) (B x) -> prog (A T) (B T).

Theorem seq_inst : forall N L G T, nabla (x:tm),
  seq N (L x) (G x) -> seq N (L T) (G T).

Theorem lt_s : forall A B,
  lt A B -> lt A (s B).

Theorem sr : forall E V A M N N',
  nat N' -> lt N N' -> seq N nl (atom (eval E V)) ->
  nat M -> seq M nl (atom (of E A)) ->
  exists P, nat P /\ seq P nl (atom (of V A)).

Define tridot : atmlist -> o -> prop by
  tridot L G := exists N, nat N /\ seq N L G.

% lem:deriv-forward
Theorem lem1 :
  forall L, tridot L tt.

Theorem lem2 :
  forall L G1 G2, tridot L G1 -> tridot L (or G1 G2).

Theorem lem3 :
  forall L G1 G2, tridot L G2 -> tridot L (or G1 G2).

Theorem lem4 :
  forall L G1 G2, tridot L G1 -> tridot L G2 -> tridot L (and G1 G2).

Theorem lem5 :
  forall L A G, tridot (cons A L) G -> tridot L (imp A G).

Theorem lem6 :
  forall L G, (nabla x, tridot L (G x)) -> tridot L (all G).

Theorem lem7 :
  forall L G T, tridot L (G T) -> tridot L (ex G).