Nominal/Fv.thy
changeset 1486 f86710d35146
parent 1482 a98c15866300
child 1487 b55b78e63913
equal deleted inserted replaced
1485:c004e7448dca 1486:f86710d35146
   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)