diff -r 4b0563bc4b03 -r 7d8949da7d99 Quot/Nominal/Nominal2_Eqvt.thy
--- a/Quot/Nominal/Nominal2_Eqvt.thy	Wed Feb 24 17:32:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,304 +0,0 @@
-(*  Title:      Nominal2_Eqvt
-    Authors:    Brian Huffman, Christian Urban
-
-    Equivariance, Supp and Fresh Lemmas for Operators. 
-    (Contains most, but not all such lemmas.)
-*)
-theory Nominal2_Eqvt
-imports Nominal2_Base
-uses ("nominal_thmdecls.ML")
-     ("nominal_permeq.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 image_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 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"
-*)
-
-
-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)
-
-section {* Equivariance automation *}
-
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
-
-use "nominal_thmdecls.ML"
-setup "Nominal_ThmDecls.setup"
-
-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 *)
-  permute_eqvt supp_eqvt fresh_eqvt
-  permute_pure
-
-  (* datatypes *)
-  permute_prod.simps append_eqvt rev_eqvt set_eqvt
-  fst_eqvt snd_eqvt
-
-  (* sets *)
-  empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
-  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt
-
-thm eqvts
-thm eqvts_raw
-
-text {* helper lemmas for the eqvt_tac *}
-
-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
-
-use "nominal_permeq.ML"
-
-
-lemma "p \<bullet> (A \<longrightarrow> B = C)"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) 
-oops
-
-lemma "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
-oops
-
-lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
-oops
-
-lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
-oops
-
-lemma "p \<bullet> (\<lambda>q. q \<bullet> (r \<bullet> x)) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
-oops
-
-lemma "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
-oops
-
-
-end
\ No newline at end of file