author | wenzelm |
Tue, 14 Jun 2005 21:56:55 +0200 | |
changeset 16390 | 305ce441869d |
parent 16148 | 5f15a14122dc |
child 17113 | 3b67c1809e1c |
permissions | -rw-r--r-- |
8364 | 1 |
(* Title: Pure/Isar/rule_cases.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Manage local contexts of rules. |
|
6 |
*) |
|
7 |
||
8 |
signature RULE_CASES = |
|
9 |
sig |
|
10530 | 10 |
val consumes: int -> 'a attribute |
11 |
val consumes_default: int -> 'a attribute |
|
8364 | 12 |
val name: string list -> thm -> thm |
8427 | 13 |
val case_names: string list -> 'a attribute |
12761 | 14 |
val save: thm -> thm -> thm |
10530 | 15 |
val get: thm -> string list * int |
16 |
val add: thm -> thm * (string list * int) |
|
10811 | 17 |
type T |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
18 |
val make: bool -> term option -> Sign.sg * term -> string list -> (string * T option) list |
8427 | 19 |
val rename_params: string list list -> thm -> thm |
8364 | 20 |
val params: string list list -> 'a attribute |
16390 | 21 |
type tactic |
8364 | 22 |
end; |
23 |
||
24 |
structure RuleCases: RULE_CASES = |
|
25 |
struct |
|
26 |
||
10811 | 27 |
(* names *) |
28 |
||
29 |
val consumes_tagN = "consumes"; |
|
30 |
val cases_tagN = "cases"; |
|
31 |
val case_conclN = "case"; |
|
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
32 |
val case_hypsN = "hyps"; |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
33 |
val case_premsN = "prems"; |
10811 | 34 |
|
35 |
||
10530 | 36 |
(* number of consumed facts *) |
8364 | 37 |
|
12761 | 38 |
fun lookup_consumes thm = |
10530 | 39 |
let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in |
12761 | 40 |
(case Library.assoc (Thm.tags_of_thm thm, consumes_tagN) of |
15531 | 41 |
NONE => NONE |
42 |
| SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ()) |
|
10530 | 43 |
| _ => err ()) |
44 |
end; |
|
45 |
||
15531 | 46 |
fun put_consumes NONE th = th |
47 |
| put_consumes (SOME n) th = th |
|
12761 | 48 |
|> Drule.untag_rule consumes_tagN |
49 |
|> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]); |
|
10530 | 50 |
|
12761 | 51 |
val save_consumes = put_consumes o lookup_consumes; |
52 |
||
15531 | 53 |
fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x; |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
54 |
fun consumes_default n x = |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
55 |
if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x; |
8364 | 56 |
|
57 |
||
58 |
(* case names *) |
|
59 |
||
15531 | 60 |
fun put_case_names NONE thm = thm |
61 |
| put_case_names (SOME names) thm = |
|
12761 | 62 |
thm |
63 |
|> Drule.untag_rule cases_tagN |
|
64 |
|> Drule.tag_rule (cases_tagN, names); |
|
8364 | 65 |
|
12761 | 66 |
fun lookup_case_names thm = Library.assoc (Thm.tags_of_thm thm, cases_tagN); |
10530 | 67 |
|
12761 | 68 |
val save_case_names = put_case_names o lookup_case_names; |
15531 | 69 |
val name = put_case_names o SOME; |
8427 | 70 |
fun case_names ss = Drule.rule_attribute (K (name ss)); |
8364 | 71 |
|
10530 | 72 |
|
73 |
(* access hints *) |
|
74 |
||
12761 | 75 |
fun save thm = save_case_names thm o save_consumes thm; |
76 |
||
77 |
fun get thm = |
|
78 |
let |
|
15973 | 79 |
val n = if_none (lookup_consumes thm) 0; |
12761 | 80 |
val ss = |
81 |
(case lookup_case_names thm of |
|
15531 | 82 |
NONE => map Library.string_of_int (1 upto (Thm.nprems_of thm - n)) |
83 |
| SOME ss => ss); |
|
12761 | 84 |
in (ss, n) end; |
85 |
||
8364 | 86 |
fun add thm = (thm, get thm); |
10530 | 87 |
|
8364 | 88 |
|
89 |
(* prepare cases *) |
|
90 |
||
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
91 |
type T = |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
92 |
{fixes: (string * typ) list, |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
93 |
assumes: (string * term list) list, |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
94 |
binds: (indexname * term option) list}; |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
95 |
|
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
96 |
fun prep_case is_open sg (split, raw_prop) name = |
8364 | 97 |
let |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
98 |
val prop = Drule.norm_hhf sg raw_prop; |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
99 |
|
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
100 |
val xs = Logic.strip_params prop; |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
101 |
val rename = if is_open then I else map (apfst Syntax.internal); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
102 |
val named_xs = |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
103 |
(case split of |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
104 |
NONE => rename xs |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
105 |
| SOME t => |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
106 |
let val (us, vs) = splitAt (length (Logic.strip_params t), xs) |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
107 |
in rename us @ vs end); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
108 |
|
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
109 |
val asms = map (curry Term.list_abs named_xs) (Logic.strip_assums_hyp prop); |
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
110 |
val named_asms = |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
111 |
(case split of |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
112 |
NONE => [("", asms)] |
15531 | 113 |
| SOME t => |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
114 |
let val (hyps, prems) = splitAt (length (Logic.strip_assums_hyp t), asms) |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
115 |
in [(case_hypsN, hyps), (case_premsN, prems)] end); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
116 |
|
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
117 |
val concl = Term.list_abs (named_xs, Logic.strip_assums_concl prop); |
15531 | 118 |
val bind = ((case_conclN, 0), SOME (ObjectLogic.drop_judgment sg concl)); |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
119 |
in (name, SOME {fixes = named_xs, assumes = named_asms, binds = [bind]}) end; |
8364 | 120 |
|
14404
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
13668
diff
changeset
|
121 |
fun make is_open split (sg, prop) names = |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
122 |
let |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
123 |
val nprems = Logic.count_prems (prop, 0); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
124 |
fun add_case name (cases, i) = |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
125 |
((case try (fn () => |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
126 |
(Option.map (curry Logic.nth_prem i) split, Logic.nth_prem (i, prop))) () of |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
127 |
NONE => (name, NONE) |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
128 |
| SOME sp => prep_case is_open sg sp name) :: cases, i - 1); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
129 |
in |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
130 |
fold_rev add_case (Library.drop (length names - nprems, names)) ([], length names) |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
131 |
|> #1 |
10811 | 132 |
end; |
8364 | 133 |
|
134 |
||
8427 | 135 |
(* params *) |
8364 | 136 |
|
11002 | 137 |
fun rename_params xss thm = foldln Thm.rename_params_rule xss thm |
10530 | 138 |
|> save thm; |
8364 | 139 |
|
140 |
fun params xss = Drule.rule_attribute (K (rename_params xss)); |
|
141 |
||
16390 | 142 |
|
143 |
(* tactics with cases *) |
|
144 |
||
145 |
type tactic = thm -> (thm * (string * T option) list) Seq.seq; |
|
146 |
||
8364 | 147 |
end; |