Removed all [simp] attributes, these will be added later when I set up the simplifier. Proved simplification rule for dependent fst.

3 files changed, 51 insertions, 31 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 9b7c3e2..7794601 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -34,7 +34,7 @@ consts
   is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
 
 axiomatization where
-  inhabited_implies_type: "\<And>a A. a : A \<Longrightarrow> A : U"
+  inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U"
 
 
 section \<open>Type families\<close>
diff --git a/Prod.thy b/Prod.thy
index 7cce7f0..bfb4f42 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -16,40 +16,47 @@ axiomatization
   \<comment> \<open>Application binds tighter than abstraction.\<close>
   appl :: "[Term, Term] \<Rightarrow> Term"  (infixl "`" 60)
 
+
+section \<open>Syntax\<close>
+
 syntax
   "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"          ("(3\<Prod>_:_./ _)" 30)
   "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<^bold>\<lambda>_:_./ _)" 30)
   "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"    ("(3PROD _:_./ _)" 30)
   "_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3%%_:_./ _)" 30)
 
-\<comment> \<open>The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>.\<close>
+text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>."
+
 translations
   "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
   "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
   "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
   "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
 
-\<comment> \<open>Type rules\<close>
+
+section \<open>Type rules\<close>
+
 axiomatization where
-  Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U"
+  Prod_form: "\<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. \<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"
+  Prod_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"
+  Prod_elim: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a"
 and
-  Prod_comp [simp]: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
+  Prod_comp: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
 and
-  Prod_uniq [simp]: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+
+text "The type rules should be able to be used as introduction rules by the standard reasoner:"
 
-\<comment> \<open>The funny thing about the first premises of the computation and uniqueness rules is that they introduce a variable B that doesn't actually explicitly appear in the statement of the conclusion.
-In a sense, they say something like "if this condition holds for some type family B... (then we can apply the rule)".
-This forces the theorem prover to search for a suitable B. Is this additional overhead necessary?
-It *is* a safety check for well-formedness...\<close>
+lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
 
 text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
 
-\<comment> \<open>Nondependent functions are a special case.\<close>
+text "Nondependent functions are a special case."
+
 abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
   where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"
 
+
 end
\ No newline at end of file
diff --git a/Sum.thy b/Sum.thy
index fbfc15a..8e7ccd6 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -15,6 +15,9 @@ axiomatization
   pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
   indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term"  ("(1indSum[_,/ _])")
 
+
+section \<open>Syntax\<close>
+
 syntax
   "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<Sum>_:_./ _)" 20)
   "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3SUM _:_./ _)" 20)
@@ -23,30 +26,35 @@ translations
   "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
   "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
 
+
+section \<open>Type rules\<close>
+
 axiomatization where
-  Sum_form [intro]: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U"
+  Sum_form: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U"
 and
-  Sum_intro [intro]: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
+  Sum_intro: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
 and
-  Sum_elim [elim]: "\<And>A B C f p. \<lbrakk>
+  Sum_elim: "\<And>A B C f p. \<lbrakk>
     C: \<Sum>x:A. B x \<rightarrow> U;
     \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
     p : \<Sum>x:A. B x
     \<rbrakk> \<Longrightarrow> indSum[A,B] C f p : C p"
 and
-  Sum_comp [simp]: "\<And>A B C f a b. \<lbrakk>
+  Sum_comp: "\<And>A B C f a b. \<lbrakk>
     C: \<Sum>x:A. B x \<rightarrow> U;
     \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
     a : A;
     b : B a
     \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b"
 
+lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
+
 \<comment> \<open>Nondependent pair\<close>
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"
 
 
-section \<open>Projections\<close>
+section \<open>Projection functions\<close>
 
 consts
   fst :: "[Term, 'a] \<Rightarrow> Term"  ("(1fst[/_,/ _])")
@@ -74,23 +82,28 @@ begin
     "snd_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p"
 end
 
-text "Properties of projections:"  
+text "Simplifying projections:"
 
-lemma fst_dep_comp:
+lemma fst_dep_comp:  (* Potential for automation *)
   assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
   shows "fst[A,B]`(a,b) \<equiv> a"
-proof (unfold fst_dep_def)  (* GOOD AUTOMATION EXAMPLE *)
-  have "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A, B] (\<lambda>_. A) (\<lambda>x y. x) p : A" ..
-  moreover have "(a, b) : \<Sum>x:A. B x" using assms ..
-  then have "fst[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" unfolding fst_dep_def by (simp add: Prod_comp)
-  have "A : U" using assms(2) ..
-  then have "\<lambda>_. A: \<Sum>x:A. B x \<rightarrow> U" .
-  moreover have "\<And>x y. x : A \<Longrightarrow> (\<lambda>x y. x) x y : A" .
-  moreover 
-  ultimately show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by simp
-qed
+proof (unfold fst_dep_def)
+  \<comment> "Write about this proof: unfolding, how we set up the introduction rules (explain \<open>..\<close>), do a trace of the proof, explain the meaning of keywords, etc."
 
-thm Sum_comp
+  have *: "A : U" using assms(2) ..  (* I keep thinking this should not have to be done explicitly, but rather automated. *)
+  
+  then have "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A" ..
+  
+  moreover have "(a,b) : \<Sum>x:A. B x" using assms ..
+  
+  ultimately have "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv>
+    indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" ..
+  
+  also have "indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a"
+    by (rule Sum_comp) (rule *, assumption, (rule assms)+)
+  
+  finally show "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv> a" .
+qed
 
 lemma snd_dep_comp:
   assumes "a : A" and "b : B a"