expand_list_case -> split_list_case
authornipkow
Mon Nov 03 08:08:14 1997 +0100 (1997-11-03)
changeset 4069d6d06a03a2e9
parent 4068 99224854a0ac
child 4070 3a6e1e562aed
expand_list_case -> split_list_case
src/HOL/List.ML
src/HOL/ex/Sorting.ML
src/HOLCF/IOA/ABP/Correctness.ML
     1.1 --- a/src/HOL/List.ML	Sun Nov 02 14:01:38 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Mon Nov 03 08:08:14 1997 +0100
     1.3 @@ -48,8 +48,6 @@
     1.4  
     1.5  (** list_case **)
     1.6  
     1.7 -val expand_list_case = split_list_case;
     1.8 -
     1.9  val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    1.10  by (induct_tac "xs" 1);
    1.11  by (REPEAT(resolve_tac prems 1));
    1.12 @@ -197,17 +195,17 @@
    1.13  
    1.14  goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
    1.15  by (asm_simp_tac (!simpset addsimps [hd_append]
    1.16 -                           addsplits [expand_list_case]) 1);
    1.17 +                           addsplits [split_list_case]) 1);
    1.18  qed "hd_append2";
    1.19  Addsimps [hd_append2];
    1.20  
    1.21  goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
    1.22 -by (simp_tac (!simpset addsplits [expand_list_case]) 1);
    1.23 +by (simp_tac (!simpset addsplits [split_list_case]) 1);
    1.24  qed "tl_append";
    1.25  
    1.26  goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
    1.27  by (asm_simp_tac (!simpset addsimps [tl_append]
    1.28 -                           addsplits [expand_list_case]) 1);
    1.29 +                           addsplits [split_list_case]) 1);
    1.30  qed "tl_append2";
    1.31  Addsimps [tl_append2];
    1.32  
     2.1 --- a/src/HOL/ex/Sorting.ML	Sun Nov 02 14:01:38 1997 +0100
     2.2 +++ b/src/HOL/ex/Sorting.ML	Mon Nov 03 08:08:14 1997 +0100
     2.3 @@ -30,7 +30,7 @@
     2.4  val prems = goalw Sorting.thy [transf_def]
     2.5    "transf(le) ==> sorted1 le xs = sorted le xs";
     2.6  by (list.induct_tac "xs" 1);
     2.7 -by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_list_case])));
     2.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [split_list_case])));
     2.9  by (cut_facts_tac prems 1);
    2.10  by (Fast_tac 1);
    2.11  qed "sorted1_is_sorted";
     3.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Sun Nov 02 14:01:38 1997 +0100
     3.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Mon Nov 03 08:08:14 1997 +0100
     3.3 @@ -49,7 +49,7 @@
     3.4   by (List.list.induct_tac "l" 1);
     3.5   by (Simp_tac 1);
     3.6   by (Simp_tac 1);
     3.7 - by (rtac (expand_list_case RS iffD2) 1);
     3.8 + by (rtac (split_list_case RS iffD2) 1);
     3.9   by (Asm_full_simp_tac 1);
    3.10   by (REPEAT (rtac allI 1)); 
    3.11   by (rtac impI 1); 
    3.12 @@ -68,7 +68,7 @@
    3.13  by (rotate 1 1);
    3.14  by (asm_full_simp_tac list_ss 1);
    3.15  by (Simp_tac 1);
    3.16 -by (rtac (expand_list_case RS iffD2) 1);
    3.17 +by (rtac (split_list_case RS iffD2) 1);
    3.18  by (asm_full_simp_tac list_ss 1);
    3.19  by (REPEAT (rtac allI 1)); 
    3.20   by (rtac impI 1); 
    3.21 @@ -100,7 +100,7 @@
    3.22  goal Correctness.thy "!!l.[| l~=[] |] ==>   \
    3.23  \   hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
    3.24   by (Simp_tac 1);
    3.25 - by (rtac (expand_list_case RS iffD2) 1);
    3.26 + by (rtac (split_list_case RS iffD2) 1);
    3.27   by (asm_full_simp_tac list_ss 1);
    3.28   by (REPEAT (rtac allI 1)); 
    3.29   by (rtac impI 1);