339 val thy = Local_Theory.exit_global lthy2a; |
339 val thy = Local_Theory.exit_global lthy2a; |
340 val thy_name = Context.theory_name thy |
340 val thy_name = Context.theory_name thy |
341 |
341 |
342 (* definition of raw fv_functions *) |
342 (* definition of raw fv_functions *) |
343 val _ = warning "Definition of raw fv-functions"; |
343 val _ = warning "Definition of raw fv-functions"; |
344 val lthy3 = Theory_Target.init NONE thy; |
344 val lthy3 = Named_Target.init NONE thy; |
345 |
345 |
346 val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
346 val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
347 if get_STEPS lthy3 > 2 |
347 if get_STEPS lthy3 > 2 |
348 then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
348 then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
349 else raise TEST lthy3 |
349 else raise TEST lthy3 |
575 val thy = Local_Theory.exit_global lthy12c; |
575 val thy = Local_Theory.exit_global lthy12c; |
576 val perm_names = map (fn x => "permute_" ^ x) qty_names |
576 val perm_names = map (fn x => "permute_" ^ x) qty_names |
577 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
577 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
578 (* use Local_Theory.theory_result *) |
578 (* use Local_Theory.theory_result *) |
579 val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy; |
579 val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy; |
580 val lthy13 = Theory_Target.init NONE thy'; |
580 val lthy13 = Named_Target.init NONE thy'; |
581 |
581 |
582 val q_name = space_implode "_" qty_names; |
582 val q_name = space_implode "_" qty_names; |
583 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
583 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
584 val _ = warning "Lifting induction"; |
584 val _ = warning "Lifting induction"; |
585 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; |
585 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; |
616 val _ = warning "Supports"; |
616 val _ = warning "Supports"; |
617 val supports = map (prove_supports lthy20 q_perm) qconstrs; |
617 val supports = map (prove_supports lthy20 q_perm) qconstrs; |
618 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
618 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
619 val thy3 = Local_Theory.exit_global lthy20; |
619 val thy3 = Local_Theory.exit_global lthy20; |
620 val _ = warning "Instantiating FS"; |
620 val _ = warning "Instantiating FS"; |
621 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
621 val lthy21 = Class.instantiation (qty_full_names, [], @{sort fs}) thy3; |
622 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
622 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
623 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
623 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
624 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos; |
624 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos; |
625 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
625 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
626 val _ = warning "Support Equations"; |
626 val _ = warning "Support Equations"; |