Definition: ml_apply
f(x) ==  let y ⟵ in y

Lemma: ml_apply-sq
[A:Type]. ∀[f:Top]. ∀[x:A].  f(x) supposing valueall-type(A)

Lemma: ml_apply-sqle
[f,x:Base].  f(x) ≤ supposing ¬is-exception(f(x))

Lemma: ml_apply_wf
[A,B:Type]. ∀[f:A ⟶ B]. ∀[x:A].  f(x) ∈ supposing valueall-type(A)

Definition: spreadcons
let a.b in t[a; b] ==  let a,b in t[a; b]

Lemma: spreadcons_wf
[T,A:Type]. ∀[t:T ⟶ (T List) ⟶ A]. ∀[l:T List].  let a.b in t[a;b] ∈ supposing 0 < ||l||

Definition: ml_match_pair
ml_match_pair(e;e1,t1.p1[e1; t1];e2,t2.p2[e2; t2];t) ==
  if is pair then let e1,e2 
                      in let b1,t1 p1[e1; t] 
                         in if b1 then p2[e2; t1] else <ff, t1> fi  otherwise <ff, t>

Definition: ml_match_nil
ml_match_nil(e;t) ==  <null(e), t>

Lemma: ml_match_nil_wf
[T:Type]. ∀[e:Top List]. ∀[t:T].  (ml_match_nil(e;t) ∈ 𝔹 × T)

Definition: ml-length
ml-length(l) ==  fix((λlength,l. if null(l) then else let in length(as) fi ))(l)

Lemma: ml-length-sq
[T:Type]. ∀[l:T List]. (ml-length(l) ||l||) supposing valueall-type(T)

