src/HOL/Nominal/nominal_atoms.ML
changeset 26820 2909150bd614
parent 26773 ba8b1a8a12a7
child 27095 c1c27955d7dd
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed May 07 10:59:34 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed May 07 10:59:35 2008 +0200
     1.3 @@ -436,7 +436,6 @@
     1.4        val pt2           = @{thm "pt2"};
     1.5        val pt3           = @{thm "pt3"};
     1.6        val at_pt_inst    = @{thm "at_pt_inst"};
     1.7 -      val pt_set_inst   = @{thm "pt_set_inst"}; 
     1.8        val pt_unit_inst  = @{thm "pt_unit_inst"};
     1.9        val pt_prod_inst  = @{thm "pt_prod_inst"}; 
    1.10        val pt_nprod_inst = @{thm "pt_nprod_inst"}; 
    1.11 @@ -497,7 +496,6 @@
    1.12            val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
    1.13            val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
    1.14            val pt_thm_unit  = pt_unit_inst;
    1.15 -          val pt_thm_set   = pt_inst RS pt_set_inst
    1.16         in
    1.17          thy
    1.18          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.19 @@ -508,7 +506,6 @@
    1.20          |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.21                                      (pt_proof pt_thm_nprod)
    1.22          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    1.23 -        |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    1.24       end) ak_names thy13; 
    1.25  
    1.26         (********  fs_<ak> class instances  ********)
    1.27 @@ -584,7 +581,6 @@
    1.28         val cp_fun_inst     = @{thm "cp_fun_inst"};
    1.29         val cp_option_inst  = @{thm "cp_option_inst"};
    1.30         val cp_noption_inst = @{thm "cp_noption_inst"};
    1.31 -       val cp_set_inst     = @{thm "cp_set_inst"};
    1.32         val pt_perm_compose = @{thm "pt_perm_compose"};
    1.33  
    1.34         val dj_pp_forget    = @{thm "dj_perm_perm_forget"};
    1.35 @@ -646,7 +642,6 @@
    1.36              val cp_thm_fun  = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)));
    1.37              val cp_thm_optn = cp_inst RS cp_option_inst;
    1.38              val cp_thm_noptn = cp_inst RS cp_noption_inst;
    1.39 -            val cp_thm_set = cp_inst RS cp_set_inst;
    1.40          in
    1.41           thy'
    1.42           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
    1.43 @@ -655,7 +650,6 @@
    1.44           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    1.45           |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.46           |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    1.47 -         |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
    1.48          end) ak_names thy) ak_names thy25;
    1.49  
    1.50       (* show that discrete nominal types are permutation types, finitely     *)
    1.51 @@ -765,6 +759,9 @@
    1.52         val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
    1.53         val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
    1.54         val subseteq_eqvt       = @{thm "Nominal.pt_subseteq_eqvt"};
    1.55 +       val insert_eqvt         = @{thm "Nominal.insert_eqvt"};
    1.56 +       val set_eqvt            = @{thm "Nominal.set_eqvt"};
    1.57 +       val perm_set_eq         = @{thm "Nominal.perm_set_eq"};
    1.58  
    1.59         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.60         (* types; this allows for example to use abs_perm (which is a      *)
    1.61 @@ -922,6 +919,9 @@
    1.62              ||>> PureThy.add_thmss
    1.63                let val thms1 = inst_pt_at [subseteq_eqvt]
    1.64                in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    1.65 +            ||>> PureThy.add_thmss [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])]
    1.66 +            ||>> PureThy.add_thmss [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])]
    1.67 +            ||>> PureThy.add_thmss [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])]
    1.68              ||>> PureThy.add_thmss
    1.69                let val thms1 = inst_pt_at [fresh_aux]
    1.70                    and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]