Commit before testing polymorphic equality eliminator

9 files changed, 108 insertions, 56 deletions

diff --git a/Coprod.thy b/Coprod.thy
index a301e7e..d47c24e 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -44,17 +44,17 @@ and
     \<And>y. y: B \<Longrightarrow> d(y): C(inr(y));
     b: B
     \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inr(b)) \<equiv> d(b)"
-
+(*
 text "Admissible formation inference rules:"
 
 axiomatization where
   Coprod_form_cond1: "\<And>i A B. A + B: U(i) \<Longrightarrow> A: U(i)"
 and
   Coprod_form_cond2: "\<And>i A B. A + B: U(i) \<Longrightarrow> B: U(i)"
-
-lemmas Coprod_rules [intro] = Coprod_form Coprod_intro1 Coprod_intro2
-                              Coprod_elim Coprod_comp1 Coprod_comp2
-lemmas Coprod_form_conds [intro] = Coprod_form_cond1 Coprod_form_cond2
+*)
+lemmas Coprod_rules [intro] =
+  Coprod_form Coprod_intro1 Coprod_intro2 Coprod_elim Coprod_comp1 Coprod_comp2
+(*lemmas Coprod_form_conds [intro] = Coprod_form_cond1 Coprod_form_cond2 *)
 lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2
 
 
diff --git a/Equal.thy b/Equal.thy
index 8bd7875..d910bb8 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -28,11 +28,11 @@ translations
 section \<open>Type rules\<close>
 
 axiomatization where
-  Equal_form: "\<And>i A a b. \<lbrakk>A: U(i); a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)"
+  Equal_form: "\<lbrakk>A: U(i); a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)"
 and
-  Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a): a =\<^sub>A a"
+  Equal_intro: "a : A \<Longrightarrow> refl(a): a =\<^sub>A a"
 and
-  Equal_elim: "\<And>i A C f a b p. \<lbrakk>
+  Equal_elim: "\<lbrakk>
     \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i);
     \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
     a: A;
@@ -40,23 +40,23 @@ and
     p: a =\<^sub>A b
     \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(b)(p) : C(a)(b)(p)"
 and
-  Equal_comp: "\<And>i A C f a. \<lbrakk>
+  Equal_comp: "\<lbrakk>
     \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i);
     \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
     a: A
     \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(a)(refl(a)) \<equiv> f(a)"
 
 text "Admissible inference rules for equality type formation:"
-
+(*
 axiomatization where
-  Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)"
+  Equal_form_cond1: "a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)"
 and
-  Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> a: A"
+  Equal_form_cond2: "a =\<^sub>A b: U(i) \<Longrightarrow> a: A"
 and
-  Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> b: A"
-
+  Equal_form_cond3: "a =\<^sub>A b: U(i) \<Longrightarrow> b: A"
+*)
 lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp
-lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3
+(*lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*)
 lemmas Equal_comps [comp] = Equal_comp
 
 
diff --git a/EqualProps.thy b/EqualProps.thy
index 17c7fa6..9d23a99 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -15,20 +15,25 @@ begin
 
 section \<open>Symmetry / Path inverse\<close>
 
-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"
+definition inv :: "[Term, Term] \<Rightarrow> (Term \<Rightarrow> Term)"  ("(1inv[_,/ _])")
+  where "inv[x,y] \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) x y p"
 
 
 lemma inv_type:
-  assumes "A : U(i)" and "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)
+  assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "inv[x,y](p): y =\<^sub>A x"
+unfolding inv_def
+proof
+  show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> y =\<^sub>A x: U(i)" using assms(1) ..
+  show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
+qed (fact assms)+
 
-corollary assumes "x =\<^sub>A y : U(i)" and "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 : U(i)" and "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
-  unfolding inv_def by (simplify lems: assms)
+lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) \<equiv> refl(a)"
+unfolding inv_def
+proof
+  show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
+  show "\<And>x. x: A \<Longrightarrow> x =\<^sub>A x: U(i)" using assms(1) ..
+qed (fact assms)
 
 
 section \<open>Transitivity / Path composition\<close>
@@ -42,10 +47,8 @@ definition rcompose :: "Term \<Rightarrow> Term"  ("(1rcompose[_])")
     x y p"
 
 
-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"
+definition compose :: "[Term, Term, Term] \<Rightarrow> [Term, Term] \<Rightarrow> Term"  ("(1compose[ _,/ _,/ _])")
+  where "compose[x,y,z] \<equiv> \<lambda>p."
 
 
 lemma compose_type:
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 614419e..e94ca5c 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -56,6 +56,7 @@ and
   U_cumulative: "\<And>A i j. \<lbrakk>A: U(i); i <- j\<rbrakk> \<Longrightarrow> A: U(j)"
     \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close>
 
+
 section \<open>Type families\<close>
 
 text "
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 8351c3c..f80b99b 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -57,9 +57,9 @@ method derive uses lems unfolds = (
   unfold unfolds |
   simple lems: lems |
   match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> |
-  rule U_hierarchy |
+  rule U_hierarchy (*|
   (rule U_cumulative, simple lems: lems) |
-  (rule U_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>)
+  (rule U_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>)*)
   )+
 
 
diff --git a/Prod.thy b/Prod.thy
index 01cd006..5391943 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -41,20 +41,21 @@ abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarro
 section \<open>Type rules\<close>
 
 axiomatization where
-  Prod_form: "\<And>i A B. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x): U(i)"
+  Prod_form: "\<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x): U(i)"
 and
-  Prod_intro: "\<And>i A B b. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b(x): \<Prod>x:A. B(x)"
+  Prod_intro: "\<lbrakk>A: U(i); \<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: "\<And>A B f a. \<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)"
+  Prod_elim: "\<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)"
 and