Lemma: ml-length_wf
[T:Type]. ∀[l:T List]. (ml-length(l) ∈ ℕsupposing valueall-type(T)

Definition: ml-map
ml-map(f;l) ==  fix((λmap,f,l. if null(l) then [] else let in [f(a) map(f)(as)] fi ))(f)(l)

Lemma: ml-map-sq
[A,B:Type].  ∀[f:A ⟶ B]. ∀[l:A List].  (ml-map(f;l) map(f;l)) supposing (valueall-type(A) ∧ A) ∧ value-type(B)

Lemma: ml-map_wf
[A,B:Type].  ∀[f:A ⟶ B]. ∀[l:A List].  (ml-map(f;l) ∈ List) supposing (valueall-type(A) ∧ A) ∧ value-type(B)

Definition: ml-filter
ml-filter(P;L) ==
  fix((λfilter,P,L. if null(L) then [] else let x.y in if P(x) then [x filter(P)(y)] else filter(P)(y) fi  fi ))(P\000C)(L)

Lemma: ml-filter-sq
[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[l:A List].  (ml-filter(P;l) filter(P;l)) supposing valueall-type(A) ∧ A

Lemma: ml-filter_wf
[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[l:A List].  (ml-filter(P;l) ∈ List) supposing valueall-type(A) ∧ A

Definition: ml-reduce
ml-reduce(f;b;l) ==  fix((λreduce,f,b,l. if null(l) then else let in f(a)(reduce(f)(b)(as)) fi ))(f)(b)(l)

Lemma: ml-reduce-sq
  (∀[f:A ⟶ B ⟶ B]. ∀[l:A List]. ∀[b:B].  (ml-reduce(f;b;l) reduce(f;b;l))) supposing 
     ((valueall-type(A) ∧ A) and 

Lemma: ml-reduce_wf
  (∀[f:A ⟶ B ⟶ B]. ∀[l:A List]. ∀[b:B].  (ml-reduce(f;b;l) ∈ B)) supposing 
     ((valueall-type(A) ∧ A) and 

Definition: ml-accumulate
ml-accumulate(f;b;l) ==  fix((λaccumulate,f,b,l. if null(l) then else let in accumulate(f)(f(b)(a))(as) fi ))\000C(f)(b)(l)

Lemma: ml-accumulate-sq
  (∀[f:B ⟶ A ⟶ B]. ∀[l:A List]. ∀[b:B].
     (ml-accumulate(f;b;l) accumulate (with value and list item a):
                             over list:
                             with starting value:
                              b))) supposing 
     ((valueall-type(A) ∧ A) and 

Lemma: ml-accumulate_wf
  (∀[f:B ⟶ A ⟶ B]. ∀[l:A List]. ∀[b:B].  (ml-accumulate(f;b;l) ∈ B)) supposing 
     ((valueall-type(A) ∧ A) and 

Definition: ml-insert-int
ml-insert-int(x;l) ==
  fix((λinsert_int,x,l. if null(l)
                       then [x]
                       else let 
                            in if x <then [x l] else let insert_int(x)(as) in [a y] fi 
                       fi ))(x)(l)

Lemma: ml-insert-int-sq
[l:ℤ List]. ∀[x:ℤ].  (ml-insert-int(x;l) insert-int(x;l))

Lemma: ml-insert-int_wf
[l:ℤ List]. ∀[x:ℤ].  (ml-insert-int(x;l) ∈ ℤ List)

Definition: ml-revappend
ml-revappend(as;bs) ==  fix((λrevappend,l,x. if null(l) then else let a.b in revappend(b)([a x]) fi ))(as)(bs)

Lemma: ml-revappend-sq
[T:Type]. ∀[as,bs:T List].  (ml-revappend(as;bs) rev(as) bs) supposing valueall-type(T)

Lemma: ml-revappend_wf
[T:Type]. ∀[as,bs:T List].  (ml-revappend(as;bs) ∈ List) supposing valueall-type(T)

Definition: ml-append
ml-append(as;bs) ==  fix((λappend,as,bs. if null(as) then bs else let a.more as in [a append(more)(bs)] fi ))(as)(bs\000C)

Lemma: ml-append-sq
[T:Type]. ∀[as,bs:T List].  (ml-append(as;bs) eager-append(as;bs)) supposing valueall-type(T)

Lemma: ml-append_wf
[T:Type]. ∀[as,bs:T List].  (ml-append(as;bs) ∈ List) supposing valueall-type(T)

Definition: ml-maprevappend
ml-maprevappend(f;as;bs) ==
  fix((λrevappend,f,l,x. if null(l) then else let a.b in revappend(f)(b)([f(a) x]) fi ))(f)(as)(bs)

Lemma: ml-maprevappend-sq
[T,A:Type]. ∀[f:A ⟶ T].
  ∀[as:A List]. ∀[bs:T List].  (ml-maprevappend(f;as;bs) map(f;rev(as)) bs) 
  supposing valueall-type(T) ∧ valueall-type(A) ∧ A

Lemma: ml-maprevappend_wf
[T,A:Type]. ∀[f:A ⟶ T].
  ∀[as:A List]. ∀[bs:T List].  (ml-maprevappend(f;as;bs) ∈ List) supposing valueall-type(T) ∧ valueall-type(A) ∧ A

Lemma: eager-map-append-sq
  ∀[A:Type]. ∀[f:A ⟶ T]. ∀[as:A List]. ∀[bs:T List].  (eager-map-append(f;as;bs) map(f;rev(as)) bs) 
  supposing value-type(T)

Definition: ml-prodmap
ml-prodmap(f;as;bs) ==
  fix((λprodmap,f,as,bs. if null(as) then [] else let a.more as in ml-maprevappend(f(a);bs;prodmap(f)(more)(bs)) fi ))\000C(f)(as)(bs)

Lemma: ml-prodmap-sq
  ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].  (ml-prodmap(f;as;bs) eager-product-map(f;as;bs)) 
  supposing valueall-type(T) ∧ valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B

Lemma: ml-prodmap_wf
  ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].  (ml-prodmap(f;as;bs) ∈ List) 
  supposing valueall-type(T) ∧ valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B

Definition: ml_insert_int
ml_insert_int(x;l) ==
  fix((λinsert_int,x,l. if null(l)
                       then [x]
                       else let 
                            in if x <then [x l] else [a insert_int(x)(as)] fi 
                       fi )) 

Lemma: ml_insert_int-sq
[l:ℤ List]. ∀[x:ℤ].  (ml_insert_int(x;l) insert-int(x;l))

Lemma: ml_insert_int_wf
[l:ℤ List]. ∀[x:ℤ].  (ml_insert_int(x;l) ∈ ℤ List)

Definition: ml_merge_int
ml_merge_int(as;bs) ==
  λas,bs. ml-reduce(fix((λinsert_int,x,l. if null(l)
                                         then [x]
                                         else let 
                                              in if x <then [x l] else [a insert_int(x)(as)] fi 
                                         fi ));as;bs)(as)(bs)

Lemma: ml_merge_int-sq
[bs,as:ℤ List].  (ml_merge_int(as;bs) merge-int(as;bs))

Lemma: ml_merge_int_wf
[as,bs:ℤ List].  (ml_merge_int(as;bs) ∈ ℤ List)

Definition: ml-select
ml-select(n;L) ==  fix((λselect,n,L. let x,y in if n <then else select(n 1)(y) fi ))(n)(L)

Lemma: ml-select-sq
[T:Type]. ∀[L:T List]. ∀[n:ℤ].  (ml-select(n;L) L[n]) supposing valueall-type(T)

Lemma: ml-select_wf
[T:Type]. ∀[L:T List]. ∀[n:ℕ||L||].  (ml-select(n;L) ∈ T) supposing valueall-type(T)

Definition: ml-gcd
ml-gcd(a;b) ==  fix((λgcd,a,b. if (b =z 0) then else gcd(b)(a rem b) fi ))(a)(b)

Lemma: ml-gcd-sq
[y,x:ℤ].  (ml-gcd(x;y) better-gcd(x;y))

Lemma: ml-gcd_wf
[x,y:ℤ].  (ml-gcd(x;y) ∈ ℤ)

Lemma: eager-accum-list_accum
[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T'].
  eager-accum(x,a.f[x;a];y;l) accumulate (with value and list item a):
                                over list:
                                with starting value:
  supposing valueall-type(T')

Definition: gcd-list
gcd-list(L) ==  eager-accum(a,b.better-gcd(a;b);hd(L);tl(L))

Lemma: gcd-list_wf
[L:ℤ List+]. (gcd-list(L) ∈ ℤ)

Definition: ml-gcd-list
ml-gcd-list(L) ==  ml-accumulate(λa,b. ml-gcd(a;b);hd(L);tl(L))

Lemma: ml-gcd-list-sq
[L:ℤ List+]. (ml-gcd-list(L) gcd-list(L))

Lemma: ml-gcd-list_wf
[L:ℤ List+]. (ml-gcd-list(L) ∈ ℤ)

Definition: ml-absval
ml-absval(x) ==  λx.if 0 <then else -x fi (x)

Lemma: ml-absval-sq
[x:ℤ]. (ml-absval(x) |x|)

Lemma: ml-absval_wf
[x:ℤ]. (ml-absval(x) ∈ ℤ)

Home Index