renaming of contrapos rules
authorpaulson
Tue Oct 17 10:21:12 2000 +0200 (2000-10-17)
changeset 10231178a272bceeb
parent 10230 5eb935d6cc69
child 10232 529c65b5dcde
renaming of contrapos rules
src/HOL/HOL_lemmas.ML
src/HOL/Induct/Multiset.ML
src/HOL/NatDef.ML
src/HOL/Ord.ML
src/HOL/Real/PNat.ML
src/HOL/TLA/Memory/Memory.ML
src/HOL/TLA/Memory/MemoryImplementation.ML
src/HOL/TLA/TLA.ML
src/HOL/Wellfounded_Relations.ML
src/HOL/cladata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL_lemmas.ML	Tue Oct 17 10:20:43 2000 +0200
     1.2 +++ b/src/HOL/HOL_lemmas.ML	Tue Oct 17 10:21:12 2000 +0200
     1.3 @@ -200,17 +200,19 @@
     1.4  val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
     1.5  by (rtac (major RS notE RS notI) 1);
     1.6  by (etac minor 1) ;
     1.7 -qed "contrapos";
     1.8 +qed "contrapos_nn";
     1.9  
    1.10 +Goal "t ~= s ==> s ~= t";
    1.11 +by (etac contrapos_nn 1); 
    1.12 +by (etac sym 1); 
    1.13 +qed "not_sym";
    1.14 +
    1.15 +(*still used in HOLCF*)
    1.16  val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
    1.17 -by (rtac (minor RS contrapos) 1);
    1.18 +by (rtac (minor RS contrapos_nn) 1);
    1.19  by (etac major 1) ;
    1.20  qed "rev_contrapos";
    1.21  
    1.22 -(* t ~= s ==> s ~= t *)
    1.23 -bind_thm("not_sym", sym COMP rev_contrapos);
    1.24 -
    1.25 -
    1.26  section "Existential quantifier";
    1.27  
    1.28  Goalw [Ex_def] "P x ==> EX x::'a. P x";
    1.29 @@ -307,14 +309,7 @@
    1.30  by (dtac p2 1);
    1.31  by (etac notE 1);
    1.32  by (rtac p1 1);
    1.33 -qed "contrapos2";
    1.34 -
    1.35 -val [p1,p2] = Goal "[| P;  Q ==> ~ P |] ==> ~ Q";
    1.36 -by (rtac notI 1);
    1.37 -by (dtac p2 1);
    1.38 -by (etac notE 1);
    1.39 -by (rtac p1 1);
    1.40 -qed "swap2";
    1.41 +qed "contrapos_pp";
    1.42  
    1.43  
    1.44  section "Unique existence";
     2.1 --- a/src/HOL/Induct/Multiset.ML	Tue Oct 17 10:20:43 2000 +0200
     2.2 +++ b/src/HOL/Induct/Multiset.ML	Tue Oct 17 10:21:12 2000 +0200
     2.3 @@ -632,7 +632,7 @@
     2.4  qed "mult_less_not_sym";
     2.5  
     2.6  (* [| M<N;  ~P ==> N<M |] ==> P *)
     2.7 -bind_thm ("mult_less_asym", mult_less_not_sym RS swap);
     2.8 +bind_thm ("mult_less_asym", mult_less_not_sym RS contrapos_np);
     2.9  
    2.10  Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)";
    2.11  by Auto_tac;
     3.1 --- a/src/HOL/NatDef.ML	Tue Oct 17 10:20:43 2000 +0200
     3.2 +++ b/src/HOL/NatDef.ML	Tue Oct 17 10:21:12 2000 +0200
     3.3 @@ -156,7 +156,7 @@
     3.4  qed "less_not_sym";
     3.5  
     3.6  (* [| n<m; ~P ==> m<n |] ==> P *)
     3.7 -bind_thm ("less_asym", less_not_sym RS swap);
     3.8 +bind_thm ("less_asym", less_not_sym RS contrapos_np);
     3.9  
    3.10  Goalw [less_def] "~ n<(n::nat)";
    3.11  by (rtac (wf_pred_nat RS wf_trancl RS wf_not_refl) 1);
     4.1 --- a/src/HOL/Ord.ML	Tue Oct 17 10:20:43 2000 +0200
     4.2 +++ b/src/HOL/Ord.ML	Tue Oct 17 10:21:12 2000 +0200
     4.3 @@ -59,7 +59,7 @@
     4.4  qed "order_less_not_sym";
     4.5  
     4.6  (* [| n<m;  ~P ==> m<n |] ==> P *)
     4.7 -bind_thm ("order_less_asym", order_less_not_sym RS swap);
     4.8 +bind_thm ("order_less_asym", order_less_not_sym RS contrapos_np);
     4.9  
    4.10  (* Transitivity *)
    4.11  
     5.1 --- a/src/HOL/Real/PNat.ML	Tue Oct 17 10:20:43 2000 +0200
     5.2 +++ b/src/HOL/Real/PNat.ML	Tue Oct 17 10:21:12 2000 +0200
     5.3 @@ -244,7 +244,7 @@
     5.4  qed "pnat_less_not_sym";
     5.5  
     5.6  (* [| x < y;  ~P ==> y < x |] ==> P *)
     5.7 -bind_thm ("pnat_less_asym", pnat_less_not_sym RS swap);
     5.8 +bind_thm ("pnat_less_asym", pnat_less_not_sym RS contrapos_np);
     5.9  
    5.10  Goalw [pnat_less_def] "~ y < (y::pnat)";
    5.11  by Auto_tac;
     6.1 --- a/src/HOL/TLA/Memory/Memory.ML	Tue Oct 17 10:20:43 2000 +0200
     6.2 +++ b/src/HOL/TLA/Memory/Memory.ML	Tue Oct 17 10:21:12 2000 +0200
     6.3 @@ -119,7 +119,7 @@
     6.4   by (action_simp_tac (simpset()addsimps[Read_def,enabled_ex])
     6.5                       [ReadInner_enabled,exI] [] 1);
     6.6   by (force_tac (mem_css addDs2 [base_pair]) 1);
     6.7 -by (etac swap 1);
     6.8 +by (etac contrapos_np 1);
     6.9  by (action_simp_tac (simpset() addsimps [Write_def,enabled_ex])
    6.10  	            [WriteInner_enabled,exI] [] 1);
    6.11  qed "RNext_enabled";
     7.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Oct 17 10:20:43 2000 +0200
     7.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Oct 17 10:21:12 2000 +0200
     7.3 @@ -648,7 +648,7 @@
     7.4  by (action_simp_tac (simpset()) []
     7.5  	            (map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1);
     7.6  by (auto_tac (MI_css addsimps2 [SF_def]));
     7.7 -by (etac swap 1);
     7.8 +by (etac contrapos_np 1);
     7.9  by (auto_tac (MI_css addSIs2 [S6MClkReply_enabled] addSEs2 [STL4E, DmdImplE]));
    7.10  qed "S6_live";
    7.11  
     8.1 --- a/src/HOL/TLA/TLA.ML	Tue Oct 17 10:20:43 2000 +0200
     8.2 +++ b/src/HOL/TLA/TLA.ML	Tue Oct 17 10:21:12 2000 +0200
     8.3 @@ -245,7 +245,7 @@
     8.4  
     8.5  Goal "|- (<>(F | G)) = (<>F | <>G)";
     8.6  by (auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]));
     8.7 -by (ALLGOALS (EVERY' [etac swap, 
     8.8 +by (ALLGOALS (EVERY' [etac contrapos_np, 
     8.9                        merge_box_tac, 
    8.10                        fast_tac (temp_cs addSEs [STL4E])]));
    8.11  qed "DmdOr";
    8.12 @@ -286,7 +286,7 @@
    8.13  by (Clarsimp_tac 1);
    8.14  by (etac dup_boxE 1);
    8.15  by (merge_box_tac 1);
    8.16 -by (etac swap 1);
    8.17 +by (etac contrapos_np 1);
    8.18  by (fast_tac (temp_cs addSEs [STL4E]) 1);
    8.19  qed "BoxDmd";
    8.20  
    8.21 @@ -524,7 +524,7 @@
    8.22  Goalw [dmd_def] "|- []($P --> P` | Q`) --> (stable P) | <>Q";
    8.23  by (clarsimp_tac (temp_css addSDs2 [BoxPrime]) 1);
    8.24  by (merge_box_tac 1);
    8.25 -by (etac swap 1);
    8.26 +by (etac contrapos_np 1);
    8.27  by (fast_tac (temp_cs addSEs [Stable]) 1);
    8.28  qed "unless";
    8.29  
    8.30 @@ -1020,7 +1020,7 @@
    8.31  
    8.32  Goalw [aall_def] "|- (AALL x. F x) --> F x";
    8.33  by (Clarsimp_tac 1);
    8.34 -by (etac swap 1);
    8.35 +by (etac contrapos_np 1);
    8.36  by (force_tac (temp_css addSIs2 [eexI]) 1);
    8.37  qed "aallE";
    8.38  
     9.1 --- a/src/HOL/Wellfounded_Relations.ML	Tue Oct 17 10:20:43 2000 +0200
     9.2 +++ b/src/HOL/Wellfounded_Relations.ML	Tue Oct 17 10:21:12 2000 +0200
     9.3 @@ -143,7 +143,7 @@
     9.4   by (etac exE 1);
     9.5   by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
     9.6   by (Blast_tac 1);
     9.7 -by (etac swap 1);
     9.8 +by (etac contrapos_np 1);
     9.9  by (Asm_full_simp_tac 1);
    9.10  by (Clarify_tac 1);
    9.11  by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
    10.1 --- a/src/HOL/cladata.ML	Tue Oct 17 10:20:43 2000 +0200
    10.2 +++ b/src/HOL/cladata.ML	Tue Oct 17 10:21:12 2000 +0200
    10.3 @@ -54,7 +54,7 @@
    10.4  structure BasicClassical: BASIC_CLASSICAL = Classical; 
    10.5  open BasicClassical;
    10.6  
    10.7 -bind_thm ("swap", inst "Pa" "?Q" swap);
    10.8 +bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
    10.9  
   10.10  structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
   10.11    that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
    11.1 --- a/src/HOL/simpdata.ML	Tue Oct 17 10:20:43 2000 +0200
    11.2 +++ b/src/HOL/simpdata.ML	Tue Oct 17 10:21:12 2000 +0200
    11.3 @@ -307,8 +307,8 @@
    11.4    val disjE          = disjE
    11.5    val conjE          = conjE
    11.6    val exE            = exE
    11.7 -  val contrapos      = contrapos
    11.8 -  val contrapos2     = contrapos2
    11.9 +  val contrapos      = contrapos_nn
   11.10 +  val contrapos2     = contrapos_pp
   11.11    val notnotD        = notnotD
   11.12    end;
   11.13