18 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
18 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
19 struct |
19 struct |
20 |
20 |
21 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
21 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
22 |
22 |
23 (* @chunk definitions *) |
23 (* @chunk definitions_aux *) |
24 fun define_aux s ((binding, syn), (attr, trm)) lthy = |
24 fun definitions_aux s ((binding, syn), (attr, trm)) lthy = |
25 let |
25 let |
26 val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy |
26 val ((_, (_, thm)), lthy) = |
|
27 LocalTheory.define s ((binding, syn), (attr, trm)) lthy |
27 in |
28 in |
28 (thm, lthy) |
29 (thm, lthy) |
29 end |
30 end |
30 |
31 (* @end *) |
31 fun DEFINITION params' rules preds preds' Tss lthy = |
32 |
32 let |
33 (* @chunk definitions *) |
33 val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules |
34 fun definitions params rules preds preds' Tss lthy = |
|
35 let |
|
36 val thy = ProofContext.theory_of lthy |
|
37 val rules' = map (ObjectLogic.atomize_term thy) rules |
34 in |
38 in |
35 fold_map (fn ((((R, _), syn), pred), Ts) => |
39 fold_map (fn ((((R, _), syn), pred), Ts) => |
36 let |
40 let |
37 val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts)) |
41 val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts)) |
38 |
42 |
39 val t0 = list_comb (pred, zs); |
43 val t0 = list_comb (pred, zs); |
40 val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; |
44 val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; |
41 val t2 = fold_rev mk_all preds' t1; |
45 val t2 = fold_rev mk_all preds' t1; |
42 val t3 = fold_rev lambda (params' @ zs) t2; |
46 val t3 = fold_rev lambda (params @ zs) t2; |
43 in |
47 in |
44 define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3)) |
48 definitions_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3)) |
45 end) (preds ~~ preds' ~~ Tss) lthy |
49 end) (preds ~~ preds' ~~ Tss) lthy |
46 end |
50 end |
47 (* @end *) |
51 (* @end *) |
48 |
52 |
49 fun inst_spec ct = |
53 fun inst_spec ct = |
123 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
127 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
124 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds; |
128 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds; |
125 val Tss = map (binder_types o fastype_of) preds'; |
129 val Tss = map (binder_types o fastype_of) preds'; |
126 val (ass,rules) = split_list specs; |
130 val (ass,rules) = split_list specs; |
127 |
131 |
128 val (defs, lthy1) = DEFINITION params' rules preds preds' Tss lthy |
132 val (defs, lthy1) = definitions params' rules preds preds' Tss lthy |
129 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
133 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
130 |
134 |
131 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
135 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
132 |
136 |
133 val intros = INTROS rules preds' defs lthy1 lthy2 |
137 val intros = INTROS rules preds' defs lthy1 lthy2 |
188 parser >> |
192 parser >> |
189 (fn (((loc, preds), params), specs) => |
193 (fn (((loc, preds), params), specs) => |
190 Toplevel.local_theory loc (add_inductive preds params specs)) |
194 Toplevel.local_theory loc (add_inductive preds params specs)) |
191 |
195 |
192 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
196 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
193 OuterKeyword.thy_decl ind_decl; |
197 OuterKeyword.thy_decl ind_decl |
194 (* @end *) |
198 (* @end *) |
195 |
199 |
196 end; |
200 end; |