src/HOL/Nominal/nominal_atoms.ML
changeset 46180 72ee700e1d8f
parent 45979 296d9a9c8d24
child 46961 5c6955f487e5
equal deleted inserted replaced
46179:47bcf3d5d1f0 46180:72ee700e1d8f
   540           fun pt_proof thm = 
   540           fun pt_proof thm = 
   541               EVERY [Class.intro_classes_tac [],
   541               EVERY [Class.intro_classes_tac [],
   542                      rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
   542                      rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
   543 
   543 
   544           val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
   544           val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
   545           val pt_thm_set   = at_thm RS (pt_inst RS pt_set_inst);
   545           val pt_thm_set   = pt_inst RS pt_set_inst;
   546           val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
   546           val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
   547           val pt_thm_optn  = pt_inst RS pt_optn_inst; 
   547           val pt_thm_optn  = pt_inst RS pt_optn_inst; 
   548           val pt_thm_list  = pt_inst RS pt_list_inst;
   548           val pt_thm_list  = pt_inst RS pt_list_inst;
   549           val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
   549           val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
   550           val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
   550           val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
   633        val cp_prod_inst    = @{thm "cp_prod_inst"};
   633        val cp_prod_inst    = @{thm "cp_prod_inst"};
   634        val cp_list_inst    = @{thm "cp_list_inst"};
   634        val cp_list_inst    = @{thm "cp_list_inst"};
   635        val cp_fun_inst     = @{thm "cp_fun_inst"};
   635        val cp_fun_inst     = @{thm "cp_fun_inst"};
   636        val cp_option_inst  = @{thm "cp_option_inst"};
   636        val cp_option_inst  = @{thm "cp_option_inst"};
   637        val cp_noption_inst = @{thm "cp_noption_inst"};
   637        val cp_noption_inst = @{thm "cp_noption_inst"};
       
   638        val cp_set_inst     = @{thm "cp_set_inst"};
   638        val pt_perm_compose = @{thm "pt_perm_compose"};
   639        val pt_perm_compose = @{thm "pt_perm_compose"};
   639 
   640 
   640        val dj_pp_forget    = @{thm "dj_perm_perm_forget"};
   641        val dj_pp_forget    = @{thm "dj_perm_perm_forget"};
   641 
   642 
   642        (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
   643        (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
   694             val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
   695             val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
   695             val cp_thm_list = cp_inst RS cp_list_inst;
   696             val cp_thm_list = cp_inst RS cp_list_inst;
   696             val cp_thm_fun  = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)));
   697             val cp_thm_fun  = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)));
   697             val cp_thm_optn = cp_inst RS cp_option_inst;
   698             val cp_thm_optn = cp_inst RS cp_option_inst;
   698             val cp_thm_noptn = cp_inst RS cp_noption_inst;
   699             val cp_thm_noptn = cp_inst RS cp_noption_inst;
       
   700             val cp_thm_set = cp_inst RS cp_set_inst;
   699         in
   701         in
   700          thy'
   702          thy'
   701          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   703          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   702          |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   704          |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   703          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   705          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   704          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   706          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   705          |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   707          |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   706          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   708          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
       
   709          |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
   707         end) ak_names thy) ak_names thy25;
   710         end) ak_names thy) ak_names thy25;
   708 
   711 
   709      (* show that discrete nominal types are permutation types, finitely     *)
   712      (* show that discrete nominal types are permutation types, finitely     *)
   710      (* supported and have the commutation property                          *)
   713      (* supported and have the commutation property                          *)
   711      (* discrete types have a permutation operation defined as pi o x = x;   *)
   714      (* discrete types have a permutation operation defined as pi o x = x;   *)
   815        val fresh_perm_app      = @{thm "Nominal.pt_fresh_perm_app"};    
   818        val fresh_perm_app      = @{thm "Nominal.pt_fresh_perm_app"};    
   816        val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
   819        val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
   817        val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
   820        val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
   818        val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
   821        val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
   819        val subseteq_eqvt       = @{thm "Nominal.pt_subseteq_eqvt"};
   822        val subseteq_eqvt       = @{thm "Nominal.pt_subseteq_eqvt"};
   820        val insert_eqvt         = @{thm "Nominal.pt_insert_eqvt"};
       
   821        val set_eqvt            = @{thm "Nominal.pt_set_eqvt"};
       
   822        val perm_set_eq         = @{thm "Nominal.perm_set_eq"};
       
   823 
   823 
   824        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
   824        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
   825        (* types; this allows for example to use abs_perm (which is a      *)
   825        (* types; this allows for example to use abs_perm (which is a      *)
   826        (* collection of theorems) instead of thm abs_fun_pi with explicit *)
   826        (* collection of theorems) instead of thm abs_fun_pi with explicit *)
   827        (* instantiations.                                                 *)
   827        (* instantiations.                                                 *)
   983               let val thms1 = inst_pt_at [set_diff_eqvt]
   983               let val thms1 = inst_pt_at [set_diff_eqvt]
   984               in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   984               in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   985             ||>> add_thmss_string
   985             ||>> add_thmss_string
   986               let val thms1 = inst_pt_at [subseteq_eqvt]
   986               let val thms1 = inst_pt_at [subseteq_eqvt]
   987               in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   987               in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   988             ||>> add_thmss_string [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])]
       
   989             ||>> add_thmss_string [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])]
       
   990             ||>> add_thmss_string [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])]
       
   991             ||>> add_thmss_string
   988             ||>> add_thmss_string
   992               let val thms1 = inst_pt_at [fresh_aux]
   989               let val thms1 = inst_pt_at [fresh_aux]
   993                   and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   990                   and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   994               in  [(("fresh_aux", thms1 @ thms2),[])] end  
   991               in  [(("fresh_aux", thms1 @ thms2),[])] end  
   995             ||>> add_thmss_string
   992             ||>> add_thmss_string