src/HOL/Sum.ML
changeset 7254 fc7f95f293da
parent 7087 67c6706578ed
child 7293 959e060f4a2f
     1.1 --- a/src/HOL/Sum.ML	Wed Aug 18 16:05:27 1999 +0200
     1.2 +++ b/src/HOL/Sum.ML	Wed Aug 18 16:11:14 1999 +0200
     1.3 @@ -116,11 +116,11 @@
     1.4  
     1.5  (** sum_case -- the selection operator for sums **)
     1.6  
     1.7 -Goalw [sum_case_def] "sum_case f g (Inl x) = f(x)";
     1.8 +Goalw [sum_case_def] "basic_sum_case f g (Inl x) = f(x)";
     1.9  by (Blast_tac 1);
    1.10  qed "sum_case_Inl";
    1.11  
    1.12 -Goalw [sum_case_def] "sum_case f g (Inr x) = g(x)";
    1.13 +Goalw [sum_case_def] "basic_sum_case f g (Inr x) = g(x)";
    1.14  by (Blast_tac 1);
    1.15  qed "sum_case_Inr";
    1.16  
    1.17 @@ -143,31 +143,31 @@
    1.18  by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
    1.19  qed "sum_induct";
    1.20  
    1.21 -Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    1.22 +Goal "basic_sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    1.23  by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    1.24              etac ssubst, rtac sum_case_Inl,
    1.25              etac ssubst, rtac sum_case_Inr]);
    1.26  qed "surjective_sum";
    1.27  
    1.28 -Goal "R(sum_case f g s) = \
    1.29 +Goal "R(basic_sum_case f g s) = \
    1.30  \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
    1.31  by (res_inst_tac [("s","s")] sumE 1);
    1.32  by Auto_tac;
    1.33  qed "split_sum_case";
    1.34  
    1.35 -Goal "P (sum_case f g s) = \
    1.36 +Goal "P (basic_sum_case f g s) = \
    1.37  \     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
    1.38  by (stac split_sum_case 1);
    1.39  by (Blast_tac 1);
    1.40  qed "split_sum_case_asm";
    1.41  
    1.42  (*Prevents simplification of f and g: much faster*)
    1.43 -Goal "s=t ==> sum_case f g s = sum_case f g t";
    1.44 +Goal "s=t ==> basic_sum_case f g s = basic_sum_case f g t";
    1.45  by (etac arg_cong 1);
    1.46  qed "sum_case_weak_cong";
    1.47  
    1.48  val [p1,p2] = Goal
    1.49 -  "[| sum_case f1 f2 = sum_case g1 g2;  \
    1.50 +  "[| basic_sum_case f1 f2 = basic_sum_case g1 g2;  \
    1.51  \     [| f1 = g1; f2 = g2 |] ==> P |] \
    1.52  \  ==> P";
    1.53  by (rtac p2 1);