diff options
author | Josh Chen | 2018-07-09 11:17:50 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-09 11:17:50 +0200 |
commit | 6389f18fd17e4333aba3fcdcc9ed2810d4cb1da5 (patch) | |
tree | 33665cf1631895d723a031536dfcf8cc15ecf932 /Proj.thy | |
parent | decb363a30a30c1875bf4b93bc544c28edf3149e (diff) |
Pre-universe implementation commit
Diffstat (limited to '')
-rw-r--r-- | Proj.thy | 41 |
1 files changed, 16 insertions, 25 deletions
@@ -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 |