TAPL Typed Arithmetic Expressions

system.slf

package tapl;

terminals true false if then else value steporvalue Bool

syntax

t ::= true |
      false |
      if t then t else t

T ::= Bool

// a judgement is a statement whose derivation is justified
// by a tree of rules labeled by inference rules
judgment eval: t -> t

// a judgement is followed by a series of inference rules
// that define the judgment's semantics

----------------------------- e-iftrue
if true then t2 else t3 -> t2


------------------------------ e-iffalse
if false then t2 else t3 -> t2


t1 -> t1'
----------------------------------------------- e-if
if t1 then t2 else t3 -> if t1' then t2 else t3


judgment typing: t : T


----------- t-true
true : Bool


----------- t-false
false: Bool

t1 : Bool
t2 : T
t3 : T
------------------------- t-if
if t1 then t2 else t3 : T

judgment values: t value


---------- v-true
true value


----------- v-false
false value


judgment steporvalue: t steporvalue

t value
------------- sv-values
t steporvalue

t -> t'
------------- sv-step
t steporvalue


theorem progress:
  forall d1: t : T
  exists t steporvalue.

  d2: t steporvalue by induction on d1:
    case rule

      ---------------- t-true
      dtp: true : Bool
    is
      d3: t value by rule v-true
      d4: t steporvalue by rule sv-values on d3
    end case

    case rule

      ----------------- t-false
      dtp: false : Bool
    is
      d3: t value by rule v-false
      d4: t steporvalue by rule sv-values on d3
    end case

    case rule
      dip1: t1 : Bool
      dip2: t2 : T
      dip3: t3 : T
      ------------------------------- t-if
      dic1: if t1 then t2 else t3 : T
    is
      d3: t1 steporvalue by induction hypothesis on dip1
      d4: t steporvalue by case analysis on d3:
        case rule
          dsvp: t' value
          -------------------- sv-values
          dsvc: t' steporvalue
        is
          d5: t steporvalue by case analysis on dsvp:
            case rule

              ---------------- v-true
              dstp: true value
            is
              d6: if t1 then t2 else t3 -> t2 by rule e-iftrue
              d7: t steporvalue by rule sv-step on d6
            end case

            case rule

              ----------------- v-false
              dsfp: false value
            is
              d6: if t1 then t2 else t3 -> t2 by rule e-iffalse
              d7: t steporvalue by rule sv-step on d6
            end case

          end case analysis
        end case

        case rule
          dsp: t' -> t''
          ------------------- sv-step
          dsc: t' steporvalue
        is
          d5: if t1 then t2 else t3 -> if t'' then t2 else t3 by rule e-if on dsp
          d6: t steporvalue by rule sv-step on d5
        end case
      end case analysis
    end case
  end induction
end theorem