diff options
author | Josh Chen | 2018-06-17 19:08:22 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-17 19:08:22 +0200 |
commit | 7d8becd9e936c7a1212731ee92a85909c780f250 (patch) | |
tree | 4b7ec93e1641e6ef189f4208415160526fd21864 | |
parent | 5161a0356d8752f3b1b4f4385e799bca92718814 (diff) |
Eliminators must be completely parametrized at the meta-level.
-rw-r--r-- | Sum.thy | 19 |
1 files changed, 5 insertions, 14 deletions
@@ -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: |