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