author | wenzelm |
Sat, 15 Oct 2005 00:08:01 +0200 | |
changeset 17852 | a06b185a26d7 |
parent 17361 | 008b14a7afc4 |
child 17861 | 28d3483afbbc |
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 |
17361 | 18 |
val make: bool -> term option -> theory * term -> string list -> (string * T option) list |
19 |
val simple: bool -> theory * term -> string -> string * T option |
|
8427 | 20 |
val rename_params: string list list -> thm -> thm |
8364 | 21 |
val params: string list list -> 'a attribute |
16390 | 22 |
type tactic |
17113 | 23 |
val NO_CASES: Tactical.tactic -> tactic |
8364 | 24 |
end; |
25 |
||
26 |
structure RuleCases: RULE_CASES = |
|
27 |
struct |
|
28 |
||
10811 | 29 |
(* names *) |
30 |
||
31 |
val consumes_tagN = "consumes"; |
|
32 |
val cases_tagN = "cases"; |
|
33 |
val case_conclN = "case"; |
|
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
34 |
val case_hypsN = "hyps"; |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
35 |
val case_premsN = "prems"; |
10811 | 36 |
|
37 |
||
10530 | 38 |
(* number of consumed facts *) |
8364 | 39 |
|
12761 | 40 |
fun lookup_consumes thm = |
10530 | 41 |
let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in |
17184 | 42 |
(case AList.lookup (op =) (Thm.tags_of_thm thm) (consumes_tagN) of |
15531 | 43 |
NONE => NONE |
44 |
| SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ()) |
|
10530 | 45 |
| _ => err ()) |
46 |
end; |
|
47 |
||
15531 | 48 |
fun put_consumes NONE th = th |
49 |
| put_consumes (SOME n) th = th |
|
12761 | 50 |
|> Drule.untag_rule consumes_tagN |
51 |
|> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]); |
|
10530 | 52 |
|
12761 | 53 |
val save_consumes = put_consumes o lookup_consumes; |
54 |
||
15531 | 55 |
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
|
56 |
fun consumes_default n x = |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
57 |
if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x; |
8364 | 58 |
|
59 |
||
60 |
(* case names *) |
|
61 |
||
15531 | 62 |
fun put_case_names NONE thm = thm |
63 |
| put_case_names (SOME names) thm = |
|
12761 | 64 |
thm |
65 |
|> Drule.untag_rule cases_tagN |
|
66 |
|> Drule.tag_rule (cases_tagN, names); |
|
8364 | 67 |
|
17184 | 68 |
fun lookup_case_names thm = AList.lookup (op =) (Thm.tags_of_thm thm) cases_tagN; |
10530 | 69 |
|
12761 | 70 |
val save_case_names = put_case_names o lookup_case_names; |
15531 | 71 |
val name = put_case_names o SOME; |
8427 | 72 |
fun case_names ss = Drule.rule_attribute (K (name ss)); |
8364 | 73 |
|
10530 | 74 |
|
75 |
(* access hints *) |
|
76 |
||
12761 | 77 |
fun save thm = save_case_names thm o save_consumes thm; |
78 |
||
79 |
fun get thm = |
|
80 |
let |
|
15973 | 81 |
val n = if_none (lookup_consumes thm) 0; |
12761 | 82 |
val ss = |
83 |
(case lookup_case_names thm of |
|
15531 | 84 |
NONE => map Library.string_of_int (1 upto (Thm.nprems_of thm - n)) |
85 |
| SOME ss => ss); |
|
12761 | 86 |
in (ss, n) end; |
87 |
||
8364 | 88 |
fun add thm = (thm, get thm); |
10530 | 89 |
|
8364 | 90 |
|
91 |
(* prepare cases *) |
|
92 |
||
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
93 |
type T = |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
94 |
{fixes: (string * typ) list, |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
95 |
assumes: (string * term list) list, |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
96 |
binds: (indexname * term option) list}; |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
97 |
|
17167 | 98 |
fun unskolem x = |
99 |
(case try Syntax.dest_skolem x of SOME x' => x' | NONE => x); |
|
100 |
||
17361 | 101 |
fun prep_case is_open thy (split, raw_prop) name = |
8364 | 102 |
let |
17361 | 103 |
val prop = Drule.norm_hhf thy raw_prop; |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
104 |
|
17167 | 105 |
val xs = map (apfst unskolem) (Logic.strip_params prop); |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
106 |
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
|
107 |
val named_xs = |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
108 |
(case split of |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
109 |
NONE => rename xs |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
110 |
| SOME t => |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
111 |
let val (us, vs) = splitAt (length (Logic.strip_params t), xs) |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
112 |
in rename us @ vs end); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
113 |
|
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
114 |
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
|
115 |
val named_asms = |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
116 |
(case split of |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
117 |
NONE => [("", asms)] |
15531 | 118 |
| SOME t => |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
119 |
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
|
120 |
in [(case_hypsN, hyps), (case_premsN, prems)] end); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
121 |
|
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
122 |
val concl = Term.list_abs (named_xs, Logic.strip_assums_concl prop); |
17361 | 123 |
val bind = ((case_conclN, 0), SOME (ObjectLogic.drop_judgment thy concl)); |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
124 |
in (name, SOME {fixes = named_xs, assumes = named_asms, binds = [bind]}) end; |
8364 | 125 |
|
17361 | 126 |
fun make is_open split (thy, prop) names = |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
127 |
let |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
128 |
val nprems = Logic.count_prems (prop, 0); |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
129 |
fun add_case name (cases, i) = |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
130 |
((case try (fn () => |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
131 |
(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
|
132 |
NONE => (name, NONE) |
17361 | 133 |
| SOME sp => prep_case is_open thy sp name) :: cases, i - 1); |
16148
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
134 |
in |
5f15a14122dc
make: T option -- actually remove undefined cases;
wenzelm
parents:
15973
diff
changeset
|
135 |
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
|
136 |
|> #1 |
10811 | 137 |
end; |
8364 | 138 |
|
17361 | 139 |
fun simple is_open (thy, prop) = prep_case is_open thy (NONE, prop); |
140 |
||
8364 | 141 |
|
8427 | 142 |
(* params *) |
8364 | 143 |
|
11002 | 144 |
fun rename_params xss thm = foldln Thm.rename_params_rule xss thm |
10530 | 145 |
|> save thm; |
8364 | 146 |
|
147 |
fun params xss = Drule.rule_attribute (K (rename_params xss)); |
|
148 |
||
16390 | 149 |
|
150 |
(* tactics with cases *) |
|
151 |
||
152 |
type tactic = thm -> (thm * (string * T option) list) Seq.seq; |
|
153 |
||
17113 | 154 |
fun NO_CASES tac = Seq.map (rpair []) o tac; |
155 |
||
8364 | 156 |
end; |
17113 | 157 |
|
158 |
val NO_CASES = RuleCases.NO_CASES; |