Renamed sum_case to basic_sum_case and removed translations for sum_case
authorberghofe
Wed Aug 18 16:11:14 1999 +0200 (1999-08-18)
changeset 7254fc7f95f293da
parent 7253 a494a78fea39
child 7255 853bdbe9973d
Renamed sum_case to basic_sum_case and removed translations for sum_case
to avoid conflicts with the constant sum_case introduced in Datatype.thy.
src/HOL/Sum.ML
src/HOL/Sum.thy
     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);
     2.1 --- a/src/HOL/Sum.thy	Wed Aug 18 16:05:27 1999 +0200
     2.2 +++ b/src/HOL/Sum.thy	Wed Aug 18 16:11:14 1999 +0200
     2.3 @@ -27,23 +27,20 @@
     2.4  (* abstract constants and syntax *)
     2.5  
     2.6  consts
     2.7 -  Inl           :: "'a => 'a + 'b"
     2.8 -  Inr           :: "'b => 'a + 'b"
     2.9 -  sum_case      :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
    2.10 +  Inl            :: "'a => 'a + 'b"
    2.11 +  Inr            :: "'b => 'a + 'b"
    2.12 +  basic_sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
    2.13  
    2.14    (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
    2.15    Plus          :: "['a set, 'b set] => ('a + 'b) set"        (infixr 65)
    2.16    Part          :: ['a set, 'b => 'a] => 'a set
    2.17  
    2.18 -translations
    2.19 -  "case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
    2.20 -
    2.21  local
    2.22  
    2.23  defs
    2.24    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
    2.25    Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
    2.26 -  sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
    2.27 +  sum_case_def  "basic_sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
    2.28                                        & (!y. p=Inr(y) --> z=g(y))"
    2.29  
    2.30    sum_def       "A Plus B == (Inl``A) Un (Inr``B)"