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 ((Binding.binding * typ) * mixfix) list -> (*{predicates}*) |
5 ((Binding.binding * typ) * mixfix) list -> (*{predicates}*) |
6 (Binding.binding * typ) list -> (*{parameters}*) |
6 (Binding.binding * typ) list -> (*{parameters}*) |
7 (Attrib.binding * term) list -> (*{rules}*) |
7 ((Binding.binding * Attrib.src list) * term) list -> (*{rules}*) |
8 local_theory -> (thm list * thm list) * local_theory |
8 local_theory -> 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) list list -> (*{rules}*) |
12 (Attrib.binding * string) list -> (*{rules}*) |
13 local_theory -> 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 |
19 |
|
20 |
20 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 |
21 |
22 |
22 fun inst_spec ct = Drule.instantiate' |
23 fun inst_spec ct = |
23 [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
24 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
24 |
25 |
25 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
26 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}); |
27 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); |
27 |
28 |
28 fun add_inductive_i preds_syn params intrs lthy = |
29 (* @chunk induction_rules *) |
29 let |
30 fun INDUCTION rules preds' Tss defs lthy1 lthy2 = |
30 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
31 let |
31 val preds = map (fn ((R, T), _) => |
32 val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2; |
32 list_comb (Free (Binding.base_name R, T), params')) preds_syn; |
33 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss); |
33 val Tss = map (binder_types o fastype_of) preds; |
34 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
|
35 val rules'' = map (subst_free (preds' ~~ Ps)) rules; |
34 |
36 |
35 (* making the definition *) |
37 fun prove_indrule ((R, P), Ts) = |
|
38 let |
|
39 val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
|
40 val zs = map Free (znames ~~ Ts) |
36 |
41 |
37 val intrs' = map |
42 val prem = HOLogic.mk_Trueprop (list_comb (R, zs)) |
38 (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs; |
43 val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs))) |
|
44 in |
|
45 Goal.prove lthy4 [] [prem] goal |
|
46 (fn {prems, ...} => EVERY1 |
|
47 ([ObjectLogic.full_atomize_tac, |
|
48 cut_facts_tac prems, |
|
49 K (rewrite_goals_tac defs)] @ |
|
50 map (fn ct => dtac (inst_spec ct)) cPs @ |
|
51 [assume_tac])) |> |
|
52 singleton (ProofContext.export lthy4 lthy1) |
|
53 end; |
|
54 in |
|
55 map prove_indrule (preds' ~~ Ps ~~ Tss) |
|
56 end |
|
57 (* @end *) |
39 |
58 |
40 val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => |
59 (* @chunk intro_rules *) |
41 let val zs = map Free (Variable.variant_frees lthy intrs' |
60 fun INTROS rules preds' defs lthy1 lthy2 = |
42 (map (pair "z") Ts)) |
61 let |
43 in |
62 fun prove_intro (i, r) = |
44 LocalTheory.define Thm.internalK |
|
45 ((R, syn), (Attrib.empty_binding, fold_rev lambda (params' @ zs) |
|
46 (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp) |
|
47 intrs' (list_comb (pred, zs)))))) #>> snd #>> snd |
|
48 end) (preds_syn ~~ preds ~~ Tss) lthy; |
|
49 |
|
50 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
|
51 |
|
52 |
|
53 (* proving the induction rules *) |
|
54 (* @chunk induction_rules *) |
|
55 val (Pnames, lthy3) = |
|
56 Variable.variant_fixes (replicate (length preds) "P") lthy2; |
|
57 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) |
|
58 (Pnames ~~ Tss); |
|
59 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
|
60 val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs; |
|
61 |
|
62 fun prove_indrule ((R, P), Ts) = |
|
63 let |
|
64 val (znames, lthy4) = |
|
65 Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
|
66 val zs = map Free (znames ~~ Ts) |
|
67 in |
|
68 Goal.prove lthy4 [] |
|
69 [HOLogic.mk_Trueprop (list_comb (R, zs))] |
|
70 (Logic.list_implies (intrs'', |
|
71 HOLogic.mk_Trueprop (list_comb (P, zs)))) |
|
72 (fn {prems, ...} => EVERY |
|
73 ([ObjectLogic.full_atomize_tac 1, |
|
74 cut_facts_tac prems 1, |
|
75 rewrite_goals_tac defs] @ |
|
76 map (fn ct => dtac (inst_spec ct) 1) cPs @ |
|
77 [assume_tac 1])) |> |
|
78 singleton (ProofContext.export lthy4 lthy1) |
|
79 end; |
|
80 |
|
81 val indrules = map prove_indrule (preds ~~ Ps ~~ Tss); |
|
82 (* @end *) |
|
83 |
|
84 (* proving the introduction rules *) |
|
85 (* @chunk intro_rules *) |
|
86 fun prove_intr (i, (_, r)) = |
|
87 Goal.prove lthy2 [] [] r |
63 Goal.prove lthy2 [] [] r |
88 (fn {prems, context = ctxt} => EVERY |
64 (fn {prems, context = ctxt} => EVERY |
89 [ObjectLogic.rulify_tac 1, |
65 [ObjectLogic.rulify_tac 1, |
90 rewrite_goals_tac defs, |
66 rewrite_goals_tac defs, |
91 REPEAT (resolve_tac [allI, impI] 1), |
67 REPEAT (resolve_tac [@{thm allI},@{thm impI}] 1), |
92 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
68 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
93 let |
69 let |
94 val (prems1, prems2) = |
70 val (prems1, prems2) = chop (length prems - length rules) prems; |
95 chop (length prems - length intrs) prems; |
71 val (params1, params2) = chop (length params - length preds') params; |
96 val (params1, params2) = |
|
97 chop (length params - length preds) params |
|
98 in |
72 in |
99 rtac (ObjectLogic.rulify |
73 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
100 (all_elims params1 (nth prems2 i))) 1 THEN |
74 THEN |
101 EVERY (map (fn prem => |
75 EVERY1 (map (fn prem => |
102 SUBPROOF (fn {prems = prems', concl, ...} => |
76 SUBPROOF (fn {prems = prems', concl, ...} => |
103 let |
77 let |
|
78 |
104 val prem' = prems' MRS prem; |
79 val prem' = prems' MRS prem; |
105 val prem'' = case prop_of prem' of |
80 val prem'' = case prop_of prem' of |
106 _ $ (Const (@{const_name All}, _) $ _) => |
81 _ $ (Const (@{const_name All}, _) $ _) => |
107 prem' |> all_elims params2 |> |
82 prem' |> all_elims params2 |
108 imp_elims prems2 |
83 |> imp_elims prems2 |
109 | _ => prem' |
84 | _ => prem'; |
110 in rtac prem'' 1 end) ctxt' 1) prems1) |
85 in rtac prem'' 1 end) ctxt') prems1) |
111 end) ctxt 1]) |> |
86 end) ctxt 1]) |> |
112 singleton (ProofContext.export lthy2 lthy1); |
87 singleton (ProofContext.export lthy2 lthy1) |
113 |
88 in |
114 val intr_ths = map_index prove_intr intrs; |
89 map_index prove_intro rules |
115 (* @end *) |
90 end |
116 |
|
117 (* storing the theorems *) |
|
118 (* @chunk storing *) |
|
119 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn); |
|
120 val case_names = map (Binding.base_name o fst o fst) intrs |
|
121 (* @end *) |
|
122 in |
|
123 lthy1 |> |
|
124 LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
|
125 ((Binding.qualify mut_name a, atts), [([th], [])])) |
|
126 (intrs ~~ intr_ths)) |-> |
|
127 (fn intr_thss => LocalTheory.note Thm.theoremK |
|
128 ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intr_thss)) |>> |
|
129 snd ||>> |
|
130 (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
|
131 ((Binding.qualify (Binding.base_name R) (Binding.name "induct"), |
|
132 [Attrib.internal (K (RuleCases.case_names case_names)), |
|
133 Attrib.internal (K (RuleCases.consumes 1)), |
|
134 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
|
135 (preds_syn ~~ indrules)) #>> maps snd) |
|
136 end; |
|
137 |
|
138 (* @chunk add_inductive *) |
|
139 fun add_inductive preds params specs lthy = |
|
140 let |
|
141 val ((vars, specs'), _) = Specification.read_specification (preds @ params) specs lthy; |
|
142 val (preds', params') = chop (length preds) vars; |
|
143 val specs'' = map (apsnd the_single) specs' |
|
144 val params'' = map fst params' |
|
145 in |
|
146 snd (add_inductive_i preds' params'' specs'' lthy) |
|
147 end; |
|
148 (* @end *) |
91 (* @end *) |
149 |
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 |
150 |
100 |
151 (* outer syntax *) |
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 |
|
117 (* @end *) |
|
118 |
|
119 (* @chunk add_inductive_i *) |
|
120 fun add_inductive_i preds params specs lthy = |
|
121 let |
|
122 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
|
123 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds; |
|
124 val Tss = map (binder_types o fastype_of) preds'; |
|
125 val (ass,rules) = split_list specs; |
|
126 |
|
127 val (defs, lthy1) = DEFINITION params' rules preds preds' Tss lthy |
|
128 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
|
129 |
|
130 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
|
131 |
|
132 val intros = INTROS rules preds' defs lthy1 lthy2 |
|
133 |
|
134 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds); |
|
135 val case_names = map (Binding.base_name o fst o fst) specs |
|
136 in |
|
137 lthy1 |
|
138 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
|
139 ((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
|
140 |-> (fn intross => LocalTheory.note Thm.theoremK |
|
141 ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intross)) |
|
142 |>> snd |
|
143 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
|
144 ((Binding.qualify (Binding.base_name R) (Binding.name "induct"), |
|
145 [Attrib.internal (K (RuleCases.case_names case_names)), |
|
146 Attrib.internal (K (RuleCases.consumes 1)), |
|
147 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
|
148 (preds ~~ inducts)) #>> maps snd) |
|
149 |> snd |
|
150 end |
|
151 (* @end *) |
|
152 |
|
153 (* @chunk add_inductive *) |
|
154 fun read_specification' vars specs lthy = |
|
155 let |
|
156 val specs' = map (fn (a, s) => [(a, [s])]) specs |
|
157 val ((varst, specst), _) = Specification.read_specification vars specs' lthy |
|
158 val specst' = map (apsnd the_single) specst |
|
159 in |
|
160 (varst, specst') |
|
161 end |
|
162 |
|
163 fun add_inductive preds params specs lthy = |
|
164 let |
|
165 val (vars, specs') = read_specification' (preds @ params) specs lthy; |
|
166 val (preds', params') = chop (length preds) vars; |
|
167 val params'' = map fst params' |
|
168 in |
|
169 add_inductive_i preds' params'' specs' lthy |
|
170 end; |
|
171 (* @end *) |
|
172 |
152 (* @chunk syntax *) |
173 (* @chunk syntax *) |
153 val parser = |
174 val parser = |
154 OuterParse.opt_target -- |
175 OuterParse.opt_target -- |
155 OuterParse.fixes -- |
176 OuterParse.fixes -- |
156 OuterParse.for_fixes -- |
177 OuterParse.for_fixes -- |
157 Scan.optional |
178 Scan.optional |
158 (OuterParse.$$$ "where" |-- |
179 (OuterParse.$$$ "where" |-- |
159 OuterParse.!!! |
180 OuterParse.!!! |
160 (OuterParse.enum1 "|" |
181 (OuterParse.enum1 "|" |
161 ((SpecParse.opt_thm_name ":" -- |
182 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] |
162 (OuterParse.prop >> single)) >> single))) [] |
|
163 |
|
164 |
183 |
165 val ind_decl = |
184 val ind_decl = |
166 parser >> |
185 parser >> |
167 (fn (((loc, preds), params), specs) => |
186 (fn (((loc, preds), params), specs) => |
168 Toplevel.local_theory loc (add_inductive preds params specs)); |
187 Toplevel.local_theory loc (add_inductive preds params specs)) |
169 |
188 |
170 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
189 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
171 OuterKeyword.thy_decl ind_decl; |
190 OuterKeyword.thy_decl ind_decl; |
172 (* @end *) |
191 (* @end *) |
173 |
192 |