From 5161a0356d8752f3b1b4f4385e799bca92718814 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 17 Jun 2018 00:48:01 +0200
Subject: Decided on a new proper scheme for type rules using the idea of
 implicit well-formed contexts and guaranteed conclusion well-formedness.
 Product type rules now follow this scheme.

---
 HoTT_Theorems.thy | 43 ++++++++++++++++++++-----------------------
 1 file changed, 20 insertions(+), 23 deletions(-)

(limited to 'HoTT_Theorems.thy')

diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index ab5374d..871c553 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -16,42 +16,39 @@ section \<open>\<Prod> type\<close>
 
 subsection \<open>Typing functions\<close>
 
-text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following."                                                   
+text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following."
 
-lemma "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
+proposition assumes "A : U" shows "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" using assms ..
 
-proposition "A \<equiv> B \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A"
+proposition
+  assumes "A : U" and "A \<equiv> B"
+  shows "\<^bold>\<lambda>x:A. x : B\<rightarrow>A"
 proof -
-  assume "A \<equiv> B"
-  then have *: "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
-
-  have "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
-  with * show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" by simp
+  have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp
+  moreover have "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" using assms(1) ..
+  ultimately show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" by simp
 qed
 
-proposition "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
+proposition
+  assumes "A : U" and "B : U"
+  shows "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
 proof
-  fix a
-  assume "a : A"
-  then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" ..
-
-  ML_val \<open>@{context} |> Variable.names_of\<close>
-
-qed
+  fix x
+  assume "x : A"
+  with assms(2) show "\<^bold>\<lambda>y:B. x : B\<rightarrow>A" ..
+qed (rule assms)
 
 
 subsection \<open>Function application\<close>
 
-proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by simp
+proposition assumes "a : A" shows "(\<^bold>\<lambda>x:A. x)`a \<equiv> a" using assms by simp
 
 text "Currying:"
 
-term "lambda A (\<lambda>x. \<^bold>\<lambda>y:B(x). y)"
-
-thm Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"]
-
-lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a \<equiv> \<^bold>\<lambda>y:B(a). y"
-proof (rule Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"])
+lemma
+  assumes "a : A"
+  shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a \<equiv> \<^bold>\<lambda>y:B(a). y"
+proof
   show "\<And>x. a : A \<Longrightarrow> x : A \<Longrightarrow> \<^bold>\<lambda>y:B x. y : B x \<rightarrow> B x"
 
 lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a`b \<equiv> b"  by simp
-- 
cgit v1.2.3