From 7a89ec1e72f61179767c6488177c6d12e69388c5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 12 Aug 2018 13:04:16 +0200
Subject: Commit before testing polymorphic equality eliminator

---
 Sum.thy | 27 +++++++++++++--------------
 1 file changed, 13 insertions(+), 14 deletions(-)

(limited to 'Sum.thy')

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
 
-- 
cgit v1.2.3