blob: c72947a305ff4ffdd034ad7174ad130b09f57d34 (
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
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
|
(* 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 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>)
@(Elim.rules ctxt))
in (resolve_from_net_tac ctxt net) i end
else no_tac)
in
CHANGED o REPEAT o 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)
(*Combinator runs tactic and tries to discharge all new typing side conditions*)
fun SIDE_CONDS tac ctxt =
let
val side_cond_tac =
if Config.get ctxt auto_typechk then typechk_tac ctxt else known_tac ctxt
in
tac THEN_ALL_NEW (TRY o side_cond_tac)
end
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 =
SIDE_CONDS (resolve_tac ctxt (mk_rules 0 [] ths)) ctxt
(*Attempts destruct-resolution with the n-th premise of the given rules*)
fun dest_tac opt_n ths ctxt = SIDE_CONDS (dresolve_tac ctxt
(mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths))
ctxt
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 elims_tac opt_tm ctxt = case opt_tm of
NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (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.get_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)
end
open Tactics
|
