src/HOL/Nominal/nominal_atoms.ML
changeset 45979 296d9a9c8d24
parent 45839 43a5b86bc102
child 46180 72ee700e1d8f
equal deleted inserted replaced
45978:d3325de5f299 45979:296d9a9c8d24
   492       val pt_nprod_inst = @{thm "pt_nprod_inst"}; 
   492       val pt_nprod_inst = @{thm "pt_nprod_inst"}; 
   493       val pt_list_inst  = @{thm "pt_list_inst"};
   493       val pt_list_inst  = @{thm "pt_list_inst"};
   494       val pt_optn_inst  = @{thm "pt_option_inst"};
   494       val pt_optn_inst  = @{thm "pt_option_inst"};
   495       val pt_noptn_inst = @{thm "pt_noption_inst"};
   495       val pt_noptn_inst = @{thm "pt_noption_inst"};
   496       val pt_fun_inst   = @{thm "pt_fun_inst"};
   496       val pt_fun_inst   = @{thm "pt_fun_inst"};
       
   497       val pt_set_inst   = @{thm "pt_set_inst"};
   497 
   498 
   498      (* for all atom-kind combinations <ak>/<ak'> show that        *)
   499      (* for all atom-kind combinations <ak>/<ak'> show that        *)
   499      (* every <ak> is an instance of pt_<ak'>; the proof for       *)
   500      (* every <ak> is an instance of pt_<ak'>; the proof for       *)
   500      (* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *)
   501      (* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *)
   501      val thy13 = fold (fn ak_name => fn thy =>
   502      val thy13 = fold (fn ak_name => fn thy =>
   539           fun pt_proof thm = 
   540           fun pt_proof thm = 
   540               EVERY [Class.intro_classes_tac [],
   541               EVERY [Class.intro_classes_tac [],
   541                      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];
   542 
   543 
   543           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);
   544           val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
   546           val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
   545           val pt_thm_optn  = pt_inst RS pt_optn_inst; 
   547           val pt_thm_optn  = pt_inst RS pt_optn_inst; 
   546           val pt_thm_list  = pt_inst RS pt_list_inst;
   548           val pt_thm_list  = pt_inst RS pt_list_inst;
   547           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);
   548           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);
   549           val pt_thm_unit  = pt_unit_inst;
   551           val pt_thm_unit  = pt_unit_inst;
   550        in
   552        in
   551         thy
   553         thy
   552         |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
   554         |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
       
   555         |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
   553         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   556         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   554         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
   557         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
   555         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   558         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   556         |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   559         |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   557         |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   560         |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])