# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273051494 -3600
# Node ID 2725853f43b9338df771cba94769a827e58b56ff
# Parent  65bdcc42baddb7c9d71509debd475583a6651d07
solved the problem with equivariance by first eta-normalising the goal

diff -r 65bdcc42badd -r 2725853f43b9 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed May 05 10:24:54 2010 +0100
@@ -384,6 +384,12 @@
 apply(perm_simp exclude: The)
 oops
 
+lemma 
+  fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
+  shows "(p \<bullet> (P The)) = foo"
+apply(perm_simp exclude: The)
+oops
+
 thm eqvts
 thm eqvts_raw
 
diff -r 65bdcc42badd -r 2725853f43b9 Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Wed May 05 10:24:54 2010 +0100
@@ -75,9 +75,9 @@
 *)
 fun transform_prem ctxt names thm =
 let
-  fun split_conj names (Const ("op &", _) $ p $ q) = 
-      (case head_of p of
-         Const (name, _) => if name mem names then SOME q else NONE
+  fun split_conj names (Const ("op &", _) $ f1 $ f2) = 
+      (case head_of f1 of
+         Const (name, _) => if name mem names then SOME f2 else NONE
        | _ => NONE)
   | split_conj _ _ = NONE;
 in
@@ -102,6 +102,7 @@
   SUBPROOF (fn {prems, context as ctxt, ...} =>
     let
       val prems' = map (transform_prem ctxt pred_names) prems
+
       val tac1 = resolve_tac prems'
       val tac2 = EVERY' [ rtac pi_intro_rule, 
             eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
diff -r 65bdcc42badd -r 2725853f43b9 Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Wed May 05 10:24:54 2010 +0100
@@ -97,7 +97,7 @@
         val term_insts = map SOME [p, f, x]                        
       in
         if has_bad_head bad_hds trm
-        then Conv.no_conv ctrm
+        then Conv.all_conv ctrm
         else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
       end
   | _ => Conv.no_conv ctrm
@@ -115,11 +115,11 @@
 let
   fun msg trm =
     let
-      val hd = head_of trm 
+      val hd = head_of trm
     in 
-    if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
-    else (if strict_flag then error else warning) 
-           ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+      if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
+      else (if strict_flag then error else warning) 
+             ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
     end
 
   val _ = case (term_of ctrm) of
@@ -130,7 +130,7 @@
   Conv.all_conv ctrm 
 end
 
-(* main conversion *)
+(* main conversion *) 
 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
 let
   val first_conv_wrapper = 
@@ -150,13 +150,19 @@
     ] ctrm
 end
 
+(* the eqvt-tactics first eta-normalise goals in 
+   order to avoid problems with inductions in the
+   equivaraince command. *)
+
 (* raises an error if some permutations cannot be eliminated *)
 fun eqvt_strict_tac ctxt user_thms bad_hds = 
-  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt)
+  CONVERSION (More_Conv.top_conv 
+    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt)
 
 (* prints a warning message if some permutations cannot be eliminated *)
 fun eqvt_tac ctxt user_thms bad_hds = 
-  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt)
+  CONVERSION (More_Conv.top_conv 
+    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt)
 
 (* setup of the configuration value *)
 val setup =
@@ -169,9 +175,7 @@
 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
   (Scan.repeat (Args.const true))) []
 
-val args_parser =  
-  add_thms_parser -- exclude_consts_parser ||
-  exclude_consts_parser -- add_thms_parser >> swap
+val args_parser =  add_thms_parser -- exclude_consts_parser 
 
 fun perm_simp_meth (thms, consts) ctxt = 
   SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
diff -r 65bdcc42badd -r 2725853f43b9 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Wed May 05 10:24:54 2010 +0100
@@ -72,6 +72,7 @@
 declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha
+equivariance alpha_trm_raw
 thm eqvts_raw
 
 
diff -r 65bdcc42badd -r 2725853f43b9 Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Wed May 05 10:24:54 2010 +0100
@@ -658,7 +658,7 @@
 (* for the moment, we force it to be       *)
 
 (*declare permute_pure[eqvt]*)
-(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *)
 
 thm eqvts
 thm eqvts_raw
@@ -669,7 +669,7 @@
 equivariance alpha_tkind_raw
 
 thm eqvts
-thm eqvts_raw*)
+thm eqvts_raw
 
 end
 
diff -r 65bdcc42badd -r 2725853f43b9 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Wed May 05 10:24:54 2010 +0100
@@ -27,12 +27,11 @@
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
 thm trm_assg.fv[simplified trm_assg.supp(1-2)]
 
-(*
-setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
 declare permute_trm_raw_permute_assg_raw.simps[eqvt]
 declare alpha_gen_eqvt[eqvt]
+
 equivariance alpha_trm_raw
-*)
+
 
 end