Extensibella: Extensibella Example: mtc:bool

Language Specification

File: defs.sos

Module mtc:bool

Builds on mtc:shared_declarations

e ::= ...
    | trueE
    | falseE
    | ifThenElse(e, e, e)

v ::= ...
    | trueVal
    | falseVal

ty ::= ...
     | boolTy


--------------------- [T-True]
typeOf G trueE boolTy


---------------------- [T-False]
typeOf G falseE boolTy


typeOf G C boolTy
typeOf G T Ty
typeOf G F Ty
------------------------------- [T-IfThenElse]
typeOf G ifThenElse(C, T, F) Ty



-------------------- [E-True]
eval G trueE trueVal


---------------------- [E-False]
eval G falseE falseVal


eval G C trueVal
eval G T V
---------------------------- [E-IfThenElse-True]
eval G ifThenElse(C, T, F) V


eval G C falseVal
eval G F V
---------------------------- [E-IfThenElse-False]
eval G ifThenElse(C, T, F) V



------------------------ [VT-True]
valueType trueVal boolTy


------------------------- [VT-False]
valueType falseVal boolTy



evalStep C C1
------------------------------------------------- [ES-If-Step]
evalStep ifThenElse(C, T, F) ifThenElse(C1, T, F)


---------------------------------- [ES-If-True]
evalStep ifThenElse(trueE, T, F) T


----------------------------------- [ES-If-False]
evalStep ifThenElse(falseE, T, F) F



----------- [V-True]
value trueE


------------ [V-False]
value falseE



--------------------- [S-True]
subst X R trueE trueE


----------------------- [S-False]
subst X R falseE falseE


subst X R C C1
subst X R T T1
subst X R F F1
---------------------------------------------------- [S-If]
subst X R ifThenElse(C, T, F) ifThenElse(C1, T1, F1)



------------------ [C-BoolTy-True]
canon boolTy trueE


------------------- [T-BoolTy-False]
canon boolTy falseE






-------------------- [Proj-True]
|{e}- trueE ~~> nilE


--------------------- [Proj-False]
|{e}- falseE ~~> nilE


---------------------------------- [Proj-IfThenElse]
|{e}- ifThenElse(C, T, F) ~~> nilE


---------------------- [Proj-TrueVal]
|{v}- trueVal ~~> nilV


----------------------- [Proj-FalseVal]
|{v}- falseVal ~~> nilV


----------------------- [Proj-BoolTy]
|{ty}- boolTy ~~> nilTy

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

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

Module mtc:bool.

Prove mtc:shared_declarations:type_preservation. [Show Proof]

%E-True
 case Ty. search.
%E-False
 case Ty. search.
%E-IfThenElse-True
 Ty: case Ty. apply IH to _ Ty1 Ev2. search.
%E-IfThenElse-False
 Ty: case Ty. apply IH to _ Ty2 Ev2. search.


Prove mtc:shared_declarations:value_evalStep_false. [Show Proof]

%V-True
 case Ev.
%V-False
 case Ev.


Prove mtc:shared_declarations:subst_unique. [Show Proof]

%S-True
 case SB. search.
%S-False
 case SB. search.
%S-If
 SB: case SB. apply IH to SA1 SB. apply IH to SA2 SB1.
 apply IH to SA3 SB2. search.


Prove mtc:shared_declarations:evalStep_unique. [Show Proof]

%ES-If-Step
 EvB: case EvB.
   %ES-If-Step
    apply IH to EvA1 EvB. search.
   %ES-If-True
    case EvA1.
   %ES-If-False
    case EvA1.
%ES-If-True
 EvB: case EvB.
   %ES-If-Step
    case EvB.
   %ES-If-True
    search.
%ES-If-False
 EvB: case EvB.
   %ES-If-Step
    case EvB.
   %ES-If-False
    search.


Prove mtc:shared_declarations:ty_lookup. [Show Proof]

%T-True
 search.
%T-False
 search.
%T-IfThenElse
 apply IH to Ty1 L. apply IH to Ty2 L. apply IH to Ty3 L. search.


Prove mtc:shared_declarations:subst_preservation. [Show Proof]

%S-True
 case Ty. search.
%S-False
 case Ty. search.
%S-If
 Ty: case Ty. apply IH to Ty S1 RTy. apply IH to Ty1 S2 RTy.
 apply IH to Ty2 S3 RTy. search.


Prove mtc:shared_declarations:evalStep_type_preservation. [Show Proof]

%ES-If-Step
 Ty: case Ty. apply IH to Ty Ev1. search.
%IS-If-True
 case Ty. search.
%ES-If-False
 case Ty. search.


Prove mtc:shared_declarations:canonical_form. [Show Proof]

%C-BoolTy-True
 case Ty. search.
%C-BoolTy-False
 case Ty. search.


Prove mtc:shared_declarations:subst_is. [Show Proof]

%S-True
 search.
%S-False
 search.
%S-If
 case IsE. apply IH to _ _ S1. apply IH to _ _ S2. apply IH to _ _ S3.
 search.


Prove mtc:shared_declarations:evalStep_is. [Show Proof]

%ES-If-Step
 case IsE. apply IH to _ Ev1. search.
%ES-If-True
 case IsE. search.
%ES-If-False
 case IsE. search.


Prove mtc:shared_declarations:subst_total. [Show Proof]

%trueE
 search.
%falseE
 search.
%ifThenElse
 apply IH to IsE1 IsX IsR. apply IH to IsE2 IsX IsR.
 apply IH to IsE3 IsX IsR. search.


Prove mtc:shared_declarations:progress. [Show Proof]

%T-True
 search.
%T-False
 search.
%T-IfThenElse
 case IsE. Or: apply IH to _ Ty1. E: case Or.
   %value C
    C: apply canonical_form to E Ty1. case C.
      %C-BoolTy-True
       search.
      %C-BoolTy-False
       search.
   %evalStep C E'
    search.

Back to example home