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;


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