From f12983b1b53c71fc416155ac4b7e2b11ed8ca9ef Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 May 2020 22:16:42 +0200
Subject: change variable name in elim rules and fix small mistake

---
 hott/Nat.thy                | 14 +++++++-------
 spartan/data/List.thy       | 35 +++++++++++++----------------------
 spartan/data/Maybe.thy      |  4 ++++
 spartan/data/More_Types.thy |  3 ++-
 4 files changed, 26 insertions(+), 30 deletions(-)

diff --git a/hott/Nat.thy b/hott/Nat.thy
index c36154e..e8657a4 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -18,24 +18,24 @@ where
   NatE: "\<lbrakk>
     n: Nat;
     c\<^sub>0: C 0;
-    \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
+    \<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k);
     \<And>n. n: Nat \<Longrightarrow> C n: U i
-    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n: C n" and
+    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) n: C n" and
 
   Nat_comp_zero: "\<lbrakk>
     c\<^sub>0: C 0;
-    \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
+    \<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k);
     \<And>n. n: Nat \<Longrightarrow> C n: U i
-    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) 0 \<equiv> c\<^sub>0" and
+    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) 0 \<equiv> c\<^sub>0" and
 
   Nat_comp_suc: "\<lbrakk>
     n: Nat;
     c\<^sub>0: C 0;
-    \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
+    \<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k);
     \<And>n. n: Nat \<Longrightarrow> C n: U i
     \<rbrakk> \<Longrightarrow>
-      NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) (suc n) \<equiv>
-        f n (NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n)"
+      NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) (suc n) \<equiv>
+        f n (NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) n)"
 
 lemmas
   [intros] = NatF Nat_zero Nat_suc and
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index 3399da6..52f042b 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -1,3 +1,5 @@
+chapter \<open>Lists\<close>
+
 theory List
 imports Maybe
 
@@ -22,24 +24,24 @@ where
   ListE: "\<lbrakk>
     xs: List A;
     c\<^sub>0: C (nil A);
-    \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+    \<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 c. f x xs c) xs: C xs" and
+    \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) xs: C xs" and
 
   List_comp_nil: "\<lbrakk>
     c\<^sub>0: C (nil A);
-    \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+    \<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 c. f x xs c) (nil A) \<equiv> c\<^sub>0" and
+    \<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
 
   List_comp_cons: "\<lbrakk>
     xs: List A;
     c\<^sub>0: C (nil A);
-    \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+    \<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 c. f x xs c) (cons A x xs) \<equiv>
-        f x xs (ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) xs)"
+      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)"
 
 lemmas
   [intros] = ListF List_nil List_cons and
@@ -70,11 +72,6 @@ translations
 
 section \<open>Standard functions\<close>
 
-\<comment> \<open>
-definition "head A \<equiv> \<lambda>xs: List A.
-  ListRec A (Maybe A) (Maybe.none A) (\<lambda>x _ _. Maybe.some A x) xs"
-\<close>
-
 Lemma (derive) head:
   assumes "A: U i" "xs: List A"
   shows "Maybe A"
@@ -83,11 +80,8 @@ proof (elim xs)
   show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro
 qed
 
-thm head_def \<comment> \<open>head ?A ?xs \<equiv> ListRec ?A (Maybe ?A) none (\<lambda>x xs c. some x) ?xs\<close>
-
-\<comment> \<open>
-definition "tail A \<equiv> \<lambda>xs: List A. ListRec A (List A) (nil A) (\<lambda>x xs _. xs) xs"
-\<close>
+thm head_def
+  \<comment> \<open>head ?A ?xs \<equiv> ListRec ?A (Maybe ?A) none (\<lambda>x xs c. some x) ?xs\<close>
 
 Lemma (derive) tail:
   assumes "A: U i" "xs: List A"
@@ -98,11 +92,7 @@ proof (elim xs)
 qed
 
 thm tail_def
-
-\<comment> \<open>
-definition "map A B \<equiv> \<lambda>f: A \<rightarrow> B. \<lambda>xs: List A.
-  ListRec A (List B) (nil B) (\<lambda>x _ c. cons B (f `x) c) xs"
-\<close>
+  \<comment> \<open>tail ?A ?xs \<equiv> ListRec ?A (List ?A) [] (\<lambda>x xs c. xs) ?xs\<close>
 
 Lemma (derive) map:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
@@ -115,6 +105,7 @@ proof (elim xs)
 qed
 
 thm map_def
+  \<comment> \<open>map ?A ?B ?f ?xs \<equiv> ListRec ?A (List ?B) [] (\<lambda>x xs. cons ?B (?f x)) ?xs\<close>
 
 definition head_i ("head")
   where [implicit]: "head xs \<equiv> List.head ? xs"
diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy
index dc3ad04..98f5283 100644
--- a/spartan/data/Maybe.thy
+++ b/spartan/data/Maybe.thy
@@ -1,8 +1,12 @@
+chapter \<open>Maybe type\<close>
+
 theory Maybe
 imports More_Types
 
 begin
 
+text \<open>Defined as a sum.\<close>
+
 definition "Maybe A \<equiv> A \<or> \<top>"
 definition "none A \<equiv> inr A \<top> tt"
 definition "some A a \<equiv> inl A \<top> a"
diff --git a/spartan/data/More_Types.thy b/spartan/data/More_Types.thy
index f0cee6d..fecf378 100644
--- a/spartan/data/More_Types.thy
+++ b/spartan/data/More_Types.thy
@@ -1,9 +1,10 @@
+chapter \<open>Some standard types\<close>
+
 theory More_Types
 imports Spartan
 
 begin
 
-
 section \<open>Sum type\<close>
 
 axiomatization
-- 
cgit v1.2.3