diff options
author | Robert Norton <rmn30@cam.ac.uk> | 2019-09-04 17:28:22 +0100 |
---|---|---|
committer | Robert Norton <rmn30@cam.ac.uk> | 2019-09-04 17:28:22 +0100 |
commit | e918e17c081bc24bbf2ae213c211b9dabc276324 (patch) | |
tree | 7621be42dcb86adfaf59f4351498dc7325f6bed2 /prover_snapshots/hol4/lib/lem/lem_functionScript.sml | |
parent | 50033a227e89d679cd42b070e7e096586275357c (diff) | |
parent | 3d75de27c854072b82493a73e01c69d27624bf94 (diff) | |
download | sail-riscv-vmem_ext.zip sail-riscv-vmem_ext.tar.gz sail-riscv-vmem_ext.tar.bz2 |
Merge remote-tracking branch 'origin/master' into vmem_ext.vmem_ext
Diffstat (limited to 'prover_snapshots/hol4/lib/lem/lem_functionScript.sml')
-rw-r--r-- | prover_snapshots/hol4/lib/lem/lem_functionScript.sml | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/prover_snapshots/hol4/lib/lem/lem_functionScript.sml b/prover_snapshots/hol4/lib/lem/lem_functionScript.sml new file mode 100644 index 0000000..2f6f52b --- /dev/null +++ b/prover_snapshots/hol4/lib/lem/lem_functionScript.sml @@ -0,0 +1,72 @@ +(*Generated by Lem from function.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_boolTheory lem_basic_classesTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "lem_function" + +(******************************************************************************) +(* A library for common operations on functions *) +(******************************************************************************) + +(*open import Bool Basic_classes*) + +(*open import {coq} `Program.Basics`*) + +(* ----------------------- *) +(* identity function *) +(* ----------------------- *) + +(*val id : forall 'a. 'a -> 'a*) +(*let id x= x*) + + +(* ----------------------- *) +(* constant function *) +(* ----------------------- *) + +(*val const : forall 'a 'b. 'a -> 'b -> 'a*) + + +(* ----------------------- *) +(* function composition *) +(* ----------------------- *) + +(*val comb : forall 'a 'b 'c. ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)*) +(*let comb f g= (fun x -> f (g x))*) + + +(* ----------------------- *) +(* function application *) +(* ----------------------- *) + +(*val $ [apply] : forall 'a 'b. ('a -> 'b) -> ('a -> 'b)*) +(*let $ f= (fun x -> f x)*) + +(*val $> [rev_apply] : forall 'a 'b. 'a -> ('a -> 'b) -> 'b*) +(*let $> x f= f x*) + +(* ----------------------- *) +(* flipping argument order *) +(* ----------------------- *) + +(*val flip : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)*) +(*let flip f= (fun x y -> f y x)*) + + +(* currying / uncurrying *) + +(*val curry : forall 'a 'b 'c. (('a * 'b) -> 'c) -> 'a -> 'b -> 'c*) +val _ = Define ` + ((curry:('a#'b -> 'c) -> 'a -> 'b -> 'c) f= (\ a b . f (a, b)))`; + + +(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*) +val _ = Define ` + ((uncurry:('a -> 'b -> 'c) -> 'a#'b -> 'c) f (a,b)= (f a b))`; + +val _ = export_theory() + |