src/HOL/Datatype.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7293 959e060f4a2f
child 9108 9fff97d29837
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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 
    12 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    13 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    14             etac ssubst, rtac sum_case_Inl,
    15             etac ssubst, rtac sum_case_Inr]);
    16 qed "surjective_sum";
    17 
    18 (*Prevents simplification of f and g: much faster*)
    19 Goal "s=t ==> sum_case f g s = sum_case f g t";
    20 by (etac arg_cong 1);
    21 qed "sum_case_weak_cong";
    22 
    23 val [p1,p2] = Goal
    24   "[| sum_case f1 f2 = sum_case g1 g2;  \
    25 \     [| f1 = g1; f2 = g2 |] ==> P |] \
    26 \  ==> P";
    27 by (rtac p2 1);
    28 by (rtac ext 1);
    29 by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
    30 by (Asm_full_simp_tac 1);
    31 by (rtac ext 1);
    32 by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
    33 by (Asm_full_simp_tac 1);
    34 qed "sum_case_inject";