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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
|
(* Title: tactics.ML
Author: Joshua Chen
General tactics for dependent type theory.
*)
structure Tactics(* :
sig
val assumptions_tac: Proof.context -> int -> tactic
val known_tac: Proof.context -> int -> tactic
val typechk_tac: Proof.context -> int -> tactic
val auto_typechk: bool Config.T
val SIDE_CONDS: (int -> tactic) -> Proof.context -> int -> tactic
val rule_tac: thm list -> Proof.context -> int -> tactic
val dest_tac: int option -> thm list -> Proof.context -> int -> tactic
val intro_tac: Proof.context -> int -> tactic
val intros_tac: Proof.context -> int -> tactic
val old_elims_tac: term option -> Proof.context -> int -> tactic
end *) = struct
(*An assumption tactic that only solves typing goals with rigid terms and
judgmental equalities without schematic variables*)
fun assumptions_tac ctxt = SUBGOAL (fn (goal, i) =>
let
val concl = Logic.strip_assums_concl goal
in
if
Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl)
orelse not ((exists_subterm is_Var) concl)
then assume_tac ctxt i
else no_tac
end)
(*Solves typing goals with rigid term by resolving with context facts and
simplifier premises, or arbitrary goals by *non-unifying* assumption*)
fun known_tac ctxt = SUBGOAL (fn (goal, i) =>
let
val concl = Logic.strip_assums_concl goal
in
((if Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl)
then
let val ths = map fst (Facts.props (Proof_Context.facts_of ctxt))
in resolve_tac ctxt (ths @ Simplifier.prems_of ctxt) end
else K no_tac)
ORELSE' assumptions_tac ctxt) i
end)
(*Typechecking: try to solve goals of the form "a: A" where a is rigid*)
fun typechk_tac ctxt =
let
val tac = SUBGOAL (fn (goal, i) =>
if Lib.rigid_typing_concl goal
then
let val net = Tactic.build_net
((Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>)
@(Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)
@(map #1 (Elim.rules ctxt)))
in (resolve_from_net_tac ctxt net) i end
else no_tac)
in
REPEAT_ALL_NEW (known_tac ctxt ORELSE' tac)
end
(*Many methods try to automatically discharge side conditions by typechecking.
Switch this flag off to discharge by non-unifying assumption instead.*)
val auto_typechk = Attrib.setup_config_bool \<^binding>\<open>auto_typechk\<close> (K true)
fun side_cond_tac ctxt = CHANGED o REPEAT o
(if Config.get ctxt auto_typechk then typechk_tac ctxt else known_tac ctxt)
(*Combinator runs tactic and tries to discharge all new typing side conditions*)
fun SIDE_CONDS tac ctxt = tac THEN_ALL_NEW (TRY o side_cond_tac ctxt)
local
fun mk_rules _ ths [] = ths
| mk_rules n ths ths' =
let val ths'' = foldr1 (op @)
(map (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => []) ths')
in
mk_rules n (ths @ ths') ths''
end
in
(*Resolves with given rules, discharging as many side conditions as possible*)
fun rule_tac ths ctxt = resolve_tac ctxt (mk_rules 0 [] ths)
(*Attempts destruct-resolution with the n-th premise of the given rules*)
fun dest_tac opt_n ths ctxt = dresolve_tac ctxt
(mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths)
end
(*Applies some introduction rule*)
fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS
(resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)) ctxt i)
fun intros_tac ctxt = SUBGOAL (fn (_, i) =>
(CHANGED o REPEAT o CHANGED o intro_tac ctxt) i)
(*Basic elimination tactic, only uses existing type judgments from the context
(performs no type synthesis)*)
fun old_elims_tac opt_tm ctxt = case opt_tm of
NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (map #1 (Elim.rules ctxt)) i)
| SOME tm => SUBGOAL (fn (goal, i) =>
let
fun elim_rule typing =
let
val hd = head_of (Lib.type_of_typing typing)
val opt_rl = Elim.lookup_rule ctxt hd
in
case opt_rl of
NONE => Drule.dummy_thm
| SOME (rl, _) => Drule.infer_instantiate' ctxt
[SOME (Thm.cterm_of ctxt tm)] rl
end
val template = Lib.typing_of_term tm
val facts = Proof_Context.facts_of ctxt
val candidate_typings = Facts.could_unify facts template
val candidate_rules =
map (elim_rule o Thm.prop_of o #1) candidate_typings
val prems = Logic.strip_assums_hyp goal
val candidate_typings' =
filter (fn prem => Term.could_unify (template, prem)) prems
val candidate_rules' = map elim_rule candidate_typings'
in
(resolve_tac ctxt candidate_rules
ORELSE' eresolve_tac ctxt candidate_rules') i
end)
(* Revamped general induction/elimination *)
(*Pushes a context/goal premise typing t:T into a \<Prod>-type*)
fun internalize_fact_tac t =
Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl = raw_concl, ...} =>
let
val concl = Logic.strip_assums_concl (Thm.term_of raw_concl)
val C = Lib.type_of_typing concl
val B = Thm.cterm_of ctxt (Lib.lambda_var t C)
val a = Thm.cterm_of ctxt t
(*The resolvent is PiE[where ?B=B and ?a=a]*)
val resolvent =
Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
in
HEADGOAL (resolve_tac ctxt [resolvent])
(*known_tac infers the correct type T inferred by unification*)
THEN SOMEGOAL (known_tac ctxt)
end)
(*Premises that have already been pushed into the \<Prod>-type*)
structure Inserts = Proof_Data (
type T = term Item_Net.T
val init = K (Item_Net.init Term.aconv_untyped single)
)
local
fun elim_core_tac tms types ctxt = SUBGOAL (K (
let
val rule_insts = map ((Elim.lookup_rule ctxt) o Term.head_of) types
val rules = flat (map
(fn rule_inst => case rule_inst of
NONE => []
| SOME (rl, idxnames) => [Drule.infer_instantiate ctxt
(idxnames ~~ map (Thm.cterm_of ctxt) tms) rl])
rule_insts)
in
HEADGOAL (resolve_tac ctxt rules)
THEN RANGE (replicate (length tms) (typechk_tac ctxt)) 1
end handle Option => no_tac))
in
fun elim_context_tac tms ctxt = case tms of
[] => CONTEXT_SUBGOAL (K (Context_Tactic.CONTEXT_TACTIC (HEADGOAL (
SIDE_CONDS (eresolve_tac ctxt (map #1 (Elim.rules ctxt))) ctxt))))
| major::_ => CONTEXT_SUBGOAL (fn (goal, _) =>
let
val facts = Proof_Context.facts_of ctxt
val prems = Logic.strip_assums_hyp goal
val template = Lib.typing_of_term major
val types =
map (Thm.prop_of o #1) (Facts.could_unify facts template)
@ filter (fn prem => Term.could_unify (template, prem)) prems
|> map Lib.type_of_typing
in case types of
[] => Context_Tactic.CONTEXT_TACTIC no_tac
| _ =>
let
val inserts = map (Thm.prop_of o fst) (Facts.props facts) @ prems
|> filter Lib.is_typing
|> map Lib.dest_typing
|> filter_out (fn (t, _) =>
Term.aconv (t, major) orelse Item_Net.member (Inserts.get ctxt) t)
|> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct tms T))
|> filter (fn (_, i) => i > 0)
(*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
If they are incomparable, then order by decreasing
`subterm_count [p, x, y] T`*)
|> sort (fn (((t1, _), i), ((_, T2), j)) =>
Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
|> map (#1 o #1)
val record_inserts = Inserts.map (fold Item_Net.update inserts)
val tac =
(*Push premises having a subterm in `tms` into a \<Prod>*)
fold (fn t => fn tac =>
tac THEN HEADGOAL (internalize_fact_tac t ctxt))
inserts all_tac
(*Apply elimination rule*)
THEN (HEADGOAL (
elim_core_tac tms types ctxt
(*Pull pushed premises back out*)
THEN_ALL_NEW (SUBGOAL (fn (_, i) =>
REPEAT_DETERM_N (length inserts)
(resolve_tac ctxt @{thms PiI} i)))
))
(*Side conditions*)
THEN ALLGOALS (TRY o side_cond_tac ctxt)
in
fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT
(record_inserts ctxt) (tac st)
end
end)
end
end
open Tactics
|
