--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/Nominal2_Eqvt.thy Tue Jan 26 20:07:50 2010 +0100
@@ -0,0 +1,370 @@
+(* Title: Nominal2_Eqvt
+ Authors: Brian Huffman, Christian Urban
+
+ Equivariance, Supp and Fresh Lemmas for Operators.
+*)
+theory Nominal2_Eqvt
+imports Nominal2_Base
+uses ("nominal_thmdecls.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 (- 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 (- 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 (- p \<bullet> x))"
+ unfolding Ex1_def ex_eqvt conj_eqvt all_eqvt 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_eqvt[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_eqvt:
+ shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+ unfolding mem_def permute_fun_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 (-p \<bullet> x))}"
+ unfolding Collect_def permute_fun_def ..
+
+lemma empty_eqvt:
+ shows "p \<bullet> {} = {}"
+ unfolding empty_def Collect_eqvt 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_eqvt True_eqvt ..
+
+lemma union_eqvt:
+ shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+ unfolding Un_def Collect_eqvt 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_eqvt 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_eqvt 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_eqvt 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 ..
+
+lemma supp_eqvt: "p \<bullet> supp S = supp (p \<bullet> S)"
+ unfolding supp_def
+ by (simp only: Collect_eqvt Not_eqvt finite_eqvt eq_eqvt
+ permute_eqvt [of p] swap_eqvt permute_minus_cancel)
+
+
+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 {*
+ below is a construction site for a conversion that
+ pushes permutations into a term as far as possible
+*}
+
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
+
+use "nominal_thmdecls.ML"
+setup "NominalThmDecls.setup"
+
+lemmas [eqvt] =
+ (* connectives *)
+ eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt
+ True_eqvt False_eqvt
+ imp_eqvt [folded induct_implies_def]
+
+ (* datatypes *)
+ permute_prod.simps
+ fst_eqvt snd_eqvt
+
+ (* sets *)
+ empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
+ Diff_eqvt Compl_eqvt insert_eqvt
+
+(* A simple conversion pushing permutations into a term *)
+
+ML {*
+fun OF1 thm1 thm2 = thm2 RS thm1
+
+fun get_eqvt_thms ctxt =
+ map (OF1 @{thm eq_reflection}) (NominalThmDecls.get_eqvt_thms ctxt)
+*}
+
+ML {*
+fun eqvt_conv ctxt ctrm =
+ case (term_of ctrm) of
+ (Const (@{const_name "permute"}, _) $ _ $ t) =>
+ (if is_Const (head_of t)
+ then (More_Conv.rewrs_conv (get_eqvt_thms ctxt)
+ then_conv eqvt_conv ctxt) ctrm
+ else Conv.comb_conv (eqvt_conv ctxt) ctrm)
+ | _ $ _ => Conv.comb_conv (eqvt_conv ctxt) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => eqvt_conv ctxt) ctxt ctrm
+ | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+fun eqvt_tac ctxt =
+ CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)
+*}
+
+lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"
+apply(tactic {* eqvt_tac @{context} 1 *})
+oops
+
+text {*
+ Another conversion for pushing permutations into a term.
+ It is designed not to apply rules like @{term permute_pure} to
+ applications or abstractions, only to constants or free
+ variables. Thus permutations are not removed too early, and they
+ have a chance to cancel with bound variables.
+*}
+
+definition
+ "unpermute p = permute (- p)"
+
+lemma push_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 push_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 push_bound:
+ shows "p \<bullet> unpermute p x \<equiv> x"
+ unfolding unpermute_def by simp
+
+ML {*
+structure PushData = Named_Thms
+(
+ val name = "push"
+ val description = "push permutations"
+)
+
+local
+
+fun push_apply_conv ctxt ct =
+ case (term_of ct) of
+ (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
+ let
+ val (perm, t) = Thm.dest_comb ct
+ val (_, p) = Thm.dest_comb perm
+ val (f, x) = Thm.dest_comb t
+ val a = ctyp_of_term x;
+ val b = ctyp_of_term t;
+ val ty_insts = map SOME [b, a]
+ val term_insts = map SOME [p, f, x]
+ in
+ Drule.instantiate' ty_insts term_insts @{thm push_apply}
+ end
+ | _ => Conv.no_conv ct
+
+fun push_lambda_conv ctxt ct =
+ case (term_of ct) of
+ (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
+ Conv.rewr_conv @{thm push_lambda} ct
+ | _ => Conv.no_conv ct
+
+in
+
+fun push_conv ctxt ct =
+ Conv.first_conv
+ [ Conv.rewr_conv @{thm push_bound},
+ push_apply_conv ctxt
+ then_conv Conv.comb_conv (push_conv ctxt),
+ push_lambda_conv ctxt
+ then_conv Conv.abs_conv (fn (v, ctxt) => push_conv ctxt) ctxt,
+ More_Conv.rewrs_conv (PushData.get ctxt),
+ Conv.all_conv
+ ] ct
+
+fun push_tac ctxt =
+ CONVERSION (More_Conv.bottom_conv (fn ctxt => push_conv ctxt) ctxt)
+
+end
+*}
+
+setup PushData.setup
+
+declare permute_pure [THEN eq_reflection, push]
+
+lemma push_eq [THEN eq_reflection, push]:
+ "p \<bullet> (op =) = (op =)"
+ by (simp add: expand_fun_eq permute_fun_def eq_eqvt)
+
+lemma push_All [THEN eq_reflection, push]:
+ "p \<bullet> All = All"
+ by (simp add: expand_fun_eq permute_fun_def all_eqvt)
+
+lemma push_Ex [THEN eq_reflection, push]:
+ "p \<bullet> Ex = Ex"
+ by (simp add: expand_fun_eq permute_fun_def ex_eqvt)
+
+lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"
+apply (tactic {* push_tac @{context} 1 *})
+oops
+
+lemma "p \<bullet> (\<lambda>x. A \<longrightarrow> B x = (C::bool)) = foo"
+apply (tactic {* push_tac @{context} 1 *})
+oops
+
+lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
+apply (tactic {* push_tac @{context} 1 *})
+oops
+
+lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
+apply (tactic {* push_tac @{context} 1 *})
+oops
+
+end
\ No newline at end of file