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
|
(* Title: context_tactical.ML
Author: Joshua Chen
More context tactics, and context tactic combinators.
*)
infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD
infix 0 CORELSE CAPPEND CORELSE' CAPPEND'
structure Context_Tactical:
sig
type context_tactic' = int -> context_tactic
val all_ctac: context_tactic
val no_ctac: context_tactic
val print_ctac: (Proof.context -> string) -> context_tactic
val CTHEN: context_tactic * context_tactic -> context_tactic
val CORELSE: context_tactic * context_tactic -> context_tactic
val CAPPEND: context_tactic * context_tactic -> context_tactic
val CTHEN': context_tactic' * context_tactic' -> context_tactic'
val CORELSE': context_tactic' * context_tactic' -> context_tactic'
val CAPPEND': context_tactic' * context_tactic' -> context_tactic'
val CTRY: context_tactic -> context_tactic
val CREPEAT: context_tactic -> context_tactic
val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic
val CCHANGED: context_tactic -> context_tactic
val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic'
val CREPEAT_ALL_NEW: context_tactic' -> context_tactic'
val CTHEN_ALL_NEW_FWD: context_tactic' * context_tactic' -> context_tactic'
val CREPEAT_ALL_NEW_FWD: context_tactic' -> context_tactic'
val CHEADGOAL: context_tactic' -> context_tactic
val CALLGOALS: context_tactic' -> context_tactic
end = struct
type context_tactic' = int -> context_tactic
val all_ctac = Seq.make_results o Seq.single
val no_ctac = K Seq.empty
fun print_ctac f (ctxt, st) = CONTEXT_TACTIC (print_tac ctxt (f ctxt)) (ctxt, st)
fun (ctac1 CTHEN ctac2) cst = Seq.maps_results ctac2 (ctac1 cst)
fun (ctac1 CORELSE ctac2) cst =
(case Seq.pull (ctac1 cst) of
NONE => ctac2 cst
| some => Seq.make (fn () => some))
fun (ctac1 CAPPEND ctac2) cst =
Seq.append (ctac1 cst) (Seq.make (fn () => Seq.pull (ctac2 cst)))
fun (ctac1 CTHEN' ctac2) x = ctac1 x CTHEN ctac2 x
fun (ctac1 CORELSE' ctac2) x = ctac1 x CORELSE ctac2 x
fun (ctac1 CAPPEND' ctac2) x = ctac1 x CAPPEND ctac2 x
fun CTRY ctac = ctac CORELSE all_ctac
fun CREPEAT ctac =
let
fun rep qs cst =
(case Seq.pull (Seq.filter_results (ctac cst)) of
NONE => SOME (cst, Seq.make (fn () => repq qs))
| SOME (cst', q) => rep (q :: qs) cst')
and repq [] = NONE
| repq (q :: qs) =
(case Seq.pull q of
NONE => repq qs
| SOME (cst, q) => rep (q :: qs) cst);
in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end
fun CFILTER pred ctac cst =
ctac cst
|> Seq.filter_results
|> Seq.filter pred
|> Seq.make_results
(*Only accept next states where the subgoals have changed*)
fun CCHANGED ctac (cst as (_, st)) =
CFILTER (fn (_, st') => not (Thm.eq_thm (st, st'))) ctac cst
local
fun op THEN (f, g) x = Seq.maps_results g (f x)
fun INTERVAL f i j x =
if i > j then Seq.make_results (Seq.single x)
else op THEN (f j, INTERVAL f i (j - 1)) x
(*By Peter Lammich: apply tactic to subgoals in interval in a forward manner,
skipping over emerging subgoals*)
fun INTERVAL_FWD ctac l u (cst as (_, st)) =
if l > u then all_ctac cst
else (ctac l CTHEN (fn cst' as (_, st') =>
let val ofs = Thm.nprems_of st' - Thm.nprems_of st in
if ofs < ~1
then raise THM (
"INTERVAL_FWD: tactic solved more than one goal", ~1, [st, st'])
else INTERVAL_FWD ctac (l + 1 + ofs) (u + ofs) cst'
end)) cst
in
fun (ctac1 CTHEN_ALL_NEW ctac2) i (cst as (_, st)) =
cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
cst' |> INTERVAL ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)))
(*By Peter Lammich: apply ctac2 to all subgoals emerging from ctac1, in forward
manner*)
fun (ctac1 CTHEN_ALL_NEW_FWD ctac2) i (cst as (_, st)) =
cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
cst' |> INTERVAL_FWD ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)))
end
fun CREPEAT_ALL_NEW ctac =
ctac CTHEN_ALL_NEW (CTRY o (fn i => CREPEAT_ALL_NEW ctac i))
fun CREPEAT_ALL_NEW_FWD ctac =
ctac CTHEN_ALL_NEW_FWD (CTRY o (fn i => CREPEAT_ALL_NEW_FWD ctac i))
fun CHEADGOAL ctac = ctac 1
fun CALLGOALS ctac (cst as (_, st)) =
let
fun doall 0 = all_ctac
| doall n = ctac n CTHEN doall (n - 1);
in doall (Thm.nprems_of st) cst end
end
open Context_Tactical
|
