aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Sum.thy19
1 files changed, 5 insertions, 14 deletions
diff --git a/Sum.thy b/Sum.thy
index 3db0f23..93b1e72 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -13,7 +13,7 @@ begin
axiomatization
Sum :: "[Term, Typefam] \<Rightarrow> Term" and
pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and
- indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term] \<Rightarrow> Term" ("(1indSum[_,/ _])")
+ indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1indSum[_,/ _])")
syntax
"_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20)
@@ -32,14 +32,14 @@ and
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"
+ \<rbrakk> \<Longrightarrow> indSum[A,B] C f p : C p"
and
Sum_comp [simp]: "\<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"
+ \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b"
\<comment> \<open>Nondependent pair\<close>
abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50)
@@ -74,16 +74,7 @@ begin
"snd_nondep A B \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y)"
end
-text "Properties of projections:"
-
-lemma fst_dep_type:
- assumes "p : \<Sum>x:A. B x"
- shows "fst[A,B]`p : A"
-proof -
- have "\<Sum>x:A. B x : U" using assms ..
- then have "A : U" by (rule Sum_intro)
- unfolding fst_dep_def using assms by (rule Sum_comp)
-
+text "Properties of projections:"
lemma fst_dep_comp:
assumes "a : A" and "b : B a"
@@ -101,7 +92,7 @@ lemma snd_dep_comp:
proof -
have "\<lambda>p. B fst[A,B]`p: \<Sum>x:A. B x \<rightarrow> U"
- ultimately show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by (rule Sum_comp)
+ show "snd[A,B]`(a,b) \<equiv> b" unfolding fst_dep_def
qed
lemma fst_nondep_comp: