|
7293
|
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;
|
|
9108
|
11 |
bind_thm ("sum_case_Inl", sum_case_Inl);
|
|
|
12 |
bind_thm ("sum_case_Inr", sum_case_Inr);
|
|
7293
|
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";
|