60 val recs = thms "prod.recs"; |
60 val recs = thms "prod.recs"; |
61 val simps = thms "prod.simps"; |
61 val simps = thms "prod.simps"; |
62 val size = thms "prod.size"; |
62 val size = thms "prod.size"; |
63 end; |
63 end; |
64 |
64 |
|
65 structure option = |
|
66 struct |
|
67 val distinct = thms "option.distinct"; |
|
68 val inject = thms "option.inject"; |
|
69 val exhaust = thm "option.exhaust"; |
|
70 val cases = thms "option.cases"; |
|
71 val split = thm "option.split"; |
|
72 val split_asm = thm "option.split_asm"; |
|
73 val induct = thm "option.induct"; |
|
74 val recs = thms "option.recs"; |
|
75 val simps = thms "option.simps"; |
|
76 val size = thms "option.size"; |
|
77 end; |
65 |
78 |
66 (** sum_case -- the selection operator for sums **) |
79 val elem_o2s = thm "elem_o2s"; |
67 |
80 val not_None_eq = thm "not_None_eq"; |
68 (*compatibility*) |
81 val not_Some_eq = thm "not_Some_eq"; |
69 val [sum_case_Inl, sum_case_Inr] = sum.cases; |
82 val o2s_empty_eq = thm "o2s_empty_eq"; |
70 bind_thm ("sum_case_Inl", sum_case_Inl); |
83 val option_caseE = thm "option_caseE"; |
71 bind_thm ("sum_case_Inr", sum_case_Inr); |
84 val option_map_None = thm "option_map_None"; |
72 |
85 val option_map_Some = thm "option_map_Some"; |
73 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
86 val option_map_def = thm "option_map_def"; |
74 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
87 val option_map_eq_Some = thm "option_map_eq_Some"; |
75 etac ssubst, rtac sum_case_Inl, |
88 val option_map_o_sum_case = thm "option_map_o_sum_case"; |
76 etac ssubst, rtac sum_case_Inr]); |
89 val ospec = thm "ospec"; |
77 qed "surjective_sum"; |
90 val sum_case_inject = thm "sum_case_inject"; |
78 |
91 val sum_case_weak_cong = thm "sum_case_weak_cong"; |
79 (*Prevents simplification of f and g: much faster*) |
92 val surjective_sum = thm "surjective_sum"; |
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"; |
|