From 831f33468f227c0dc96bd31380236f2c77e70c52 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 9 Jul 2020 13:35:39 +0200
Subject: Non-annotated object lambda

---
 spartan/lib/List.thy       | 12 ++++++------
 spartan/lib/Maybe.thy      | 13 +++++--------
 spartan/lib/More_Types.thy | 12 ++++++------
 3 files changed, 17 insertions(+), 20 deletions(-)

(limited to 'spartan/lib')

diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 11b8406..a755859 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -26,13 +26,13 @@ where
     c\<^sub>0: C (nil A);
     \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs);
     \<And>xs. xs: List A \<Longrightarrow> C xs: U i
-    \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) xs: C xs" and
+    \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs: C xs" and
 
   List_comp_nil: "\<lbrakk>
     c\<^sub>0: C (nil A);
     \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs);
     \<And>xs. xs: List A \<Longrightarrow> C xs: U i
-    \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) (nil A) \<equiv> c\<^sub>0" and
+    \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (nil A) \<equiv> c\<^sub>0" and
 
   List_comp_cons: "\<lbrakk>
     xs: List A;
@@ -40,15 +40,15 @@ where
     \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs);
     \<And>xs. xs: List A \<Longrightarrow> C xs: U i
     \<rbrakk> \<Longrightarrow>
-      ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) (cons A x xs) \<equiv>
-        f x xs (ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) xs)"
+      ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (cons A x xs) \<equiv>
+        f x xs (ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs)"
 
 lemmas
   [intros] = ListF List_nil List_cons and
   [elims "?xs"] = ListE and
   [comps] = List_comp_nil List_comp_cons
 
-abbreviation "ListRec A C \<equiv> ListInd A (\<lambda>_. C)"
+abbreviation "ListRec A C \<equiv> ListInd A (fn _. C)"
 
 Lemma list_cases [cases]:
   assumes
@@ -56,7 +56,7 @@ Lemma list_cases [cases]:
     nil_case: "c\<^sub>0: C (nil A)" and
     cons_case: "\<And>x xs. \<lbrakk>x: A; xs: List A\<rbrakk> \<Longrightarrow> f x xs: C (cons A x xs)" and
     "\<And>xs. xs: List A \<Longrightarrow> C xs: U i"
-  shows "?List_cases A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs. f x xs) xs: C xs"
+  shows "C xs"
   by (elim xs) (fact nil_case, rule cons_case)
 
 
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 6729812..d821920 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -24,7 +24,7 @@ Definition MaybeInd:
     "c\<^sub>0: C (none A)"
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "m: Maybe A"
-  shows "?MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) m: C m"
+  shows "C m"
   supply assms[unfolded Maybe_def none_def some_def]
   apply (elim m)
   \<guillemotright> unfolding Maybe_def .
@@ -38,7 +38,7 @@ Lemma Maybe_comp_none:
     "c\<^sub>0: C (none A)"
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
-  shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (none A) \<equiv> c\<^sub>0"
+  shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
   supply assms[unfolded Maybe_def some_def none_def]
   unfolding MaybeInd_def none_def by reduce
 
@@ -49,7 +49,7 @@ Lemma Maybe_comp_some:
     "c\<^sub>0: C (none A)"
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
-  shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (some A a) \<equiv> f a"
+  shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
   supply assms[unfolded Maybe_def some_def none_def]
   unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
 
@@ -62,11 +62,8 @@ lemmas
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
 
-definition none_i ("none")
-  where [implicit]: "none \<equiv> Maybe.none ?"
-
-definition some_i ("some")
-  where [implicit]: "some a \<equiv> Maybe.some ? a"
+definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none ?"
+definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some ? a"
 
 translations
   "none" \<leftharpoondown> "CONST Maybe.none A"
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/More_Types.thy
index 38ba2aa..0d7096f 100644
--- a/spartan/lib/More_Types.thy
+++ b/spartan/lib/More_Types.thy
@@ -25,21 +25,21 @@ axiomatization where
     \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
     \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
     \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) s: C s" and
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) s: C s" and
 
   Sum_comp_inl: "\<lbrakk>
     a: A;
     \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
     \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
     \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) (inl A B a) \<equiv> c a" and
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inl A B a) \<equiv> c a" and
 
   Sum_comp_inr: "\<lbrakk>
     b: B;
     \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
     \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
     \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) (inr A B b) \<equiv> d b"
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inr A B b) \<equiv> d b"
 
 lemmas
   [intros] = SumF Sum_inl Sum_inr and
@@ -67,13 +67,13 @@ axiomatization where
 
   TopI: "tt: \<top>" and
 
-  TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (\<lambda>x. C x) c a: C a" and
+  TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c a: C a" and
 
-  Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (\<lambda>x. C x) c tt \<equiv> c"
+  Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c tt \<equiv> c"
 and
   BotF: "\<bottom>: U i" and
 
-  BotE: "\<lbrakk>x: \<bottom>; \<And>x. x: \<bottom> \<Longrightarrow> C x: U i\<rbrakk> \<Longrightarrow> BotInd (\<lambda>x. C x) x: C x"
+  BotE: "\<lbrakk>x: \<bottom>; \<And>x. x: \<bottom> \<Longrightarrow> C x: U i\<rbrakk> \<Longrightarrow> BotInd (fn x. C x) x: C x"
 
 lemmas
   [intros] = TopF TopI BotF and
-- 
cgit v1.2.3