---

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

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

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

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

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

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

Definition: ml_match_pair
ml_match_pair(e;e1,t1.p1[e1; t1];e2,t2.p2[e2; t2];t) ==
  if e is a pair then let e1,e2 = e 
                      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 0 else let a.as = l in 1 + 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 a.as = l 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) ∈ B 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 = L 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) ∈ A List) supposing valueall-type(A) ∧ A

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

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

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

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

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

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

Definition: ml-insert-int
ml-insert-int(x;l) ==
  fix((λinsert_int,x,l. if null(l)
                       then [x]
                       else let a.as = l 
                            in if x <z a + 1 then [x / l] else let y = 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 x else let a.b = l 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) ∈ T 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) ∈ T List) supposing valueall-type(T)

Definition: ml-maprevappend
ml-maprevappend(f;as;bs) ==
  fix((λrevappend,f,l,x. if null(l) then x else let a.b = l 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) ∈ T List) supposing valueall-type(T) ∧ valueall-type(A) ∧ A

Lemma: eager-map-append-sq
∀[T:Type]
  ∀[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
∀[T,A,B:Type].
  ∀[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
∀[T,A,B:Type].
  ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].  (ml-prodmap(f;as;bs) ∈ T 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 a.as = l 
                            in if x <z a + 1 then [x / l] else [a / insert_int(x)(as)] 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_merge_int
ml_merge_int(as;bs) ==
  λas,bs. ml-reduce(fix((λinsert_int,x,l. if null(l)
                                         then [x]
                                         else let a.as = l 
                                              in if x <z a + 1 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 = L in if n <z 1 then x 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 a 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 x and list item a):
                                 f[x;a]
                                over list:
                                  l
                                with starting value:
                                 y) 
  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 <z x then x else -x fi (x)

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

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



Home Index