-  Prod_comp: "\<And>i A B b a. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i); \<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: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)"
 and
-  Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
 
 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).
 "
 
+(*
 text "
   In addition to the usual type rules, it is a meta-theorem (*PROVE THIS!*) that whenever \<open>\<Prod>x:A. B x: U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>.
   
@@ -62,14 +63,15 @@ text "
 "
 
 axiomatization where
-  Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
+  Prod_form_cond1: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
 and
-  Prod_form_cond2: "\<And>i A B. (\<Prod>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
+  Prod_form_cond2: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
+*)
 
 text "Set up the standard reasoner to use the type rules:"
 
 lemmas Prod_rules = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
-lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2
+(*lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2*)
 lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
 
@@ -84,9 +86,9 @@ where
 and
   Unit_intro: "\<star>: \<one>"
 and
-  Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(a) : C(a)"
+  Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(a) : C(a)"
 and
-  Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c"
+  Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c"
 
 lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp
 lemmas Unit_comps [comp] = Unit_comp
diff --git a/Proj.thy b/Proj.thy
index 717df65..b1c21c1 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -18,8 +18,49 @@ abbreviation snd :: "Term \<Rightarrow> Term" where "snd \<equiv> \<lambda>p. in
 
 text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
 
-lemma assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
- by (derive lems: assms
+
+lemma fst_type:
+  assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
+proof
+  show "A: U(i)" using assms(1) by (rule Sum_forms)
+qed (fact assms | assumption)+
+
+
+lemma fst_comp:
+  assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a"
+proof
+  show "\<And>x. x: A \<Longrightarrow> x: A" .
+qed (rule assms)+
+
+
+lemma snd_type:
+  assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)"
+proof
+  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)"
+  proof -
+    have "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> fst(p): A" using assms(1) by (rule fst_type)
+    with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_forms)
+  qed
+
+  fix x y
+  assume asm: "x: A" "y: B(x)"
+  show "y: B(fst <x,y>)"
+  proof (subst fst_comp)
+    show "A: U(i)" using assms(1) by (rule Sum_forms)
+    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" using assms(1) by (rule Sum_forms)
+  qed (rule asm)+
+qed (fact assms)
+
+
+lemma snd_comp:
+  assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "snd(<a,b>) \<equiv> b"
+proof
+  show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" .
+  show "a: A" by (fact assms)
+  show "b: B(a)" by (fact assms)
+  show *: "B(a): U(i)" using assms(3) by (rule assms(2))
+  show "B(a): U(i)" by (fact *)
+qed
 
 
 end
\ No newline at end of file
diff --git a/Sum.thy b/Sum.thy
index cdfe5bd..eddb464 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -14,7 +14,7 @@ section \<open>Constants and syntax\<close>
 
 axiomatization
   Sum :: "[Term, Typefam] \<Rightarrow> Term" and
-  pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
+  pair :: "[Term, Term] \<Rightarrow> Term"  ("(1<_,/ _>)") and
   indSum :: "[[Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<Sum>)")
 
 syntax
@@ -34,34 +34,33 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
 section \<open>Type rules\<close>
 
 axiomatization where
-  Sum_form: "\<And>i A B. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x): U(i)"
+  Sum_form: "\<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x): U(i)"
 and
-  Sum_intro: "\<And>i A B a b. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i); a: A; b: B(a)\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B(x)"
+  Sum_intro: "\<lbrakk>B: A \<longrightarrow> U(i); a: A; b: B(a)\<rbrakk> \<Longrightarrow> <a,b> : \<Sum>x:A. B(x)"
 and
-  Sum_elim: "\<And>i A B C f p. \<lbrakk>
+  Sum_elim: "\<lbrakk>
     C: \<Sum>x:A. B(x) \<longrightarrow> U(i);
-    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C((x,y));
+    \<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> ind\<^sub>\<Sum>(f)(p) : C(p)"  (* What does writing \<lambda>x y. f(x, y) change? *)
 and
-  Sum_comp: "\<And>i A B C f a b. \<lbrakk>
-    A: U(i);
-    B: A \<longrightarrow> U(i);
+  Sum_comp: "\<lbrakk>
     C: \<Sum>x:A. B(x) \<longrightarrow> U(i);
-    \<And>x y. \<lbrakk>x: A; y :B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C((x,y));
+    B: A \<longrightarrow> U(i);
+    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C(<x,y>);
     a: A;
     b: B(a)
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)((a,b)) \<equiv> f(a)(b)"
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)(<a,b>) \<equiv> f(a)(b)"
 
 text "Admissible inference rules for sum formation:"
 
 axiomatization where
-  Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
+  Sum_form_cond1: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
 and
-  Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
+  Sum_form_cond2: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
 
 lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
-lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2
+lemmas Sum_forms = Sum_form Sum_form_cond1 Sum_form_cond2
 lemmas Sum_comps [comp] = Sum_comp
 
 
@@ -73,7 +72,7 @@ axiomatization
 where
   Empty_form: "\<zero> : U(O)"
 and
-  Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
+  Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
 
 lemmas Empty_rules [intro] = Empty_form Empty_elim
 
diff --git a/scratch.thy b/scratch.thy
index e06fb7e..3141120 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,6 +3,12 @@ theory scratch
 
 begin
 
+
+lemma "U(O): U(O)"
+proof (rule inhabited_implies_type)
+  show "\<nat>: U(O)" ..
+qed
+
 lemma
   assumes "\<Sum>x:A. B(x): U(i)" "(a,b): \<Sum>x:A. B(x)"
   shows "a : A"