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