# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267634849 -3600
# Node ID 80441e27dfd6ca456003e74575fd4d53382e1edf
# Parent  c6e521a2a0b1b228a94cc35527385cd4af7d953b
Code for solving symp goals with multiple existentials.

diff -r c6e521a2a0b1 -r 80441e27dfd6 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 03 15:28:25 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 03 17:47:29 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" (* For testing *)
+imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
 
 (* Bindings are given as a list which has a length being equal
@@ -328,14 +328,18 @@
 by auto
 
 ML {*
-fun symp_tac induct inj eqvt =
-  (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-  (REPEAT o etac conjE THEN' etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN'
-  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
-  (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
-  (etac @{thm alpha_gen_compose_sym} THEN' 
-    (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt)))))
+fun symp_tac induct inj eqvt ctxt =
+  ind_tac induct THEN_ALL_NEW
+  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs
+  THEN_ALL_NEW
+  REPEAT o etac @{thm exi_neg}
+  THEN_ALL_NEW
+  split_conjs THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
+  (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [
+    (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})),
+    (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
+  ])
 *}
 
 ML {*
@@ -402,7 +406,7 @@
   val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
   val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
   fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1;
-  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1;
+  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
   fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
   val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
   val symt = Goal.prove ctxt' [] [] symg symp_tac';
diff -r c6e521a2a0b1 -r 80441e27dfd6 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Wed Mar 03 15:28:25 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 03 17:47:29 2010 +0100
@@ -146,7 +146,9 @@
 by auto
 
 ML {*
-  fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+ML {*
   fun all_eqvts ctxt =
     Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
   val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
@@ -161,7 +163,7 @@
 
 ML {*
 fun alpha_eqvt_tac induct simps ctxt =
-  indtac induct THEN_ALL_NEW
+  ind_tac induct THEN_ALL_NEW
   simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW