cleanup for split_all_tac as wrapper in claset()
authoroheimb
Mon Apr 27 19:32:19 1998 +0200 (1998-04-27)
changeset 4838196100237656
parent 4837 eab729051897
child 4839 a7322db15065
cleanup for split_all_tac as wrapper in claset()
NEWS
src/HOL/IOA/Solve.ML
src/HOL/Map.ML
src/HOL/Trancl.ML
     1.1 --- a/NEWS	Mon Apr 27 19:30:40 1998 +0200
     1.2 +++ b/NEWS	Mon Apr 27 19:32:19 1998 +0200
     1.3 @@ -24,14 +24,16 @@
     1.4    combines rewriting and classical reasoning (and whatever other tools)
     1.5    similarly to auto_tac, but is aimed to solve the given subgoal totally.
     1.6  
     1.7 -* added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
     1.8 +* added option_map_eq_Some to simpset() and claset()
     1.9 +
    1.10  * New directory HOL/UNITY: Chandy and Misra's UNITY formalism
    1.11  
    1.12  * split_all_tac is now much faster and fails if there is nothing to split.
    1.13    Existing (fragile) proofs may require adaption because the order and the
    1.14    names of the automatically generated variables have changed.
    1.15    split_all_tac has moved within claset() from usafe wrappers to safe wrappers,
    1.16 -  which means that !!-bound variables are splitted much more aggressively.
    1.17 +  which means that !!-bound variables are splitted much more aggressively,
    1.18 +  and safe_tac and clarify_tac now split such variables.
    1.19    If this splitting is not appropriate, use delSWrapper "split_all_tac".
    1.20  
    1.21  * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
     2.1 --- a/src/HOL/IOA/Solve.ML	Mon Apr 27 19:30:40 1998 +0200
     2.2 +++ b/src/HOL/IOA/Solve.ML	Mon Apr 27 19:32:19 1998 +0200
     2.3 @@ -74,7 +74,7 @@
     2.4  \    %i. fst (snd ex i))")]  bexI 1);
     2.5  (* fst(s) is in projected execution *)
     2.6   by (Simp_tac 1);
     2.7 - by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
     2.8 + by (fast_tac (claset() delSWrapper"split_all_tac")1);
     2.9  (* projected execution is indeed an execution *)
    2.10  by (asm_full_simp_tac
    2.11        (simpset() addsimps [executions_def,is_execution_fragment_def,
    2.12 @@ -94,7 +94,7 @@
    2.13  \    %i. snd (snd ex i))")]  bexI 1);
    2.14  (* fst(s) is in projected execution *)
    2.15   by (Simp_tac 1);
    2.16 - by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
    2.17 + by (fast_tac (claset() delSWrapper"split_all_tac")1);
    2.18  (* projected execution is indeed an execution *)
    2.19  by (asm_full_simp_tac
    2.20        (simpset() addsimps [executions_def,is_execution_fragment_def,
     3.1 --- a/src/HOL/Map.ML	Mon Apr 27 19:30:40 1998 +0200
     3.2 +++ b/src/HOL/Map.ML	Mon Apr 27 19:32:19 1998 +0200
     3.3 @@ -63,9 +63,8 @@
     3.4  goal thy "map_of xs k = Some y --> (k,y):set xs";
     3.5  by (list.induct_tac "xs" 1);
     3.6  by  (Simp_tac 1);
     3.7 +by (split_all_tac 1);
     3.8  by (Asm_simp_tac 1);
     3.9 -by (split_all_tac 1);
    3.10 -by (Simp_tac 1);
    3.11  qed_spec_mp "map_of_SomeD";
    3.12  
    3.13  section "dom";
     4.1 --- a/src/HOL/Trancl.ML	Mon Apr 27 19:30:40 1998 +0200
     4.2 +++ b/src/HOL/Trancl.ML	Mon Apr 27 19:32:19 1998 +0200
     4.3 @@ -160,8 +160,7 @@
     4.4  qed "rtrancl_converseI";
     4.5  
     4.6  goal Trancl.thy "(r^-1)^* = (r^*)^-1";
     4.7 -by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]
     4.8 -			addSaltern ("split_all_tac", split_all_tac)));
     4.9 +by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
    4.10  qed "rtrancl_converse";
    4.11  
    4.12  val major::prems = goal Trancl.thy
    4.13 @@ -339,7 +338,7 @@
    4.14  
    4.15  
    4.16  goal Trancl.thy "(r^+)^= = r^*";
    4.17 -by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
    4.18 +by Safe_tac;
    4.19  by  (etac trancl_into_rtrancl 1);
    4.20  by (etac rtranclE 1);
    4.21  by  (Auto_tac );
    4.22 @@ -349,7 +348,7 @@
    4.23  Addsimps[reflcl_trancl];
    4.24  
    4.25  goal Trancl.thy "(r^=)^+ = r^*";
    4.26 -by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
    4.27 +by Safe_tac;
    4.28  by  (dtac trancl_into_rtrancl 1);
    4.29  by  (Asm_full_simp_tac 1);
    4.30  by (etac rtranclE 1);