387 val lhs_arg = foldr1 HOLogic.mk_prod bound_args |
387 val lhs_arg = foldr1 HOLogic.mk_prod bound_args |
388 val lhs = mk_pair (lhs_binds, lhs_arg); |
388 val lhs = mk_pair (lhs_binds, lhs_arg); |
389 val rhs_binds = fv_binds args2 rbinds; |
389 val rhs_binds = fv_binds args2 rbinds; |
390 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2; |
390 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2; |
391 val rhs = mk_pair (rhs_binds, rhs_arg); |
391 val rhs = mk_pair (rhs_binds, rhs_arg); |
392 val _ = tracing (PolyML.makestring bound_in_ty_nos); |
|
393 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); |
392 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); |
394 val _ = tracing (PolyML.makestring fvs); |
|
395 val fv = mk_compound_fv fvs; |
393 val fv = mk_compound_fv fvs; |
396 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); |
394 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); |
397 val _ = tracing (PolyML.makestring alphas); |
|
398 val alpha = mk_compound_alpha alphas; |
395 val alpha = mk_compound_alpha alphas; |
399 val pi = foldr1 add_perm (distinct (op =) rpis); |
396 val pi = foldr1 add_perm (distinct (op =) rpis); |
400 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
397 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
401 val _ = tracing (PolyML.makestring alpha_gen_pre); |
|
402 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
398 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
403 in |
399 in |
404 alpha_gen |
400 alpha_gen |
405 end |
401 end |
406 else |
402 else |
447 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
443 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
448 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
444 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
449 val fv_names_all = fv_names_fst @ fv_bn_names; |
445 val fv_names_all = fv_names_fst @ fv_bn_names; |
450 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
446 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
451 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
447 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
452 (* val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*) |
|
453 val (fvs, lthy') = (Primrec.add_primrec |
448 val (fvs, lthy') = (Primrec.add_primrec |
454 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
449 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
455 val (fvs2, lthy'') = |
450 val (fvs2, lthy'') = |
456 if fv_eqs_snd = [] then (([], []), lthy') else |
451 if fv_eqs_snd = [] then (([], []), lthy') else |
457 (Primrec.add_primrec |
452 (Primrec.add_primrec |
594 rtac induct THEN_ALL_NEW |
589 rtac induct THEN_ALL_NEW |
595 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW |
590 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW |
596 split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
591 split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
597 THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
592 THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
598 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
593 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
599 add_0_left supp_zero_perm Int_empty_left}) |
594 add_0_left supp_zero_perm Int_empty_left split_conv}) |
600 *} |
595 *} |
601 |
596 |
602 |
597 |
603 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
598 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
604 apply (erule exE) |
599 apply (erule exE) |