author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57743 | 0af2d5dfb0ac |
parent 56231 | b98813774a63 |
child 58014 | 47ecbef7274b |
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 |
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55639
diff
changeset
|
15 |
val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic |
18229
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, |
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
24 |
assumes: (binding * term list) list, |
18608 | 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 |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53380
diff
changeset
|
34 |
val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm -> |
18237 | 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, |
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
65 |
assumes: (binding * term list) list, |
18608 | 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 |
|
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
94 |
fun extract_assumes _ _ NONE prop = ([(Binding.empty, Logic.strip_assums_hyp prop)], []) |
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
95 |
| extract_assumes qualifier 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
|
96 |
let |
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
97 |
val qual = Binding.qualify true qualifier o Binding.name; |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
98 |
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
|
99 |
chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop) |
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
100 |
fun extract ((hyp_name, hyp) :: rest) = (qual hyp_name, hyp :: map snd rest); |
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
101 |
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
|
102 |
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
|
103 |
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
|
104 |
val named_hyps = map extract (partition_eq (eq_fst op =) pairs); |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
105 |
in (named_hyps, [(qual case_premsN, prems)]) end; |
18608 | 106 |
|
42496 | 107 |
fun bindings args = map (apfst Binding.name) args; |
108 |
||
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
109 |
fun extract_case thy (case_outline, raw_prop) name hyp_names concls = |
18608 | 110 |
let |
111 |
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop); |
|
112 |
val len = length props; |
|
113 |
val nested = is_some case_outline andalso len > 1; |
|
114 |
||
115 |
fun extract prop = |
|
116 |
let |
|
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
117 |
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
|
118 |
val abs_fixes = fold_rev Term.abs (fixes1 @ fixes2); |
18608 | 119 |
fun abs_fixes1 t = |
120 |
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
|
121 |
else |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45525
diff
changeset
|
122 |
fold_rev Term.abs fixes1 |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45525
diff
changeset
|
123 |
(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
|
124 |
val (assumes1, assumes2) = |
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
125 |
extract_assumes name hyp_names case_outline prop |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
126 |
|> pairself (map (apsnd (maps Logic.dest_conjunctions))); |
18608 | 127 |
|
35625 | 128 |
val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop); |
18608 | 129 |
val binds = |
130 |
(case_conclN, concl) :: dest_binops concls concl |
|
131 |
|> map (fn (x, t) => ((x, 0), SOME (abs_fixes t))); |
|
132 |
in |
|
133 |
((fixes1, map (apsnd (map abs_fixes1)) assumes1), |
|
134 |
((fixes2, map (apsnd (map abs_fixes)) assumes2), binds)) |
|
135 |
end; |
|
136 |
||
137 |
val cases = map extract props; |
|
138 |
||
139 |
fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) = |
|
42496 | 140 |
Case {fixes = bindings (fixes1 @ fixes2), |
141 |
assumes = assumes1 @ assumes2, binds = binds, cases = []}; |
|
18608 | 142 |
fun inner_case (_, ((fixes2, assumes2), binds)) = |
42496 | 143 |
Case {fixes = bindings fixes2, assumes = assumes2, binds = binds, cases = []}; |
18608 | 144 |
fun nested_case ((fixes1, assumes1), _) = |
42496 | 145 |
Case {fixes = bindings fixes1, assumes = assumes1, binds = [], |
18608 | 146 |
cases = map string_of_int (1 upto len) ~~ map inner_case cases}; |
147 |
in |
|
148 |
if len = 0 then NONE |
|
149 |
else if len = 1 then SOME (common_case (hd cases)) |
|
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19012
diff
changeset
|
150 |
else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE |
18608 | 151 |
else SOME (nested_case (hd cases)) |
152 |
end; |
|
153 |
||
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
154 |
fun make rule_struct (thy, prop) cases = |
18608 | 155 |
let |
156 |
val n = length cases; |
|
21576 | 157 |
val nprems = Logic.count_prems prop; |
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
158 |
fun add_case ((name, hyp_names), concls) (cs, i) = |
18608 | 159 |
((case try (fn () => |
160 |
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of |
|
161 |
NONE => (name, NONE) |
|
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
46219
diff
changeset
|
162 |
| SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1); |
34058 | 163 |
in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end; |
18608 | 164 |
|
165 |
in |
|
166 |
||
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
167 |
val make_common = make NONE; |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
168 |
fun make_nested rule_struct = make (SOME rule_struct); |
18608 | 169 |
|
170 |
fun apply args = |
|
171 |
let |
|
172 |
fun appl (Case {fixes, assumes, binds, cases}) = |
|
173 |
let |
|
174 |
val assumes' = map (apsnd (map (app args))) assumes; |
|
175 |
val binds' = map (apsnd (Option.map (app args))) binds; |
|
176 |
val cases' = map (apsnd appl) cases; |
|
177 |
in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end; |
|
178 |
in appl end; |
|
179 |
||
180 |
end; |
|
181 |
||
182 |
||
183 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
184 |
(** tactics with cases **) |
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 |
type cases_tactic = thm -> (cases * thm) Seq.seq; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
187 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
188 |
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
|
189 |
fun NO_CASES tac = CASES [] tac; |
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 SUBGOAL_CASES tac i st = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
192 |
(case try Logic.nth_prem (i, Thm.prop_of st) of |
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55639
diff
changeset
|
193 |
SOME goal => tac (goal, i, st) st |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
194 |
| NONE => Seq.empty); |
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 |
fun (tac1 THEN_ALL_NEW_CASES tac2) i st = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
197 |
st |> tac1 i |> Seq.maps (fn (cases, st') => |
18237 | 198 |
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
|
199 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
200 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
201 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
202 |
(** consume facts **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
203 |
|
18477 | 204 |
local |
205 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53380
diff
changeset
|
206 |
fun unfold_prems ctxt n defs th = |
18477 | 207 |
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
|
208 |
else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt true defs)) th; |
18477 | 209 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53380
diff
changeset
|
210 |
fun unfold_prems_concls ctxt defs th = |
18477 | 211 |
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th |
212 |
else |
|
22900 | 213 |
Conv.fconv_rule |
23418 | 214 |
(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
|
215 |
(Conv.prems_conv ~1 (Raw_Simplifier.rewrite ctxt true defs)))) th; |
18477 | 216 |
|
217 |
in |
|
218 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53380
diff
changeset
|
219 |
fun consume ctxt defs facts ((xx, n), th) = |
18237 | 220 |
let val m = Int.min (length facts, n) in |
18477 | 221 |
th |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53380
diff
changeset
|
222 |
|> 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
|
223 |
|> unfold_prems_concls ctxt defs |
33957 | 224 |
|> Drule.multi_resolve (take m facts) |
225 |
|> Seq.map (pair (xx, (n - m, drop m facts))) |
|
18237 | 226 |
end; |
10811 | 227 |
|
18477 | 228 |
end; |
229 |
||
10811 | 230 |
val consumes_tagN = "consumes"; |
231 |
||
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
232 |
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
|
233 |
(case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of |
23657 | 234 |
NONE => NONE |
235 |
| SOME s => |
|
55639 | 236 |
(case Lexicon.read_nat s of |
237 |
SOME n => SOME n |
|
23657 | 238 |
| _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th]))); |
10530 | 239 |
|
18477 | 240 |
fun get_consumes th = the_default 0 (lookup_consumes th); |
241 |
||
15531 | 242 |
fun put_consumes NONE th = th |
243 |
| 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
|
244 |
|> 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
|
245 |
|> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n)); |
10530 | 246 |
|
18477 | 247 |
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th; |
248 |
||
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
249 |
fun default_consumes n th = |
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset
|
250 |
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
|
251 |
|
12761 | 252 |
val save_consumes = put_consumes o lookup_consumes; |
253 |
||
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
254 |
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
|
255 |
|
8364 | 256 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
257 |
|
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
258 |
(** equality constraints **) |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
259 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
260 |
val constraints_tagN = "constraints"; |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
261 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
262 |
fun lookup_constraints th = |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
263 |
(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
|
264 |
NONE => NONE |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
265 |
| SOME s => |
55639 | 266 |
(case Lexicon.read_nat s of |
267 |
SOME n => SOME n |
|
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
268 |
| _ => 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
|
269 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
270 |
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
|
271 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
272 |
fun put_constraints NONE th = th |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
273 |
| put_constraints (SOME n) th = th |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
274 |
|> Thm.untag_rule constraints_tagN |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
275 |
|> 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
|
276 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
277 |
val save_constraints = put_constraints o lookup_constraints; |
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
278 |
|
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
279 |
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
|
280 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
281 |
|
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
282 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
283 |
(** case names **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
284 |
|
23657 | 285 |
val implode_args = space_implode ";"; |
286 |
val explode_args = space_explode ";"; |
|
287 |
||
18237 | 288 |
val case_names_tagN = "case_names"; |
8364 | 289 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
290 |
fun add_case_names NONE = I |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
291 |
| 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
|
292 |
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
|
293 |
#> Thm.tag_rule (case_names_tagN, implode_args names); |
8364 | 294 |
|
23657 | 295 |
fun lookup_case_names th = |
296 |
AList.lookup (op =) (Thm.get_tags th) case_names_tagN |
|
297 |
|> Option.map explode_args; |
|
10530 | 298 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
299 |
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
|
300 |
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
|
301 |
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
|
302 |
|
8364 | 303 |
|
10530 | 304 |
|
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
305 |
(** 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
|
306 |
|
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
307 |
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
|
308 |
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
|
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 |
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
|
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 |
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
|
313 |
| 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
|
314 |
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
|
315 |
#> 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
|
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 |
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
|
318 |
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
|
319 |
|> 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
|
320 |
|
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
321 |
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
|
322 |
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
|
323 |
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
|
324 |
|
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42496
diff
changeset
|
325 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
326 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
327 |
(** case conclusions **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
328 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
329 |
val case_concl_tagN = "case_conclusion"; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
330 |
|
23657 | 331 |
fun get_case_concl name (a, b) = |
332 |
if a = case_concl_tagN then |
|
333 |
(case explode_args b of c :: cs => if c = name then SOME cs else NONE) |
|
334 |
else NONE; |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
335 |
|
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset
|
336 |
fun add_case_concl (name, cs) = Thm.map_tags (fn tags => |
23657 | 337 |
filter_out (is_some o get_case_concl name) tags @ |
338 |
[(case_concl_tagN, implode_args (name :: cs))]); |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
339 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
340 |
fun get_case_concls th name = |
23657 | 341 |
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
|
342 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
343 |
fun save_case_concls th = |
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset
|
344 |
let val concls = Thm.get_tags th |> map_filter |
23657 | 345 |
(fn (a, b) => |
55639 | 346 |
if a = case_concl_tagN |
347 |
then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE) |
|
23657 | 348 |
else NONE) |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
349 |
in fold add_case_concl concls end; |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
350 |
|
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
351 |
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
|
352 |
|
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 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
355 |
(** inner rule **) |
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 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
|
358 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
359 |
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
|
360 |
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
|
361 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
362 |
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
|
363 |
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
|
364 |
#> 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
|
365 |
|
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
366 |
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
|
367 |
|
45525
59561859c452
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents:
45375
diff
changeset
|
368 |
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
|
369 |
|
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
370 |
|
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 |
(** case declarations **) |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
373 |
|
10530 | 374 |
(* access hints *) |
375 |
||
33303
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
376 |
fun save th = |
1e1210f31207
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents:
31794
diff
changeset
|
377 |
save_consumes th #> |
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
34916
diff
changeset
|
378 |
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
|
379 |
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
|
380 |
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
|
381 |
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
|
382 |
save_inner_rule th; |
12761 | 383 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
384 |
fun get th = |
12761 | 385 |
let |
18477 | 386 |
val n = get_consumes th; |
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
387 |
val cases = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
388 |
(case lookup_case_names th of |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
389 |
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
|
390 |
| SOME names => map (fn name => (name, get_case_concls th name)) names); |
55639 | 391 |
val cases_hyps = |
392 |
(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
|
393 |
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
|
394 |
| 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
|
395 |
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
|
396 |
in (map regroup (cases ~~ cases_hyps), n) end; |
10530 | 397 |
|
8364 | 398 |
|
8427 | 399 |
(* params *) |
8364 | 400 |
|
18229
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
401 |
fun rename_params xss th = |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
402 |
th |
e5a624483a23
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents:
18188
diff
changeset
|
403 |
|> 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
|
404 |
|> save th; |
8364 | 405 |
|
18728 | 406 |
fun params xss = Thm.rule_attribute (K (rename_params xss)); |
8364 | 407 |
|
18477 | 408 |
|
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
409 |
(* internalize parameter names *) |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
410 |
|
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
411 |
fun internalize_params rule = |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
412 |
let |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
413 |
fun rename prem = |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
414 |
let val xs = |
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
415 |
map (Name.internal o Name.clean o fst) (Logic.strip_params prem) |
45328 | 416 |
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
|
417 |
fun rename_prems prop = |
36354 | 418 |
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
|
419 |
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
|
420 |
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
|
421 |
|
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34058
diff
changeset
|
422 |
|
18477 | 423 |
|
424 |
(** mutual_rule **) |
|
425 |
||
426 |
local |
|
427 |
||
428 |
fun equal_cterms ts us = |
|
35408 | 429 |
is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us)); |
18477 | 430 |
|
19917 | 431 |
fun prep_rule n th = |
18477 | 432 |
let |
19917 | 433 |
val th' = Thm.permute_prems 0 n th; |
33957 | 434 |
val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th'); |
18477 | 435 |
val th'' = Drule.implies_elim_list th' (map Thm.assume prems); |
436 |
in (prems, (n, th'')) end; |
|
437 |
||
438 |
in |
|
439 |
||
19917 | 440 |
fun mutual_rule _ [] = NONE |
441 |
| mutual_rule _ [th] = SOME ([0], th) |
|
442 |
| mutual_rule ctxt (ths as th :: _) = |
|
18477 | 443 |
let |
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30364
diff
changeset
|
444 |
val ((_, ths'), ctxt') = Variable.import true ths ctxt; |
19917 | 445 |
val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths'; |
446 |
val (ns, rls) = split_list (map #2 rules); |
|
18477 | 447 |
in |
448 |
if not (forall (equal_cterms prems o #1) rules) then NONE |
|
449 |
else |
|
450 |
SOME (ns, |
|
19917 | 451 |
rls |
23418 | 452 |
|> Conjunction.intr_balanced |
18477 | 453 |
|> Drule.implies_intr_list prems |
19917 | 454 |
|> singleton (Variable.export ctxt' ctxt) |
455 |
|> save th |
|
18477 | 456 |
|> put_consumes (SOME 0)) |
457 |
end; |
|
458 |
||
459 |
end; |
|
460 |
||
19917 | 461 |
fun strict_mutual_rule ctxt ths = |
462 |
(case mutual_rule ctxt ths of |
|
18581 | 463 |
NONE => error "Failed to join given rules into one mutual rule" |
464 |
| SOME res => res); |
|
465 |
||
8364 | 466 |
end; |
17113 | 467 |
|
33368 | 468 |
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
|
469 |
open Basic_Rule_Cases; |