Pre-universe implementation commit

6 files changed, 104 insertions, 70 deletions

diff --git a/EqualProps.thy b/EqualProps.thy
index cb267c6..43b4eb5 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -19,16 +19,14 @@ definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
   where "inv[A,x,y] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) x y p"
 
 
-lemma inv_type:
-  assumes "p : x =\<^sub>A y"
-  shows "inv[A,x,y]`p : y =\<^sub>A x"
+lemma inv_type: assumes "x : A" and "y : A" shows "inv[A,x,y] : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
   unfolding inv_def
   by (derive lems: assms)
-      
 
-lemma inv_comp:
-  assumes "a : A"
-  shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
+corollary assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x"
+  by (derive lems: inv_type assms)
+
+lemma inv_comp: assumes "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
   unfolding inv_def by (simplify lems: assms)
 
 
@@ -43,27 +41,24 @@ definition rcompose :: "Term \<Rightarrow> Term"  ("(1rcompose[_])")
     x y p"
 
 
-text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>."
+text "``Natural'' composition function, of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>."
 
 abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
   where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:(x =\<^sub>A y). \<^bold>\<lambda>q:(y =\<^sub>A z). rcompose[A]`x`y`p`z`q"
 
 
 lemma compose_type:
-  assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z"
-  shows "compose[A,x,y,z]`p`q : x =\<^sub>A z"
+assumes "x : A" and "y : A" and "z : A" shows "compose[A,x,y,z] : x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
   unfolding rcompose_def
   by (derive lems: assms)
 
-
-lemma compose_comp:
-  assumes "a : A"
-  shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
+lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
   unfolding rcompose_def
   by (simplify lems: assms)
 
 
-lemmas Equal_simps [intro] = inv_comp compose_comp
+lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp
+lemmas EqualProps_comps [comp] = inv_comp compose_comp
 
 
 end
\ No newline at end of file
diff --git a/HoTT.thy b/HoTT.thy
index 948dd14..fa50f61 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -21,4 +21,4 @@ EqualProps
 Proj
 
 begin
-end
+end
\ No newline at end of file
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 60e5167..d119c1f 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -10,7 +10,7 @@ theory HoTT_Base
 begin
 
 
-section \<open>Setup\<close>
+section \<open>Named theorems\<close>
 
 text "Named theorems to be used by proof methods later (see HoTT_Methods.thy).
 
@@ -21,7 +21,7 @@ named_theorems wellform
 named_theorems comp
 
 
-section \<open>Metalogical definitions\<close>
+section \<open>Foundational definitions\<close>
 
 text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
 We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ``\<open>a\<close> is a type''."
@@ -29,6 +29,27 @@ We do not implement universes, and simply use \<open>a : U\<close> as a convenie
 typedecl Term
 
 
+section \<open>Universes\<close>
+
+ML \<open>
+(* Produces universe terms and judgments on-the-fly *)
+fun Ui_type_oracle (x: int) = 
+  let
+    val f = Sign.declare_const @{context} ((Binding.name ("U" ^ Int.toString x), @{typ Term}), NoSyn);
+    val (trm, thy) = f @{theory};
+  in
+    Theory.setup (fn thy => #2 (f thy));
+    Thm.cterm_of (Proof_Context.init_global thy) (trm)
+  end
+\<close>
+
+(*
+Sign.add_consts: (binding * typ * mixfix) list -> theory -> theory
+Thm.cterm_of: Proof.context -> term -> cterm
+Thm.add_oracle: binding * (’a -> cterm) -> theory -> (string * (’a -> thm)) * theory
+*)
+
+
 section \<open>Judgments\<close>
 
 text "We formalize the judgments \<open>a : A\<close> and \<open>A : U\<close> separately, in contrast to the HoTT book where the latter is considered an instance of the former.
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 1f11230..9a101e5 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -13,11 +13,6 @@ theory HoTT_Methods
 begin
 
 
-text "The methods \<open>simple\<close>, \<open>wellformed\<close>, \<open>derive\<close>, and \<open>simplify\<close> should together should suffice to automatically prove most HoTT theorems.
-We also provide a method
-"
-
-
 section \<open>Setup\<close>
 
 text "Import the \<open>subst\<close> method, used by \<open>simplify\<close>."
@@ -67,9 +62,10 @@ method derive uses lems unfolds = (
 
 subsection \<open>Simplification\<close>
 
-text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> simplify lambda applications and attempt to solve definitional equations.
+text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> attempt to solve definitional equations by simplifying lambda applications.
 
-\<open>rsimplify\<close> can also be used to search for lambda expressions inhabiting given types.
+\<open>simplify\<close> is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules.
+In this case use \<open>rsimplify\<close> instead.
 
 Since these methods use \<open>derive\<close>, it is often (but not always) the case that theorems provable with \<open>derive\<close> are also provable with them.
 (Whether this is the case depends on whether the call to \<open>subst (0) comp\<close> fails.)"
diff --git a/Proj.thy b/Proj.thy
index 805a624..31deaf9 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -47,16 +47,12 @@ section \<open>Properties\<close>
 
 text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
 
-lemma fst_dep_type:
-  assumes "p : \<Sum>x:A. B x"
-  shows "fst[A,B]`p : A"
+lemma fst_dep_type: assumes "p : \<Sum>x:A. B x" shows "fst[A,B]`p : A"
   unfolding fst_dep_def
   by (derive lems: assms)
 
 
-lemma fst_dep_comp:
-  assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
-  shows "fst[A,B]`(a,b) \<equiv> a"
+lemma fst_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \<equiv> a"
   unfolding fst_dep_def
   by (simplify lems: assms)
 
