5 let oapp = define `!f x y. oapp f x (SOME y) = f y /\ oapp f x NONE = x`;;
6 let odflt = new_definition `odflt = oapp I`;;
7 let obind = new_definition `obind f = oapp f NONE`;;
8 let omap = new_definition `omap f = obind (\x. SOME (f x))`;;
9 let pcomp = new_definition `pcomp f g x = obind f (g x)`;;
12 let odflt_alt = Sections.section_proof ["x"]
13 `(!y. odflt x (SOME y) = y) /\ odflt x NONE = x`
15 (((((use_arg_then2 ("odflt", [odflt]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("oapp", [oapp]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
19 let obind_alt = Sections.section_proof ["f"]
20 `obind f NONE = NONE /\ (!x. obind f (SOME x) = f x)`
22 (((((use_arg_then2 ("obind", [obind]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("oapp", [oapp]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
26 let omap_alt = Sections.section_proof ["f"]
27 `omap f NONE = NONE /\ (!x. omap f (SOME x) = SOME (f x))`
29 (((((use_arg_then2 ("omap", [omap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("obind", [obind]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("oapp", [oapp]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
33 let eq_sym = Sections.section_proof ["x";"y"]
36 ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
40 let eq_trans = Sections.section_proof ["x";"y";"z"]
41 `x = y ==> y = z ==> x = z`
43 ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
47 let f_equal = Sections.section_proof ["f";"x";"y"]
50 ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
54 let f_equal2 = Sections.section_proof ["f";"x1";"y1";"x2";"y2"]
55 `x1 = y1 ==> x2 = y2 ==> f x1 x2 = f y1 y2`
57 ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
61 let etrans = eq_trans;;
62 let congr1 = f_equal;;
63 let congr2 = f_equal2;;
66 let eq_ext = Sections.section_proof ["f";"g"]
67 `(!x. f x = g x) <=> f = g`
69 (((THENL) (split_tac) [(DISCH_THEN (fun snd_th -> (use_arg_then2 ("EQ_EXT", [EQ_EXT])) (thm_tac (match_mp_then snd_th MP_TAC)))); (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))]) THEN (done_tac));
72 (* Section Injections *)
73 Sections.begin_section "Injections";;
74 (Sections.add_section_var (mk_var ("f", (`:A -> R`))));;
75 let injective = new_definition `injective f <=> (!x1 x2. f x1 = f x2 ==> x1 = x2)`;;
76 let cancel = new_definition `cancel f g <=> !x. g (f x) = x`;;
77 let pcancel = new_definition `pcancel f g <=> !x. g (f x) = SOME x`;;
78 let ocancel = new_definition `ocancel g h <=> !x. oapp h x (g x) = x`;;
81 let can_pcan = Sections.section_proof ["g"]
82 `cancel f g ==> pcancel f (\y. SOME (g y))`
84 (((((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pcancel", [pcancel]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
88 let pcan_inj = Sections.section_proof ["g"]
89 `pcancel f g ==> injective f`
91 (((((use_arg_then2 ("pcancel", [pcancel]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("injective", [injective]))(thm_tac (new_rewrite [] []))))) THEN (move ["can"]) THEN (move ["x1"]) THEN (move ["x2"]) THEN (move ["f_eq"]));
92 ((((fun arg_tac -> (use_arg_then2 ("can", [])) (fun fst_arg -> (use_arg_then2 ("x2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then2 ("can", [])) (fun fst_arg -> (use_arg_then2 ("x1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (injectivity "option")))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
96 let can_inj = Sections.section_proof ["g"]
97 `cancel f g ==> injective f`
99 (((((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("injective", [injective]))(thm_tac (new_rewrite [] []))))) THEN (move ["can"]) THEN (move ["x1"]) THEN (move ["x2"]) THEN (move ["f_eq"]));
100 (((((fun arg_tac -> (use_arg_then2 ("can", [])) (fun fst_arg -> (use_arg_then2 ("x1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("can", [])) (fun fst_arg -> (use_arg_then2 ("x2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
104 let canLR = Sections.section_proof ["g";"x";"y"]
105 `cancel f g ==> x = f y ==> g x = y`
107 (((((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] [])))) THEN (move ["can"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
111 let canRL = Sections.section_proof ["g";"x";"y"]
112 `cancel f g ==> f x = y ==> x = g y`
114 (((((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] [])))) THEN (move ["can"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
117 (* Finalization of the section Injections *)
118 let can_pcan = Sections.finalize_theorem can_pcan;;
119 let pcan_inj = Sections.finalize_theorem pcan_inj;;
120 let can_inj = Sections.finalize_theorem can_inj;;
121 let canLR = Sections.finalize_theorem canLR;;
122 let canRL = Sections.finalize_theorem canRL;;
123 Sections.end_section "Injections";;
126 let some_inj = Sections.section_proof []
129 (((((use_arg_then2 ("injective", [injective]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (injectivity "option")))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
132 (* Section InjectionsTheory *)
133 Sections.begin_section "InjectionsTheory";;
134 (Sections.add_section_var (mk_var ("f", (`:B -> A`))); Sections.add_section_var (mk_var ("g", (`:B -> A`))));;
135 (Sections.add_section_var (mk_var ("h", (`:C -> B`))));;
138 let inj_id = Sections.section_proof []
141 (((((use_arg_then2 ("injective", [injective]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
144 (* Lemma inj_can_sym *)
145 let inj_can_sym = Sections.section_proof ["f'"]
146 `cancel f f' ==> injective f' ==> cancel f' f`
148 (((repeat_tactic 2 0 (((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("injective", [injective]))(thm_tac (new_rewrite [] []))))) THEN (move ["can1"]) THEN (move ["inj"]) THEN (move ["x"]));
149 ((((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("can1", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
153 let inj_comp = Sections.section_proof []
154 `injective f ==> injective h ==> injective (f o h)`
156 (((repeat_tactic 3 0 (((use_arg_then2 ("injective", [injective]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 2 0 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))))) THEN (move ["inj_f"]) THEN (move ["inj_h"]) THEN (move ["x1"]) THEN (move ["x2"]));
157 ((BETA_TAC THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("inj_f", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("inj_h", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
161 let can_comp = Sections.section_proof ["f'";"h'"]
162 `cancel f f' ==> cancel h h' ==> cancel (f o h) (h' o f')`
164 ((((repeat_tactic 3 0 (((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 2 0 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))))) THEN (move ["f_can"]) THEN (move ["h_can"]) THEN (move ["x"])) THEN (done_tac));
167 (* Lemma pcan_pcomp *)
168 let pcan_pcomp = Sections.section_proof ["f'";"h'"]
169 `pcancel f f' ==> pcancel h h' ==> pcancel (f o h) (pcomp h' f')`
171 ((((repeat_tactic 3 0 (((use_arg_then2 ("pcancel", [pcancel]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("pcomp", [pcomp]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("obind", [obind]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("oapp", [oapp]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
175 let eq_inj = Sections.section_proof []
176 `injective f ==> (!x. f x = g x) ==> injective g`
178 (((((use_arg_then2 ("eq_ext", [eq_ext]))(thm_tac (new_rewrite [] [])))) THEN (move ["inj"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
182 let eq_can = Sections.section_proof ["f'";"g'"]
183 `cancel f f' ==> (!x. f x = g x) ==> (!x. f' x = g' x) ==> cancel g g'`
185 (((repeat_tactic 1 9 (((use_arg_then2 ("eq_ext", [eq_ext]))(thm_tac (new_rewrite [] []))))) THEN (move ["can"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
188 (* Lemma inj_can_eq *)
189 let inj_can_eq = Sections.section_proof ["f'"]
190 `cancel f f' ==> injective f' ==> cancel g f' ==> f = g`
192 ((((repeat_tactic 2 0 (((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("injective", [injective]))(thm_tac (new_rewrite [] []))))) THEN (move ["f_can"]) THEN (move ["inj"]) THEN (move ["g_can"])) THEN ((((use_arg_then2 ("eq_ext", [eq_ext]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["x"])));
193 ((((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)) THEN (done_tac));
196 (* Finalization of the section InjectionsTheory *)
197 let inj_id = Sections.finalize_theorem inj_id;;
198 let inj_can_sym = Sections.finalize_theorem inj_can_sym;;
199 let inj_comp = Sections.finalize_theorem inj_comp;;
200 let can_comp = Sections.finalize_theorem can_comp;;
201 let pcan_pcomp = Sections.finalize_theorem pcan_pcomp;;
202 let eq_inj = Sections.finalize_theorem eq_inj;;
203 let eq_can = Sections.finalize_theorem eq_can;;
204 let inj_can_eq = Sections.finalize_theorem inj_can_eq;;
205 Sections.end_section "InjectionsTheory";;
207 (* Section Bijections *)
208 Sections.begin_section "Bijections";;
209 (Sections.add_section_var (mk_var ("f", (`:B -> A`))));;
210 let bijective = new_definition `bijective f <=> ?g. cancel f g /\ cancel g f`;;
211 (Sections.add_section_hyp "bijf" (`bijective f`));;
214 let bij_inj = Sections.section_proof []
217 ((((use_arg_then2 ("bijf", [])) (disch_tac [])) THEN (clear_assumption "bijf") THEN BETA_TAC) THEN ((((use_arg_then2 ("bijective", [bijective]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["g"])) THEN (case THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("can_inj", [can_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) THEN (done_tac));
220 (* Lemma bij_can_sym *)
221 let bij_can_sym = Sections.section_proof ["f'"]
222 `cancel f' f <=> cancel f f'`
224 ((THENL_FIRST) (split_tac) (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("inj_can_sym", [inj_can_sym])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("bij_inj", [bij_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac)));
225 ((((use_arg_then2 ("bijf", [])) (disch_tac [])) THEN (clear_assumption "bijf") THEN BETA_TAC) THEN ((((use_arg_then2 ("bijective", [bijective]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["g"])) THEN (case THEN ALL_TAC)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("cancel", [cancel]))(thm_tac (new_rewrite [] []))))) THEN (move ["gf"]) THEN (move ["fg"]) THEN (move ["f'f"]) THEN (move ["x"])));
226 (((((fun arg_tac -> (use_arg_then2 ("fg", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f'f", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
229 (* Lemma bij_can_eq *)
230 let bij_can_eq = Sections.section_proof ["f'";"f''"]
231 `cancel f f' ==> cancel f f'' ==> f' = f''`
233 (((((fun arg_tac -> (use_arg_then2 ("bij_can_sym", [bij_can_sym])) (fun fst_arg -> (use_arg_then2 ("f''", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("bij_can_sym", [bij_can_sym]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["can1"]) THEN (move ["can2"]));
234 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj_can_eq", [inj_can_eq])) (fun fst_arg -> (use_arg_then2 ("can1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("bij_inj", [bij_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("can2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
237 (* Finalization of the section Bijections *)
238 let bij_inj = Sections.finalize_theorem bij_inj;;
239 let bij_can_sym = Sections.finalize_theorem bij_can_sym;;
240 let bij_can_eq = Sections.finalize_theorem bij_can_eq;;
241 Sections.end_section "Bijections";;
243 (* Section BijectionsTheory *)
244 Sections.begin_section "BijectionsTheory";;
245 (Sections.add_section_var (mk_var ("f", (`:BB -> AA`))));;
246 (Sections.add_section_var (mk_var ("h", (`:CC -> BB`))));;
249 let eq_bij = Sections.section_proof []
250 `bijective f ==> !g. (!x. f x = g x) ==> bijective g`
252 (((((use_arg_then2 ("eq_ext", [eq_ext]))(thm_tac (new_rewrite [] [])))) THEN (move ["bij"]) THEN (move ["g"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
256 let bij_comp = Sections.section_proof []
257 `bijective f ==> bijective h ==> bijective (f o h)`
259 ((repeat_tactic 3 0 (((use_arg_then2 ("bijective", [bijective]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["g"])) THEN (case THEN ((move ["can_fg"]) THEN (move ["can_gf"]))) THEN (case THEN ((move ["r"]) THEN (case THEN ((move ["can_hr"]) THEN (move ["can_rh"]))))));
260 (((fun arg_tac -> arg_tac (Arg_term (`r o g`))) (term_tac exists_tac)) THEN (split_tac));
261 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("can_comp", [can_comp])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("g", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("r", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
262 ((((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("can_fg", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN BETA_TAC) THEN (DISCH_THEN apply_tac) THEN (done_tac));
263 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("can_comp", [can_comp])) (fun fst_arg -> (use_arg_then2 ("r", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("g", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
264 ((((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("can_rh", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN BETA_TAC) THEN (DISCH_THEN apply_tac) THEN (done_tac));
267 (* Lemma bij_can_bij *)
268 let bij_can_bij = Sections.section_proof []
269 `bijective f ==> !f'. cancel f f' ==> bijective f'`
271 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("bij_can_sym", [bij_can_sym])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["can_sym"]) THEN (move ["f'"]) THEN (move ["can_ff'"])) THEN (((use_arg_then2 ("bijective", [bijective]))(thm_tac (new_rewrite [] [])))));
272 (((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("can_sym", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
275 (* Finalization of the section BijectionsTheory *)
276 let eq_bij = Sections.finalize_theorem eq_bij;;
277 let bij_comp = Sections.finalize_theorem bij_comp;;
278 let bij_can_bij = Sections.finalize_theorem bij_can_bij;;
279 Sections.end_section "BijectionsTheory";;
281 (* Section Involutions *)
282 Sections.begin_section "Involutions";;
283 (Sections.add_section_var (mk_var ("f", (`:A -> A`))));;
284 let involutive = new_definition `involutive f <=> cancel f f`;;
285 (Sections.add_section_hyp "Hf" (`involutive f`));;
288 let inv_inj = Sections.section_proof []
291 ((((use_arg_then2 ("Hf", [])) (disch_tac [])) THEN (clear_assumption "Hf") THEN BETA_TAC) THEN ((((use_arg_then2 ("involutive", [involutive]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("can_inj", [can_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
295 let inv_bij = Sections.section_proof []
298 ((((use_arg_then2 ("bijective", [bijective]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("Hf", [])) (disch_tac [])) THEN (clear_assumption "Hf") THEN BETA_TAC) THEN (((use_arg_then2 ("involutive", [involutive]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
301 (* Finalization of the section Involutions *)
302 let inv_inj = Sections.finalize_theorem inv_inj;;
303 let inv_bij = Sections.finalize_theorem inv_bij;;
304 Sections.end_section "Involutions";;
306 (* Section OperationProperties *)
307 Sections.begin_section "OperationProperties";;
309 (* Section SopTisR *)
310 Sections.begin_section "SopTisR";;
311 let left_inverse = new_definition `left_inverse e inv op = !x. op (inv x) x = e`;;
312 let right_inverse = new_definition `right_inverse e inv op = !x. op x (inv x) = e`;;
313 let left_injective = new_definition `left_injective op = !x. injective (\y. op y x)`;;
314 let right_injective = new_definition `right_injective op = !y. injective (op y)`;;
316 (* Finalization of the section SopTisR *)
317 Sections.end_section "SopTisR";;
319 (* Section SopTisS *)
320 Sections.begin_section "SopTisS";;
321 let right_id = new_definition `right_id e op = !x. op x e = x`;;
322 let left_zero = new_definition `left_zero z op = !x. op z x = z`;;
323 let right_commutative = new_definition
324 `right_commutative op = !x y z. op (op x y) z = op (op x z) y`;;
325 let left_distributive = new_definition
326 `left_distributive op add = !x y z. op (add x y) z = add (op x z) (op y z)`;;
327 let right_loop = new_definition
328 `right_loop inv op = !y. cancel (\x. op x y) (\x. op x (inv y))`;;
329 let rev_right_loop = new_definition
330 `rev_right_loop inv op = !y. cancel (\x. op x (inv y)) (\x. op x y)`;;
332 (* Finalization of the section SopTisS *)
333 Sections.end_section "SopTisS";;
335 (* Section SopTisT *)
336 Sections.begin_section "SopTisT";;
337 let left_id = new_definition `left_id e op = !x. op e x = x`;;
338 let right_zero = new_definition `right_zero z op = !x. op x z = z`;;
339 let left_commutative = new_definition
340 `left_commutative op = !x y z. op x (op y z) = op y (op x z)`;;
341 let right_distributive = new_definition
342 `right_distributive op add = !x y z. op x (add y z) = add (op x y) (op x z)`;;
343 let left_loop = new_definition
344 `left_loop inv op = !x. cancel (op x) (op (inv x))`;;
345 let rev_left_loop = new_definition
346 `rev_left_loop inv op = !x. cancel (op (inv x)) (op x)`;;
348 (* Finalization of the section SopTisT *)
349 Sections.end_section "SopTisT";;
351 (* Section SopSisT *)
352 Sections.begin_section "SopSisT";;
353 let self_inverse = new_definition `self_inverse e op = !x. op x x = e`;;
354 let commutative = new_definition `commutative op = !x y. op x y = op y x`;;
356 (* Finalization of the section SopSisT *)
357 Sections.end_section "SopSisT";;
359 (* Section SopSisS *)
360 Sections.begin_section "SopSisS";;
361 let idempotent = new_definition `idempotent op = !x. op x x = x`;;
362 let associative = new_definition `associative op = !x y z. op x (op y z) = op (op x y) z`;;
364 (* Finalization of the section SopSisS *)
365 Sections.end_section "SopSisS";;
367 (* Finalization of the section OperationProperties *)
368 Sections.end_section "OperationProperties";;
370 (* Close the module *)