--- a/Nominal/Nominal2_Base.thy Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Nominal2_Base.thy Mon Jun 04 21:39:51 2012 +0100
@@ -799,6 +799,21 @@
{* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
{* pushes permutations inside, raises an error if it cannot solve all permutations. *}
+simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ss => fn ctrm =>
+ case term_of (Thm.dest_arg ctrm) of
+ Free _ => NONE
+ | Var _ => NONE
+ | Const (@{const_name permute}, _) $ _ $ _ => NONE
+ | _ =>
+ let
+ val ctxt = Simplifier.the_context ss
+ val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm
+ handle ERROR _ => Thm.reflexive ctrm
+ in
+ if Thm.is_reflexive thm then NONE else SOME(thm)
+ end
+*}
+
subsubsection {* Equivariance for permutations and swapping *}
@@ -876,10 +891,6 @@
shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
by (simp add: permute_fun_def permute_bool_def)
-lemma Let_eqvt [eqvt]:
- shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
- unfolding Let_def permute_fun_app_eq ..
-
lemma True_eqvt [eqvt]:
shows "p \<bullet> True = True"
unfolding permute_bool_def ..
@@ -920,7 +931,7 @@
assumes unique: "\<exists>!x. P x"
shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
apply(rule the1_equality [symmetric])
- apply(simp add: ex1_eqvt2[symmetric])
+ apply(simp only: ex1_eqvt2[symmetric])
apply(simp add: permute_bool_def unique)
apply(simp add: permute_bool_def)
apply(rule theI'[OF unique])
@@ -940,84 +951,76 @@
lemma inter_eqvt [eqvt]:
shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
- unfolding Int_def
- by (perm_simp) (rule refl)
+ unfolding Int_def by simp
lemma Bex_eqvt [eqvt]:
shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
- unfolding Bex_def
- by (perm_simp) (rule refl)
+ unfolding Bex_def by simp
lemma Ball_eqvt [eqvt]:
shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
- unfolding Ball_def
- by (perm_simp) (rule refl)
+ unfolding Ball_def by simp
lemma image_eqvt [eqvt]:
shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
- unfolding image_def
- by (perm_simp) (rule refl)
+ unfolding image_def by simp
lemma Image_eqvt [eqvt]:
shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)"
- unfolding Image_def
- by (perm_simp) (rule refl)
+ unfolding Image_def by simp
lemma UNIV_eqvt [eqvt]:
shows "p \<bullet> UNIV = UNIV"
- unfolding UNIV_def
+ unfolding UNIV_def
by (perm_simp) (rule refl)
lemma union_eqvt [eqvt]:
shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
- unfolding Un_def
- by (perm_simp) (rule refl)
+ unfolding Un_def by simp
lemma Diff_eqvt [eqvt]:
fixes A B :: "'a::pt set"
shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
- unfolding set_diff_eq
- by (perm_simp) (rule refl)
+ unfolding set_diff_eq by simp
lemma Compl_eqvt [eqvt]:
fixes A :: "'a::pt set"
shows "p \<bullet> (- A) = - (p \<bullet> A)"
- unfolding Compl_eq_Diff_UNIV
- by (perm_simp) (rule refl)
+ unfolding Compl_eq_Diff_UNIV by simp
lemma subset_eqvt [eqvt]:
shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
- unfolding subset_eq
- by (perm_simp) (rule refl)
+ unfolding subset_eq by simp
lemma psubset_eqvt [eqvt]:
shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
- unfolding psubset_eq
- by (perm_simp) (rule refl)
+ unfolding psubset_eq by simp
lemma vimage_eqvt [eqvt]:
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
- unfolding vimage_def
- by (perm_simp) (rule refl)
+ unfolding vimage_def by simp
lemma Union_eqvt [eqvt]:
shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
- unfolding Union_eq
- by (perm_simp) (rule refl)
+ unfolding Union_eq by simp
lemma Inter_eqvt [eqvt]:
shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
- unfolding Inter_eq
- by (perm_simp) (rule refl)
+ unfolding Inter_eq by simp
+
+thm foldr.simps
lemma foldr_eqvt[eqvt]:
- "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
- apply (induct b)
- apply simp_all
- apply (perm_simp)
- apply simp
+ "p \<bullet> foldr f xs = foldr (p \<bullet> f) (p \<bullet> xs)"
+ apply(induct xs)
+ apply(simp_all)
+ apply(perm_simp exclude: foldr)
+ apply(simp)
done
+thm eqvts_raw
+
+
(* FIXME: eqvt attribute *)
lemma Sigma_eqvt:
shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
@@ -1090,12 +1093,12 @@
fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})"
shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)"
unfolding lfp_def
-by (perm_simp) (rule refl)
+by simp
lemma finite_eqvt [eqvt]:
shows "p \<bullet> finite A = finite (p \<bullet> A)"
unfolding finite_def
-by (perm_simp) (rule refl)
+by simp
subsubsection {* Equivariance for product operations *}
@@ -1111,7 +1114,7 @@
lemma split_eqvt [eqvt]:
shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
unfolding split_def
- by (perm_simp) (rule refl)
+ by simp
subsubsection {* Equivariance for list operations *}
@@ -1126,7 +1129,7 @@
lemma map_eqvt [eqvt]:
shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
- by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+ by (induct xs) (simp_all)
lemma removeAll_eqvt [eqvt]:
shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
@@ -1156,15 +1159,14 @@
lemma option_map_eqvt[eqvt]:
shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
- by (cases x) (simp_all, simp add: permute_fun_app_eq)
+ by (cases x) (simp_all)
subsubsection {* Equivariance for @{typ "'a fset"} *}
lemma in_fset_eqvt [eqvt]:
shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset
-by (perm_simp) (simp)
+unfolding in_fset by simp
lemma union_fset_eqvt [eqvt]:
shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
@@ -1174,7 +1176,6 @@
shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))"
apply(descending)
unfolding list_eq_def inter_list_def
- apply(perm_simp)
apply(simp)
done
@@ -1182,7 +1183,6 @@
shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))"
apply(descending)
unfolding sub_list_def
- apply(perm_simp)
apply(simp)
done
@@ -1254,14 +1254,11 @@
lemma supp_eqvt [eqvt]:
shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
- unfolding supp_def
- by (perm_simp)
- (simp only: permute_eqvt[symmetric])
+ unfolding supp_def by simp
lemma fresh_eqvt [eqvt]:
shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
- unfolding fresh_def
- by (perm_simp) (rule refl)
+ unfolding fresh_def by simp
lemma fresh_permute_iff:
shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x"
@@ -1751,7 +1748,7 @@
using assms by (simp add: eqvt_at_def)
also have "\<dots> = (p + q) \<bullet> (f x)" by simp
also have "\<dots> = f ((p + q) \<bullet> x)"
- using assms by (simp add: eqvt_at_def)
+ using assms by (simp only: eqvt_at_def)
finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp }
then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def
by simp
@@ -1978,7 +1975,7 @@
shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
proof -
have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)"
- unfolding eqvt_def
+ unfolding eqvt_def
by (perm_simp) (simp)
have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
@@ -2334,9 +2331,7 @@
lemma fresh_star_eqvt [eqvt]:
shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
-unfolding fresh_star_def
-by (perm_simp) (rule refl)
-
+unfolding fresh_star_def by simp
section {* Induction principle for permutations *}
@@ -2709,7 +2704,8 @@
apply(blast)
apply(simp)
done
- then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
+ then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ unfolding supp_swap by auto
moreover
have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
using ** by (auto simp add: insert_eqvt)
@@ -2777,7 +2773,8 @@
apply(blast)
apply(simp)
done
- then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
+ then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)"
+ unfolding supp_swap by auto
moreover
have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
using ** by (auto simp add: insert_eqvt)
@@ -2961,7 +2958,7 @@
fixes a::"'a::at_base"
shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"
unfolding atom_eqvt[symmetric]
- by (simp add: fresh_permute_iff)
+ by (simp only: fresh_permute_iff)
section {* Infrastructure for concrete atom types *}