equal
deleted
inserted
replaced
|
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"; |