src/HOL/Datatype.ML
author berghofe
Thu Aug 19 19:00:42 1999 +0200 (1999-08-19)
changeset 7293 959e060f4a2f
child 9108 9fff97d29837
permissions -rw-r--r--
Moved sum_case stuff from Sum to Datatype.
berghofe@7293
     1
(*  Title:      HOL/Datatype.ML
berghofe@7293
     2
    ID:         $Id$
berghofe@7293
     3
    Author:     Stefan Berghofer
berghofe@7293
     4
    Copyright   1999  TU Muenchen
berghofe@7293
     5
*)
berghofe@7293
     6
berghofe@7293
     7
(** sum_case -- the selection operator for sums **)
berghofe@7293
     8
berghofe@7293
     9
(*compatibility*)
berghofe@7293
    10
val [sum_case_Inl, sum_case_Inr] = sum.cases;
berghofe@7293
    11
berghofe@7293
    12
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
berghofe@7293
    13
by (EVERY1 [res_inst_tac [("s","s")] sumE, 
berghofe@7293
    14
            etac ssubst, rtac sum_case_Inl,
berghofe@7293
    15
            etac ssubst, rtac sum_case_Inr]);
berghofe@7293
    16
qed "surjective_sum";
berghofe@7293
    17
berghofe@7293
    18
(*Prevents simplification of f and g: much faster*)
berghofe@7293
    19
Goal "s=t ==> sum_case f g s = sum_case f g t";
berghofe@7293
    20
by (etac arg_cong 1);
berghofe@7293
    21
qed "sum_case_weak_cong";
berghofe@7293
    22
berghofe@7293
    23
val [p1,p2] = Goal
berghofe@7293
    24
  "[| sum_case f1 f2 = sum_case g1 g2;  \
berghofe@7293
    25
\     [| f1 = g1; f2 = g2 |] ==> P |] \
berghofe@7293
    26
\  ==> P";
berghofe@7293
    27
by (rtac p2 1);
berghofe@7293
    28
by (rtac ext 1);
berghofe@7293
    29
by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
berghofe@7293
    30
by (Asm_full_simp_tac 1);
berghofe@7293
    31
by (rtac ext 1);
berghofe@7293
    32
by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
berghofe@7293
    33
by (Asm_full_simp_tac 1);
berghofe@7293
    34
qed "sum_case_inject";