32
|
1 |
(* @chunk SIMPLE_INDUCTIVE_PACKAGE *)
|
|
2 |
signature SIMPLE_INDUCTIVE_PACKAGE =
|
|
3 |
sig
|
|
4 |
val add_inductive_i:
|
76
|
5 |
((Binding.binding * typ) * mixfix) list -> (*{predicates}*)
|
|
6 |
(Binding.binding * typ) list -> (*{parameters}*)
|
121
|
7 |
(Attrib.binding * term) list -> (*{rules}*)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
local_theory -> local_theory
|
116
|
9 |
|
32
|
10 |
val add_inductive:
|
76
|
11 |
(Binding.binding * string option * mixfix) list -> (*{predicates}*)
|
|
12 |
(Binding.binding * string option * mixfix) list -> (*{parameters}*)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
(Attrib.binding * string) list -> (*{rules}*)
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
local_theory -> local_theory
|
32
|
15 |
end;
|
|
16 |
(* @end *)
|
|
17 |
|
|
18 |
structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
|
|
19 |
struct
|
|
20 |
|
164
|
21 |
(* @chunk make_definitions *)
|
|
22 |
fun make_defs ((binding, syn), trm) lthy =
|
111
|
23 |
let
|
514
|
24 |
val arg = ((binding, syn), ((Binding.suffix_name "_def" binding, []), trm))
|
401
|
25 |
val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy
|
111
|
26 |
in
|
|
27 |
(thm, lthy)
|
|
28 |
end
|
118
|
29 |
(* @end *)
|
111
|
30 |
|
164
|
31 |
(* @chunk definitions_aux *)
|
|
32 |
fun defs_aux lthy orules preds params (pred, arg_types) =
|
|
33 |
let
|
|
34 |
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
|
|
35 |
|
|
36 |
val fresh_args =
|
|
37 |
arg_types
|
|
38 |
|> map (pair "z")
|
|
39 |
|> Variable.variant_frees lthy orules
|
|
40 |
|> map Free
|
|
41 |
in
|
|
42 |
list_comb (pred, fresh_args)
|
|
43 |
|> fold_rev (curry HOLogic.mk_imp) orules
|
|
44 |
|> fold_rev mk_all preds
|
|
45 |
|> fold_rev lambda (params @ fresh_args)
|
|
46 |
end
|
|
47 |
(* @end *)
|
|
48 |
|
118
|
49 |
(* @chunk definitions *)
|
164
|
50 |
fun definitions rules params preds prednames syns arg_typess lthy =
|
111
|
51 |
let
|
562
|
52 |
val orules = map (Object_Logic.atomize_term lthy) rules
|
164
|
53 |
val defs =
|
|
54 |
map (defs_aux lthy orules preds params) (preds ~~ arg_typess)
|
111
|
55 |
in
|
164
|
56 |
fold_map make_defs (prednames ~~ syns ~~ defs) lthy
|
111
|
57 |
end
|
|
58 |
(* @end *)
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
fun inst_spec ct =
|
562
|
61 |
Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec};
|
|
62 |
|
|
63 |
fun dtac ctxt thm = dresolve_tac ctxt [thm]
|
|
64 |
fun rtac ctxt thm = resolve_tac ctxt [thm]
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
|
164
|
66 |
(* @chunk induction_tac *)
|
552
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
fun induction_tac ctxt defs prems insts =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
EVERY1 [Object_Logic.full_atomize_tac ctxt,
|
164
|
69 |
cut_facts_tac prems,
|
552
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
rewrite_goal_tac ctxt defs,
|
562
|
71 |
EVERY' (map (dtac ctxt o inst_spec) insts),
|
|
72 |
assume_tac ctxt]
|
164
|
73 |
(* @end *)
|
|
74 |
|
|
75 |
(* @chunk induction_rules *)
|
|
76 |
fun inductions rules defs parnames preds Tss lthy1 =
|
|
77 |
let
|
|
78 |
val (_, lthy2) = Variable.add_fixes parnames lthy1
|
|
79 |
|
|
80 |
val Ps = replicate (length preds) "P"
|
|
81 |
val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2
|
562
|
82 |
|
164
|
83 |
val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
|
|
84 |
val newpreds = map Free (newprednames ~~ Tss')
|
562
|
85 |
val cnewpreds = map (Thm.cterm_of lthy3) newpreds
|
164
|
86 |
val rules' = map (subst_free (preds ~~ newpreds)) rules
|
|
87 |
|
|
88 |
fun prove_induction ((pred, newpred), Ts) =
|
|
89 |
let
|
|
90 |
val (newargnames, lthy4) =
|
|
91 |
Variable.variant_fixes (replicate (length Ts) "z") lthy3;
|
|
92 |
val newargs = map Free (newargnames ~~ Ts)
|
|
93 |
|
|
94 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
|
|
95 |
val goal = Logic.list_implies
|
|
96 |
(rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
|
|
97 |
in
|
|
98 |
Goal.prove lthy4 [] [prem] goal
|
552
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
(fn {prems, context, ...} => induction_tac context defs prems cnewpreds)
|
475
|
100 |
|> singleton (Proof_Context.export lthy4 lthy1)
|
164
|
101 |
end
|
|
102 |
in
|
|
103 |
map prove_induction (preds ~~ newpreds ~~ Tss)
|
|
104 |
end
|
|
105 |
(* @end *)
|
|
106 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp});
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
|
111
|
110 |
|
164
|
111 |
(* @chunk subproof1 *)
|
|
112 |
fun subproof2 prem params2 prems2 =
|
562
|
113 |
SUBPROOF (fn {prems, context, ...} =>
|
124
|
114 |
let
|
164
|
115 |
val prem' = prems MRS prem;
|
|
116 |
val prem'' =
|
562
|
117 |
case Thm.prop_of prem' of
|
164
|
118 |
_ $ (Const (@{const_name All}, _) $ _) =>
|
|
119 |
prem' |> all_elims params2
|
|
120 |
|> imp_elims prems2
|
|
121 |
| _ => prem';
|
|
122 |
in
|
562
|
123 |
rtac context prem'' 1
|
164
|
124 |
end)
|
|
125 |
(* @end *)
|
32
|
126 |
|
164
|
127 |
(* @chunk subproof2 *)
|
|
128 |
fun subproof1 rules preds i =
|
|
129 |
SUBPROOF (fn {params, prems, context = ctxt', ...} =>
|
|
130 |
let
|
|
131 |
val (prems1, prems2) = chop (length prems - length rules) prems;
|
294
|
132 |
val (params1, params2) = chop (length params - length preds) (map snd params);
|
124
|
133 |
in
|
562
|
134 |
rtac ctxt' (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1
|
164
|
135 |
THEN
|
|
136 |
EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
|
|
137 |
end)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
138 |
(* @end *)
|
32
|
139 |
|
165
|
140 |
fun introductions_tac defs rules preds i ctxt =
|
552
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
EVERY1 [Object_Logic.rulify_tac ctxt,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
rewrite_goal_tac ctxt defs,
|
562
|
143 |
REPEAT o (resolve_tac ctxt [@{thm allI},@{thm impI}]),
|
165
|
144 |
subproof1 rules preds i ctxt]
|
|
145 |
|
|
146 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
(* @chunk intro_rules *)
|
165
|
148 |
fun introductions rules parnames preds defs lthy1 =
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
let
|
164
|
150 |
val (_, lthy2) = Variable.add_fixes parnames lthy1
|
|
151 |
|
|
152 |
fun prove_intro (i, goal) =
|
|
153 |
Goal.prove lthy2 [] [] goal
|
165
|
154 |
(fn {context, ...} => introductions_tac defs rules preds i context)
|
475
|
155 |
|> singleton (Proof_Context.export lthy2 lthy1)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
in
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
157 |
map_index prove_intro rules
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
158 |
end
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
159 |
(* @end *)
|
32
|
160 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
(* @chunk add_inductive_i *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
fun add_inductive_i preds params specs lthy =
|
124
|
163 |
let
|
159
|
164 |
val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params;
|
|
165 |
val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds;
|
124
|
166 |
val Tss = map (binder_types o fastype_of) preds';
|
165
|
167 |
val (ass, rules) = split_list specs; (* FIXME: ass not used? *)
|
32
|
168 |
|
164
|
169 |
val prednames = map (fst o fst) preds
|
|
170 |
val syns = map snd preds
|
|
171 |
val parnames = map (Binding.name_of o fst) params
|
|
172 |
|
|
173 |
val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy;
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
174 |
|
164
|
175 |
val inducts = inductions rules defs parnames preds' Tss lthy1
|
|
176 |
|
165
|
177 |
val intros = introductions rules parnames preds' defs lthy1
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
|
159
|
179 |
val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds);
|
|
180 |
val case_names = map (Binding.name_of o fst o fst) specs
|
124
|
181 |
in
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
182 |
lthy1
|
394
|
183 |
|> Local_Theory.notes (map (fn (((a, atts), _), th) =>
|
159
|
184 |
((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros))
|
394
|
185 |
|-> (fn intross => Local_Theory.note
|
159
|
186 |
((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross))
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
|>> snd
|
394
|
188 |
||>> (Local_Theory.notes (map (fn (((R, _), _), th) =>
|
159
|
189 |
((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
|
375
|
190 |
[Attrib.internal (K (Rule_Cases.case_names case_names)),
|
|
191 |
Attrib.internal (K (Rule_Cases.consumes 1)),
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
192 |
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
193 |
(preds ~~ inducts)) #>> maps snd)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
|> snd
|
124
|
195 |
end
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
196 |
(* @end *)
|
562
|
197 |
val _ = Proof_Context.read_stmt
|
120
|
198 |
(* @chunk read_specification *)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
199 |
fun read_specification' vars specs lthy =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
200 |
let
|
562
|
201 |
val specs' = map (fn (a, s) => ((a, s), [],[])) specs
|
|
202 |
val ((varst, specst),_) =
|
|
203 |
Specification.read_multi_specs vars specs' lthy
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
204 |
in
|
562
|
205 |
(varst, specst)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
206 |
end
|
120
|
207 |
(* @end *)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
208 |
|
120
|
209 |
(* @chunk add_inductive *)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
210 |
fun add_inductive preds params specs lthy =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
211 |
let
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
212 |
val (vars, specs') = read_specification' (preds @ params) specs lthy;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
213 |
val (preds', params') = chop (length preds) vars;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
214 |
val params'' = map fst params'
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
in
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
add_inductive_i preds' params'' specs' lthy
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
end;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
218 |
(* @end *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
219 |
|
116
|
220 |
(* @chunk parser *)
|
120
|
221 |
val spec_parser =
|
426
|
222 |
Parse.opt_target --
|
562
|
223 |
Parse.vars --
|
426
|
224 |
Parse.for_fixes --
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
225 |
Scan.optional
|
426
|
226 |
(Parse.$$$ "where" |--
|
|
227 |
Parse.!!!
|
|
228 |
(Parse.enum1 "|"
|
|
229 |
(Parse_Spec.opt_thm_name ":" -- Parse.prop))) []
|
116
|
230 |
(* @end *)
|
32
|
231 |
|
116
|
232 |
(* @chunk syntax *)
|
129
|
233 |
val specification =
|
120
|
234 |
spec_parser >>
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
235 |
(fn (((loc, preds), params), specs) =>
|
562
|
236 |
Toplevel.local_theory NONE loc (add_inductive preds params specs))
|
32
|
237 |
|
562
|
238 |
val _ = Outer_Syntax.command @{command_keyword "simple_inductive"} "define inductive predicates"
|
514
|
239 |
specification
|
562
|
240 |
|
32
|
241 |
(* @end *)
|
|
242 |
|
|
243 |
end;
|