Extensibella Example: mtc:natCase

Language Specification

File: defs.sos

[Reduce File] [Raw File] 
Module mtc:natCase

Builds on mtc:arith

e ::= ...
    | natCase(e, e, string, e)
    /*case E of {z => Z; s X => S}  is  natCase(E, Z, X, S)*/


typeOf G E natTy
typeOf G Z Ty
typeOf (X, natTy)::G S Ty
------------------------------- [T-NatCase]
typeOf G natCase(E, Z, X, S) Ty



eval G E numVal(z)
eval G Z V
---------------------------- [E-NatCase-Z]
eval G natCase(E, Z, X, S) V


eval G E numVal(s(N))
eval (X, numVal(N))::G S V
---------------------------- [E-NatCase-S]
eval G natCase(E, Z, X, S) V



evalStep E E1
------------------------------------------------- [ES-NatCase-Step]
evalStep natCase(E, Z, X, S) natCase(E1, Z, X, S)


----------------------------------- [ES-NatCase-Z]
evalStep natCase(num(z), Z, X, S) Z


subst X num(N) S S1
--------------------------------------- [ES-NatCase-S]
evalStep natCase(num(s(N)), Z, X, S) S1



subst X R E E1
subst X R Z Z1
--------------------------------------------------- [S-NatCase-Same]
subst X R natCase(E, Z, X, S) natCase(E1, Z1, X, S)


X != Y
subst X R E E1
subst X R Z Z1
subst X R S S1
---------------------------------------------------- [S-NatCase-Diff]
subst X R natCase(E, Z, Y, S) natCase(E1, Z1, Y, S1)






---------------------------------- [Proj-NatCase]
|{e}- natCase(E, Z, X, S) ~~> nilE

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:natCase.

Prove mtc:arith:fix_nat.


Prove mtc:shared_declarations:type_preservation. [Show Proof]



Prove mtc:shared_declarations:value_evalStep_false.


Prove mtc:shared_declarations:subst_unique. [Show Proof]



Prove mtc:shared_declarations:evalStep_unique. [Show Proof]



Prove mtc:shared_declarations:ty_lookup. [Show Proof]



Prove mtc:shared_declarations:subst_preservation. [Show Proof]



Prove mtc:shared_declarations:evalStep_type_preservation. [Show Proof]



Prove mtc:shared_declarations:canonical_form.


Prove mtc:shared_declarations:subst_is. [Show Proof]



Prove mtc:shared_declarations:evalStep_is. [Show Proof]



Prove mtc:shared_declarations:subst_total. [Show Proof]



Prove mtc:shared_declarations:progress. [Show Proof]
Back to example home