--- a/Nominal-General/Nominal2_Eqvt.thy Fri Apr 30 10:31:32 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Fri Apr 30 10:32:34 2010 +0200
@@ -12,254 +12,15 @@
("nominal_eqvt.ML")
begin
-section {* Logical Operators *}
-lemma eq_eqvt:
- shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
- unfolding permute_eq_iff permute_bool_def ..
-
-lemma if_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:
- shows "p \<bullet> True = True"
- unfolding permute_bool_def ..
-
-lemma False_eqvt:
- shows "p \<bullet> False = False"
- unfolding permute_bool_def ..
-
-lemma imp_eqvt:
- shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma conj_eqvt:
- shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma disj_eqvt:
- shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma Not_eqvt:
- shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
- by (simp add: permute_bool_def)
-
-lemma all_eqvt:
- shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-lemma all_eqvt2:
- shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
- unfolding permute_fun_def permute_bool_def
- by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-lemma ex_eqvt:
- shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
-lemma ex_eqvt2:
- shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
- unfolding permute_fun_def permute_bool_def
- by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
-lemma ex1_eqvt:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
- unfolding Ex1_def
- by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt)
-
-lemma ex1_eqvt2:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
- unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt
- by simp
-
-lemma the_eqvt:
- 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
-
-section {* Set Operations *}
-
-lemma mem_permute_iff:
- shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-unfolding mem_def permute_fun_def permute_bool_def
-by simp
-
-lemma mem_eqvt:
- shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
- unfolding mem_permute_iff permute_bool_def by simp
-
-lemma not_mem_eqvt:
- shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
- unfolding mem_def permute_fun_def by (simp add: Not_eqvt)
-
-lemma Collect_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))}"
- unfolding Collect_def permute_fun_def ..
-
-lemma empty_eqvt:
- shows "p \<bullet> {} = {}"
- unfolding empty_def Collect_eqvt2 False_eqvt ..
-
-lemma supp_set_empty:
- shows "supp {} = {}"
- by (simp add: supp_def empty_eqvt)
-
-lemma fresh_set_empty:
- shows "a \<sharp> {}"
- by (simp add: fresh_def supp_set_empty)
-
-lemma UNIV_eqvt:
- shows "p \<bullet> UNIV = UNIV"
- unfolding UNIV_def Collect_eqvt2 True_eqvt ..
-
-lemma union_eqvt:
- shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
- unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp
-
-lemma inter_eqvt:
- shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
- unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp
-
-lemma Diff_eqvt:
- fixes A B :: "'a::pt set"
- shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
- unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp
-
-lemma Compl_eqvt:
- fixes A :: "'a::pt set"
- shows "p \<bullet> (- A) = - (p \<bullet> A)"
- unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..
-
-lemma insert_eqvt:
- shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
- unfolding permute_set_eq_image image_insert ..
-
-lemma vimage_eqvt:
- shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
- unfolding vimage_def permute_fun_def [where f=f]
- unfolding Collect_eqvt2 mem_eqvt ..
-
-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:
- shows "p \<bullet> finite A = finite (p \<bullet> A)"
- unfolding finite_permute_iff permute_bool_def ..
-
-
-section {* List Operations *}
-
-lemma append_eqvt:
- shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
- by (induct xs) auto
-
-lemma supp_append:
- shows "supp (xs @ ys) = supp xs \<union> supp ys"
- by (induct xs) (auto simp add: supp_Nil supp_Cons)
-
-lemma fresh_append:
- shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
- by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
-
-lemma rev_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 set_eqvt:
- shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
- by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
-
-(* needs finite support premise
-lemma supp_set:
- fixes x :: "'a::pt"
- shows "supp (set xs) = supp xs"
-*)
-
-lemma map_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)
-
-section {* Product Operations *}
-
-lemma fst_eqvt:
- "p \<bullet> (fst x) = fst (p \<bullet> x)"
- by (cases x) simp
-
-lemma snd_eqvt:
- "p \<bullet> (snd x) = snd (p \<bullet> x)"
- by (cases x) simp
-
-section {* Units *}
-
-lemma supp_unit:
- shows "supp () = {}"
- by (simp add: supp_def)
-
-lemma fresh_unit:
- shows "a \<sharp> ()"
- by (simp add: fresh_def supp_unit)
-
-lemma permute_eqvt_raw:
- shows "p \<bullet> permute = permute"
-apply(simp add: expand_fun_eq permute_fun_def)
-apply(subst permute_eqvt)
-apply(simp)
-done
-
-
-section {* Equivariance automation *}
+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"
-ML {* Thm.full_rules *}
-lemmas [eqvt] =
- (* connectives *)
- eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt
- True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt
- imp_eqvt [folded induct_implies_def]
-
- (* nominal *)
- supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt
-
- (* datatypes *)
- permute_prod.simps append_eqvt rev_eqvt set_eqvt
- map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps
-
- (* sets *)
- empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
- Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
-
-
-lemmas [eqvt_raw] =
- permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)
-
-text {* helper lemmas for the eqvt_tac *}
+text {* helper lemmas for the perm_simp *}
definition
"unpermute p = permute (- p)"
@@ -279,7 +40,8 @@
shows "p \<bullet> unpermute p x \<equiv> x"
unfolding unpermute_def by simp
-(* provides perm_simp methods *)
+text {* provides perm_simp methods *}
+
use "nominal_permeq.ML"
setup Nominal_Permeq.setup
@@ -291,6 +53,249 @@
{* 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: expand_fun_eq permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
+section {* 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 imp_eqvt[eqvt]:
+ shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+lemma conj_eqvt[eqvt]:
+ shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+ by (simp add: 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 Not_eqvt[eqvt]:
+ shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
+ by (simp add: permute_bool_def)
+
+lemma all_eqvt[eqvt]:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
+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_eqvt[eqvt]:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
+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_eqvt[eqvt]:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ unfolding Ex1_def
+ by (perm_simp) (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 (- 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
+
+section {* Set Operations *}
+
+lemma mem_permute_iff:
+ shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
+ unfolding mem_def permute_fun_def permute_bool_def
+ by simp
+
+lemma mem_eqvt[eqvt]:
+ shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+ unfolding mem_def
+ by (perm_simp) (rule refl)
+
+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 empty_eqvt[eqvt]:
+ shows "p \<bullet> {} = {}"
+ unfolding empty_def
+ by (perm_simp) (rule refl)
+
+lemma supp_set_empty:
+ shows "supp {} = {}"
+ unfolding supp_def
+ by (simp add: empty_eqvt)
+
+lemma fresh_set_empty:
+ shows "a \<sharp> {}"
+ by (simp add: fresh_def supp_set_empty)
+
+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 inter_eqvt[eqvt]:
+ shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ unfolding Int_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 insert_eqvt[eqvt]:
+ shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
+ unfolding permute_set_eq_image image_insert ..
+
+lemma vimage_eqvt[eqvt]:
+ shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+ unfolding vimage_def
+ 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 supp_append:
+ shows "supp (xs @ ys) = supp xs \<union> supp ys"
+ by (induct xs) (auto simp add: supp_Nil supp_Cons)
+
+lemma fresh_append:
+ shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
+ by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+
+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 set_eqvt[eqvt]:
+ shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
+ by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
+
+(* needs finite support premise
+lemma supp_set:
+ fixes x :: "'a::pt"
+ shows "supp (set xs) = supp xs"
+*)
+
+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)
+
+section {* 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
+
+section {* Units *}
+
+lemma supp_unit:
+ shows "supp () = {}"
+ by (simp add: supp_def)
+
+lemma fresh_unit:
+ shows "a \<sharp> ()"
+ by (simp add: fresh_def supp_unit)
+
+
+section {* additional lemmas *}
+
+ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "Pair"} *}
+
+lemmas [eqvt] =
+ imp_eqvt [folded induct_implies_def]
+
+ (* nominal *)
+ supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt
+
+ (* datatypes *)
+ permute_prod.simps Pair_eqvt permute_list.simps
+
+ (* sets *)
+ image_eqvt
+
+
+section {* Test cases *}
+
+
declare [[trace_eqvt = true]]
lemma
@@ -365,17 +370,15 @@
apply(perm_simp exclude: The)
oops
-
thm eqvts
thm eqvts_raw
-ML {*
-Nominal_ThmDecls.is_eqvt @{context} @{term "supp"}
-*}
+ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
-(* automatic equivariance procedure for
- inductive definitions *)
+section {*
+ Automatic equivariance procedure for inductive definitions *}
+
use "nominal_eqvt.ML"
end