From a245a3e2194b4d5a6e7fbac8fa10598e96307e57 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 30 Jan 2019 15:43:47 +0100
Subject: Begin refactor

---
 HoTT_Base.thy | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 9e8fee7..93ef70e 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,9 +1,7 @@
 (*
-Title:  HoTT_Base.thy
-Author: Joshua Chen
-Date:   2018
+Homotopy Type Theory
 
-Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy.
+Foundational setup and definitions
 *)
 
 theory HoTT_Base
@@ -11,13 +9,12 @@ imports Pure
 
 begin
 
-
 section \<open>Basic setup\<close>
 
 declare[[eta_contract=false]]
 
-typedecl t  \<comment> \<open>Type of object types and terms\<close>
-typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
+typedecl t  \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
+typedecl ord  \<comment> \<open>Type of meta-numerals\<close>
 
 axiomatization
   O   :: ord and
@@ -34,12 +31,10 @@ declare
   leq_min [intro!]
   lt_trans [intro]
 
-
-section \<open>Judgment\<close>
+section \<open>Typing judgment\<close>
 
 judgment hastype :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
 
-
 section \<open>Universes\<close>
 
 axiomatization
@@ -50,8 +45,8 @@ where
   U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
 
 text \<open>
-Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
-One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
+Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination.
+Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 
 @{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}.
 \<close>
-- 
cgit v1.2.3


From 843d53d64983593d765a203605cd2aab00ed8361 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 30 Jan 2019 16:09:50 +0100
Subject: Remove "constrained" notation for type families. Clean and document.

---
 HoTT_Base.thy | 33 +++++++++++++--------------------
 1 file changed, 13 insertions(+), 20 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 93ef70e..99ab5ce 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,8 +1,15 @@
-(*
-Homotopy Type Theory
+(********
+Isabelle/HoTT: Foundational definitions and notation
+Jan 2019
 
-Foundational setup and definitions
-*)
+This file is the starting point, and contains the base setup and definitions of the object logic.
+Among other things, it defines:
+
+* Meta-numerals to index the universe hierarchy, and related axioms.
+* The universe hierarchy and its governing rules.
+* Named theorems for later use by proof methods.
+
+********)
 
 theory HoTT_Base
 imports Pure
@@ -11,7 +18,7 @@ begin
 
 section \<open>Basic setup\<close>
 
-declare[[eta_contract=false]]
+declare[[eta_contract=false]] (* I'm not actually sure this does anything... *)
 
 typedecl t  \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 typedecl ord  \<comment> \<open>Type of meta-numerals\<close>
@@ -51,26 +58,13 @@ Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 @{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}.
 \<close>
 
-
-section \<open>Type families\<close>
-
-abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop"  ("(1_:/ _ \<longrightarrow> _)")
-  where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)"
-
-text \<open>
-The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"}, where @{term "A::t"} and @{term "B::t"} are small types.
-\<close>
-
-type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families\<close>
-
-
 section \<open>Named theorems\<close>
 
 named_theorems comp
 named_theorems form
 
 text \<open>
-Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
+The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}.
 
 @{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
 
@@ -80,5 +74,4 @@ These are mainly used by the \<open>cumulativity\<close> method, which lifts typ
 
 (* Todo: Set up the Simplifier! *)
 
-
 end
-- 
cgit v1.2.3


From 07d312b312c3058551353bcf403a1dc7c7c83311 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 31 Jan 2019 15:51:24 +0100
Subject: Text remarks

---
 HoTT_Base.thy | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 99ab5ce..bb47a74 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -2,7 +2,7 @@
 Isabelle/HoTT: Foundational definitions and notation
 Jan 2019
 
-This file is the starting point, and contains the base setup and definitions of the object logic.
+This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
 Among other things, it defines:
 
 * Meta-numerals to index the universe hierarchy, and related axioms.
@@ -18,7 +18,7 @@ begin
 
 section \<open>Basic setup\<close>
 
-declare[[eta_contract=false]] (* I'm not actually sure this does anything... *)
+declare[[eta_contract=false]] (* Does this option actually do anything? *)
 
 typedecl t  \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 typedecl ord  \<comment> \<open>Type of meta-numerals\<close>
@@ -55,9 +55,13 @@ text \<open>
 Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination.
 Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 
-@{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}.
+@{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}.
 \<close>
 
+section \<open>Type families\<close>
+
+abbrev (input) 
+
 section \<open>Named theorems\<close>
 
 named_theorems comp
-- 
cgit v1.2.3


From 7a7e27f4a1efd69e9ab43b95d3c7ead61a743e55 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 4 Feb 2019 11:53:47 +0100
Subject: 1. Change syntax to rely less on unicode/control symbols. 2. Begin
 work on object-level type inference and input syntax help.

---
 HoTT_Base.thy | 65 ++++++++++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 53 insertions(+), 12 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index bb47a74..a5280ce 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -5,7 +5,7 @@ Jan 2019
 This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
 Among other things, it defines:
 
-* Meta-numerals to index the universe hierarchy, and related axioms.
+* Containers for storing type information of object-level terms.
 * The universe hierarchy and its governing rules.
 * Named theorems for later use by proof methods.
 
@@ -16,12 +16,56 @@ imports Pure
 
 begin
 
-section \<open>Basic setup\<close>
+section \<open>Terms and typing\<close>
 
-declare[[eta_contract=false]] (* Does this option actually do anything? *)
+typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 
-typedecl t  \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
-typedecl ord  \<comment> \<open>Type of meta-numerals\<close>
+consts has_type :: "[t, t] \<Rightarrow> prop"  \<comment> \<open>The judgment coercion\<close>
+
+text \<open>
+We create a dedicated container in which to store object-level typing information whenever a typing judgment that does not depend on assumptions is proved.
+\<close>
+
+ML \<open>
+signature TYPINGS =
+sig
+  val get: term -> term
+end
+
+structure Typings: TYPINGS = 
+struct
+
+structure Typing_Data = Theory_Data
+(
+  type T = term Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+
+  fun merge (tbl, tbl') =
+    let
+      val key_vals = map (Symtab.lookup_key tbl') (Symtab.keys tbl')
+      val updates = map (fn SOME kv => Symtab.update kv) key_vals
+      fun f u t = u t
+    in fold f updates tbl end
+)
+
+fun get tm =
+  case Symtab.lookup (Typing_Data.get @{theory}) (Syntax.string_of_term @{context} tm) of
+    SOME tm' => tm'
+  | NONE => raise Fail "No typing information available"
+
+end
+\<close>
+
+syntax "_has_type" :: "[t, t] \<Rightarrow> prop"  ("3(_:/ _)")
+
+parse_translation \<open>
+
+\<close>
+
+section \<open>Universes\<close>
+
+typedecl ord \<comment> \<open>Type of meta-numerals\<close>
 
 axiomatization
   O   :: ord and
@@ -38,12 +82,6 @@ declare
   leq_min [intro!]
   lt_trans [intro]
 
-section \<open>Typing judgment\<close>
-
-judgment hastype :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
-
-section \<open>Universes\<close>
-
 axiomatization
   U :: "ord \<Rightarrow> t"
 where
@@ -60,7 +98,10 @@ Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 
 section \<open>Type families\<close>
 
-abbrev (input) 
+abbreviation (input) constraint :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop"  ("(1_:/ _ \<leadsto> _)")
+where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)"
+
+text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close>
 
 section \<open>Named theorems\<close>
 
-- 
cgit v1.2.3


From d70da13b7fd36509c1d843d139a0b99c6acb8cc6 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Feb 2019 18:15:58 +0100
Subject: Type inference setup begun - first use-case for function composition.

---
 HoTT_Base.thy | 57 +++++++++------------------------------------------------
 1 file changed, 9 insertions(+), 48 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index a5280ce..aa13815 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -3,11 +3,11 @@ Isabelle/HoTT: Foundational definitions and notation
 Jan 2019
 
 This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
-Among other things, it defines:
+Among other things, it:
 
-* Containers for storing type information of object-level terms.
-* The universe hierarchy and its governing rules.
-* Named theorems for later use by proof methods.
+* Sets up object-level type inference functionality (via typing.ML).
+* Defines the universe hierarchy and its governing rules.
+* Defines named theorems for later use by proof methods.
 
 ********)
 
@@ -20,48 +20,9 @@ section \<open>Terms and typing\<close>
 
 typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 
-consts has_type :: "[t, t] \<Rightarrow> prop"  \<comment> \<open>The judgment coercion\<close>
+judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
 
-text \<open>
-We create a dedicated container in which to store object-level typing information whenever a typing judgment that does not depend on assumptions is proved.
-\<close>
-
-ML \<open>
-signature TYPINGS =
-sig
-  val get: term -> term
-end
-
-structure Typings: TYPINGS = 
-struct
-
-structure Typing_Data = Theory_Data
-(
-  type T = term Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-
-  fun merge (tbl, tbl') =
-    let
-      val key_vals = map (Symtab.lookup_key tbl') (Symtab.keys tbl')
-      val updates = map (fn SOME kv => Symtab.update kv) key_vals
-      fun f u t = u t
-    in fold f updates tbl end
-)
-
-fun get tm =
-  case Symtab.lookup (Typing_Data.get @{theory}) (Syntax.string_of_term @{context} tm) of
-    SOME tm' => tm'
-  | NONE => raise Fail "No typing information available"
-
-end
-\<close>
-
-syntax "_has_type" :: "[t, t] \<Rightarrow> prop"  ("3(_:/ _)")
-
-parse_translation \<open>
-
-\<close>
+ML_file "typing.ML"
 
 section \<open>Universes\<close>
 
@@ -85,13 +46,13 @@ declare
 axiomatization
   U :: "ord \<Rightarrow> t"
 where
-  U_hierarchy: "i < j \<Longrightarrow> U i: U j" and                               
+  U_hierarchy: "i < j \<Longrightarrow> U i: U j" and
   U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and
   U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
 
 text \<open>
-Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination.
-Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
+Using method @{method rule} with @{thm U_cumulative} and @{thm U_cumulative'} is unsafe: if applied blindly it will very easily lead to non-termination.
+Instead use @{method elim}, or instantiate the rules suitably.
 
 @{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}.
 \<close>
-- 
cgit v1.2.3


From 8759a6ff0dbe5f0e9dbc28ab2711c54bed7ffa44 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Feb 2019 18:29:10 +0100
Subject: Decided to keep terms eta-expanded

---
 HoTT_Base.thy | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index aa13815..88cf986 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -18,6 +18,8 @@ begin
 
 section \<open>Terms and typing\<close>
 
+declare[[eta_contract=false]]
+
 typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 
 judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
-- 
cgit v1.2.3


From 64d2a5c60acce40113362c9d7eca8cd633362d23 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Feb 2019 18:32:43 +0100
Subject: Add cong named theorem for congruence rules

---
 HoTT_Base.thy | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 88cf986..e74ef31 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -68,16 +68,19 @@ text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type
 
 section \<open>Named theorems\<close>
 
-named_theorems comp
 named_theorems form
+named_theorems comp
+named_theorems cong
 
 text \<open>
 The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}.
 
-@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
-
 @{attribute form} declares type formation rules.
 These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes.
+
+@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute cong} declares congruence rules, the definitional equality rules of the type theory.
 \<close>
 
 (* Todo: Set up the Simplifier! *)
-- 
cgit v1.2.3

