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