diff options
author | Josh Chen | 2018-09-11 08:59:16 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-11 08:59:16 +0200 |
commit | 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 (patch) | |
tree | 48fd7cf1d921067e276f2d981ec20f133693baaa /ProdProps.thy | |
parent | bed5d559b62cf3f3acb75b28c2e192e274f46cc1 (diff) |
Go back to higher-order application notation
Diffstat (limited to '')
-rw-r--r-- | ProdProps.thy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/ProdProps.thy b/ProdProps.thy index 1af6ad3..14556af 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -18,7 +18,7 @@ text " " lemma compose_assoc: - assumes "A: U(i)" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D(x)" + assumes "A: U i" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D x" shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)" proof (subst (0 1 2 3) compose_def) show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)" @@ -31,19 +31,19 @@ proof (subst (0 1 2 3) compose_def) proof compute show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (routine lems: assms) qed - show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" by (routine lems: assms) + show "\<And>x. x: B \<Longrightarrow> h`(g`x): D (g`x)" by (routine lems: assms) qed (routine lems: assms) qed fact qed lemma compose_comp: - assumes "A: U(i)" and "\<And>x. x: A \<Longrightarrow> b(x): B" and "\<And>x. x: B \<Longrightarrow> c(x): C(x)" - shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" + assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x" + shows "(\<^bold>\<lambda>x. c x) \<circ> (\<^bold>\<lambda>x. b x) \<equiv> \<^bold>\<lambda>x. c (b x)" proof (subst compose_def, subst Prod_eq) - show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a" + show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c x)`((\<^bold>\<lambda>x. b x)`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a" proof compute - show "\<And>a. a: A \<Longrightarrow> c((\<^bold>\<lambda>x. b(x))`a) \<equiv> (\<^bold>\<lambda>x. c(b(x)))`a" + show "\<And>a. a: A \<Longrightarrow> c ((\<^bold>\<lambda>x. b x)`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a" by (derive lems: assms) qed (routine lems: assms) qed (derive lems: assms) |