blob: a68f79b9e598a9c1b28c98aaa535ecdfd500caa6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
(* Title: HoTT/ProdProps.thy
Author: Josh Chen
Properties of the dependent product
*)
theory ProdProps
imports
HoTT_Methods
Prod
begin
section \<open>Composition\<close>
text "
The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Prod>-type definitional equality, and the correct substitutions in the subgoals thereafter.
"
lemma compose_assoc:
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)"
proof (subst Prod_eq)
\<comment> \<open>Todo: set the Simplifier (or other simplification methods) up to use \<open>Prod_eq\<close>!\<close>
show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
proof compute
show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
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)
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)"
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"
proof compute
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)
text "Set up the \<open>compute\<close> method to automatically simplify function compositions."
lemmas compose_comp [comp]
end
|
