blob: 07fbfc41d048ca86905dd55066b296713f752374 (
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
77
78
79
80
|
(* Title: HoTT/HoTT_Base.thy
Author: Joshua Chen
Basic setup of a homotopy type theory object logic with a Russell-style cumulative universe hierarchy.
*)
theory HoTT_Base
imports
Pure
"HOL-Eisbach.Eisbach"
begin
section ‹Basic setup›
typedecl t ― ‹Type of object types and terms›
typedecl ord ― ‹Type of meta-level numerals›
axiomatization
O :: ord and
Suc :: "ord ⇒ ord" and
lt :: "[ord, ord] ⇒ prop" (infix "<" 999)
where
lt_Suc [intro]: "n < (Suc n)" and
lt_trans [intro]: "⟦m1 < m2; m2 < m3⟧ ⟹ m1 < m3" and
Suc_monotone [simp]: "m < n ⟹ (Suc m) < (Suc n)"
method proveSuc = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
text ‹Method @{method proveSuc} proves statements of the form ‹n < (Suc (... (Suc n) ...))›.›
section ‹Judgment›
judgment hastype :: "[t, t] ⇒ prop" ("(3_:/ _)")
section ‹Universes›
axiomatization
U :: "ord ⇒ t"
where
U_hierarchy: "i < j ⟹ U i: U j" and
U_cumulative: "⟦A: U i; i < j⟧ ⟹ A: U j"
text ‹
Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
›
method cumulativity = (elim U_cumulative, proveSuc) ― ‹Proves ‹A: U i ⟹ A: U (Suc (... (Suc i) ...))›.›
method hierarchy = (rule U_hierarchy, proveSuc) ― ‹Proves ‹U i: U (Suc (... (Suc i) ...)).››
section ‹Type families›
abbreviation (input) constrained :: "[t ⇒ t, t, t] ⇒ prop" ("(1_:/ _ ⟶ _)")
where "f: A ⟶ B ≡ (⋀x. x : A ⟹ f x: B)"
text ‹
The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A ⟶ B"} where @{term "A::t"} and @{term "B::t"} are small types.
›
type_synonym tf = "t ⇒ t" ― ‹Type of type families.›
section ‹Named theorems›
text ‹
Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
‹wellform› declares necessary well-formedness conditions for type and inhabitation judgments.
‹comp› declares computation rules, which are usually passed to invocations of the method ‹subst› to perform equational rewriting.
›
named_theorems wellform
named_theorems comp
end
|
