# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1324529225 0
# Node ID 06950f2b4443bd131852efdb502c4ade20e328ca
# Parent  ff377f9d030a98d27f84d19e93d0f6074f2e29c6# Parent  19f5e7afad894cb44473d962a7d22552fb65558c
merged

diff -r ff377f9d030a -r 06950f2b4443 Nominal/Ex/CR.thy
--- a/Nominal/Ex/CR.thy	Thu Dec 22 04:46:37 2011 +0000
+++ b/Nominal/Ex/CR.thy	Thu Dec 22 04:47:05 2011 +0000
@@ -1,5 +1,7 @@
 (* CR_Takahashi from Nominal1 ported to Nominal2 *)
-theory CR imports Nominal2 begin
+theory CR 
+imports "../Nominal2" 
+begin
 
 atom_decl name
 
@@ -86,6 +88,8 @@
   bs1[intro, simp]: "M \<longrightarrow>b* M"
 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3"
 
+equivariance beta_star
+
 lemma bs3[intro, trans]:
   assumes "A \<longrightarrow>b* B"
   and     "B \<longrightarrow>b* C"
diff -r ff377f9d030a -r 06950f2b4443 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Thu Dec 22 04:46:37 2011 +0000
+++ b/Nominal/nominal_eqvt.ML	Thu Dec 22 04:47:05 2011 +0000
@@ -28,30 +28,24 @@
 
 (** equivariance tactics **)
 
-val perm_boolE = @{thm permute_boolE}
-
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro  = 
   let
     val thy = Proof_Context.theory_of ctxt
-    val cpi = Thm.cterm_of thy (mk_minus pi)
-    val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
-    val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all}
-    val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def}
-    val eqvt_sconfig = 
-          eqvt_strict_config addpres @{thms permute_minus_cancel(2)} addexcls pred_names
+    val cpi = Thm.cterm_of thy pi
+    val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
+    val eqvt_sconfig = eqvt_strict_config addexcls pred_names
+    val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all}
+    val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def  permute_minus_cancel(2)}
   in
-    eqvt_tac ctxt (eqvt_strict_config addexcls pred_names) THEN'
+    eqvt_tac ctxt eqvt_sconfig THEN'
     SUBPROOF (fn {prems, context as ctxt, ...} =>
       let
         val prems' = map (transform_prem2 ctxt pred_names) prems
-        val tac1 = resolve_tac prems'
-        val tac2 = EVERY' [ rtac pi_intro_rule, 
-          eqvt_tac ctxt eqvt_sconfig, resolve_tac prems' ]
-        val tac3 = EVERY' [ rtac pi_intro_rule, 
-          eqvt_tac ctxt eqvt_sconfig, simp_tac simps1, 
-          simp_tac simps2, resolve_tac prems']
+        val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems'
+        val prems''' = map (simplify simps2 o simplify simps1) prems''
+
       in
-        (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 
+        HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) 
       end) ctxt
   end