# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273401439 -3600
# Node ID 0532006ec7ec6af2151040b5341322e8a7c0c6b6
# Parent  b1d64b7ce2b787458aa717ddf7a42da9421b332d
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied

diff -r b1d64b7ce2b7 -r 0532006ec7ec Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Fri May 07 12:28:11 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun May 09 11:37:19 2010 +0100
@@ -280,6 +280,11 @@
   "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 {* Units *}
 
 lemma supp_unit:
@@ -386,10 +391,16 @@
 
 lemma 
   fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
-  shows "(p \<bullet> (P The)) = foo"
+  shows "p \<bullet> (P The) = foo"
 apply(perm_simp exclude: The)
 oops
 
+lemma
+  fixes  P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
+  shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
+apply(perm_simp)
+oops
+
 thm eqvts
 thm eqvts_raw
 
diff -r b1d64b7ce2b7 -r 0532006ec7ec Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Fri May 07 12:28:11 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Sun May 09 11:37:19 2010 +0100
@@ -23,18 +23,11 @@
 
   the string list contains constants that should not be
   analysed (for example there is no raw eqvt-lemma for
-  the constant The; therefore it should not be analysed 
+  the constant The); therefore it should not be analysed 
 
 - setting [[trace_eqvt = true]] switches on tracing 
   information  
 
-
-TODO:
-
- - provide a proper parser for the method (see Nominal2_Eqvt)
-   
- - proably the list of bad constant should be a dataslot
-
 *)
 
 structure Nominal_Permeq: NOMINAL_PERMEQ =
@@ -76,17 +69,10 @@
   Conv.no_conv ctrm
 end
 
-(* conversion for applications: 
-   only applies the conversion, if the head of the
-   application is not a "bad head" *)
-fun has_bad_head bad_hds trm = 
-  case (head_of trm) of 
-    Const (s, _) => member (op=) bad_hds s 
-  | _ => false 
-
-fun eqvt_apply_conv bad_hds ctrm =
+(* conversion for applications *)
+fun eqvt_apply_conv ctrm =
   case (term_of ctrm) of
-    Const (@{const_name "permute"}, _) $ _ $ (trm $ _) =>
+    Const (@{const_name "permute"}, _) $ _ $ (_ $ _) =>
       let
         val (perm, t) = Thm.dest_comb ctrm
         val (_, p) = Thm.dest_comb perm
@@ -96,9 +82,7 @@
         val ty_insts = map SOME [b, a]
         val term_insts = map SOME [p, f, x]                        
       in
-        if has_bad_head bad_hds trm
-        then Conv.all_conv ctrm
-        else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
+        Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
       end
   | _ => Conv.no_conv ctrm
 
@@ -109,18 +93,19 @@
       Conv.rewr_conv @{thm eqvt_lambda} ctrm
   | _ => Conv.no_conv ctrm
 
+
 (* conversion that raises an error or prints a warning message, 
    if a permutation on a constant or application cannot be analysed *)
-fun progress_info_conv ctxt strict_flag bad_hds ctrm =
+
+fun is_excluded excluded (Const (a, _)) = member (op=) excluded a 
+  | is_excluded _ _ = false 
+
+fun progress_info_conv ctxt strict_flag excluded ctrm =
 let
   fun msg trm =
-    let
-      val hd = head_of trm
-    in 
-      if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then ()
-      else (if strict_flag then error else warning) 
-             ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
-    end
+    if is_excluded excluded trm then () else 
+      (if strict_flag then error else warning) 
+        ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
 
   val _ = case (term_of ctrm) of
       Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
@@ -131,7 +116,7 @@
 end
 
 (* main conversion *) 
-fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
+fun eqvt_conv ctxt strict_flag user_thms excluded ctrm =
 let
   val first_conv_wrapper = 
     if trace_enabled ctxt 
@@ -143,10 +128,10 @@
 in
   first_conv_wrapper
     [ More_Conv.rewrs_conv pre_thms,
-      eqvt_apply_conv bad_hds,
+      eqvt_apply_conv,
       eqvt_lambda_conv,
       More_Conv.rewrs_conv post_thms,
-      progress_info_conv ctxt strict_flag bad_hds
+      progress_info_conv ctxt strict_flag excluded
     ] ctrm
 end
 
@@ -155,14 +140,14 @@
    equivaraince command. *)
 
 (* raises an error if some permutations cannot be eliminated *)
-fun eqvt_strict_tac ctxt user_thms bad_hds = 
+fun eqvt_strict_tac ctxt user_thms excluded = 
   CONVERSION (More_Conv.top_conv 
-    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt)
+    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt)
 
 (* prints a warning message if some permutations cannot be eliminated *)
-fun eqvt_tac ctxt user_thms bad_hds = 
+fun eqvt_tac ctxt user_thms excluded = 
   CONVERSION (More_Conv.top_conv 
-    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt)
+    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt)
 
 (* setup of the configuration value *)
 val setup =