7293

1 
(* Title: HOL/Datatype.ML


2 
ID: $Id$

11954

3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen


4 
License: GPL (GNU GENERAL PUBLIC LICENSE)

7293

5 
*)


6 

11954

7 
(** legacy ML bindings **)


8 


9 
structure bool =


10 
struct


11 
val distinct = thms "bool.distinct";


12 
val inject = thms "bool.inject";


13 
val exhaust = thm "bool.exhaust";


14 
val cases = thms "bool.cases";


15 
val split = thm "bool.split";


16 
val split_asm = thm "bool.split_asm";


17 
val induct = thm "bool.induct";


18 
val recs = thms "bool.recs";


19 
val simps = thms "bool.simps";


20 
val size = thms "bool.size";


21 
end;


22 


23 
structure sum =


24 
struct


25 
val distinct = thms "sum.distinct";


26 
val inject = thms "sum.inject";


27 
val exhaust = thm "sum.exhaust";


28 
val cases = thms "sum.cases";


29 
val split = thm "sum.split";


30 
val split_asm = thm "sum.split_asm";


31 
val induct = thm "sum.induct";


32 
val recs = thms "sum.recs";


33 
val simps = thms "sum.simps";


34 
val size = thms "sum.size";


35 
end;


36 


37 
structure unit =


38 
struct


39 
val distinct = thms "unit.distinct";


40 
val inject = thms "unit.inject";


41 
val exhaust = thm "unit.exhaust";


42 
val cases = thms "unit.cases";


43 
val split = thm "unit.split";


44 
val split_asm = thm "unit.split_asm";


45 
val induct = thm "unit.induct";


46 
val recs = thms "unit.recs";


47 
val simps = thms "unit.simps";


48 
val size = thms "unit.size";


49 
end;


50 


51 
structure prod =


52 
struct


53 
val distinct = thms "prod.distinct";


54 
val inject = thms "prod.inject";


55 
val exhaust = thm "prod.exhaust";


56 
val cases = thms "prod.cases";


57 
val split = thm "prod.split";


58 
val split_asm = thm "prod.split_asm";


59 
val induct = thm "prod.induct";


60 
val recs = thms "prod.recs";


61 
val simps = thms "prod.simps";


62 
val size = thms "prod.size";


63 
end;


64 


65 

7293

66 
(** sum_case  the selection operator for sums **)


67 


68 
(*compatibility*)


69 
val [sum_case_Inl, sum_case_Inr] = sum.cases;

9108

70 
bind_thm ("sum_case_Inl", sum_case_Inl);


71 
bind_thm ("sum_case_Inr", sum_case_Inr);

7293

72 


73 
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";

11954

74 
by (EVERY1 [res_inst_tac [("s","s")] sumE,

7293

75 
etac ssubst, rtac sum_case_Inl,


76 
etac ssubst, rtac sum_case_Inr]);


77 
qed "surjective_sum";


78 


79 
(*Prevents simplification of f and g: much faster*)


80 
Goal "s=t ==> sum_case f g s = sum_case f g t";


81 
by (etac arg_cong 1);


82 
qed "sum_case_weak_cong";


83 


84 
val [p1,p2] = Goal


85 
"[ sum_case f1 f2 = sum_case g1 g2; \


86 
\ [ f1 = g1; f2 = g2 ] ==> P ] \


87 
\ ==> P";


88 
by (rtac p2 1);


89 
by (rtac ext 1);


90 
by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);


91 
by (Asm_full_simp_tac 1);


92 
by (rtac ext 1);


93 
by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);


94 
by (Asm_full_simp_tac 1);


95 
qed "sum_case_inject";
