# HG changeset patch
# User paulson
# Date 971770872 -7200
# Node ID 178a272bceeb49e2a42db48b8e14fc73a8be6a63
# Parent  5eb935d6cc69cdd3874242e4713f7498ae87b1f2
renaming of contrapos rules

diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -200,17 +200,19 @@
 val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
 by (rtac (major RS notE RS notI) 1);
 by (etac minor 1) ;
-qed "contrapos";
+qed "contrapos_nn";
 
+Goal "t ~= s ==> s ~= t";
+by (etac contrapos_nn 1); 
+by (etac sym 1); 
+qed "not_sym";
+
+(*still used in HOLCF*)
 val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
-by (rtac (minor RS contrapos) 1);
+by (rtac (minor RS contrapos_nn) 1);
 by (etac major 1) ;
 qed "rev_contrapos";
 
-(* t ~= s ==> s ~= t *)
-bind_thm("not_sym", sym COMP rev_contrapos);
-
-
 section "Existential quantifier";
 
 Goalw [Ex_def] "P x ==> EX x::'a. P x";
@@ -307,14 +309,7 @@
 by (dtac p2 1);
 by (etac notE 1);
 by (rtac p1 1);
-qed "contrapos2";
-
-val [p1,p2] = Goal "[| P;  Q ==> ~ P |] ==> ~ Q";
-by (rtac notI 1);
-by (dtac p2 1);
-by (etac notE 1);
-by (rtac p1 1);
-qed "swap2";
+qed "contrapos_pp";
 
 
 section "Unique existence";
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/Induct/Multiset.ML
--- a/src/HOL/Induct/Multiset.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -632,7 +632,7 @@
 qed "mult_less_not_sym";
 
 (* [| M<N;  ~P ==> N<M |] ==> P *)
-bind_thm ("mult_less_asym", mult_less_not_sym RS swap);
+bind_thm ("mult_less_asym", mult_less_not_sym RS contrapos_np);
 
 Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)";
 by Auto_tac;
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/NatDef.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -156,7 +156,7 @@
 qed "less_not_sym";
 
 (* [| n<m; ~P ==> m<n |] ==> P *)
-bind_thm ("less_asym", less_not_sym RS swap);
+bind_thm ("less_asym", less_not_sym RS contrapos_np);
 
 Goalw [less_def] "~ n<(n::nat)";
 by (rtac (wf_pred_nat RS wf_trancl RS wf_not_refl) 1);
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/Ord.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -59,7 +59,7 @@
 qed "order_less_not_sym";
 
 (* [| n<m;  ~P ==> m<n |] ==> P *)
-bind_thm ("order_less_asym", order_less_not_sym RS swap);
+bind_thm ("order_less_asym", order_less_not_sym RS contrapos_np);
 
 (* Transitivity *)
 
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/Real/PNat.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -244,7 +244,7 @@
 qed "pnat_less_not_sym";
 
 (* [| x < y;  ~P ==> y < x |] ==> P *)
-bind_thm ("pnat_less_asym", pnat_less_not_sym RS swap);
+bind_thm ("pnat_less_asym", pnat_less_not_sym RS contrapos_np);
 
 Goalw [pnat_less_def] "~ y < (y::pnat)";
 by Auto_tac;
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -119,7 +119,7 @@
  by (action_simp_tac (simpset()addsimps[Read_def,enabled_ex])
                      [ReadInner_enabled,exI] [] 1);
  by (force_tac (mem_css addDs2 [base_pair]) 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (action_simp_tac (simpset() addsimps [Write_def,enabled_ex])
 	            [WriteInner_enabled,exI] [] 1);
 qed "RNext_enabled";
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/TLA/Memory/MemoryImplementation.ML
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -648,7 +648,7 @@
 by (action_simp_tac (simpset()) []
 	            (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1);
 by (auto_tac (MI_css addsimps2 [SF_def]));
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (auto_tac (MI_css addSIs2 [S6MClkReply_enabled] addSEs2 [STL4E, DmdImplE]));
 qed "S6_live";
 
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/TLA/TLA.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -245,7 +245,7 @@
 
 Goal "|- (<>(F | G)) = (<>F | <>G)";
 by (auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]));
-by (ALLGOALS (EVERY' [etac swap, 
+by (ALLGOALS (EVERY' [etac contrapos_np, 
                       merge_box_tac, 
                       fast_tac (temp_cs addSEs [STL4E])]));
 qed "DmdOr";
@@ -286,7 +286,7 @@
 by (Clarsimp_tac 1);
 by (etac dup_boxE 1);
 by (merge_box_tac 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (fast_tac (temp_cs addSEs [STL4E]) 1);
 qed "BoxDmd";
 
@@ -524,7 +524,7 @@
 Goalw [dmd_def] "|- []($P --> P` | Q`) --> (stable P) | <>Q";
 by (clarsimp_tac (temp_css addSDs2 [BoxPrime]) 1);
 by (merge_box_tac 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (fast_tac (temp_cs addSEs [Stable]) 1);
 qed "unless";
 
@@ -1020,7 +1020,7 @@
 
 Goalw [aall_def] "|- (AALL x. F x) --> F x";
 by (Clarsimp_tac 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (force_tac (temp_css addSIs2 [eexI]) 1);
 qed "aallE";
 
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/Wellfounded_Relations.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -143,7 +143,7 @@
  by (etac exE 1);
  by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
  by (Blast_tac 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
 by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/cladata.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -54,7 +54,7 @@
 structure BasicClassical: BASIC_CLASSICAL = Classical; 
 open BasicClassical;
 
-bind_thm ("swap", inst "Pa" "?Q" swap);
+bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
 
 structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
   that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
diff -r 5eb935d6cc69 -r 178a272bceeb src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/simpdata.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -307,8 +307,8 @@
   val disjE          = disjE
   val conjE          = conjE
   val exE            = exE
-  val contrapos      = contrapos
-  val contrapos2     = contrapos2
+  val contrapos      = contrapos_nn
+  val contrapos2     = contrapos_pp
   val notnotD        = notnotD
   end;