author | wenzelm |
Tue, 09 Dec 2014 19:39:40 +0100 | |
changeset 59119 | c90c02940964 |
parent 58828 | 6d076fdd933d |
child 59621 | 291934bac95e |
permissions | -rw-r--r-- |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: ZF/Tools/ind_cases.ML |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, LMU Muenchen |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
3 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
4 |
Generic inductive cases facility for (co)inductive definitions. |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
5 |
*) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
6 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
7 |
signature IND_CASES = |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
8 |
sig |
36541
de1862c4a308
more explicit treatment of context, although not fully localized;
wenzelm
parents:
35762
diff
changeset
|
9 |
val declare: string -> (Proof.context -> conv) -> theory -> theory |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
10 |
val inductive_cases: (Attrib.binding * string list) list -> theory -> theory |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
11 |
end; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
12 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
13 |
structure IndCases: IND_CASES = |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
14 |
struct |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
15 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
16 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
17 |
(* theory data *) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
18 |
|
33522 | 19 |
structure IndCasesData = Theory_Data |
22846 | 20 |
( |
36864 | 21 |
type T = (Proof.context -> conv) Symtab.table; |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
22 |
val empty = Symtab.empty; |
16424 | 23 |
val extend = I; |
33522 | 24 |
fun merge data = Symtab.merge (K true) data; |
22846 | 25 |
); |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
26 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
27 |
|
17412 | 28 |
fun declare name f = IndCasesData.map (Symtab.update (name, f)); |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
29 |
|
36541
de1862c4a308
more explicit treatment of context, although not fully localized;
wenzelm
parents:
35762
diff
changeset
|
30 |
fun smart_cases ctxt s = |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
31 |
let |
42361 | 32 |
val thy = Proof_Context.theory_of ctxt; |
18678 | 33 |
fun err msg = cat_error msg ("Malformed set membership statement: " ^ s); |
36541
de1862c4a308
more explicit treatment of context, although not fully localized;
wenzelm
parents:
35762
diff
changeset
|
34 |
val A = Syntax.read_prop ctxt s handle ERROR msg => err msg; |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
35 |
val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop |
18678 | 36 |
(Logic.strip_imp_concl A)))))) handle TERM _ => err ""; |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
37 |
in |
17412 | 38 |
(case Symtab.lookup (IndCasesData.get thy) c of |
15531 | 39 |
NONE => error ("Unknown inductive cases rule for set " ^ quote c) |
36541
de1862c4a308
more explicit treatment of context, although not fully localized;
wenzelm
parents:
35762
diff
changeset
|
40 |
| SOME f => f ctxt (Thm.cterm_of thy A)) |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
41 |
end; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
42 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
43 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
44 |
(* inductive_cases command *) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
45 |
|
12609 | 46 |
fun inductive_cases args thy = |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
47 |
let |
42361 | 48 |
val ctxt = Proof_Context.init_global thy; |
12609 | 49 |
val facts = args |> map (fn ((name, srcs), props) => |
56031 | 50 |
((name, map (Attrib.attribute_cmd ctxt) srcs), |
36541
de1862c4a308
more explicit treatment of context, although not fully localized;
wenzelm
parents:
35762
diff
changeset
|
51 |
map (Thm.no_attributes o single o smart_cases ctxt) props)); |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
36960
diff
changeset
|
52 |
in thy |> Global_Theory.note_thmss "" facts |> snd end; |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
53 |
|
24867 | 54 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
42361
diff
changeset
|
55 |
Outer_Syntax.command @{command_spec "inductive_cases"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
42361
diff
changeset
|
56 |
"create simplified instances of elimination rules (improper)" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
57 |
(Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop) |
24867 | 58 |
>> (Toplevel.theory o inductive_cases)); |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
59 |
|
58828 | 60 |
|
61 |
(* ind_cases method *) |
|
62 |
||
63 |
val _ = |
|
64 |
Theory.setup |
|
65 |
(Method.setup @{binding "ind_cases"} |
|
66 |
(Scan.lift (Scan.repeat1 Args.name_inner_syntax) >> |
|
67 |
(fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props))) |
|
68 |
"dynamic case analysis on sets"); |
|
69 |
||
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
70 |
end; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
71 |