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_Methods.thy
Author: Joshua Chen
Date: 2018
Method setup for the HoTT logic.
*)
theory HoTT_Methods
imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
begin
section ‹Handling universes›
method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
method hierarchy = (rule U_hierarchy, provelt)
method cumulativity declares form = (
((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) |
((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
)
text ‹
Methods @{method provelt}, @{method hierarchy}, and @{method cumulativity} prove statements of the form
▪ ‹n < (Suc (... (Suc n) ...))›,
▪ ‹U i: U (Suc (... (Suc i) ...))›, and
▪ @{prop "A: U i ⟹ A: U j"}, where @{prop "i ≤ j"}
respectively.
›
section ‹Deriving typing judgments›
method routine uses add = (assumption | rule add | rule)+
text ‹
The method @{method routine} proves type judgments @{prop "a : A"} using the rules declared @{attribute intro} in the respective theory files, as well as additional provided lemmas passed using the modifier ‹add›.
›
section ‹Substitution and simplification›
ML_file "~~/src/Tools/misc_legacy.ML"
ML_file "~~/src/Tools/IsaPlanner/isand.ML"
ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
ML_file "~~/src/Tools/eqsubst.ML"
― ‹Import the @{method subst} method, used for substituting definitional equalities.›
method compute declares comp = (subst comp)
text ‹
Method @{method compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context.
Premises of the rule(s) applied are added as new subgoals.
›
section ‹Derivation search›
text ‹
Combine @{method routine} and @{method compute} to search for derivations of judgments.
Also handle universes using @{method hierarchy} and @{method cumulativity}.
›
method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
section ‹Induction›
text ‹
Placeholder section for the automation of induction, i.e. using the elimination rules.
At the moment one must directly apply them with ‹rule X_elim›.
›
end
|
