made the type sets instance of the "cp" type-class
authorurbanc
Wed Mar 28 01:09:23 2007 +0200 (2007-03-28)
changeset 2253635debf264656
parent 22535 cbee450f88a6
child 22537 c55f5631a4ec
made the type sets instance of the "cp" type-class
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 27 19:39:40 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 28 01:09:23 2007 +0200
     1.3 @@ -543,6 +543,7 @@
     1.4         val cp_fun_inst     = thm "cp_fun_inst";
     1.5         val cp_option_inst  = thm "cp_option_inst";
     1.6         val cp_noption_inst = thm "cp_noption_inst";
     1.7 +       val cp_set_inst     = thm "cp_set_inst";
     1.8         val pt_perm_compose = thm "pt_perm_compose";
     1.9  
    1.10         val dj_pp_forget    = thm "dj_perm_perm_forget";
    1.11 @@ -586,6 +587,7 @@
    1.12         (*      functions                                                *)
    1.13         (*      options                                                  *)
    1.14         (*      noptions                                                 *)
    1.15 +       (*      sets                                                     *)
    1.16         (* are instances of cp_<ak>_<ai> for every <ak>/<ai>-combination *)
    1.17         val thy26 = fold (fn ak_name => fn thy =>
    1.18  	fold (fn ak_name' => fn thy' =>
    1.19 @@ -603,6 +605,7 @@
    1.20              val cp_thm_fun  = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)));
    1.21              val cp_thm_optn = cp_inst RS cp_option_inst;
    1.22              val cp_thm_noptn = cp_inst RS cp_noption_inst;
    1.23 +            val cp_thm_set = cp_inst RS cp_set_inst;
    1.24          in
    1.25           thy'
    1.26           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
    1.27 @@ -611,6 +614,7 @@
    1.28           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    1.29           |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.30           |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    1.31 +         |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
    1.32          end) ak_names thy) ak_names thy25;
    1.33  
    1.34       (* show that discrete nominal types are permutation types, finitely     *)