# HG changeset patch # User berghofe # Date 1210150775 -7200 # Node ID 2909150bd6145c45af017bbac712cb77c4470600 # Parent 56036226028b97e88517cba8edb784e4501d223a - Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq diff -r 56036226028b -r 2909150bd614 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed May 07 10:59:34 2008 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed May 07 10:59:35 2008 +0200 @@ -436,7 +436,6 @@ val pt2 = @{thm "pt2"}; val pt3 = @{thm "pt3"}; val at_pt_inst = @{thm "at_pt_inst"}; - val pt_set_inst = @{thm "pt_set_inst"}; val pt_unit_inst = @{thm "pt_unit_inst"}; val pt_prod_inst = @{thm "pt_prod_inst"}; val pt_nprod_inst = @{thm "pt_nprod_inst"}; @@ -497,7 +496,6 @@ val pt_thm_prod = pt_inst RS (pt_inst RS pt_prod_inst); val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst); val pt_thm_unit = pt_unit_inst; - val pt_thm_set = pt_inst RS pt_set_inst in thy |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun) @@ -508,7 +506,6 @@ |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod) |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit) - |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set) end) ak_names thy13; (******** fs_ class instances ********) @@ -584,7 +581,6 @@ val cp_fun_inst = @{thm "cp_fun_inst"}; val cp_option_inst = @{thm "cp_option_inst"}; val cp_noption_inst = @{thm "cp_noption_inst"}; - val cp_set_inst = @{thm "cp_set_inst"}; val pt_perm_compose = @{thm "pt_perm_compose"}; val dj_pp_forget = @{thm "dj_perm_perm_forget"}; @@ -646,7 +642,6 @@ val cp_thm_fun = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst))); val cp_thm_optn = cp_inst RS cp_option_inst; val cp_thm_noptn = cp_inst RS cp_noption_inst; - val cp_thm_set = cp_inst RS cp_set_inst; in thy' |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit) @@ -655,7 +650,6 @@ |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn) - |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set) end) ak_names thy) ak_names thy25; (* show that discrete nominal types are permutation types, finitely *) @@ -765,6 +759,9 @@ val pt_perm_supp_ineq = @{thm "Nominal.pt_perm_supp_ineq"}; val pt_perm_supp = @{thm "Nominal.pt_perm_supp"}; val subseteq_eqvt = @{thm "Nominal.pt_subseteq_eqvt"}; + val insert_eqvt = @{thm "Nominal.insert_eqvt"}; + val set_eqvt = @{thm "Nominal.set_eqvt"}; + val perm_set_eq = @{thm "Nominal.perm_set_eq"}; (* Now we collect and instantiate some lemmas w.r.t. all atom *) (* types; this allows for example to use abs_perm (which is a *) @@ -922,6 +919,9 @@ ||>> PureThy.add_thmss let val thms1 = inst_pt_at [subseteq_eqvt] in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end + ||>> PureThy.add_thmss [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])] + ||>> PureThy.add_thmss [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])] + ||>> PureThy.add_thmss [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])] ||>> PureThy.add_thmss let val thms1 = inst_pt_at [fresh_aux] and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]