blob: 1c921bd28dcb76303860e0df410a54dffb83b0af (
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
58
59
60
61
|
theory scratch
imports HoTT
begin
(* Typechecking *)
schematic_goal "⟦a : A; b : B⟧ ⟹ (a,b) : ?A" by simple
(* Simplification *)
notepad begin
assume asm:
"f`a ≡ g"
"g`b ≡ ❙λx:A. d"
"c : A"
"d : B"
have "f`a`b`c ≡ d" by (simp add: asm | rule comp | derive lems: asm)+
end
lemma "a : A ⟹ indEqual[A] (λx y _. y =⇩A x) (λx. refl(x)) a a refl(a) ≡ refl(a)"
by verify_simp
lemma "⟦a : A; ⋀x. x : A ⟹ b x : X⟧ ⟹ (❙λx:A. b x)`a ≡ b a"
by verify_simp
lemma
assumes "a : A" and "⋀x. x : A ⟹ b x : B x"
shows "(❙λx:A. b x)`a ≡ b a"
by (verify_simp lems: assms)
lemma "⟦a : A; b : B a; B: A → U⟧ ⟹ (❙λx:A. ❙λy:B x. c x y)`a`b ≡ c a b"
oops
lemma
assumes
"(❙λx:A. ❙λy:B x. c x y)`a ≡ ❙λy:B a. c a y"
"(❙λy:B a. c a y)`b ≡ c a b"
shows "(❙λx:A. ❙λy:B x. c x y)`a`b ≡ c a b"
apply (simp add: assms)
done
lemmas lems =
Prod_comp[where ?A = "B a" and ?b = "λb. c a b" and ?a = b]
Prod_comp[where ?A = A and ?b = "λx. ❙λy:B x. c x y" and ?a = a]
lemma
assumes
"a : A"
"b : B a"
"B: A → U"
"⋀x y. ⟦x : A; y : B x⟧ ⟹ c x y : D x y"
shows "(❙λx:A. ❙λy:B x. c x y)`a`b ≡ c a b"
apply (verify_simp lems: assms)
end
|
