blob: aa6fca2ff9744af115767c8f6cc287847b221463 (
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(* Title: HoTT/HoTT_Methods.thy
Author: Josh Chen
Date: Jun 2018
Method setup for the HoTT library.
Relies on Eisbach, which for the moment lives in HOL/Eisbach.
*)
theory HoTT_Methods
imports
"HOL-Eisbach.Eisbach"
"HOL-Eisbach.Eisbach_Tools"
HoTT_Base
Prod
Sum
begin
text "This method finds a proof of any valid typing judgment derivable from a given wellformed judgment."
method wellformed uses jdgmt = (
match jdgmt in
"?a : ?A" ⇒ ‹
rule HoTT_Base.inhabited_implies_type[OF jdgmt] |
wellformed jdgmt: HoTT_Base.inhabited_implies_type[OF jdgmt]
› ¦
"A : U" for A ⇒ ‹
match (A) in
"∏x:?A. ?B x" ⇒ ‹
rule Prod.Prod_form_cond1[OF jdgmt] |
rule Prod.Prod_form_cond2[OF jdgmt] |
catch ‹wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]› ‹fail› |
catch ‹wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]› ‹fail›
› ¦
"∑x:?A. ?B x" ⇒ ‹
rule Sum.Sum_form_cond1[OF jdgmt] |
rule Sum.Sum_form_cond2[OF jdgmt] |
catch ‹wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]› ‹fail› |
catch ‹wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]› ‹fail›
›
› ¦
"PROP ?P ⟹ PROP Q" for Q ⇒ ‹
catch ‹rule Prod.Prod_form_cond1[OF jdgmt]› ‹fail› |
catch ‹rule Prod.Prod_form_cond2[OF jdgmt]› ‹fail› |
catch ‹rule Sum.Sum_form_cond1[OF jdgmt]› ‹fail› |
catch ‹rule Sum.Sum_form_cond2[OF jdgmt]› ‹fail› |
catch ‹wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]› ‹fail› |
catch ‹wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]› ‹fail› |
catch ‹wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]› ‹fail› |
catch ‹wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]› ‹fail›
›
)
notepad ― ‹Examples using ‹wellformed››
begin
assume 0: "f : ∑x:A. B x"
have "∑x:A. B x : U" by (wellformed jdgmt: 0)
have "A : U" by (wellformed jdgmt: 0)
have "B: A → U" by (wellformed jdgmt: 0)
assume 1: "f : ∏x:A. ∏y: B x. C x y"
have "A : U" by (wellformed jdgmt: 1)
have "B: A → U" by (wellformed jdgmt: 1)
have "⋀x. x : A ⟹ C x: B x → U" by (wellformed jdgmt: 1)
assume 2: "g : ∑x:A. ∏y: B x. ∑z: C x y. D x y z"
have a: "A : U" by (wellformed jdgmt: 2)
have b: "B: A → U" by (wellformed jdgmt: 2)
have c: "⋀x. x : A ⟹ C x : B x → U" by (wellformed jdgmt: 2)
have d: "⋀x y. ⟦x : A; y : B x⟧ ⟹ D x y : C x y → U" by (wellformed jdgmt: 2)
end
end
|
