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";
