1 files changed, 72 insertions, 0 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_function.thy b/snapshots/isabelle/lib/lem/Lem_function.thy
new file mode 100644
index 00000000..29c1fb04
--- /dev/null
+++ b/snapshots/isabelle/lib/lem/Lem_function.thy
@@ -0,0 +1,72 @@
+chapter \<open>Generated by Lem from function.lem.\<close>
+
+theory "Lem_function" 
+
+imports 
+ 	 Main
+	 "Lem_bool" 
+	 "Lem_basic_classes" 
+
+begin 
+
+(******************************************************************************)
+(* 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*)
+definition curry  :: "('a*'b \<Rightarrow> 'c)\<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c "  where 
+     " curry f = ( (\<lambda> a b .  f (a, b)))"
+
+
+(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*)
+fun uncurry  :: "('a \<Rightarrow> 'b \<Rightarrow> 'c)\<Rightarrow> 'a*'b \<Rightarrow> 'c "  where 
+     " uncurry f (a,b) = ( f a b )"
+
+end