author | wenzelm |
Fri, 26 Jul 2002 21:09:39 +0200 | |
changeset 13425 | 119ae829ad9b |
parent 12809 | 787ecc2ac737 |
child 13596 | ee5f79b210c1 |
permissions | -rw-r--r-- |
8364 | 1 |
(* Title: Pure/Isar/rule_cases.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
8807 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
8364 | 5 |
|
6 |
Manage local contexts of rules. |
|
7 |
*) |
|
8 |
||
9 |
signature RULE_CASES = |
|
10 |
sig |
|
10530 | 11 |
val consumes: int -> 'a attribute |
12 |
val consumes_default: int -> 'a attribute |
|
8364 | 13 |
val name: string list -> thm -> thm |
8427 | 14 |
val case_names: string list -> 'a attribute |
12761 | 15 |
val save: thm -> thm -> thm |
10530 | 16 |
val get: thm -> string list * int |
17 |
val add: thm -> thm * (string list * int) |
|
10811 | 18 |
type T |
12166 | 19 |
val empty: T |
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
20 |
val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list |
8427 | 21 |
val rename_params: string list list -> thm -> thm |
8364 | 22 |
val params: string list list -> 'a attribute |
23 |
end; |
|
24 |
||
25 |
structure RuleCases: RULE_CASES = |
|
26 |
struct |
|
27 |
||
10811 | 28 |
(* names *) |
29 |
||
30 |
val consumes_tagN = "consumes"; |
|
31 |
val cases_tagN = "cases"; |
|
32 |
val case_conclN = "case"; |
|
33 |
||
34 |
||
10530 | 35 |
(* number of consumed facts *) |
8364 | 36 |
|
12761 | 37 |
fun lookup_consumes thm = |
10530 | 38 |
let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in |
12761 | 39 |
(case Library.assoc (Thm.tags_of_thm thm, consumes_tagN) of |
40 |
None => None |
|
41 |
| Some [s] => (case Syntax.read_nat s of Some n => Some n | _ => err ()) |
|
10530 | 42 |
| _ => err ()) |
43 |
end; |
|
44 |
||
12761 | 45 |
fun put_consumes None th = th |
46 |
| put_consumes (Some n) th = th |
|
47 |
|> Drule.untag_rule consumes_tagN |
|
48 |
|> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]); |
|
10530 | 49 |
|
12761 | 50 |
val save_consumes = put_consumes o lookup_consumes; |
51 |
||
52 |
fun consumes n x = Drule.rule_attribute (K (put_consumes (Some n))) x; |
|
10530 | 53 |
fun consumes_default n x = if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x; |
8364 | 54 |
|
55 |
||
56 |
(* case names *) |
|
57 |
||
12761 | 58 |
fun put_case_names None thm = thm |
59 |
| put_case_names (Some names) thm = |
|
60 |
thm |
|
61 |
|> Drule.untag_rule cases_tagN |
|
62 |
|> Drule.tag_rule (cases_tagN, names); |
|
8364 | 63 |
|
12761 | 64 |
fun lookup_case_names thm = Library.assoc (Thm.tags_of_thm thm, cases_tagN); |
10530 | 65 |
|
12761 | 66 |
val save_case_names = put_case_names o lookup_case_names; |
67 |
val name = put_case_names o Some; |
|
8427 | 68 |
fun case_names ss = Drule.rule_attribute (K (name ss)); |
8364 | 69 |
|
10530 | 70 |
|
71 |
(* access hints *) |
|
72 |
||
12761 | 73 |
fun save thm = save_case_names thm o save_consumes thm; |
74 |
||
75 |
fun get thm = |
|
76 |
let |
|
77 |
val n = if_none (lookup_consumes thm) 0; |
|
78 |
val ss = |
|
79 |
(case lookup_case_names thm of |
|
80 |
None => map Library.string_of_int (1 upto (Thm.nprems_of thm - n)) |
|
81 |
| Some ss => ss); |
|
82 |
in (ss, n) end; |
|
83 |
||
8364 | 84 |
fun add thm = (thm, get thm); |
10530 | 85 |
|
8364 | 86 |
|
87 |
(* prepare cases *) |
|
88 |
||
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
89 |
type T = |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
90 |
{fixes: (string * typ) list, |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
91 |
assumes: (string * term list) list, |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
92 |
binds: (indexname * term option) list}; |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
93 |
|
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
94 |
val hypsN = "hyps"; |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
95 |
val premsN = "prems"; |
10530 | 96 |
|
12166 | 97 |
val empty = {fixes = [], assumes = [], binds = []}; |
98 |
||
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
99 |
fun prep_case is_open split sg prop name i = |
8364 | 100 |
let |
12809
787ecc2ac737
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12761
diff
changeset
|
101 |
val Bi = Drule.norm_hhf sg (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop)))); |
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
102 |
val xs = map (if is_open then I else apfst Syntax.internal) (Logic.strip_params Bi); |
10811 | 103 |
val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); |
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
104 |
val named_asms = |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
105 |
(case split of None => [("", asms)] |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
106 |
| Some t => |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
107 |
let val h = length (Logic.strip_assums_hyp |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
108 |
(hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs t))))) |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
109 |
in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end); |
10872 | 110 |
val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi); |
12809
787ecc2ac737
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12761
diff
changeset
|
111 |
val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl)); |
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
112 |
in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end; |
8364 | 113 |
|
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
114 |
fun make is_open split (sg, prop) names = |
12809
787ecc2ac737
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12761
diff
changeset
|
115 |
let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in |
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
116 |
foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1)) |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
12809
diff
changeset
|
117 |
(Library.drop (length names - nprems, names), ([], length names)) |> #1 |
10811 | 118 |
end; |
8364 | 119 |
|
120 |
||
8427 | 121 |
(* params *) |
8364 | 122 |
|
11002 | 123 |
fun rename_params xss thm = foldln Thm.rename_params_rule xss thm |
10530 | 124 |
|> save thm; |
8364 | 125 |
|
126 |
fun params xss = Drule.rule_attribute (K (rename_params xss)); |
|
127 |
||
128 |
end; |