304 val inducts = #inducts dtinfo; |
304 val inducts = #inducts dtinfo; |
305 val _ = tracing "Defining permutations, fv and alpha"; |
305 val _ = tracing "Defining permutations, fv and alpha"; |
306 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
306 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
307 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
307 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
308 val raw_binds_flat = map (map flat) raw_binds; |
308 val raw_binds_flat = map (map flat) raw_binds; |
309 val (((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
309 val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
310 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
310 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
311 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
311 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
312 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
312 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
313 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
313 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
314 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
314 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
323 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 |
323 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 |
324 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5; |
324 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5; |
325 val (fv_bn_eqvts, lthy6a) = |
325 val (fv_bn_eqvts, lthy6a) = |
326 if fv_ts_bn = [] then ([], lthy6) else |
326 if fv_ts_bn = [] then ([], lthy6) else |
327 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts) |
327 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts) |
328 (fv_ts_bn ~~ (map snd bns)) lthy6; |
328 (fv_ts_bn ~~ bn_nos) lthy6; |
329 val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts) |
329 val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts) |
330 fun alpha_eqvt_tac' _ = |
330 fun alpha_eqvt_tac' _ = |
331 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
331 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
332 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
332 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
333 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
333 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
363 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
363 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
364 fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
364 fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
365 else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1 |
365 else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1 |
366 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
366 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
367 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
367 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
368 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
368 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
369 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
369 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
|
370 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
370 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
371 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
371 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
372 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
372 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
373 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
373 val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
374 val (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
374 val _ = tracing "Lifting permutations"; |
375 val _ = tracing "Lifting permutations"; |
375 val thy = Local_Theory.exit_global lthy12c; |
376 val thy = Local_Theory.exit_global lthy12c; |
376 val perm_names = map (fn x => "permute_" ^ x) qty_names |
377 val perm_names = map (fn x => "permute_" ^ x) qty_names |
377 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
378 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
378 val lthy13 = Theory_Target.init NONE thy'; |
379 val lthy13 = Theory_Target.init NONE thy'; |
379 val q_name = space_implode "_" qty_names; |
380 val q_name = space_implode "_" qty_names; |
380 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
381 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
381 val _ = tracing "Lifting induction"; |
382 val _ = tracing "Lifting induction"; |
382 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
383 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
383 val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct); |
384 val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct); |
|
385 fun note_suffix s th ctxt = |
|
386 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
384 fun note_simp_suffix s th ctxt = |
387 fun note_simp_suffix s th ctxt = |
385 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
388 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
386 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
389 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
387 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
390 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
388 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
391 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
411 val supports = map (prove_supports lthy20 q_perm) consts; |
414 val supports = map (prove_supports lthy20 q_perm) consts; |
412 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys); |
415 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys); |
413 val thy3 = Local_Theory.exit_global lthy20; |
416 val thy3 = Local_Theory.exit_global lthy20; |
414 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
417 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
415 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
418 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
416 val lthy22 = Class.prove_instantiation_instance tac lthy21 handle _ => lthy20 |
419 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
417 in |
420 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
418 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy22) |
421 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
|
422 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; |
|
423 val lthy23 = note_suffix "supp" q_supp lthy22; |
|
424 in |
|
425 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy23) |
419 end |
426 end |
420 *} |
427 *} |
421 |
428 |
422 |
429 |
423 ML {* |
430 ML {* |