author | wenzelm |
Tue, 02 Sep 2008 16:55:33 +0200 | |
changeset 28084 | a05ca48ef263 |
parent 28083 | 103d9282a946 |
child 30515 | bca05b17b618 |
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 |
ID: $Id$ |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, LMU Muenchen |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
4 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
5 |
Generic inductive cases facility for (co)inductive definitions. |
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 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
8 |
signature IND_CASES = |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
9 |
sig |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
10 |
val declare: string -> (simpset -> cterm -> thm) -> theory -> theory |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
11 |
val inductive_cases: (Attrib.binding * string list) list -> theory -> theory |
18708 | 12 |
val setup: theory -> theory |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
13 |
end; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
14 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
15 |
structure IndCases: IND_CASES = |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
16 |
struct |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
17 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
18 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
19 |
(* theory data *) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
20 |
|
16424 | 21 |
structure IndCasesData = TheoryDataFun |
22846 | 22 |
( |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
23 |
type T = (simpset -> cterm -> thm) Symtab.table; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
24 |
val empty = Symtab.empty; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
25 |
val copy = I; |
16424 | 26 |
val extend = I; |
27 |
fun merge _ tabs : T = Symtab.merge (K true) tabs; |
|
22846 | 28 |
); |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
29 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
30 |
|
17412 | 31 |
fun declare name f = IndCasesData.map (Symtab.update (name, f)); |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
32 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
33 |
fun smart_cases thy ss read_prop s = |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
34 |
let |
18678 | 35 |
fun err msg = cat_error msg ("Malformed set membership statement: " ^ s); |
36 |
val A = read_prop s handle ERROR msg => err msg; |
|
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
37 |
val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop |
18678 | 38 |
(Logic.strip_imp_concl A)))))) handle TERM _ => err ""; |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
39 |
in |
17412 | 40 |
(case Symtab.lookup (IndCasesData.get thy) c of |
15531 | 41 |
NONE => error ("Unknown inductive cases rule for set " ^ quote c) |
20342 | 42 |
| SOME f => f ss (Thm.cterm_of thy A)) |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
43 |
end; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
44 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
45 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
46 |
(* inductive_cases command *) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
47 |
|
12609 | 48 |
fun inductive_cases args thy = |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
49 |
let |
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
22846
diff
changeset
|
50 |
val read_prop = Syntax.read_prop (ProofContext.init thy); |
12609 | 51 |
val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop; |
52 |
val facts = args |> map (fn ((name, srcs), props) => |
|
18728 | 53 |
((name, map (Attrib.attribute thy) srcs), |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12716
diff
changeset
|
54 |
map (Thm.no_attributes o single o mk_cases) props)); |
27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
24867
diff
changeset
|
55 |
in thy |> PureThy.note_thmss "" facts |> snd end; |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
56 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
57 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
58 |
(* ind_cases method *) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
59 |
|
21879 | 60 |
fun mk_cases_meth (props, ctxt) = |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
61 |
props |
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
22846
diff
changeset
|
62 |
|> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt)) |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
63 |
|> Method.erule 0; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
64 |
|
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27691
diff
changeset
|
65 |
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source)); |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
66 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
67 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
68 |
(* package setup *) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
69 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
70 |
val setup = |
22846 | 71 |
Method.add_methods |
72 |
[("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")]; |
|
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
73 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
74 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
75 |
(* outer syntax *) |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
76 |
|
17057 | 77 |
local structure P = OuterParse and K = OuterKeyword in |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
78 |
|
24867 | 79 |
val _ = |
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
80 |
OuterSyntax.command "inductive_cases" |
24867 | 81 |
"create simplified instances of elimination rules (improper)" K.thy_script |
82 |
(P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop) |
|
83 |
>> (Toplevel.theory o inductive_cases)); |
|
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
84 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
85 |
end; |
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
86 |
|
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset
|
87 |
end; |
15705 | 88 |