src/HOL/Nominal/nominal_atoms.ML
changeset 18600 20ad06db427b
parent 18579 002d371401f5
child 18626 b6596f579e40
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jan 07 11:36:58 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jan 07 11:43:42 2006 +0100
     1.3 @@ -374,6 +374,7 @@
     1.4        val pt_set_inst   = thm "pt_set_inst"; 
     1.5        val pt_unit_inst  = thm "pt_unit_inst";
     1.6        val pt_prod_inst  = thm "pt_prod_inst"; 
     1.7 +      val pt_nprod_inst = thm "pt_nprod_inst"; 
     1.8        val pt_list_inst  = thm "pt_list_inst";   
     1.9        val pt_optn_inst  = thm "pt_option_inst";   
    1.10        val pt_noptn_inst = thm "pt_noption_inst";   
    1.11 @@ -410,6 +411,7 @@
    1.12       (*      option(pt_<ak>)            *)
    1.13       (*      list(pt_<ak>)              *)
    1.14       (*      *(pt_<ak>,pt_<ak>)         *)
    1.15 +     (*      nprod(pt_<ak>,pt_<ak>)     *)
    1.16       (*      unit                       *)
    1.17       (*      set(pt_<ak>)               *)
    1.18       (* are instances of pt_<ak>        *)
    1.19 @@ -428,6 +430,7 @@
    1.20            val pt_thm_optn  = pt_inst RS pt_optn_inst; 
    1.21            val pt_thm_list  = pt_inst RS pt_list_inst;
    1.22            val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
    1.23 +          val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
    1.24            val pt_thm_unit  = pt_unit_inst;
    1.25            val pt_thm_set   = pt_inst RS pt_set_inst
    1.26         in 
    1.27 @@ -437,6 +440,8 @@
    1.28          |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    1.29          |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.30          |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    1.31 +        |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.32 +                                    (pt_proof pt_thm_nprod)
    1.33          |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    1.34          |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    1.35       end) ak_names thy13; 
    1.36 @@ -448,6 +453,7 @@
    1.37         val fs_at_inst     = thm "fs_at_inst";
    1.38         val fs_unit_inst   = thm "fs_unit_inst";
    1.39         val fs_prod_inst   = thm "fs_prod_inst";
    1.40 +       val fs_nprod_inst  = thm "fs_nprod_inst";
    1.41         val fs_list_inst   = thm "fs_list_inst";
    1.42         val fs_option_inst = thm "fs_option_inst";
    1.43         val dj_supp        = thm "dj_supp"
    1.44 @@ -476,6 +482,7 @@
    1.45         (* shows that                  *)
    1.46         (*    unit                     *)
    1.47         (*    *(fs_<ak>,fs_<ak>)       *)
    1.48 +       (*    nprod(fs_<ak>,fs_<ak>)   *)
    1.49         (*    list(fs_<ak>)            *)
    1.50         (*    option(fs_<ak>)          *) 
    1.51         (* are instances of fs_<ak>    *)
    1.52 @@ -486,14 +493,17 @@
    1.53            val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
    1.54            fun fs_proof thm = EVERY [AxClass.intro_classes_tac [], rtac (thm RS fs1) 1];      
    1.55  
    1.56 -          val fs_thm_unit = fs_unit_inst;
    1.57 -          val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst);
    1.58 -          val fs_thm_list = fs_inst RS fs_list_inst;
    1.59 -          val fs_thm_optn = fs_inst RS fs_option_inst;
    1.60 +          val fs_thm_unit  = fs_unit_inst;
    1.61 +          val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
    1.62 +          val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst);
    1.63 +          val fs_thm_list  = fs_inst RS fs_list_inst;
    1.64 +          val fs_thm_optn  = fs_inst RS fs_option_inst;
    1.65          in 
    1.66           thy 
    1.67           |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    1.68 -         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)    
    1.69 +         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    1.70 +         |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.71 +                                     (fs_proof fs_thm_nprod) 
    1.72           |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    1.73           |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    1.74          end) ak_names thy20;