From 2781c68f0fdb435827097efc497c2172d6050e50 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 2 Apr 2020 23:27:06 +0200
Subject: 1. make id function an abbrev. 2. fix reduce method

---
 spartan/theories/Identity.thy |  2 +-
 spartan/theories/Spartan.thy  | 12 +++++-------
 2 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy
index 0edf20e..19b8b7a 100644
--- a/spartan/theories/Identity.thy
+++ b/spartan/theories/Identity.thy
@@ -261,7 +261,7 @@ Lemma transport_comp [comps]:
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
   shows "trans P (refl a) \<equiv> id (P a)"
-  unfolding transport_def id_def by reduce
+  unfolding transport_def by reduce
 
 \<comment> \<open>TODO: Build transport automation!\<close>
 
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy
index ac12937..a79f209 100644
--- a/spartan/theories/Spartan.thy
+++ b/spartan/theories/Spartan.thy
@@ -242,7 +242,7 @@ setup \<open>
     ctxt addSolver (mk_solver "" typechk_tac))
 \<close>
 
-method reduce uses add = (simp add: comps add | subst comps, reduce add: add)+
+method reduce uses add = (simp add: comps add | subst comps)+
 
 
 section \<open>Implicit notations\<close>
@@ -355,23 +355,21 @@ translations "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
 
 subsection \<open>Identity function\<close>
 
-definition id where "id A \<equiv> \<lambda>x: A. x"
+abbreviation id where "id A \<equiv> \<lambda>x: A. x"
 
 lemma
-  idI [typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
-  id_comp [comps]: "x: A \<Longrightarrow> (id A) x \<equiv> x"
-  unfolding id_def by reduce
+  id_type[typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
+  id_comp [comps]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close>
+  by reduce
 
 lemma id_left [comps]:
   assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
   shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f"
-  unfolding id_def
   by (subst eta_exp[of f]) (reduce, rule eta)
 
 lemma id_right [comps]:
   assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
   shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
-  unfolding id_def
   by (subst eta_exp[of f]) (reduce, rule eta)
 
 lemma id_U [typechk]:
-- 
cgit v1.2.3