216 |
216 |
217 (* noting the raw permutations as eqvt theorems *) |
217 (* noting the raw permutations as eqvt theorems *) |
218 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
218 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
219 |
219 |
220 val _ = trace_msg (K "Defining raw fv- and bn-functions...") |
220 val _ = trace_msg (K "Defining raw fv- and bn-functions...") |
221 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
221 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) = |
222 define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs |
222 define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs |
223 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
223 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
224 |
224 |
225 (* defining the permute_bn functions *) |
225 (* defining the permute_bn functions *) |
226 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
226 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
233 |
233 |
234 val _ = trace_msg (K "Defining alpha relations...") |
234 val _ = trace_msg (K "Defining alpha relations...") |
235 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
235 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
236 define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
236 define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
237 |
237 |
|
238 val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct)) |
|
239 val _ = tracing ("alpha_intros\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_intros)) |
|
240 |
238 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
241 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
239 |
242 |
240 val _ = trace_msg (K "Proving distinct theorems...") |
243 val _ = trace_msg (K "Proving distinct theorems...") |
241 val alpha_distincts = |
244 val alpha_distincts = |
242 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names |
245 raw_prove_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names |
243 |
246 |
244 val _ = trace_msg (K "Proving eq-iff theorems...") |
247 val _ = trace_msg (K "Proving eq-iff theorems...") |
245 val alpha_eq_iff = |
248 val alpha_eq_iff = |
246 mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
249 raw_prove_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
247 |
250 |
248 val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") |
251 val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") |
249 val raw_bn_eqvt = |
252 val raw_bn_eqvt = |
250 raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4 |
253 raw_prove_eqvt raw_bns raw_bn_inducts (raw_bn_defs @ raw_perm_simps) lthy4 |
251 |
254 |
252 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) |
255 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) |
253 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4) |
256 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4) |
254 |
257 |
255 val raw_fv_eqvt = |
258 val raw_fv_eqvt = |
285 alpha_trans_thms lthy5 |
288 alpha_trans_thms lthy5 |
286 |
289 |
287 val _ = trace_msg (K "Proving alpha implies bn...") |
290 val _ = trace_msg (K "Proving alpha implies bn...") |
288 val alpha_bn_imp_thms = |
291 val alpha_bn_imp_thms = |
289 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
292 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
|
293 |
|
294 val _ = tracing ("alpha_bn_imp_thms:\n" ^ cat_lines (map (Syntax.string_of_term lthy5 o prop_of) alpha_bn_imp_thms)) |
290 |
295 |
291 val _ = trace_msg (K "Proving respectfulness...") |
296 val _ = trace_msg (K "Proving respectfulness...") |
292 val raw_funs_rsp_aux = |
297 val raw_funs_rsp_aux = |
293 raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
298 raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
294 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 |
299 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 |
379 |
384 |
380 val _ = trace_msg (K "Lifting of theorems...") |
385 val _ = trace_msg (K "Lifting of theorems...") |
381 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
386 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
382 prod.cases} |
387 prod.cases} |
383 |
388 |
384 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
389 val (((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), qbn_inducts), |
|
390 lthyA) = |
385 lthy9a |
391 lthy9a |
386 |> lift_thms qtys [] alpha_distincts |
392 |> lift_thms qtys [] alpha_distincts |
387 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
393 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
388 ||>> lift_thms qtys [] raw_fv_defs |
394 ||>> lift_thms qtys [] raw_fv_defs |
389 ||>> lift_thms qtys [] raw_bn_defs |
395 ||>> lift_thms qtys [] raw_bn_defs |
390 ||>> lift_thms qtys [] raw_perm_simps |
396 ||>> lift_thms qtys [] raw_perm_simps |
391 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
397 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
|
398 ||>> lift_thms qtys [] raw_bn_inducts |
392 |
399 |
393 val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = |
400 val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = |
394 lthyA |
401 lthyA |
395 |> lift_thms qtys [] raw_size_eqvt |
402 |> lift_thms qtys [] raw_size_eqvt |
396 ||>> lift_thms qtys [] [raw_induct_thm] |
403 ||>> lift_thms qtys [] [raw_induct_thm] |
397 ||>> lift_thms qtys [] raw_exhaust_thms |
404 ||>> lift_thms qtys [] raw_exhaust_thms |
398 ||>> lift_thms qtys [] raw_size_thms |
405 ||>> lift_thms qtys [] raw_size_thms |
399 ||>> lift_thms qtys [] raw_perm_bn_simps |
406 ||>> lift_thms qtys [] raw_perm_bn_simps |
400 ||>> lift_thms qtys [] alpha_refl_thms |
407 ||>> lift_thms qtys [] alpha_refl_thms |
401 |
408 |
402 val qinducts = Project_Rule.projections lthyA qinduct |
409 val qinducts = Project_Rule.projections lthyB qinduct |
403 |
410 |
404 val _ = trace_msg (K "Proving supp lemmas and fs-instances...") |
411 val _ = trace_msg (K "Proving supp lemmas and fs-instances...") |
405 val qsupports_thms = |
412 val qsupports_thms = |
406 prove_supports lthyB qperm_simps (flat qtrms) |
413 prove_supports lthyB qperm_simps (flat qtrms) |
407 |
414 |
468 |> Local_Theory.declaration false (K (fold register_info infos)) |
475 |> Local_Theory.declaration false (K (fold register_info infos)) |
469 |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) |
476 |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) |
470 ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs') |
477 ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs') |
471 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
478 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
472 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
479 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
|
480 ||>> Local_Theory.note ((thms_suffix "bn_inducts", []), qbn_inducts) |
473 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
481 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
474 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
482 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", [eqvt_attr]), qfv_qbn_eqvts) |
475 ||>> Local_Theory.note ((thms_suffix "size", [simp_attr]), qsize_simps) |
483 ||>> Local_Theory.note ((thms_suffix "size", [simp_attr]), qsize_simps) |
476 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
484 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
477 ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) |
485 ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) |
478 ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts) |
486 ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts) |
479 ||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts) |
487 ||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts) |