--- a/Quot/Nominal/Nominal2_Eqvt.thy	Wed Feb 03 09:25:21 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Wed Feb 03 12:06:10 2010 +0100
@@ -6,6 +6,7 @@
 theory Nominal2_Eqvt
 imports Nominal2_Base
 uses ("nominal_thmdecls.ML")
+     ("nominal_permeq.ML")
 begin
 
 section {* Logical Operators *}
@@ -43,25 +44,40 @@
   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_eqvt conj_eqvt all_eqvt imp_eqvt eq_eqvt
+  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_eqvt[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])
@@ -78,12 +94,16 @@
   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_eqvt False_eqvt ..
+  unfolding empty_def Collect_eqvt2 False_eqvt ..
 
 lemma supp_set_empty:
   shows "supp {} = {}"
@@ -95,20 +115,20 @@
 
 lemma UNIV_eqvt:
   shows "p \<bullet> UNIV = UNIV"
-  unfolding UNIV_def Collect_eqvt True_eqvt ..
+  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_eqvt disj_eqvt mem_eqvt by simp
+  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_eqvt conj_eqvt mem_eqvt by simp
+  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_eqvt conj_eqvt Not_eqvt mem_eqvt by simp
+  unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp
 
 lemma Compl_eqvt:
   fixes A :: "'a::pt set"
@@ -122,7 +142,7 @@
 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 ..
+  unfolding Collect_eqvt2 mem_eqvt ..
 
 lemma image_eqvt:
   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
@@ -139,11 +159,6 @@
   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 *}
 
@@ -205,22 +220,20 @@
 
 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"
+setup "Nominal_ThmDecls.setup"
 
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
-  True_eqvt False_eqvt
+  True_eqvt False_eqvt ex_eqvt all_eqvt
   imp_eqvt [folded induct_implies_def]
 
+  (* nominal *)
+  permute_eqvt supp_eqvt fresh_eqvt
+
   (* datatypes *)
   permute_prod.simps
   fst_eqvt snd_eqvt
@@ -229,142 +242,56 @@
   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)  
-*}
+declare permute_pure [eqvt]
 
-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
-*}
+thm eqvt
 
-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.
-*}
+text {* helper lemmas for the eqvt_tac *}
 
 definition
   "unpermute p = permute (- p)"
 
-lemma push_apply:
-  fixes f :: "'a::pt \<Rightarrow> 'b::pt" and x :: "'a::pt"
+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 push_lambda:
+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 push_bound:
+lemma eqvt_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
+use "nominal_permeq.ML"
 
-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 *}) 
+lemma "p \<bullet> (A \<longrightarrow> B = C)"
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) 
 oops
 
-lemma "p \<bullet> (\<lambda>x. A \<longrightarrow> B x = (C::bool)) = foo"
-apply (tactic {* push_tac @{context} 1 *})
+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 {* push_tac @{context} 1 *})
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
 oops
 
 lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
-apply (tactic {* push_tac @{context} 1 *})
+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