@@ -86,9 +82,7 @@ qed
 \<close>
 
 
-lemma snd_dep_type:
-  assumes "p : \<Sum>x:A. B x"
-  shows "snd[A,B]`p : B (fst[A,B]`p)"
+lemma snd_dep_type: assumes "p : \<Sum>x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)"
   unfolding fst_dep_def snd_dep_def
   by (simplify lems: assms)
 
@@ -103,9 +97,7 @@ qed (assumption | rule assms)+
 \<close>
 
 
-lemma snd_dep_comp:
-  assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
-  shows "snd[A,B]`(a,b) \<equiv> b"
+lemma snd_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \<equiv> b"
   unfolding snd_dep_def fst_dep_def
   by (simplify lems: assms)
 
@@ -132,18 +124,14 @@ qed
 \<close>
 
 
-text "For non-dependent projection functions:"
+text "Nondependent projections:"
 
-lemma fst_nondep_type:
-  assumes "p : A \<times> B"
-  shows "fst[A,B]`p : A"
+lemma fst_nondep_type: assumes "p : A \<times> B" shows "fst[A,B]`p : A"
   unfolding fst_nondep_def 
   by (derive lems: assms)
 
 
-lemma fst_nondep_comp:
-  assumes "a : A" and "b : B"
-  shows "fst[A,B]`(a,b) \<equiv> a"
+lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \<equiv> a"
   unfolding fst_nondep_def
   by (simplify lems: assms)
 
@@ -160,9 +148,7 @@ qed
 \<close>
 
 
-lemma snd_nondep_type:
-  assumes "p : A \<times> B"
-  shows "snd[A,B]`p : B"
+lemma snd_nondep_type: assumes "p : A \<times> B" shows "snd[A,B]`p : B"
   unfolding snd_nondep_def
   by (derive lems: assms)
 
@@ -177,9 +163,7 @@ qed (rule assms)
 \<close>
 
 
-lemma snd_nondep_comp:
-  assumes "a : A" and "b : B"
-  shows "snd[A,B]`(a,b) \<equiv> b"
+lemma snd_nondep_comp: assumes "a : A" and "b : B" shows "snd[A,B]`(a,b) \<equiv> b"
   unfolding snd_nondep_def
   by (simplify lems: assms)
 
@@ -196,4 +180,11 @@ qed
 \<close>
 
 
+lemmas Proj_rules [intro] =
+  fst_dep_type snd_dep_type fst_nondep_type snd_nondep_type
+  fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
+
+lemmas Proj_comps [comp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
+
+
 end
\ No newline at end of file
diff --git a/scratch.thy b/scratch.thy
index 1c921bd..3f66083 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,8 +3,11 @@ theory scratch
 
 begin
 
+term "UN"
+
 (* Typechecking *)
-schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" by simple
+schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A"
+  by derive
 
 
 (* Simplification *)
@@ -17,45 +20,73 @@ assume asm:
   "c : A"
   "d : B"
 
-have "f`a`b`c \<equiv> d" by (simp add: asm | rule comp | derive lems: asm)+
+have "f`a`b`c \<equiv> d" by (simplify lems: asm)
 
 end
 
 lemma "a : A \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)"
-  by verify_simp
+  by simplify
 
 lemma "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
-  by verify_simp
+  by simplify
+
+schematic_goal "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x"
+  by rsimplify
 
 lemma
   assumes "a : A" and "\<And>x. x : A \<Longrightarrow> b x : B x"
   shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
-  by (verify_simp lems: assms)
+  by (simplify lems: assms)
 
-lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-oops
+lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U; \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk>
+  \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
+  by (simplify)
 
 lemma
   assumes
     "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a \<equiv> \<^bold>\<lambda>y:B a. c a y"
     "(\<^bold>\<lambda>y:B a. c a y)`b \<equiv> c a b"
   shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-apply (simp add: assms)
-done
-
-lemmas lems =
-  Prod_comp[where ?A = "B a" and ?b = "\<lambda>b. c a b" and ?a = b]
-  Prod_comp[where ?A = A and ?b = "\<lambda>x. \<^bold>\<lambda>y:B x. c x y" and ?a = a]
+by (simplify lems: assms)
 
 lemma
-  assumes
-    "a : A"
-    "b : B a"
-    "B: A \<rightarrow> U"
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y"
-  shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-apply (verify_simp lems: assms)
+assumes
+  "a : A"
+  "b : B a"
+  "B: A \<rightarrow> U"
+  "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y"
+shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
+by (simplify lems: assms)
 
+lemma
+assumes
+  "a : A"
+  "b : B a"
+  "c : C a b"
+  "B: A \<rightarrow> U"
+  "\<And>x. x : A\<Longrightarrow> C x: B x \<rightarrow> U"
+  "\<And>x y z. \<lbrakk>x : A; y : B x; z : C x y\<rbrakk> \<Longrightarrow> d x y z : D x y z"
+shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. \<^bold>\<lambda>z:C x y. d x y z)`a`b`c \<equiv> d a b c"
+by (simplify lems: assms)
+
+
+(* HERE IS HOW WE ATTEMPT TO DO PATH INDUCTION --- VERY GOOD CANDIDATE FOR THESIS SECTION *)
+
+schematic_goal "\<lbrakk>A : U; x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
+  apply (rule Prod_intro)
+  apply (rule Equal_form)
+  apply assumption+
+  apply (rule Equal_elim)
+  back
+  back
+  back
+  back
+  back
+  back
+  back
+  back back back back back back
+
+thm comp
 
 
 end
\ No newline at end of file