# HG changeset patch # User Cezary Kaliszyk # Date 1273594825 -7200 # Node ID e25b0fff0dd2767138f8f051dce3e284163b0e6d # Parent 2205b572bc9b81512533f2a4c1138b38772d0ad8 Include raw permutation definitions in eqvt diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/Classical.thy Tue May 11 18:20:25 2010 +0200 @@ -68,8 +68,6 @@ thm alpha.intros -declare permute_trm_raw.simps[eqvt] - equivariance alpha equivariance alpha_trm_raw thm eqvts_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Tue May 11 18:20:25 2010 +0200 @@ -652,8 +652,6 @@ thm eqvts thm eqvts_raw -declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt] - equivariance alpha_tkind_raw thm eqvts diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/Ex1rec.thy --- a/Nominal/Ex/Ex1rec.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/Ex1rec.thy Tue May 11 18:20:25 2010 +0200 @@ -30,8 +30,6 @@ ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} thm lam_bp.fv[simplified lam_bp.supp(1-2)] -declare permute_lam_raw_permute_bp_raw.simps[eqvt] - equivariance alpha_lam_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/Ex2.thy Tue May 11 18:20:25 2010 +0200 @@ -27,8 +27,6 @@ thm trm_pat.distinct thm trm_pat.fv[simplified trm_pat.supp(1-2)] -declare permute_trm_raw_permute_pat_raw.simps[eqvt] - equivariance alpha_trm_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/Ex3.thy --- a/Nominal/Ex/Ex3.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/Ex3.thy Tue May 11 18:20:25 2010 +0200 @@ -31,8 +31,6 @@ thm trm_pat.fv[simplified trm_pat.supp(1-2)] -declare permute_trm_raw_permute_pat_raw.simps[eqvt] - equivariance alpha_trm_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/ExLet.thy --- a/Nominal/Ex/ExLet.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExLet.thy Tue May 11 18:20:25 2010 +0200 @@ -34,12 +34,7 @@ (*thm trm_lts.supp*) thm trm_lts.fv[simplified trm_lts.supp(1-2)] - -declare permute_trm_raw_permute_lts_raw.simps[eqvt] - -equivariance alpha_trm_raw - - +equivariance alpha_bn_raw primrec permute_bn_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/ExLetMult.thy --- a/Nominal/Ex/ExLetMult.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExLetMult.thy Tue May 11 18:20:25 2010 +0200 @@ -22,8 +22,6 @@ thm trm_lts.induct thm trm_lts.fv[simplified trm_lts.supp] -declare permute_trm_raw_permute_lts_raw.simps[eqvt] - equivariance alpha_trm_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/ExLetRec.thy --- a/Nominal/Ex/ExLetRec.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExLetRec.thy Tue May 11 18:20:25 2010 +0200 @@ -32,8 +32,6 @@ thm trm_lts.supp thm trm_lts.fv[simplified trm_lts.supp] -declare permute_trm_raw_permute_lts_raw.simps[eqvt] - equivariance alpha_trm_raw (* why is this not in HOL simpset? *) diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/ExPS3.thy --- a/Nominal/Ex/ExPS3.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExPS3.thy Tue May 11 18:20:25 2010 +0200 @@ -35,8 +35,6 @@ thm exp_pat.fv thm exp_pat.supp(1-2) -declare permute_exp_raw_permute_pat_raw.simps[eqvt] - equivariance alpha_exp_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/ExPS6.thy --- a/Nominal/Ex/ExPS6.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExPS6.thy Tue May 11 18:20:25 2010 +0200 @@ -32,8 +32,6 @@ thm exp_pat.distinct thm exp_pat.supp -declare permute_exp_raw_permute_pat_raw.simps[eqvt] - equivariance alpha_exp_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/ExPS7.thy --- a/Nominal/Ex/ExPS7.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExPS7.thy Tue May 11 18:20:25 2010 +0200 @@ -28,8 +28,6 @@ thm exp_lrb_lrbs.eq_iff thm exp_lrb_lrbs.supp -declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt] - equivariance alpha_exp_raw end diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExPS8.thy Tue May 11 18:20:25 2010 +0200 @@ -48,9 +48,6 @@ thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff - -declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt] - equivariance alpha_exp_raw end diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/LF.thy --- a/Nominal/Ex/LF.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/LF.thy Tue May 11 18:20:25 2010 +0200 @@ -20,8 +20,6 @@ thm kind_ty_trm.supp -declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt] - equivariance alpha_trm_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Tue May 11 18:20:25 2010 +0200 @@ -15,7 +15,6 @@ declare lam.perm[eqvt] -declare permute_lam_raw.simps[eqvt] equivariance alpha_lam_raw section {* Strong Induction Principles*} @@ -259,7 +258,6 @@ | a3: "\pi. ({atom name}, lam_raw) \gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \ alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" -declare permute_lam_raw.simps[eqvt] equivariance alpha_lam_raw' thm eqvts_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/Modules.thy --- a/Nominal/Ex/Modules.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/Modules.thy Tue May 11 18:20:25 2010 +0200 @@ -68,8 +68,6 @@ thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10) thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)] -declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt] - equivariance alpha_trm_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Tue May 11 18:20:25 2010 +0200 @@ -27,8 +27,6 @@ ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} thm trm_assg.fv[simplified trm_assg.supp(1-2)] -declare permute_trm_raw_permute_assg_raw.simps[eqvt] - equivariance alpha_trm_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/TestMorePerm.thy --- a/Nominal/Ex/TestMorePerm.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/TestMorePerm.thy Tue May 11 18:20:25 2010 +0200 @@ -26,7 +26,6 @@ thm alpha_weird_raw.intros[no_vars] thm fv_weird_raw.simps[no_vars] -declare permute_weird_raw.simps[eqvt] equivariance alpha_weird_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Tue May 11 18:20:25 2010 +0200 @@ -14,7 +14,6 @@ lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] -declare permute_ty_raw_permute_tys_raw.simps[eqvt] equivariance alpha_ty_raw diff -r 2205b572bc9b -r e25b0fff0dd2 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/NewParser.thy Tue May 11 18:20:25 2010 +0200 @@ -395,7 +395,10 @@ val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc - val thy = Local_Theory.exit_global lthy2; + + val (_, lthy2a) = Local_Theory.note ((Binding.empty, + [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; + val thy = Local_Theory.exit_global lthy2a; val thy_name = Context.theory_name thy val lthy3 = Theory_Target.init NONE thy;