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 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
10 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
11 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |
11 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |
12 (Attrib.binding * string) list -> (*{rules}*) |
12 (Attrib.binding * string list) list list -> (*{rules}*) |
13 local_theory -> (thm list * thm list) * local_theory |
13 local_theory -> 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 |
|
20 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
|
21 |
|
22 fun inst_spec ct = Drule.instantiate' |
|
23 [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
|
24 |
|
25 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
|
26 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); |
19 |
27 |
20 fun add_inductive_i preds_syn params intrs lthy = |
28 fun add_inductive_i preds_syn params intrs lthy = |
21 let |
29 let |
22 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
30 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
23 val preds = map (fn ((R, T), _) => |
31 val preds = map (fn ((R, T), _) => |
26 |
34 |
27 (* making the definition *) |
35 (* making the definition *) |
28 |
36 |
29 val intrs' = map |
37 val intrs' = map |
30 (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs; |
38 (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs; |
31 |
|
32 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P; |
|
33 |
39 |
34 val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => |
40 val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => |
35 let val zs = map Free (Variable.variant_frees lthy intrs' |
41 let val zs = map Free (Variable.variant_frees lthy intrs' |
36 (map (pair "z") Ts)) |
42 (map (pair "z") Ts)) |
37 in |
43 in |
50 Variable.variant_fixes (replicate (length preds) "P") lthy2; |
56 Variable.variant_fixes (replicate (length preds) "P") lthy2; |
51 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) |
57 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) |
52 (Pnames ~~ Tss); |
58 (Pnames ~~ Tss); |
53 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
59 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
54 val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs; |
60 val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs; |
55 |
|
56 fun inst_spec ct = Drule.instantiate' |
|
57 [SOME (ctyp_of_term ct)] [NONE, SOME ct] spec; |
|
58 |
61 |
59 fun prove_indrule ((R, P), Ts) = |
62 fun prove_indrule ((R, P), Ts) = |
60 let |
63 let |
61 val (znames, lthy4) = |
64 val (znames, lthy4) = |
62 Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
65 Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
78 val indrules = map prove_indrule (preds ~~ Ps ~~ Tss); |
81 val indrules = map prove_indrule (preds ~~ Ps ~~ Tss); |
79 (* @end *) |
82 (* @end *) |
80 |
83 |
81 (* proving the introduction rules *) |
84 (* proving the introduction rules *) |
82 (* @chunk intro_rules *) |
85 (* @chunk intro_rules *) |
83 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
|
84 val imp_elims = fold (fn th => fn th' => [th', th] MRS mp); |
|
85 |
|
86 fun prove_intr (i, (_, r)) = |
86 fun prove_intr (i, (_, r)) = |
87 Goal.prove lthy2 [] [] r |
87 Goal.prove lthy2 [] [] r |
88 (fn {prems, context = ctxt} => EVERY |
88 (fn {prems, context = ctxt} => EVERY |
89 [ObjectLogic.rulify_tac 1, |
89 [ObjectLogic.rulify_tac 1, |
90 rewrite_goals_tac defs, |
90 rewrite_goals_tac defs, |
134 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
134 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
135 (preds_syn ~~ indrules)) #>> maps snd) |
135 (preds_syn ~~ indrules)) #>> maps snd) |
136 end; |
136 end; |
137 |
137 |
138 (* @chunk add_inductive *) |
138 (* @chunk add_inductive *) |
139 fun add_inductive preds_syn params_syn intro_srcs lthy = |
139 fun add_inductive preds params specs lthy = |
140 let |
140 let |
141 val ((vars, specs), _) = Specification.read_specification |
141 val ((vars, specs'), _) = Specification.read_specification (preds @ params) specs lthy; |
142 (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs) |
142 val (preds', params') = chop (length preds) vars; |
143 lthy; |
143 val specs'' = map (apsnd the_single) specs' |
144 val (preds_syn', params_syn') = chop (length preds_syn) vars; |
144 val params'' = map fst params' |
145 val intrs = map (apsnd the_single) specs |
145 in |
146 in |
146 snd (add_inductive_i preds' params'' specs'' lthy) |
147 add_inductive_i preds_syn' (map fst params_syn') intrs lthy |
147 end; |
148 end; |
|
149 (* @end *) |
148 (* @end *) |
150 |
149 |
151 |
150 |
152 (* outer syntax *) |
151 (* outer syntax *) |
|
152 (* @chunk syntax *) |
|
153 val parser = |
|
154 OuterParse.opt_target -- |
|
155 OuterParse.fixes -- |
|
156 OuterParse.for_fixes -- |
|
157 Scan.optional |
|
158 (OuterParse.$$$ "where" |-- |
|
159 OuterParse.!!! |
|
160 (OuterParse.enum1 "|" |
|
161 ((SpecParse.opt_thm_name ":" -- |
|
162 (OuterParse.prop >> single)) >> single))) [] |
153 |
163 |
154 (* @chunk syntax *) |
|
155 local structure P = OuterParse and K = OuterKeyword in |
|
156 |
164 |
157 val ind_decl = |
165 val ind_decl = |
158 P.opt_target -- |
166 parser >> |
159 P.fixes -- P.for_fixes -- |
167 (fn (((loc, preds), params), specs) => |
160 Scan.optional (P.$$$ "where" |-- |
168 Toplevel.local_theory loc (add_inductive preds params specs)); |
161 P.!!! (P.enum1 "|" (SpecParse.opt_thm_name ":" -- P.prop))) [] >> |
|
162 (fn (((loc, preds), params), specs) => |
|
163 Toplevel.local_theory loc (add_inductive preds params specs #> snd)); |
|
164 |
169 |
165 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
170 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
166 K.thy_decl ind_decl; |
171 OuterKeyword.thy_decl ind_decl; |
167 |
|
168 end; |
|
169 (* @end *) |
172 (* @end *) |
170 |
173 |
171 end; |
174 end; |