author | wenzelm |
Tue, 06 Jun 2006 20:42:28 +0200 | |
changeset 19798 | 94f12468bbba |
parent 19482 | 9f11af8f7ef9 |
child 19917 | 8b4869928f72 |
permissions | -rw-r--r-- |
8364 | 1 |
(* Title: Pure/Isar/rule_cases.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
5 |
Annotations and local contexts of rules. |
8364 | 6 |
*) |
7 |
||
18188 | 8 |
infix 1 THEN_ALL_NEW_CASES; |
9 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
10 |
signature BASIC_RULE_CASES = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
11 |
sig |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
12 |
type cases |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
13 |
type cases_tactic |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
14 |
val CASES: cases -> tactic -> cases_tactic |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
15 |
val NO_CASES: tactic -> cases_tactic |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
16 |
val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
17 |
val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
18 |
end |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
19 |
|
8364 | 20 |
signature RULE_CASES = |
21 |
sig |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
22 |
include BASIC_RULE_CASES |
18608 | 23 |
datatype T = Case of |
24 |
{fixes: (string * typ) list, |
|
25 |
assumes: (string * term list) list, |
|
26 |
binds: (indexname * term option) list, |
|
27 |
cases: (string * T) list} |
|
28 |
val strip_params: term -> (string * typ) list |
|
29 |
val make_common: bool -> theory * term -> (string * string list) list -> cases |
|
30 |
val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases |
|
31 |
val make_simple: bool -> theory * term -> string -> cases |
|
32 |
val apply: term list -> T -> T |
|
18237 | 33 |
val consume: thm list -> thm list -> ('a * int) * thm -> |
34 |
(('a * (int * thm list)) * thm) Seq.seq |
|
18477 | 35 |
val add_consumes: int -> thm -> thm |
18728 | 36 |
val consumes: int -> attribute |
37 |
val consumes_default: int -> attribute |
|
8364 | 38 |
val name: string list -> thm -> thm |
18728 | 39 |
val case_names: string list -> attribute |
40 |
val case_conclusion: string * string list -> attribute |
|
12761 | 41 |
val save: thm -> thm -> thm |
18237 | 42 |
val get: thm -> (string * string list) list * int |
8427 | 43 |
val rename_params: string list list -> thm -> thm |
18728 | 44 |
val params: string list list -> attribute |
18477 | 45 |
val mutual_rule: thm list -> (int list * thm) option |
18581 | 46 |
val strict_mutual_rule: thm list -> int list * thm |
8364 | 47 |
end; |
48 |
||
49 |
structure RuleCases: RULE_CASES = |
|
50 |
struct |
|
51 |
||
18608 | 52 |
(** cases **) |
53 |
||
54 |
datatype T = Case of |
|
55 |
{fixes: (string * typ) list, |
|
56 |
assumes: (string * term list) list, |
|
57 |
binds: (indexname * term option) list, |
|
58 |
cases: (string * T) list}; |
|
59 |
||
60 |
type cases = (string * T option) list; |
|
61 |
||
62 |
val case_conclN = "case"; |
|
63 |
val case_hypsN = "hyps"; |
|
64 |
val case_premsN = "prems"; |
|
65 |
||
66 |
val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params; |
|
67 |
||
68 |
local |
|
69 |
||
70 |
fun abs xs t = Term.list_abs (xs, t); |
|
71 |
fun app us t = Term.betapplys (t, us); |
|
72 |
||
73 |
fun dest_binops cs tm = |
|
74 |
let |
|
75 |
val n = length cs; |
|
76 |
fun dest 0 _ = [] |
|
77 |
| dest 1 t = [t] |
|
78 |
| dest k (_ $ t $ u) = t :: dest (k - 1) u |
|
79 |
| dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]); |
|
80 |
in cs ~~ dest n tm end; |
|
81 |
||
82 |
fun extract_fixes NONE prop = (strip_params prop, []) |
|
83 |
| extract_fixes (SOME outline) prop = |
|
19012 | 84 |
chop (length (Logic.strip_params outline)) (strip_params prop); |
18608 | 85 |
|
86 |
fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], []) |
|
87 |
| extract_assumes qual (SOME outline) prop = |
|
88 |
let val (hyps, prems) = |
|
19012 | 89 |
chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop) |
18608 | 90 |
in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end; |
91 |
||
92 |
fun extract_case is_open thy (case_outline, raw_prop) name concls = |
|
93 |
let |
|
94 |
val rename = if is_open then I else (apfst Syntax.internal); |
|
95 |
||
96 |
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop); |
|
97 |
val len = length props; |
|
98 |
val nested = is_some case_outline andalso len > 1; |
|
99 |
||
100 |
fun extract prop = |
|
101 |
let |
|
102 |
val (fixes1, fixes2) = extract_fixes case_outline prop |
|
103 |
|> apfst (map rename); |
|
104 |
val abs_fixes = abs (fixes1 @ fixes2); |
|
105 |
fun abs_fixes1 t = |
|
106 |
if not nested then abs_fixes t |
|
107 |
else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t)); |
|
108 |
||
109 |
val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
110 |
|> pairself (map (apsnd (maps Logic.dest_conjunctions))); |
18608 | 111 |
|
112 |
val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop); |
|
113 |
val binds = |
|
114 |
(case_conclN, concl) :: dest_binops concls concl |
|
115 |
|> map (fn (x, t) => ((x, 0), SOME (abs_fixes t))); |
|
116 |
in |
|
117 |
((fixes1, map (apsnd (map abs_fixes1)) assumes1), |
|
118 |
((fixes2, map (apsnd (map abs_fixes)) assumes2), binds)) |
|
119 |
end; |
|
120 |
||
121 |
val cases = map extract props; |
|
122 |
||
123 |
fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) = |
|
124 |
Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []}; |
|
125 |
fun inner_case (_, ((fixes2, assumes2), binds)) = |
|
126 |
Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []}; |
|
127 |
fun nested_case ((fixes1, assumes1), _) = |
|
128 |
Case {fixes = fixes1, assumes = assumes1, binds = [], |
|
129 |
cases = map string_of_int (1 upto len) ~~ map inner_case cases}; |
|
130 |
in |
|
131 |
if len = 0 then NONE |
|
132 |
else if len = 1 then SOME (common_case (hd cases)) |
|
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19012
diff
changeset
|
133 |
else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE |
18608 | 134 |
else SOME (nested_case (hd cases)) |
135 |
end; |
|
136 |
||
137 |
fun make is_open rule_struct (thy, prop) cases = |
|
138 |
let |
|
139 |
val n = length cases; |
|
140 |
val nprems = Logic.count_prems (prop, 0); |
|
141 |
fun add_case (name, concls) (cs, i) = |
|
142 |
((case try (fn () => |
|
143 |
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of |
|
144 |
NONE => (name, NONE) |
|
145 |
| SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1); |
|
146 |
in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end; |
|
147 |
||
148 |
in |
|
149 |
||
150 |
fun make_common is_open = make is_open NONE; |
|
151 |
fun make_nested is_open rule_struct = make is_open (SOME rule_struct); |
|
152 |
fun make_simple is_open (thy, prop) name = [(name, extract_case is_open thy (NONE, prop) "" [])]; |
|
153 |
||
154 |
fun apply args = |
|
155 |
let |
|
156 |
fun appl (Case {fixes, assumes, binds, cases}) = |
|
157 |
let |
|
158 |
val assumes' = map (apsnd (map (app args))) assumes; |
|
159 |
val binds' = map (apsnd (Option.map (app args))) binds; |
|
160 |
val cases' = map (apsnd appl) cases; |
|
161 |
in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end; |
|
162 |
in appl end; |
|
163 |
||
164 |
end; |
|
165 |
||
166 |
||
167 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
168 |
(** tactics with cases **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
169 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
170 |
type cases_tactic = thm -> (cases * thm) Seq.seq; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
171 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
172 |
fun CASES cases tac st = Seq.map (pair cases) (tac st); |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
173 |
fun NO_CASES tac = CASES [] tac; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
174 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
175 |
fun SUBGOAL_CASES tac i st = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
176 |
(case try Logic.nth_prem (i, Thm.prop_of st) of |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
177 |
SOME goal => tac (goal, i) st |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
178 |
| NONE => Seq.empty); |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
179 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
180 |
fun (tac1 THEN_ALL_NEW_CASES tac2) i st = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
181 |
st |> tac1 i |> Seq.maps (fn (cases, st') => |
18237 | 182 |
CASES cases (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st)) st'); |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
183 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
184 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
185 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
186 |
(** consume facts **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
187 |
|
18477 | 188 |
local |
189 |
||
190 |
fun unfold_prems n defs th = |
|
191 |
if null defs then th |
|
192 |
else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs)) th; |
|
193 |
||
194 |
fun unfold_prems_concls defs th = |
|
195 |
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th |
|
196 |
else |
|
197 |
Drule.fconv_rule |
|
19423 | 198 |
(Drule.concl_conv ~1 (Conjunction.conv ~1 |
18477 | 199 |
(K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th; |
200 |
||
201 |
in |
|
202 |
||
203 |
fun consume defs facts ((xx, n), th) = |
|
18237 | 204 |
let val m = Int.min (length facts, n) in |
18477 | 205 |
th |
206 |
|> unfold_prems n defs |
|
207 |
|> unfold_prems_concls defs |
|
18237 | 208 |
|> Drule.multi_resolve (Library.take (m, facts)) |
18477 | 209 |
|> Seq.map (pair (xx, (n - m, Library.drop (m, facts)))) |
18237 | 210 |
end; |
10811 | 211 |
|
18477 | 212 |
end; |
213 |
||
10811 | 214 |
val consumes_tagN = "consumes"; |
215 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
216 |
fun lookup_consumes th = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
217 |
let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
218 |
(case AList.lookup (op =) (Thm.tags_of_thm th) (consumes_tagN) of |
15531 | 219 |
NONE => NONE |
220 |
| SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ()) |
|
10530 | 221 |
| _ => err ()) |
222 |
end; |
|
223 |
||
18477 | 224 |
fun get_consumes th = the_default 0 (lookup_consumes th); |
225 |
||
15531 | 226 |
fun put_consumes NONE th = th |
227 |
| put_consumes (SOME n) th = th |
|
18799 | 228 |
|> PureThy.untag_rule consumes_tagN |
18909
f1333b0ff9e5
consumes: negative argument relative to total number of prems;
wenzelm
parents:
18799
diff
changeset
|
229 |
|> PureThy.tag_rule |
f1333b0ff9e5
consumes: negative argument relative to total number of prems;
wenzelm
parents:
18799
diff
changeset
|
230 |
(consumes_tagN, [Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n)]); |
10530 | 231 |
|
18477 | 232 |
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th; |
233 |
||
12761 | 234 |
val save_consumes = put_consumes o lookup_consumes; |
235 |
||
18728 | 236 |
fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x; |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
237 |
fun consumes_default n x = |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
238 |
if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x; |
8364 | 239 |
|
240 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
241 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
242 |
(** case names **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
243 |
|
18237 | 244 |
val case_names_tagN = "case_names"; |
8364 | 245 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
246 |
fun add_case_names NONE = I |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
247 |
| add_case_names (SOME names) = |
18799 | 248 |
PureThy.untag_rule case_names_tagN |
249 |
#> PureThy.tag_rule (case_names_tagN, names); |
|
8364 | 250 |
|
18237 | 251 |
fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN; |
10530 | 252 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
253 |
val save_case_names = add_case_names o lookup_case_names; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
254 |
val name = add_case_names o SOME; |
18728 | 255 |
fun case_names ss = Thm.rule_attribute (K (name ss)); |
8364 | 256 |
|
10530 | 257 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
258 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
259 |
(** case conclusions **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
260 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
261 |
val case_concl_tagN = "case_conclusion"; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
262 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
263 |
fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
264 |
| is_case_concl _ _ = false; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
265 |
|
18799 | 266 |
fun add_case_concl (name, cs) = PureThy.map_tags (fn tags => |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
267 |
filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]); |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
268 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
269 |
fun get_case_concls th name = |
18237 | 270 |
(case find_first (is_case_concl name) (Thm.tags_of_thm th) of |
271 |
SOME (_, _ :: cs) => cs |
|
272 |
| _ => []); |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
273 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
274 |
fun save_case_concls th = |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
275 |
let val concls = Thm.tags_of_thm th |> map_filter |
18237 | 276 |
(fn (a, b :: cs) => |
277 |
if a = case_concl_tagN then SOME (b, cs) else NONE |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
278 |
| _ => NONE) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
279 |
in fold add_case_concl concls end; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
280 |
|
18728 | 281 |
fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl); |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
282 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
283 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
284 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
285 |
(** case declarations **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
286 |
|
10530 | 287 |
(* access hints *) |
288 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
289 |
fun save th = save_consumes th #> save_case_names th #> save_case_concls th; |
12761 | 290 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
291 |
fun get th = |
12761 | 292 |
let |
18477 | 293 |
val n = get_consumes th; |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
294 |
val cases = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
295 |
(case lookup_case_names th of |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
296 |
NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n)) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
297 |
| SOME names => map (fn name => (name, get_case_concls th name)) names); |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
298 |
in (cases, n) end; |
10530 | 299 |
|
8364 | 300 |
|
8427 | 301 |
(* params *) |
8364 | 302 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
303 |
fun rename_params xss th = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
304 |
th |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
305 |
|> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
306 |
|> save th; |
8364 | 307 |
|
18728 | 308 |
fun params xss = Thm.rule_attribute (K (rename_params xss)); |
8364 | 309 |
|
18477 | 310 |
|
311 |
||
312 |
(** mutual_rule **) |
|
313 |
||
314 |
local |
|
315 |
||
316 |
fun equal_cterms ts us = |
|
317 |
list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us) = EQUAL; |
|
318 |
||
319 |
fun prep_rule th = |
|
320 |
let |
|
321 |
val n = get_consumes th; |
|
322 |
val th' = Drule.freeze_all (Thm.permute_prems 0 n th); |
|
323 |
val prems = Library.take (Thm.nprems_of th' - n, Drule.cprems_of th'); |
|
324 |
val th'' = Drule.implies_elim_list th' (map Thm.assume prems); |
|
325 |
in (prems, (n, th'')) end; |
|
326 |
||
327 |
in |
|
328 |
||
329 |
fun mutual_rule [] = NONE |
|
330 |
| mutual_rule [th] = SOME ([0], th) |
|
331 |
| mutual_rule raw_rules = |
|
332 |
let |
|
333 |
val rules as (prems, _) :: _ = map prep_rule raw_rules; |
|
334 |
val (ns, ths) = split_list (map #2 rules); |
|
335 |
in |
|
336 |
if not (forall (equal_cterms prems o #1) rules) then NONE |
|
337 |
else |
|
338 |
SOME (ns, |
|
339 |
ths |
|
19423 | 340 |
|> foldr1 (uncurry Conjunction.intr) |
18477 | 341 |
|> Drule.implies_intr_list prems |
342 |
|> Drule.standard' |
|
343 |
|> save (hd raw_rules) |
|
344 |
|> put_consumes (SOME 0)) |
|
345 |
end; |
|
346 |
||
347 |
end; |
|
348 |
||
18581 | 349 |
fun strict_mutual_rule ths = |
350 |
(case mutual_rule ths of |
|
351 |
NONE => error "Failed to join given rules into one mutual rule" |
|
352 |
| SOME res => res); |
|
353 |
||
8364 | 354 |
end; |
17113 | 355 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
356 |
structure BasicRuleCases: BASIC_RULE_CASES = RuleCases; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
357 |
open BasicRuleCases; |