author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 46219 | 426ed18eba43 |
child 53380 | 08f3491c50bf |
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 |
42496 | 23 |
{fixes: (binding * typ) list, |
18608 | 24 |
assumes: (string * term list) list, |
25 |
binds: (indexname * term option) list, |
|
26 |
cases: (string * T) list} |
|
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
27 |
val case_hypsN: string |
18608 | 28 |
val strip_params: term -> (string * typ) list |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
29 |
val make_common: theory * term -> |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
30 |
((string * string list) * string list) list -> cases |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
31 |
val make_nested: term -> theory * term -> |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
32 |
((string * string list) * string list) list -> cases |
18608 | 33 |
val apply: term list -> T -> T |
18237 | 34 |
val consume: thm list -> thm list -> ('a * int) * thm -> |
35 |
(('a * (int * thm list)) * thm) Seq.seq |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
36 |
val get_consumes: thm -> int |
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
37 |
val put_consumes: int option -> thm -> thm |
18477 | 38 |
val add_consumes: int -> thm -> thm |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
39 |
val default_consumes: int -> thm -> thm |
18728 | 40 |
val consumes: int -> attribute |
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
41 |
val get_constraints: thm -> int |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
42 |
val constraints: int -> attribute |
8364 | 43 |
val name: string list -> thm -> thm |
18728 | 44 |
val case_names: string list -> attribute |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
45 |
val cases_hyp_names: string list -> string list list -> attribute |
18728 | 46 |
val case_conclusion: string * string list -> attribute |
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
47 |
val is_inner_rule: thm -> bool |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
48 |
val inner_rule: attribute |
12761 | 49 |
val save: thm -> thm -> thm |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
50 |
val get: thm -> ((string * string list) * string list) list * int |
8427 | 51 |
val rename_params: string list list -> thm -> thm |
18728 | 52 |
val params: string list list -> attribute |
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
53 |
val internalize_params: thm -> thm |
20289 | 54 |
val mutual_rule: Proof.context -> thm list -> (int list * thm) option |
55 |
val strict_mutual_rule: Proof.context -> thm list -> int list * thm |
|
8364 | 56 |
end; |
57 |
||
33368 | 58 |
structure Rule_Cases: RULE_CASES = |
8364 | 59 |
struct |
60 |
||
18608 | 61 |
(** cases **) |
62 |
||
63 |
datatype T = Case of |
|
42496 | 64 |
{fixes: (binding * typ) list, |
18608 | 65 |
assumes: (string * term list) list, |
66 |
binds: (indexname * term option) list, |
|
67 |
cases: (string * T) list}; |
|
68 |
||
69 |
type cases = (string * T option) list; |
|
70 |
||
71 |
val case_conclN = "case"; |
|
72 |
val case_hypsN = "hyps"; |
|
73 |
val case_premsN = "prems"; |
|
74 |
||
20087 | 75 |
val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params; |
18608 | 76 |
|
77 |
local |
|
78 |
||
79 |
fun app us t = Term.betapplys (t, us); |
|
80 |
||
81 |
fun dest_binops cs tm = |
|
82 |
let |
|
83 |
val n = length cs; |
|
84 |
fun dest 0 _ = [] |
|
85 |
| dest 1 t = [t] |
|
86 |
| dest k (_ $ t $ u) = t :: dest (k - 1) u |
|
87 |
| dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]); |
|
88 |
in cs ~~ dest n tm end; |
|
89 |
||
90 |
fun extract_fixes NONE prop = (strip_params prop, []) |
|
91 |
| extract_fixes (SOME outline) prop = |
|
19012 | 92 |
chop (length (Logic.strip_params outline)) (strip_params prop); |
18608 | 93 |
|
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
94 |
fun extract_assumes _ _ NONE prop = ([("", Logic.strip_assums_hyp prop)], []) |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
95 |
| extract_assumes qual hnames (SOME outline) prop = |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
96 |
let |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
97 |
val (hyps, prems) = |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
98 |
chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop) |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
99 |
fun extract ((hname,h)::ps) = (qual hname, h :: map snd ps); |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
100 |
val (hyps1,hyps2) = chop (length hnames) hyps; |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
101 |
val pairs1 = if hyps1 = [] then [] else hnames ~~ hyps1; |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
102 |
val pairs = pairs1 @ (map (pair case_hypsN) hyps2); |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
103 |
val named_hyps = map extract (partition_eq (eq_fst op =) pairs) |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
104 |
in (named_hyps, [(qual case_premsN, prems)]) end; |
18608 | 105 |
|
42496 | 106 |
fun bindings args = map (apfst Binding.name) args; |
107 |
||
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
108 |
fun extract_case thy (case_outline, raw_prop) name hnames concls = |
18608 | 109 |
let |
110 |
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop); |
|
111 |
val len = length props; |
|
112 |
val nested = is_some case_outline andalso len > 1; |
|
113 |
||
114 |
fun extract prop = |
|
115 |
let |
|
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
116 |
val (fixes1, fixes2) = extract_fixes case_outline prop; |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45525
diff
changeset
|
117 |
val abs_fixes = fold_rev Term.abs (fixes1 @ fixes2); |
18608 | 118 |
fun abs_fixes1 t = |
119 |
if not nested then abs_fixes t |
|
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45525
diff
changeset
|
120 |
else |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45525
diff
changeset
|
121 |
fold_rev Term.abs fixes1 |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45525
diff
changeset
|
122 |
(app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t)); |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
123 |
val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
124 |
|> pairself (map (apsnd (maps Logic.dest_conjunctions))); |
18608 | 125 |
|
35625 | 126 |
val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop); |
18608 | 127 |
val binds = |
128 |
(case_conclN, concl) :: dest_binops concls concl |
|
129 |
|> map (fn (x, t) => ((x, 0), SOME (abs_fixes t))); |
|
130 |
in |
|
131 |
((fixes1, map (apsnd (map abs_fixes1)) assumes1), |
|
132 |
((fixes2, map (apsnd (map abs_fixes)) assumes2), binds)) |
|
133 |
end; |
|
134 |
||
135 |
val cases = map extract props; |
|
136 |
||
137 |
fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) = |
|
42496 | 138 |
Case {fixes = bindings (fixes1 @ fixes2), |
139 |
assumes = assumes1 @ assumes2, binds = binds, cases = []}; |
|
18608 | 140 |
fun inner_case (_, ((fixes2, assumes2), binds)) = |
42496 | 141 |
Case {fixes = bindings fixes2, assumes = assumes2, binds = binds, cases = []}; |
18608 | 142 |
fun nested_case ((fixes1, assumes1), _) = |
42496 | 143 |
Case {fixes = bindings fixes1, assumes = assumes1, binds = [], |
18608 | 144 |
cases = map string_of_int (1 upto len) ~~ map inner_case cases}; |
145 |
in |
|
146 |
if len = 0 then NONE |
|
147 |
else if len = 1 then SOME (common_case (hd cases)) |
|
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19012
diff
changeset
|
148 |
else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE |
18608 | 149 |
else SOME (nested_case (hd cases)) |
150 |
end; |
|
151 |
||
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
152 |
fun make rule_struct (thy, prop) cases = |
18608 | 153 |
let |
154 |
val n = length cases; |
|
21576 | 155 |
val nprems = Logic.count_prems prop; |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
156 |
fun add_case ((name, hnames), concls) (cs, i) = |
18608 | 157 |
((case try (fn () => |
158 |
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of |
|
159 |
NONE => (name, NONE) |
|
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
160 |
| SOME p => (name, extract_case thy p name hnames concls)) :: cs, i - 1); |
34058 | 161 |
in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end; |
18608 | 162 |
|
163 |
in |
|
164 |
||
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
165 |
val make_common = make NONE; |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
166 |
fun make_nested rule_struct = make (SOME rule_struct); |
18608 | 167 |
|
168 |
fun apply args = |
|
169 |
let |
|
170 |
fun appl (Case {fixes, assumes, binds, cases}) = |
|
171 |
let |
|
172 |
val assumes' = map (apsnd (map (app args))) assumes; |
|
173 |
val binds' = map (apsnd (Option.map (app args))) binds; |
|
174 |
val cases' = map (apsnd appl) cases; |
|
175 |
in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end; |
|
176 |
in appl end; |
|
177 |
||
178 |
end; |
|
179 |
||
180 |
||
181 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
182 |
(** tactics with cases **) |
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 |
type cases_tactic = thm -> (cases * thm) Seq.seq; |
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 |
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
|
187 |
fun NO_CASES tac = CASES [] tac; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
188 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
189 |
fun SUBGOAL_CASES tac i st = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
190 |
(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
|
191 |
SOME goal => tac (goal, i) st |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
192 |
| NONE => Seq.empty); |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
193 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
194 |
fun (tac1 THEN_ALL_NEW_CASES tac2) i st = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
195 |
st |> tac1 i |> Seq.maps (fn (cases, st') => |
18237 | 196 |
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
|
197 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
198 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
199 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
200 |
(** consume facts **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
201 |
|
18477 | 202 |
local |
203 |
||
204 |
fun unfold_prems n defs th = |
|
205 |
if null defs then th |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
36354
diff
changeset
|
206 |
else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th; |
18477 | 207 |
|
208 |
fun unfold_prems_concls defs th = |
|
209 |
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th |
|
210 |
else |
|
22900 | 211 |
Conv.fconv_rule |
23418 | 212 |
(Conv.concl_conv ~1 (Conjunction.convs |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
36354
diff
changeset
|
213 |
(Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th; |
18477 | 214 |
|
215 |
in |
|
216 |
||
217 |
fun consume defs facts ((xx, n), th) = |
|
18237 | 218 |
let val m = Int.min (length facts, n) in |
18477 | 219 |
th |
220 |
|> unfold_prems n defs |
|
221 |
|> unfold_prems_concls defs |
|
33957 | 222 |
|> Drule.multi_resolve (take m facts) |
223 |
|> Seq.map (pair (xx, (n - m, drop m facts))) |
|
18237 | 224 |
end; |
10811 | 225 |
|
18477 | 226 |
end; |
227 |
||
10811 | 228 |
val consumes_tagN = "consumes"; |
229 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
230 |
fun lookup_consumes th = |
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
231 |
(case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of |
23657 | 232 |
NONE => NONE |
233 |
| SOME s => |
|
24244 | 234 |
(case Lexicon.read_nat s of SOME n => SOME n |
23657 | 235 |
| _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th]))); |
10530 | 236 |
|
18477 | 237 |
fun get_consumes th = the_default 0 (lookup_consumes th); |
238 |
||
15531 | 239 |
fun put_consumes NONE th = th |
240 |
| 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
|
241 |
|> Thm.untag_rule consumes_tagN |
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
242 |
|> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n)); |
10530 | 243 |
|
18477 | 244 |
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th; |
245 |
||
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
246 |
fun default_consumes n th = |
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
247 |
if is_some (lookup_consumes th) then th else put_consumes (SOME n) th; |
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
248 |
|
12761 | 249 |
val save_consumes = put_consumes o lookup_consumes; |
250 |
||
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
251 |
fun consumes n = Thm.mixed_attribute (apsnd (put_consumes (SOME n))); |
21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
20289
diff
changeset
|
252 |
|
8364 | 253 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
254 |
|
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
255 |
(** equality constraints **) |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
256 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
257 |
val constraints_tagN = "constraints"; |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
258 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
259 |
fun lookup_constraints th = |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
260 |
(case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
261 |
NONE => NONE |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
262 |
| SOME s => |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
263 |
(case Lexicon.read_nat s of SOME n => SOME n |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
264 |
| _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th]))); |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
265 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
266 |
fun get_constraints th = the_default 0 (lookup_constraints th); |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
267 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
268 |
fun put_constraints NONE th = th |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
269 |
| put_constraints (SOME n) th = th |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
270 |
|> Thm.untag_rule constraints_tagN |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
271 |
|> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n)); |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
272 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
273 |
val save_constraints = put_constraints o lookup_constraints; |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
274 |
|
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
275 |
fun constraints n = Thm.mixed_attribute (apsnd (put_constraints (SOME n))); |
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
276 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
277 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
278 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
279 |
(** case names **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
280 |
|
23657 | 281 |
val implode_args = space_implode ";"; |
282 |
val explode_args = space_explode ";"; |
|
283 |
||
18237 | 284 |
val case_names_tagN = "case_names"; |
8364 | 285 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
286 |
fun add_case_names NONE = I |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
287 |
| 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
|
288 |
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
|
289 |
#> Thm.tag_rule (case_names_tagN, implode_args names); |
8364 | 290 |
|
23657 | 291 |
fun lookup_case_names th = |
292 |
AList.lookup (op =) (Thm.get_tags th) case_names_tagN |
|
293 |
|> Option.map explode_args; |
|
10530 | 294 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
295 |
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
|
296 |
val name = add_case_names o SOME; |
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
297 |
fun case_names cs = Thm.mixed_attribute (apsnd (name cs)); |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
298 |
|
8364 | 299 |
|
10530 | 300 |
|
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
301 |
(** hyp names **) |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
302 |
|
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
303 |
val implode_hyps = implode_args o map (suffix "," o space_implode ","); |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
304 |
val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args; |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
305 |
|
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
306 |
val cases_hyp_names_tagN = "cases_hyp_names"; |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
307 |
|
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
308 |
fun add_cases_hyp_names NONE = I |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
309 |
| add_cases_hyp_names (SOME namess) = |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
310 |
Thm.untag_rule cases_hyp_names_tagN |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
311 |
#> Thm.tag_rule (cases_hyp_names_tagN, implode_hyps namess); |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
312 |
|
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
313 |
fun lookup_cases_hyp_names th = |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
314 |
AList.lookup (op =) (Thm.get_tags th) cases_hyp_names_tagN |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
315 |
|> Option.map explode_hyps; |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
316 |
|
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
317 |
val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names; |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
318 |
fun cases_hyp_names cs hs = |
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
319 |
Thm.mixed_attribute (apsnd (name cs #> add_cases_hyp_names (SOME hs))); |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
320 |
|
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
321 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
322 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
323 |
(** case conclusions **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
324 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
325 |
val case_concl_tagN = "case_conclusion"; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
326 |
|
23657 | 327 |
fun get_case_concl name (a, b) = |
328 |
if a = case_concl_tagN then |
|
329 |
(case explode_args b of c :: cs => if c = name then SOME cs else NONE) |
|
330 |
else NONE; |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
331 |
|
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset
|
332 |
fun add_case_concl (name, cs) = Thm.map_tags (fn tags => |
23657 | 333 |
filter_out (is_some o get_case_concl name) tags @ |
334 |
[(case_concl_tagN, implode_args (name :: cs))]); |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
335 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
336 |
fun get_case_concls th name = |
23657 | 337 |
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
|
338 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
339 |
fun save_case_concls th = |
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset
|
340 |
let val concls = Thm.get_tags th |> map_filter |
23657 | 341 |
(fn (a, b) => |
342 |
if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE) |
|
343 |
else NONE) |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
344 |
in fold add_case_concl concls end; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
345 |
|
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
346 |
fun case_conclusion concl = Thm.mixed_attribute (apsnd (add_case_concl concl)); |
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
347 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
348 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
349 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
350 |
(** inner rule **) |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
351 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
352 |
val inner_rule_tagN = "inner_rule"; |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
353 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
354 |
fun is_inner_rule th = |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
355 |
AList.defined (op =) (Thm.get_tags th) inner_rule_tagN; |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
356 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
357 |
fun put_inner_rule inner = |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
358 |
Thm.untag_rule inner_rule_tagN |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
359 |
#> inner ? Thm.tag_rule (inner_rule_tagN, ""); |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
360 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
361 |
val save_inner_rule = put_inner_rule o is_inner_rule; |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
362 |
|
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
363 |
val inner_rule = Thm.mixed_attribute (apsnd (put_inner_rule true)); |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
364 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
365 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
366 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
367 |
(** case declarations **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
368 |
|
10530 | 369 |
(* access hints *) |
370 |
||
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
371 |
fun save th = |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
372 |
save_consumes th #> |
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
373 |
save_constraints th #> |
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
374 |
save_case_names th #> |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
375 |
save_cases_hyp_names th #> |
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
376 |
save_case_concls th #> |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
377 |
save_inner_rule th; |
12761 | 378 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
379 |
fun get th = |
12761 | 380 |
let |
18477 | 381 |
val n = get_consumes th; |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
382 |
val cases = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
383 |
(case lookup_case_names th of |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
384 |
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
|
385 |
| SOME names => map (fn name => (name, get_case_concls th name)) names); |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
386 |
val cases_hyps = (case lookup_cases_hyp_names th of |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
387 |
NONE => replicate (length cases) [] |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
388 |
| SOME names => names); |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
389 |
fun regroup ((name,concls),hyps) = ((name,hyps),concls) |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
390 |
in (map regroup (cases ~~ cases_hyps), n) end; |
10530 | 391 |
|
8364 | 392 |
|
8427 | 393 |
(* params *) |
8364 | 394 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
395 |
fun rename_params xss th = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
396 |
th |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
397 |
|> 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
|
398 |
|> save th; |
8364 | 399 |
|
18728 | 400 |
fun params xss = Thm.rule_attribute (K (rename_params xss)); |
8364 | 401 |
|
18477 | 402 |
|
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
403 |
(* internalize parameter names *) |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
404 |
|
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
405 |
fun internalize_params rule = |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
406 |
let |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
407 |
fun rename prem = |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
408 |
let val xs = |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
409 |
map (Name.internal o Name.clean o fst) (Logic.strip_params prem) |
45328 | 410 |
in Logic.list_rename_params xs prem end; |
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
411 |
fun rename_prems prop = |
36354 | 412 |
let val (As, C) = Logic.strip_horn prop |
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
413 |
in Logic.list_implies (map rename As, C) end; |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
414 |
in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
415 |
|
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
416 |
|
18477 | 417 |
|
418 |
(** mutual_rule **) |
|
419 |
||
420 |
local |
|
421 |
||
422 |
fun equal_cterms ts us = |
|
35408 | 423 |
is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us)); |
18477 | 424 |
|
19917 | 425 |
fun prep_rule n th = |
18477 | 426 |
let |
19917 | 427 |
val th' = Thm.permute_prems 0 n th; |
33957 | 428 |
val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th'); |
18477 | 429 |
val th'' = Drule.implies_elim_list th' (map Thm.assume prems); |
430 |
in (prems, (n, th'')) end; |
|
431 |
||
432 |
in |
|
433 |
||
19917 | 434 |
fun mutual_rule _ [] = NONE |
435 |
| mutual_rule _ [th] = SOME ([0], th) |
|
436 |
| mutual_rule ctxt (ths as th :: _) = |
|
18477 | 437 |
let |
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30364
diff
changeset
|
438 |
val ((_, ths'), ctxt') = Variable.import true ths ctxt; |
19917 | 439 |
val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths'; |
440 |
val (ns, rls) = split_list (map #2 rules); |
|
18477 | 441 |
in |
442 |
if not (forall (equal_cterms prems o #1) rules) then NONE |
|
443 |
else |
|
444 |
SOME (ns, |
|
19917 | 445 |
rls |
23418 | 446 |
|> Conjunction.intr_balanced |
18477 | 447 |
|> Drule.implies_intr_list prems |
19917 | 448 |
|> singleton (Variable.export ctxt' ctxt) |
449 |
|> save th |
|
18477 | 450 |
|> put_consumes (SOME 0)) |
451 |
end; |
|
452 |
||
453 |
end; |
|
454 |
||
19917 | 455 |
fun strict_mutual_rule ctxt ths = |
456 |
(case mutual_rule ctxt ths of |
|
18581 | 457 |
NONE => error "Failed to join given rules into one mutual rule" |
458 |
| SOME res => res); |
|
459 |
||
8364 | 460 |
end; |
17113 | 461 |
|
33368 | 462 |
structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases; |
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
463 |
open Basic_Rule_Cases; |