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