1 (* @chunk SIMPLE_INDUCTIVE_PACKAGE *) |
1 (* @chunk SIMPLE_INDUCTIVE_PACKAGE *) |
2 signature SIMPLE_INDUCTIVE_PACKAGE = |
2 signature SIMPLE_INDUCTIVE_PACKAGE = |
3 sig |
3 sig |
4 val add_inductive_i: |
4 val add_inductive_i: |
5 ((Name.binding * typ) * mixfix) list -> (*{predicates}*) |
5 ((Binding.T * typ) * mixfix) list -> (*{predicates}*) |
6 (Name.binding * typ) list -> (*{parameters}*) |
6 (Binding.T * typ) list -> (*{parameters}*) |
7 (Attrib.binding * term) list -> (*{rules}*) |
7 (Attrib.binding * term) list -> (*{rules}*) |
8 local_theory -> (thm list * thm list) * local_theory |
8 local_theory -> (thm list * thm list) * local_theory |
9 val add_inductive: |
9 val add_inductive: |
10 (Name.binding * string option * mixfix) list -> (*{predicates}*) |
10 (Binding.T * string option * mixfix) list -> (*{predicates}*) |
11 (Name.binding * string option * mixfix) list -> (*{parameters}*) |
11 (Binding.T * string option * mixfix) list -> (*{parameters}*) |
12 (Attrib.binding * string) list -> (*{rules}*) |
12 (Attrib.binding * string) list -> (*{rules}*) |
13 local_theory -> (thm list * thm list) * local_theory |
13 local_theory -> (thm list * thm list) * local_theory |
14 end; |
14 end; |
15 (* @end *) |
15 (* @end *) |
16 |
16 |
17 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
17 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
18 struct |
18 struct |
19 |
19 |
20 fun add_inductive_i preds_syn params intrs lthy = |
20 fun add_inductive_i preds_syn params intrs lthy = |
21 let |
21 let |
22 val params' = map (fn (p, T) => Free (Name.name_of p, T)) params; |
22 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
23 val preds = map (fn ((R, T), _) => |
23 val preds = map (fn ((R, T), _) => |
24 list_comb (Free (Name.name_of R, T), params')) preds_syn; |
24 list_comb (Free (Binding.base_name R, T), params')) preds_syn; |
25 val Tss = map (binder_types o fastype_of) preds; |
25 val Tss = map (binder_types o fastype_of) preds; |
26 |
26 |
27 (* making the definition *) |
27 (* making the definition *) |
28 |
28 |
29 val intrs' = map |
29 val intrs' = map |
34 val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => |
34 val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => |
35 let val zs = map Free (Variable.variant_frees lthy intrs' |
35 let val zs = map Free (Variable.variant_frees lthy intrs' |
36 (map (pair "z") Ts)) |
36 (map (pair "z") Ts)) |
37 in |
37 in |
38 LocalTheory.define Thm.internalK |
38 LocalTheory.define Thm.internalK |
39 ((R, syn), (Attrib.no_binding, fold_rev lambda (params' @ zs) |
39 ((R, syn), (Attrib.empty_binding, fold_rev lambda (params' @ zs) |
40 (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp) |
40 (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp) |
41 intrs' (list_comb (pred, zs)))))) #>> snd #>> snd |
41 intrs' (list_comb (pred, zs)))))) #>> snd #>> snd |
42 end) (preds_syn ~~ preds ~~ Tss) lthy; |
42 end) (preds_syn ~~ preds ~~ Tss) lthy; |
43 |
43 |
44 val (_, lthy2) = Variable.add_fixes (map (Name.name_of o fst) params) lthy1; |
44 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
45 |
45 |
46 |
46 |
47 (* proving the induction rules *) |
47 (* proving the induction rules *) |
48 |
48 |
49 val (Pnames, lthy3) = |
49 val (Pnames, lthy3) = |
114 val intr_ths = map_index prove_intr intrs; |
114 val intr_ths = map_index prove_intr intrs; |
115 |
115 |
116 |
116 |
117 (* storing the theorems *) |
117 (* storing the theorems *) |
118 |
118 |
119 val mut_name = space_implode "_" (map (Name.name_of o fst o fst) preds_syn); |
119 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn); |
120 val case_names = map (Name.name_of o fst o fst) intrs |
120 val case_names = map (Binding.base_name o fst o fst) intrs |
121 in |
121 in |
122 lthy1 |> |
122 lthy1 |> |
123 LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
123 LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
124 ((Name.qualified mut_name a, atts), [([th], [])])) |
124 ((Binding.qualify mut_name a, atts), [([th], [])])) |
125 (intrs ~~ intr_ths)) |-> |
125 (intrs ~~ intr_ths)) |-> |
126 (fn intr_thss => LocalTheory.note Thm.theoremK |
126 (fn intr_thss => LocalTheory.note Thm.theoremK |
127 ((Name.qualified mut_name (Name.binding "intros"), []), maps snd intr_thss)) |>> |
127 ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intr_thss)) |>> |
128 snd ||>> |
128 snd ||>> |
129 (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
129 (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
130 ((Name.qualified (Name.name_of R) (Name.binding "induct"), |
130 ((Binding.qualify (Binding.base_name R) (Binding.name "induct"), |
131 [Attrib.internal (K (RuleCases.case_names case_names)), |
131 [Attrib.internal (K (RuleCases.case_names case_names)), |
132 Attrib.internal (K (RuleCases.consumes 1)), |
132 Attrib.internal (K (RuleCases.consumes 1)), |
133 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
133 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
134 (preds_syn ~~ indrules)) #>> maps snd) |
134 (preds_syn ~~ indrules)) #>> maps snd) |
135 end; |
135 end; |