<commit_before>(*  Title:      CCL/ex/List.thy
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge
*)

header {* Programs defined over lists *}

theory List
imports Nat
begin

definition map :: "[i=>i,i]=>i"
  where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"

definition comp :: "[i=>i,i=>i]=>i=>i"  (infixr "\<circ>" 55)
  where "f \<circ> g == (%x. f(g(x)))"

definition append :: "[i,i]=>i"  (infixr "@" 55)
  where "l @ m == lrec(l,m,%x xs g. x$g)"

axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
  where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"

definition filter :: "[i,i]=>i"
  where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"

definition flat :: "i=>i"
  where "flat(l) == lrec(l,[],%h t g. h @ g)"

definition partition :: "[i,i]=>i" where
  "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
                            if f`x then part(xs,x$a,b) else part(xs,a,x$b))
                    in part(l,[],[])"

definition insert :: "[i,i,i]=>i"
  where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"

definition isort :: "i=>i"
  where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"

definition qsort :: "i=>i" where
  "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
                                   let p be partition(f`h,t)<commit_msg>proper fact binding;<commit_after>(*  Title:      CCL/ex/List.thy
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge
*)

header {* Programs defined over lists *}

theory List
imports Nat
begin

definition map :: "[i=>i,i]=>i"
  where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"

definition comp :: "[i=>i,i=>i]=>i=>i"  (infixr "\<circ>" 55)
  where "f \<circ> g == (%x. f(g(x)))"

definition append :: "[i,i]=>i"  (infixr "@" 55)
  where "l @ m == lrec(l,m,%x xs g. x$g)"

axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
  where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"

definition filter :: "[i,i]=>i"
  where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"

definition flat :: "i=>i"
  where "flat(l) == lrec(l,[],%h t g. h @ g)"

definition partition :: "[i,i]=>i" where
  "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
                            if f`x then part(xs,x$a,b) else part(xs,a,x$b))
                    in part(l,[],[])"

definition insert :: "[i,i,i]=>i"
  where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"

definition isort :: "i=>i"
  where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"

definition qsort :: "i=>i" where
  "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
                                   let p be partition(f`h,t)
{'fraction_non_alphanumeric': 0.21888111888111889, 'fraction_numerical': 0.006993006993006993, 'mean_word_length': 3.0639204545454546, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7617366', 'n_tokens_mistral': 1233, 'n_tokens_neox': 1185, 'n_words': 334}