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 ++++++++++++++++++++-----------------------
 Prod.thy          |  2 +-
 scratch.thy       | 24 ++++++++++++++++++++++++
 3 files changed, 45 insertions(+), 24 deletions(-)
 create mode 100644 scratch.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
diff --git a/Prod.thy b/Prod.thy
index 113998e..7cce7f0 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -33,7 +33,7 @@ translations
 axiomatization where
   Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U"
 and
-  Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
+  Prod_intro [intro]: "\<And>A B b. \<lbrakk>A : U; \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
 and
   Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a"
 and
diff --git a/scratch.thy b/scratch.thy
new file mode 100644
index 0000000..331b607
--- /dev/null
+++ b/scratch.thy
@@ -0,0 +1,24 @@
+theory scratch
+  imports IFOL
+
+begin
+
+lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
+apply (erule disjE)  (* Compare with the less useful \<open>rule disjE\<close> *)
+  apply (rule disjI2)
+  apply assumption
+apply (rule disjI1)
+apply assumption
+done
+
+lemma imp_uncurry: "P \<longrightarrow> (Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R"
+apply (rule impI)
+apply (erule conjE)
+apply (drule mp)
+apply assumption
+apply (drule mp)
+apply assumption
+apply assumption
+done
+
+end
\ No newline at end of file
-- 
cgit v1.2.3