From a5692e0ba36b372b9175d7b356f4b2fd1ee3d663 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 11 Feb 2019 15:37:18 +0100
Subject: Put typing functionality into a .thy and clean up antiquotations,
 which results in some reorganization of the theory import structure.

---
 HoTT_Base.thy | 53 ++++++-----------------------------------------------
 1 file changed, 6 insertions(+), 47 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 1eaed12..9dcf6d0 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,64 +1,21 @@
 (********
-Isabelle/HoTT: Foundational definitions and notation
+Isabelle/HoTT: Basic logical definitions and notation
 Feb 2019
 
-This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
+This file completes the basic logical and functional setup of the HoTT logic.
 Among other things, it:
 
-* Calls the setup of object-level type inference functionality.
 * Defines the universe hierarchy and its governing rules.
 * Defines named theorems for later use by proof methods.
 
 ********)
 
 theory HoTT_Base
-imports Pure
-keywords "assume_type" "assume_types" :: thy_decl
+imports HoTT_Typing
 
 begin
 
-section \<open>Terms and typing\<close>
-
-typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
-
-judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
-
-section \<open>Setup non-core logic functionality\<close>
-
-declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
-
-ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close>
-  \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close>
-
-text \<open>Set up type assumption and inference functionality:\<close>
-
-ML_file "util.ML"
-ML_file "typing.ML"
-ML \<open>
-val _ =
-  let
-    fun store_typing ctxt = Typing.put_declared_typing o (Syntax.read_prop ctxt)
-  in
-    Outer_Syntax.local_theory
-      @{command_keyword "assume_type"}
-      "Declare typing assumptions"
-      (Parse.prop >>
-        (fn prop => fn lthy => Local_Theory.background_theory (store_typing lthy prop) lthy))
-  end
-
-val _ =
-  let
-    val parser = Parse.and_list (Parse.prop)
-    fun store_typings ctxt = fold (Typing.put_declared_typing o (Syntax.read_prop ctxt))
-  in
-    Outer_Syntax.local_theory
-      @{command_keyword "assume_types"}
-      "Declare typing assumptions"
-      (parser >>
-        (fn props => fn lthy => Local_Theory.background_theory (store_typings lthy props) lthy))
-  end
-\<close>
-                                                                                  
+
 section \<open>Universes\<close>
 
 typedecl ord \<comment> \<open>Type of meta-numerals\<close>
@@ -92,6 +49,7 @@ 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>
 
+
 section \<open>Type families\<close>
 
 abbreviation (input) constraint :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop"  ("(1_:/ _ \<leadsto> _)")
@@ -99,6 +57,7 @@ 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>
 
 named_theorems form
-- 
cgit v1.2.3