diff options
author | Josh Chen | 2019-03-27 14:41:16 +0100 |
---|---|---|
committer | Josh Chen | 2019-03-27 14:41:16 +0100 |
commit | b01b8ee0f3472cb728f09463d0620ac8b8066bcb (patch) | |
tree | 9d0b5842a7d55fad45f5219314d89c6cd8f31ba0 /Prod.thy | |
parent | 45c3879db6850282bc067318e31cccf42e60ac8f (diff) |
More progress. I think we are reaching the limit of what can be conveniently proved with the current implementation.
Diffstat (limited to 'Prod.thy')
-rw-r--r-- | Prod.thy | 32 |
1 files changed, 30 insertions, 2 deletions
@@ -119,8 +119,36 @@ unfolding compose_def by (derive lems: assms cong) abbreviation id :: "t \<Rightarrow> t" ("(id _)" [115] 114) where "id A \<equiv> \<lambda>x: A. x" -lemma id_type [intro]: "\<And>A. A: U i \<Longrightarrow> id A: A \<rightarrow> A" by derive - +lemma id_type: "\<And>A. A: U i \<Longrightarrow> id A: A \<rightarrow> A" by derive + +lemma id_compl: + assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" + shows "id B o[A] f \<equiv> f" +unfolding compose_def proof - + { + fix x assume [intro]: "x: A" + have "(id B)`(f`x) \<equiv> f`x" by derive + } + hence "\<lambda>x: A. (id B)`(f`x) \<equiv> \<lambda>x: A. f`x" by (derive lems: cong) derive + also have "\<lambda>x: A. f`x \<equiv> f" by derive + finally show "\<lambda>(x: A). (id B)`(f`x) \<equiv> f" by simp +qed + +lemma id_compr: + assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" + shows "f o[A] id A \<equiv> f" +unfolding compose_def proof - + { + fix x assume [intro]: "x: A" + have "f`((id A)`x) \<equiv> f`x" by derive + } + hence "\<lambda>x: A. f`((id A)`x) \<equiv> \<lambda>x: A. f`x" by (derive lems: cong) derive + also have "\<lambda>x: A. f`x \<equiv> f" by derive + finally show "\<lambda>x: A. f`((id A)`x) \<equiv> f" by simp +qed + +declare id_type [intro] +lemmas id_comp [comp] = id_compl id_compr section \<open>Universal quantification\<close> |