8 signature NOMINAL_DT_ALPHA = |
8 signature NOMINAL_DT_ALPHA = |
9 sig |
9 sig |
10 val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
10 val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
11 bclause list list list -> term list -> Proof.context -> |
11 bclause list list list -> term list -> Proof.context -> |
12 term list * term list * thm list * thm list * thm * local_theory |
12 term list * term list * thm list * thm list * thm * local_theory |
|
13 |
|
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
|
15 term list -> term list -> bn_info -> thm list * thm list |
|
16 |
|
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list |
13 end |
18 end |
14 |
19 |
15 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
20 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
16 struct |
21 struct |
|
22 |
|
23 (** definition of the inductive rules for alpha and alpha_bn **) |
17 |
24 |
18 (* construct the compound terms for prod_fv and prod_alpha *) |
25 (* construct the compound terms for prod_fv and prod_alpha *) |
19 fun mk_prod_fv (t1, t2) = |
26 fun mk_prod_fv (t1, t2) = |
20 let |
27 let |
21 val ty1 = fastype_of t1 |
28 val ty1 = fastype_of t1 |
214 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
221 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
215 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
222 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
216 |
223 |
217 val (alphas, lthy') = Inductive.add_inductive_i |
224 val (alphas, lthy') = Inductive.add_inductive_i |
218 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
225 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
219 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
226 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
220 all_alpha_names [] all_alpha_intros [] lthy |
227 all_alpha_names [] all_alpha_intros [] lthy |
221 |
228 |
222 val all_alpha_trms_loc = #preds alphas; |
229 val all_alpha_trms_loc = #preds alphas; |
223 val alpha_induct_loc = #raw_induct alphas; |
230 val alpha_induct_loc = #raw_induct alphas; |
224 val alpha_intros_loc = #intrs alphas; |
231 val alpha_intros_loc = #intrs alphas; |
233 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms |
240 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms |
234 in |
241 in |
235 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
242 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
236 end |
243 end |
237 |
244 |
|
245 |
|
246 (** produces the distinctness theorems **) |
|
247 |
|
248 (* transforms the distinctness theorems of the constructors |
|
249 to "not-alphas" of the constructors *) |
|
250 fun mk_alpha_distinct_goal alpha neq = |
|
251 let |
|
252 val (lhs, rhs) = |
|
253 neq |
|
254 |> HOLogic.dest_Trueprop |
|
255 |> HOLogic.dest_not |
|
256 |> HOLogic.dest_eq |
|
257 in |
|
258 alpha $ lhs $ rhs |
|
259 |> HOLogic.mk_not |
|
260 |> HOLogic.mk_Trueprop |
|
261 end |
|
262 |
|
263 fun distinct_tac cases distinct_thms = |
|
264 rtac notI THEN' eresolve_tac cases |
|
265 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
|
266 |
|
267 fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) = |
|
268 let |
|
269 val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt |
|
270 val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms |
|
271 val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals |
|
272 in |
|
273 Variable.export ctxt' ctxt nrels |
|
274 end |
|
275 |
|
276 fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos = |
|
277 let |
|
278 val alpha_distincts = |
|
279 map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms) |
|
280 val distinc_thms = map |
|
281 val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos |
|
282 val alpha_bn_distincts = |
|
283 map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms) |
|
284 in |
|
285 (flat alpha_distincts, flat alpha_bn_distincts) |
|
286 end |
|
287 |
|
288 |
|
289 (** produces the alpha_eq_iff simplification rules **) |
|
290 |
|
291 (* in case a theorem is of the form (C.. = C..), it will be |
|
292 rewritten to ((C.. = C..) = True) *) |
|
293 fun mk_simp_rule thm = |
|
294 case (prop_of thm) of |
|
295 @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm] |
|
296 | _ => thm |
|
297 |
|
298 fun alpha_eq_iff_tac dist_inj intros elims = |
|
299 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' |
|
300 (rtac @{thm iffI} THEN' |
|
301 RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj), |
|
302 asm_full_simp_tac (HOL_ss addsimps intros)]) |
|
303 |
|
304 fun mk_alpha_eq_iff_goal thm = |
|
305 let |
|
306 val prop = prop_of thm; |
|
307 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
|
308 val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); |
|
309 fun list_conj l = foldr1 HOLogic.mk_conj l; |
|
310 in |
|
311 if hyps = [] then HOLogic.mk_Trueprop concl |
|
312 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
|
313 end; |
|
314 |
|
315 fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = |
|
316 let |
|
317 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
|
318 val goals = map mk_alpha_eq_iff_goal thms_imp; |
|
319 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
|
320 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
|
321 in |
|
322 Variable.export ctxt' ctxt thms |
|
323 |> map mk_simp_rule |
|
324 end |
|
325 |
238 end (* structure *) |
326 end (* structure *) |
239 |
327 |