# HG changeset patch
# User paulson
# Date 850729286 -3600
# Node ID 46de4b035f009d5765b8ea73a3093d1e32265808
# Parent  13df7d6c5c3b8cdd2b6d39728ea979f1ee75fcc7
New tactic: prove_unique_tac

diff -r 13df7d6c5c3b -r 46de4b035f00 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Mon Dec 16 10:40:14 1996 +0100
+++ b/src/HOL/Auth/Message.ML	Mon Dec 16 10:41:26 1996 +0100
@@ -803,10 +803,19 @@
 						 impOfSubs analz_subset_parts]) 2 1))
        ]) i);
 
-(*Useful in many uniqueness proofs*)
+(** Useful in many uniqueness proofs **)
 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
                      assume_tac (i+1);
 
+(*Apply the EX-ALL quantifification to prove uniqueness theorems in 
+  their standard form*)
+fun prove_unique_tac lemma = 
+  EVERY' [dtac lemma,
+	  REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
+	  (*Duplicate the assumption*)
+	  forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
+	  fast_tac (!claset addSDs [spec])];
+
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 goal Set.thy "A Un (B Un A) = B Un A";