From c2dfffffb7586662c67e44a2d255a1a97ab0398b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 2 Apr 2020 17:57:48 +0200
Subject: Brand-spanking new version using Spartan infrastructure

---
 HoTT_Base.thy | 103 ----------------------------------------------------------
 1 file changed, 103 deletions(-)
 delete mode 100644 HoTT_Base.thy

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
deleted file mode 100644
index 9987b78..0000000
--- a/HoTT_Base.thy
+++ /dev/null
@@ -1,103 +0,0 @@
-(********
-Isabelle/HoTT: Basic logical definitions and notation
-Feb 2019
-
-This file completes the basic logical and functional setup of the HoTT logic. It defines:
-
-* The universe hierarchy and its governing rules.
-* Some notational abbreviations.
-* Named theorems for later use by proof methods.
-
-********)
-
-theory HoTT_Base
-imports Pure
-
-begin
-
-
-section \<open>Basic setup\<close>
-
-declare[[names_short]]
-declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
-
-typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
-
-judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(2_ :/ _)")
-
-
-section \<open>Universes\<close>
-
-typedecl ord \<comment> \<open>Type of meta-numerals\<close>
-
-axiomatization
-  O   :: ord and
-  Suc :: "ord \<Rightarrow> ord" and
-  lt  :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999) and
-  leq :: "[ord, ord] \<Rightarrow> prop"  (infix "\<le>" 999)
-where
-  lt_Suc: "n < (Suc n)" and
-  lt_trans: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
-  leq_min: "O \<le> n"
-
-declare
-  lt_Suc [intro!]
-  leq_min [intro!]
-  lt_trans [intro]
-
-axiomatization
-  U :: "ord \<Rightarrow> t"
-where
-  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"
-
-lemma U_hierarchy': "U i: U (Suc i)" by (fact U_hierarchy[OF lt_Suc])
-
-declare U_hierarchy' [intro!]
-
-text \<open>
-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}.
-
-@{thm U_hierarchy'} is declared with safe @{attribute intro} to be used by the method @{theory_text derive} to handle the universe hierarchy.
-Note that @{thm U_hierarchy} is unsafe.
-\<close>
-
-
-section \<open>Notation\<close>
-
-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>
-
-abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"  ("&_" [0] 3)
-where "&A \<equiv> \<lambda>_. A"
-
-abbreviation (input) Id :: "t \<Rightarrow> t" where "Id \<equiv> \<lambda>x. x"
-\<comment> \<open>NOTE: removing the input attribute causes term evaluations and even theorem attribute declarations to loop! Possible bug?\<close>
-
-
-section \<open>Named theorems\<close>
-
-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 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! *)
-
-end
-- 
cgit v1.2.3