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
|
(* Title: tactics.ML
Author: Joshua Chen
General tactics for dependent type theory.
*)
structure Tactics:
sig
val solve_side_conds: int Config.T
val SIDE_CONDS: int -> context_tactic' -> thm list -> context_tactic'
val rule_ctac: thm list -> context_tactic'
val dest_ctac: int option -> thm list -> context_tactic'
val intro_ctac: context_tactic'
val elim_ctac: term list -> context_tactic'
val cases_ctac: term -> context_tactic'
end = struct
(* Side conditions *)
val solve_side_conds = Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2)
fun SIDE_CONDS j ctac facts i (cst as (ctxt, st)) = cst |>
(case Config.get ctxt solve_side_conds of
1 => (ctac CTHEN_ALL_NEW (CTRY o Types.known_ctac facts)) i
| 2 => ctac i CTHEN CREPEAT_IN_RANGE (i + j) (Thm.nprems_of st - i)
(CTRY o CREPEAT_ALL_NEW_FWD (Types.check_infer facts))
| _ => ctac i)
(* rule, dest, intro *)
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*)
fun rule_ctac ths i (ctxt, st) =
TACTIC_CONTEXT ctxt (resolve_tac ctxt (mk_rules 0 [] ths) i st)
(*Attempts destruct-resolution with the n-th premise of the given rules*)
fun dest_ctac opt_n ths i (ctxt, st) =
TACTIC_CONTEXT ctxt (dresolve_tac ctxt
(mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths)
i st)
end
(*Applies an appropriate introduction rule*)
val intro_ctac = CONTEXT_TACTIC' (fn ctxt => SUBGOAL (fn (goal, i) =>
let val concl = Logic.strip_assums_concl goal in
if Lib.is_typing concl andalso Lib.is_rigid (Lib.type_of_typing concl)
then resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) i
else no_tac
end))
(* Induction/elimination *)
(*Pushes a known typing t:T into a \<Prod>-type.
This tactic is well-behaved only when t is sufficiently well specified
(otherwise there might be multiple possible judgments t:T that unify, and
which is chosen is undefined).*)
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])
(*Unify with the correct type T*)
THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.known_ctac [])
end)
fun elim_core_tac tms types ctxt =
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
resolve_tac ctxt rules
THEN' RANGE (replicate (length tms) (NO_CONTEXT_TACTIC ctxt o Types.check_infer []))
end handle Option => K no_tac
(*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)
)
fun elim_ctac tms =
case tms of
[] => CONTEXT_TACTIC' (fn ctxt => eresolve_tac ctxt (map #1 (Elim.rules ctxt)))
| major :: _ => CONTEXT_SUBGOAL (fn (goal, _) => fn cst as (ctxt, st) =>
let
val facts = map Thm.prop_of (Context_Facts.known ctxt)
val prems = Logic.strip_assums_hyp goal
val template = Lib.typing_of_term major
val types = filter (fn th => Term.could_unify (template, th)) (facts @ prems)
|> map Lib.type_of_typing
in case types of
[] => no_ctac cst
| _ =>
let
val inserts = 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[rotated]} i))))
in
TACTIC_CONTEXT (record_inserts ctxt) (tac st)
end
end)
fun cases_ctac tm =
let fun tac ctxt =
SUBGOAL (fn (goal, i) =>
let
val facts = Proof_Context.facts_of ctxt
val prems = Logic.strip_assums_hyp goal
val template = Lib.typing_of_term tm
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
val res = (case types of
[typ] => Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt tm)]
(the (Case.lookup_rule ctxt (Term.head_of typ)))
| [] => raise Option
| _ => raise error (Syntax.string_of_term ctxt tm ^ "not uniquely typed"))
handle Option =>
error ("No case rule known for " ^ (Syntax.string_of_term ctxt tm))
in
resolve_tac ctxt [res] i
end)
in CONTEXT_TACTIC' tac end
end
open Tactics
|
