|
1 (* Title: ZF/Tools/ind_cases.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, LMU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Generic inductive cases facility for (co)inductive definitions. |
|
7 *) |
|
8 |
|
9 signature IND_CASES = |
|
10 sig |
|
11 val declare: string -> (simpset -> cterm -> thm) -> theory -> theory |
|
12 val inductive_cases: ((bstring * Args.src list) * string list) -> theory -> theory |
|
13 val setup: (theory -> theory) list |
|
14 end; |
|
15 |
|
16 structure IndCases: IND_CASES = |
|
17 struct |
|
18 |
|
19 |
|
20 (* theory data *) |
|
21 |
|
22 structure IndCasesArgs = |
|
23 struct |
|
24 val name = "ZF/ind_cases"; |
|
25 type T = (simpset -> cterm -> thm) Symtab.table; |
|
26 |
|
27 val empty = Symtab.empty; |
|
28 val copy = I; |
|
29 val finish = I; |
|
30 val prep_ext = I; |
|
31 fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2); |
|
32 fun print _ _ = (); |
|
33 end; |
|
34 |
|
35 structure IndCasesData = TheoryDataFun(IndCasesArgs); |
|
36 |
|
37 fun declare name f = IndCasesData.map (fn tab => Symtab.update ((name, f), tab)); |
|
38 |
|
39 fun smart_cases thy ss read_prop s = |
|
40 let |
|
41 fun err () = error ("Malformed set membership statement: " ^ s); |
|
42 val A = read_prop s handle ERROR => err (); |
|
43 val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop |
|
44 (Logic.strip_imp_concl A)))))) handle TERM _ => err (); |
|
45 in |
|
46 (case Symtab.lookup (IndCasesData.get thy, c) of |
|
47 None => error ("Unknown inductive cases rule for set " ^ quote c) |
|
48 | Some f => f ss (Thm.cterm_of (Theory.sign_of thy) A)) |
|
49 end; |
|
50 |
|
51 |
|
52 (* inductive_cases command *) |
|
53 |
|
54 fun inductive_cases ((name, srcs), props) thy = |
|
55 let |
|
56 val read_prop = ProofContext.read_prop (ProofContext.init thy); |
|
57 val ths = map (smart_cases thy (Simplifier.simpset_of thy) read_prop) props; |
|
58 val atts = map (Attrib.global_attribute thy) srcs; |
|
59 in |
|
60 thy |> IsarThy.have_theorems_i Drule.lemmaK |
|
61 [(((name, atts), map Thm.no_attributes ths), Comment.none)] |
|
62 end; |
|
63 |
|
64 |
|
65 (* ind_cases method *) |
|
66 |
|
67 fun mk_cases_meth (ctxt, props) = |
|
68 props |
|
69 |> map (smart_cases (ProofContext.theory_of ctxt) (Simplifier.get_local_simpset ctxt) |
|
70 (ProofContext.read_prop ctxt)) |
|
71 |> Method.erule 0; |
|
72 |
|
73 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); |
|
74 |
|
75 |
|
76 (* package setup *) |
|
77 |
|
78 val setup = |
|
79 [IndCasesData.init, |
|
80 Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, |
|
81 "dynamic case analysis on sets")]]; |
|
82 |
|
83 |
|
84 (* outer syntax *) |
|
85 |
|
86 local structure P = OuterParse and K = OuterSyntax.Keyword in |
|
87 |
|
88 val ind_cases = |
|
89 P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment |
|
90 >> (Toplevel.theory o inductive_cases); |
|
91 |
|
92 val inductive_casesP = |
|
93 OuterSyntax.command "inductive_cases" |
|
94 "create simplified instances of elimination rules (improper)" K.thy_script ind_cases; |
|
95 |
|
96 val _ = OuterSyntax.add_parsers [inductive_casesP]; |
|
97 |
|
98 end; |
|
99 |
|
100 end; |