--- a/Nominal/Nominal2_Eqvt.thy Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy Mon Feb 28 15:21:10 2011 +0000
@@ -2,330 +2,13 @@
Author: Brian Huffman,
Author: Christian Urban
- Equivariance, supp and freshness lemmas for various operators
- (contains many, but not all such lemmas).
+ Test cases for perm_simp
*)
theory Nominal2_Eqvt
imports Nominal2_Base
-uses ("nominal_thmdecls.ML")
- ("nominal_permeq.ML")
- ("nominal_eqvt.ML")
begin
-section {* Permsimp and Eqvt infrastructure *}
-
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
-
-use "nominal_thmdecls.ML"
-setup "Nominal_ThmDecls.setup"
-
-
-section {* eqvt lemmas *}
-
-lemmas [eqvt] =
- conj_eqvt Not_eqvt ex_eqvt all_eqvt ex1_eqvt imp_eqvt uminus_eqvt
- imp_eqvt[folded induct_implies_def]
- all_eqvt[folded induct_forall_def]
-
- (* nominal *)
- supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt
- swap_eqvt flip_eqvt
-
- (* datatypes *)
- Pair_eqvt permute_list.simps permute_option.simps
- permute_sum.simps
-
- (* sets *)
- mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt
-
- (* fsets *)
- permute_fset fset_eqvt
-
-
-text {* helper lemmas for the perm_simp *}
-
-definition
- "unpermute p = permute (- p)"
-
-lemma eqvt_apply:
- fixes f :: "'a::pt \<Rightarrow> 'b::pt"
- and x :: "'a::pt"
- shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
- unfolding permute_fun_def by simp
-
-lemma eqvt_lambda:
- fixes f :: "'a::pt \<Rightarrow> 'b::pt"
- shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
- unfolding permute_fun_def unpermute_def by simp
-
-lemma eqvt_bound:
- shows "p \<bullet> unpermute p x \<equiv> x"
- unfolding unpermute_def by simp
-
-text {* provides perm_simp methods *}
-
-use "nominal_permeq.ML"
-setup Nominal_Permeq.setup
-
-method_setup perm_simp =
- {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
- {* pushes permutations inside. *}
-
-method_setup perm_strict_simp =
- {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
- {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
-
-(* the normal version of this lemma would cause loops *)
-lemma permute_eqvt_raw[eqvt_raw]:
- shows "p \<bullet> permute \<equiv> permute"
-apply(simp add: fun_eq_iff permute_fun_def)
-apply(subst permute_eqvt)
-apply(simp)
-done
-
-subsection {* Equivariance of Logical Operators *}
-
-lemma eq_eqvt[eqvt]:
- shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
- unfolding permute_eq_iff permute_bool_def ..
-
-lemma if_eqvt[eqvt]:
- 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 True_eqvt[eqvt]:
- shows "p \<bullet> True = True"
- unfolding permute_bool_def ..
-
-lemma False_eqvt[eqvt]:
- shows "p \<bullet> False = False"
- unfolding permute_bool_def ..
-
-lemma disj_eqvt[eqvt]:
- shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma all_eqvt2:
- shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma ex_eqvt2:
- shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma ex1_eqvt2:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma the_eqvt:
- assumes unique: "\<exists>!x. P x"
- shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
- apply(rule the1_equality [symmetric])
- apply(rule_tac p="-p" in permute_boolE)
- apply(perm_simp add: permute_minus_cancel)
- apply(rule unique)
- apply(rule_tac p="-p" in permute_boolE)
- apply(perm_simp add: permute_minus_cancel)
- apply(rule theI'[OF unique])
- done
-
-lemma the_eqvt2:
- 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 add: permute_bool_def unique)
- apply(simp add: permute_bool_def)
- apply(rule theI'[OF unique])
- done
-
-subsection {* Equivariance Set Operations *}
-
-lemma not_mem_eqvt:
- shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
- by (perm_simp) (rule refl)
-
-lemma Collect_eqvt[eqvt]:
- shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
- unfolding Collect_def permute_fun_def ..
-
-lemma Collect_eqvt2:
- shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-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)
-
-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)
-
-lemma UNIV_eqvt[eqvt]:
- shows "p \<bullet> UNIV = UNIV"
- 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)
-
-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)
-
-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)
-
-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)
-
-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)
-
-lemma image_eqvt[eqvt]:
- shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
- unfolding permute_set_eq_image
- unfolding permute_fun_def [where f=f]
- by (simp add: image_image)
-
-lemma vimage_eqvt[eqvt]:
- shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
- unfolding vimage_def
- by (perm_simp) (rule refl)
-
-lemma Union_eqvt[eqvt]:
- shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
- unfolding Union_eq
- by (perm_simp) (rule refl)
-
-lemma Sigma_eqvt:
- shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
-unfolding Sigma_def
-unfolding UNION_eq_Union_image
-by (perm_simp) (rule refl)
-
-lemma finite_permute_iff:
- shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
- unfolding permute_set_eq_vimage
- using bij_permute by (rule finite_vimage_iff)
-
-lemma finite_eqvt[eqvt]:
- shows "p \<bullet> finite A = finite (p \<bullet> A)"
- unfolding finite_permute_iff permute_bool_def ..
-
-
-section {* List Operations *}
-
-lemma append_eqvt[eqvt]:
- shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
- by (induct xs) auto
-
-lemma rev_eqvt[eqvt]:
- shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
- by (induct xs) (simp_all add: append_eqvt)
-
-lemma supp_rev:
- shows "supp (rev xs) = supp xs"
- by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
-
-lemma fresh_rev:
- shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
- by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
-
-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)
-
-lemma removeAll_eqvt[eqvt]:
- shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
- by (induct xs) (auto)
-
-lemma supp_removeAll:
- fixes x::"atom"
- shows "supp (removeAll x xs) = supp xs - {x}"
- by (induct xs)
- (auto simp add: supp_Nil supp_Cons supp_atom)
-
-lemma filter_eqvt[eqvt]:
- shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
-apply(induct xs)
-apply(simp)
-apply(simp only: filter.simps permute_list.simps if_eqvt)
-apply(simp only: permute_fun_app_eq)
-done
-
-lemma distinct_eqvt[eqvt]:
- shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
-apply(induct xs)
-apply(simp add: permute_bool_def)
-apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
-done
-
-lemma length_eqvt[eqvt]:
- shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
-by (induct xs) (simp_all add: permute_pure)
-
-
-subsection {* Equivariance Finite-Set Operations *}
-
-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)
-
-lemma union_fset_eqvt[eqvt]:
- shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
-by (induct S) (simp_all)
-
-lemma supp_union_fset:
- fixes S T::"'a::fs fset"
- shows "supp (S |\<union>| T) = supp S \<union> supp T"
-by (induct S) (auto)
-
-lemma fresh_union_fset:
- fixes S T::"'a::fs fset"
- shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
-unfolding fresh_def
-by (simp add: supp_union_fset)
-
-lemma map_fset_eqvt[eqvt]:
- shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
- by (lifting map_eqvt)
-
-
-subsection {* Product Operations *}
-
-lemma fst_eqvt[eqvt]:
- "p \<bullet> (fst x) = fst (p \<bullet> x)"
- by (cases x) simp
-
-lemma snd_eqvt[eqvt]:
- "p \<bullet> (snd x) = snd (p \<bullet> x)"
- by (cases x) simp
-
-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)
-
-
-section {* Test cases *}
-
-
declare [[trace_eqvt = false]]
(* declare [[trace_eqvt = true]] *)