380 |
380 |
381 val inject_thms = flat (map #inject dtinfos); |
381 val inject_thms = flat (map #inject dtinfos); |
382 val distinct_thms = flat (map #distinct dtinfos); |
382 val distinct_thms = flat (map #distinct dtinfos); |
383 val rel_dtinfos = List.take (dtinfos, (length dts)); |
383 val rel_dtinfos = List.take (dtinfos, (length dts)); |
384 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
384 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
385 val induct_thms = #induct dtinfo; |
385 val induct_thm = #induct dtinfo; |
386 val exhaust_thms = map #exhaust dtinfos; |
386 val exhaust_thms = map #exhaust dtinfos; |
387 |
387 |
388 (* definitions of raw permutations *) |
388 (* definitions of raw permutations *) |
389 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
389 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
390 if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts (length dts)) lthy1 |
390 if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
391 else raise TEST lthy1 |
391 else raise TEST lthy1 |
392 |
392 |
393 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
393 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
394 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
394 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
395 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
395 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
403 |
403 |
404 (* definition of raw fv_functions *) |
404 (* definition of raw fv_functions *) |
405 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
405 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
406 val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls) |
406 val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls) |
407 val ((fv, fvbn), fv_def, lthy3a) = |
407 val ((fv, fvbn), fv_def, lthy3a) = |
408 if STEPS > 3 then define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3 |
408 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
409 else raise TEST lthy3 |
409 else raise TEST lthy3 |
410 |
410 |
411 |
411 |
412 (* definition of raw alphas *) |
412 (* definition of raw alphas *) |
413 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
413 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
430 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
430 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
431 val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); |
431 val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); |
432 |
432 |
433 (* proving equivariance lemmas *) |
433 (* proving equivariance lemmas *) |
434 val _ = warning "Proving equivariance"; |
434 val _ = warning "Proving equivariance"; |
435 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thms (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
435 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
436 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thms (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
436 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
437 fun alpha_eqvt_tac' _ = |
437 fun alpha_eqvt_tac' _ = |
438 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
438 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
439 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1 |
439 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1 |
440 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
440 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
441 |
441 |
442 (* proving alpha equivalence *) |
442 (* proving alpha equivalence *) |
443 val _ = warning "Proving equivalence"; |
443 val _ = warning "Proving equivalence"; |
444 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
444 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
445 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thms alpha_eq_iff_simp lthy6; |
445 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6; |
446 val alpha_equivp = |
446 val alpha_equivp = |
447 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts |
447 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts |
448 else build_equivps alpha_ts reflps alpha_induct |
448 else build_equivps alpha_ts reflps alpha_induct |
449 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6; |
449 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6; |
450 val qty_binds = map (fn (_, b, _, _) => b) dts; |
450 val qty_binds = map (fn (_, b, _, _) => b) dts; |
499 val lthy13 = Theory_Target.init NONE thy'; |
499 val lthy13 = Theory_Target.init NONE thy'; |
500 val q_name = space_implode "_" qty_names; |
500 val q_name = space_implode "_" qty_names; |
501 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
501 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
502 val _ = warning "Lifting induction"; |
502 val _ = warning "Lifting induction"; |
503 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
503 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
504 val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thms); |
504 val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm); |
505 fun note_suffix s th ctxt = |
505 fun note_suffix s th ctxt = |
506 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
506 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
507 fun note_simp_suffix s th ctxt = |
507 fun note_simp_suffix s th ctxt = |
508 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
508 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
509 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
509 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |