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 mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
20 |
21 |
21 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
22 (* @chunk definitions *) |
|
23 fun define_aux s ((binding, syn), (attr, trm)) lthy = |
|
24 let |
|
25 val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy |
|
26 in |
|
27 (thm, lthy) |
|
28 end |
|
29 |
|
30 fun DEFINITION params' rules preds preds' Tss lthy = |
|
31 let |
|
32 val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules |
|
33 in |
|
34 fold_map (fn ((((R, _), syn), pred), Ts) => |
|
35 let |
|
36 val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts)) |
|
37 |
|
38 val t0 = list_comb (pred, zs); |
|
39 val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; |
|
40 val t2 = fold_rev mk_all preds' t1; |
|
41 val t3 = fold_rev lambda (params' @ zs) t2; |
|
42 in |
|
43 define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3)) |
|
44 end) (preds ~~ preds' ~~ Tss) lthy |
|
45 end |
|
46 (* @end *) |
22 |
47 |
23 fun inst_spec ct = |
48 fun inst_spec ct = |
24 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
49 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
25 |
50 |
26 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
51 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
27 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); |
52 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); |
|
53 |
28 |
54 |
29 (* @chunk induction_rules *) |
55 (* @chunk induction_rules *) |
30 fun INDUCTION rules preds' Tss defs lthy1 lthy2 = |
56 fun INDUCTION rules preds' Tss defs lthy1 lthy2 = |
31 let |
57 let |
32 val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2; |
58 val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2; |
85 in rtac prem'' 1 end) ctxt') prems1) |
111 in rtac prem'' 1 end) ctxt') prems1) |
86 end) ctxt 1]) |> |
112 end) ctxt 1]) |> |
87 singleton (ProofContext.export lthy2 lthy1) |
113 singleton (ProofContext.export lthy2 lthy1) |
88 in |
114 in |
89 map_index prove_intro rules |
115 map_index prove_intro rules |
90 end |
|
91 (* @end *) |
|
92 |
|
93 (* @chunk definitions *) |
|
94 fun define_aux s ((binding, syn), (attr, trm)) lthy = |
|
95 let |
|
96 val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy |
|
97 in |
|
98 (thm, lthy) |
|
99 end |
|
100 |
|
101 fun DEFINITION params' rules preds preds' Tss lthy = |
|
102 let |
|
103 val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules |
|
104 in |
|
105 fold_map (fn ((((R, _), syn), pred), Ts) => |
|
106 let |
|
107 val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts)) |
|
108 |
|
109 val t0 = list_comb (pred, zs); |
|
110 val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; |
|
111 val t2 = fold_rev mk_all preds' t1; |
|
112 val t3 = fold_rev lambda (params' @ zs) t2; |
|
113 in |
|
114 define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3)) |
|
115 end) (preds ~~ preds' ~~ Tss) lthy |
|
116 end |
116 end |
117 (* @end *) |
117 (* @end *) |
118 |
118 |
119 (* @chunk add_inductive_i *) |
119 (* @chunk add_inductive_i *) |
120 fun add_inductive_i preds params specs lthy = |
120 fun add_inductive_i preds params specs lthy = |