Sum Types

In the directory lib_sum there is a single file defining the sum type with constructors in1 and in2. Also defined is the case function (essentially the iterator for sum).

 ** Module lib_sum Imports lib_eq_basics
 $sum : (Type)->(Type)->Type(sum)
 $in1_exp : {A:Type}{B:Type}A->sum A B
 $in2_exp : {A:Type}{B:Type}B->sum A B
 $sum_elim :
    {A:Type}{B:Type}{C_sum:(sum A B)->Type}
    ({x2:A}C_sum (in1_exp A B x2))->({x1:B}C_sum (in2_exp A B x1))->
    {z:sum A B}C_sum z
  sum_double_elim = ... :
    {A:Type}{B:Type}{T_sum:(sum A B)->(sum A B)->Type}
    ({x2,x2':A}T_sum (in1_exp A B x2) (in1_exp A B x2'))->
    ({x2:A}{x1':B}T_sum (in1_exp A B x2) (in2_exp A B x1'))->
    ({x1:B}{x2':A}T_sum (in2_exp A B x1) (in1_exp A B x2'))->
    ({x1,x1':B}T_sum (in2_exp A B x1) (in2_exp A B x1'))->{z,z':sum A B}
    T_sum z z'
 ** Label (!sum!) sum
 ** Label (!sum elim!) sum_elim
 ** Label (!sum in1_exp!) in1_exp
 ** Label (!sum in2_exp!) in2_exp
[[A:Type][B:Type][C_sum:(sum A B)->Type]
 [f_in1_exp:{x2:A}C_sum (in1_exp A B x2)]
 [f_in2_exp:{x1:B}C_sum (in2_exp A B x1)][x2:A][x1:B]
    sum_elim A B C_sum f_in1_exp f_in2_exp (in1_exp A B x2)  ==>
    f_in1_exp x2
 || sum_elim A B C_sum f_in1_exp f_in2_exp (in2_exp A B x1)  ==>
    f_in2_exp x1]

  in1 = ... : {s|Type}{t|Type}s->sum s t
  in2 = ... : {s|Type}{t|Type}t->sum s t
  case = ... : {s|Type}{t|Type}{u|Type}(s->u)->(t->u)->(sum s t)->u
  sum_ind = ... :
    {s|Type}{t|Type}{P:(sum s t)->Prop}({x:s}P (in1 x))->
    ({y:t}P (in2 y))->{z:sum s t}P z
  is_in1 = ... : {s|Type}{t|Type}(sum s t)->Prop
  is_in2 = ... : {s|Type}{t|Type}(sum s t)->Prop
  in1_or_in2 = ... : {s|Type}{t|Type}{x:sum s t}(is_in1 x \/ is_in2 x)
  in1_not_in2 = ... : {s|Type}{t|Type}{x|s}not (is_in2 (in1|s|t x))
  in2_not_in1 = ... : {s|Type}{t|Type}{x|t}not (is_in1 (in2|s|t x))
  in1_inj = ... :
    {s|Type}{t|Type}{x,y:s}(Eq (in1|s|t x) (in1|s|t y))->Eq x y
  in2_inj = ... :
    {s|Type}{t|Type}{x,y:t}(Eq (in2|s|t x) (in2|s|t y))->Eq x y