316 flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) |
316 flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) |
317 val all_raw_tys = all_dtyps descr sorts |
317 val all_raw_tys = all_dtyps descr sorts |
318 val all_raw_ty_names = map (fst o dest_Type) all_raw_tys |
318 val all_raw_ty_names = map (fst o dest_Type) all_raw_tys |
319 |
319 |
320 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names |
320 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names |
321 val inject_thms = flat (map #inject dtinfos); |
321 val inject_thms = flat (map #inject dtinfos) |
322 val distinct_thms = flat (map #distinct dtinfos); |
322 val distinct_thms = flat (map #distinct dtinfos) |
323 val constr_thms = inject_thms @ distinct_thms |
323 val constr_thms = inject_thms @ distinct_thms |
324 val rel_dtinfos = List.take (dtinfos, (length dts)); |
324 |
325 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
|
326 val raw_induct_thm = #induct dtinfo; |
325 val raw_induct_thm = #induct dtinfo; |
327 val raw_induct_thms = #inducts dtinfo; |
326 val raw_induct_thms = #inducts dtinfo; |
328 val exhaust_thms = map #exhaust dtinfos; |
327 val exhaust_thms = map #exhaust dtinfos; |
329 val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys |
328 val raw_size_trms = map size_const all_raw_tys |
330 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
329 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
331 |> `(fn thms => (length thms) div 2) |
330 |> `(fn thms => (length thms) div 2) |
332 |> uncurry drop |
331 |> uncurry drop |
333 |
332 |
334 |
|
335 (* definitions of raw permutations *) |
333 (* definitions of raw permutations *) |
336 val _ = warning "Definition of raw permutations"; |
334 val _ = warning "Definition of raw permutations"; |
337 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = |
335 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = |
338 if get_STEPS lthy0 > 1 |
336 if get_STEPS lthy0 > 1 |
339 then Local_Theory.theory_result |
337 then Local_Theory.theory_result |
364 else raise TEST lthy3b |
362 else raise TEST lthy3b |
365 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
363 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
366 |
364 |
367 (* definition of alpha-distinct lemmas *) |
365 (* definition of alpha-distinct lemmas *) |
368 val _ = warning "Distinct theorems"; |
366 val _ = warning "Distinct theorems"; |
369 val (alpha_distincts, alpha_bn_distincts) = |
367 val alpha_distincts = |
370 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
368 mk_alpha_distincts lthy4 alpha_cases distinct_thms alpha_trms all_raw_tys |
371 |
369 |
372 (* definition of alpha_eq_iff lemmas *) |
370 (* definition of alpha_eq_iff lemmas *) |
373 (* they have a funny shape for the simplifier *) |
371 (* they have a funny shape for the simplifier *) |
374 val _ = warning "Eq-iff theorems"; |
372 val _ = warning "Eq-iff theorems"; |
375 val (alpha_eq_iff_simps, alpha_eq_iff) = |
373 val (alpha_eq_iff_simps, alpha_eq_iff) = |
561 val fv_rsp = flat (map snd fv_rsp_pre); |
559 val fv_rsp = flat (map snd fv_rsp_pre); |
562 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
560 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
563 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
561 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
564 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
562 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
565 else |
563 else |
566 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
564 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
567 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
565 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
568 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
566 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
569 fun const_rsp_tac _ = |
567 fun const_rsp_tac _ = |
570 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
568 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
571 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
569 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |