formal_ineqs/lib/ssrfun-compiled.hl

   1 let oapp = define `!f x y. oapp f x (SOME y) = f y /\ oapp f x NONE = x`;;
   2 let odflt = new_definition `odflt = oapp I`;;
   3 let obind = new_definition `obind f = oapp f NONE`;;
   4 let omap = new_definition `omap f = obind (\x. SOME (f x))`;;
   5 let pcomp = new_definition `pcomp f g x = obind f (g x)`;;
   6
   7 (* Lemma odflt_alt *)
   8 let odflt_alt = section_proof ["x"] `(!y. odflt x (SOME y) = y) /\ odflt x NONE = x` [
   9    (((((use_arg_then "odflt")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "oapp")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "I_THM")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  10 ];;
  11
  12 (* Lemma obind_alt *)
  13 let obind_alt = section_proof ["f"] `obind f NONE = NONE /\ (!x. obind f (SOME x) = f x)` [
  14    (((((use_arg_then "obind")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "oapp")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
  15 ];;
  16
  17 (* Lemma omap_alt *)
  18 let omap_alt = section_proof ["f"] `omap f NONE = NONE /\ (!x. omap f (SOME x) = SOME (f x))` [
  19    (((((use_arg_then "omap")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "obind")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "oapp")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
  20 ];;
  21
  22 (* Lemma eq_sym *)
  23 let eq_sym = section_proof ["x";"y"] `x = y ==> y = x` [
  24    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  25 ];;
  26
  27 (* Lemma eq_trans *)
  28 let eq_trans = section_proof ["x";"y";"z"] `x = y ==> y = z ==> x = z` [
  29    ((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));
  30 ];;
  31
  32 (* Lemma f_equal *)
  33 let f_equal = section_proof ["f";"x";"y"] `x = y ==> f x = f y` [
  34    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  35 ];;
  36
  37 (* Lemma f_equal2 *)
  38 let f_equal2 = section_proof ["f";"x1";"y1";"x2";"y2"] `x1 = y1 ==> x2 = y2 ==> f x1 x2 = f y1 y2` [
  39    ((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));
  40 ];;
  41 let erefl = eq_sym;;
  42 let esym = eq_sym;;
  43 let etrans = eq_trans;;
  44 let congr1 = f_equal;;
  45 let congr2 = f_equal2;;
  46
  47 (* Lemma eq_ext *)
  48 let eq_ext = section_proof ["f";"g"] `(!x. f x = g x) <=> f = g` [
  49    (((THENL) (split_tac) [(DISCH_THEN (fun snd_th -> (use_arg_then "EQ_EXT") (thm_tac (match_mp_then snd_th MP_TAC)))); (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))]) THEN (done_tac));
  50 ];;
  51
  52 (* Section Injections *)
  53 begin_section "Injections";;
  54 (add_section_var (mk_var ("f", (`:A -> R`))));;
  55 let injective = new_definition `injective f <=> (!x1 x2. f x1 = f x2 ==> x1 = x2)`;;
  56 let cancel = new_definition `cancel f g <=> !x. g (f x) = x`;;
  57 let pcancel = new_definition `pcancel f g <=> !x. g (f x) = SOME x`;;
  58 let ocancel = new_definition `ocancel g h <=> !x. oapp h x (g x) = x`;;
  59
  60 (* Lemma can_pcan *)
  61 let can_pcan = section_proof ["g"] `cancel f g ==> pcancel f (\y. SOME (g y))` [
  62    (((((use_arg_then "cancel")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "pcancel")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
  63 ];;
  64
  65 (* Lemma pcan_inj *)
  66 let pcan_inj = section_proof ["g"] `pcancel f g ==> injective f` [
  67    (((((use_arg_then "pcancel")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "injective")(thm_tac (new_rewrite [] []))))) THEN (move ["can"]) THEN (move ["x1"]) THEN (move ["x2"]) THEN (move ["f_eq"]));
  68    ((((fun arg_tac -> (use_arg_then "can") (fun fst_arg -> (use_arg_then "x2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then "can") (fun fst_arg -> (use_arg_then "x1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then "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));
  69 ];;
  70
  71 (* Lemma can_inj *)
  72 let can_inj = section_proof ["g"] `cancel f g ==> injective f` [
  73    (((((use_arg_then "cancel")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "injective")(thm_tac (new_rewrite [] []))))) THEN (move ["can"]) THEN (move ["x1"]) THEN (move ["x2"]) THEN (move ["f_eq"]));
  74    (((((fun arg_tac -> (use_arg_then "can") (fun fst_arg -> (use_arg_then "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_then "can") (fun fst_arg -> (use_arg_then "x2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "f_eq")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  75 ];;
  76
  77 (* Lemma canLR *)
  78 let canLR = section_proof ["g";"x";"y"] `cancel f g ==> x = f y ==> g x = y` [
  79    (((((use_arg_then "cancel")(thm_tac (new_rewrite [] [])))) THEN (move ["can"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  80 ];;
  81
  82 (* Lemma canRL *)
  83 let canRL = section_proof ["g";"x";"y"] `cancel f g ==> f x = y ==> x = g y` [
  84    (((((use_arg_then "cancel")(thm_tac (new_rewrite [] [])))) THEN (move ["can"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
  85 ];;
  86
  87 (* Finalization of the section Injections *)
  88 let can_pcan = finalize_theorem can_pcan;;
  89 let pcan_inj = finalize_theorem pcan_inj;;
  90 let can_inj = finalize_theorem can_inj;;
  91 let canLR = finalize_theorem canLR;;
  92 let canRL = finalize_theorem canRL;;
  93 end_section "Injections";;
  94
  95 (* Lemma some_inj *)
  96 let some_inj = section_proof [] `injective SOME` [
  97    (((((use_arg_then "injective")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (injectivity "option")))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  98 ];;
  99
 100 (* Section InjectionsTheory *)
 101 begin_section "InjectionsTheory";;
 102 (add_section_var (mk_var ("f", (`:B -> A`))); add_section_var (mk_var ("g", (`:B -> A`))));;
 103 (add_section_var (mk_var ("h", (`:C -> B`))));;
 104
 105 (* Lemma inj_id *)
 106 let inj_id = section_proof [] `injective I` [
 107    (((((use_arg_then "injective")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "I_THM")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 108 ];;
 109
 110 (* Lemma inj_can_sym *)
 111 let inj_can_sym = section_proof ["f'"] `cancel f f' ==> injective f' ==> cancel f' f` [
 112    (((repeat_tactic 2 0 (((use_arg_then "cancel")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "injective")(thm_tac (new_rewrite [] []))))) THEN (move ["can1"]) THEN (move ["inj"]) THEN (move ["x"]));
 113    ((((use_arg_then "inj") (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "can1")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 114 ];;
 115
 116 (* Lemma inj_comp *)
 117 let inj_comp = section_proof [] `injective f ==> injective h ==> injective (f o h)` [
 118    (((repeat_tactic 3 0 (((use_arg_then "injective")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 2 0 (((use_arg_then "o_THM")(thm_tac (new_rewrite [] [])))))) THEN (move ["inj_f"]) THEN (move ["inj_h"]) THEN (move ["x1"]) THEN (move ["x2"]));
 119    ((BETA_TAC THEN (DISCH_THEN (fun snd_th -> (use_arg_then "inj_f") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then "inj_h") (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
 120 ];;
 121
 122 (* Lemma can_comp *)
 123 let can_comp = section_proof ["f'";"h'"] `cancel f f' ==> cancel h h' ==> cancel (f o h) (h' o f')` [
 124    ((((repeat_tactic 3 0 (((use_arg_then "cancel")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 2 0 (((use_arg_then "o_THM")(thm_tac (new_rewrite [] [])))))) THEN (move ["f_can"]) THEN (move ["h_can"]) THEN (move ["x"])) THEN (done_tac));
 125 ];;
 126
 127 (* Lemma pcan_pcomp *)
 128 let pcan_pcomp = section_proof ["f'";"h'"] `pcancel f f' ==> pcancel h h' ==> pcancel (f o h) (pcomp h' f')` [
 129    ((((repeat_tactic 3 0 (((use_arg_then "pcancel")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "pcomp")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "o_THM")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then "obind")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oapp")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 130 ];;
 131
 132 (* Lemma eq_inj *)
 133 let eq_inj = section_proof [] `injective f ==> (!x. f x = g x) ==> injective g` [
 134    (((((use_arg_then "eq_ext")(thm_tac (new_rewrite [] [])))) THEN (move ["inj"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 135 ];;
 136
 137 (* Lemma eq_can *)
 138 let eq_can = section_proof ["f'";"g'"] `cancel f f' ==> (!x. f x = g x) ==> (!x. f' x = g' x) ==> cancel g g'` [
 139    (((repeat_tactic 1 9 (((use_arg_then "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));
 140 ];;
 141
 142 (* Lemma inj_can_eq *)
 143 let inj_can_eq = section_proof ["f'"] `cancel f f' ==> injective f' ==> cancel g f' ==> f = g` [
 144    ((((repeat_tactic 2 0 (((use_arg_then "cancel")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "injective")(thm_tac (new_rewrite [] []))))) THEN (move ["f_can"]) THEN (move ["inj"]) THEN (move ["g_can"])) THEN ((((use_arg_then "eq_ext")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["x"])));
 145    ((((use_arg_then "inj") (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)) THEN (done_tac));
 146 ];;
 147
 148 (* Finalization of the section InjectionsTheory *)
 149 let inj_id = finalize_theorem inj_id;;
 150 let inj_can_sym = finalize_theorem inj_can_sym;;
 151 let inj_comp = finalize_theorem inj_comp;;
 152 let can_comp = finalize_theorem can_comp;;
 153 let pcan_pcomp = finalize_theorem pcan_pcomp;;
 154 let eq_inj = finalize_theorem eq_inj;;
 155 let eq_can = finalize_theorem eq_can;;
 156 let inj_can_eq = finalize_theorem inj_can_eq;;
 157 end_section "InjectionsTheory";;
 158
 159 (* Section Bijections *)
 160 begin_section "Bijections";;
 161 (add_section_var (mk_var ("f", (`:B -> A`))));;
 162 let bijective = new_definition `bijective f <=> ?g. cancel f g /\ cancel g f`;;
 163 (add_section_hyp "bijf" (`bijective f`));;
 164
 165 (* Lemma bij_inj *)
 166 let bij_inj = section_proof [] `injective f` [
 167    ((((use_arg_then "bijf") (disch_tac [])) THEN (clear_assumption "bijf") THEN BETA_TAC) THEN ((((use_arg_then "bijective")(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["g"])) THEN (case THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "can_inj") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 168 ];;
 169
 170 (* Lemma bij_can_sym *)
 171 let bij_can_sym = section_proof ["f'"] `cancel f' f <=> cancel f f'` [
 172    ((THENL_FIRST) (split_tac) (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "bij_inj") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac)));
 173    ((((use_arg_then "bijf") (disch_tac [])) THEN (clear_assumption "bijf") THEN BETA_TAC) THEN ((((use_arg_then "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_then "cancel")(thm_tac (new_rewrite [] []))))) THEN (move ["gf"]) THEN (move ["fg"]) THEN (move ["f'f"]) THEN (move ["x"])));
 174    (((((fun arg_tac -> (use_arg_then "fg") (fun fst_arg -> (use_arg_then "x") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "f'f")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 175 ];;
 176
 177 (* Lemma bij_can_eq *)
 178 let bij_can_eq = section_proof ["f'";"f''"] `cancel f f' ==> cancel f f'' ==> f' = f''` [
 179    (((((fun arg_tac -> (use_arg_then "bij_can_sym") (fun fst_arg -> (use_arg_then "f''") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "bij_can_sym")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["can1"]) THEN (move ["can2"]));
 180    ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "inj_can_eq") (fun fst_arg -> (use_arg_then "can1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "bij_inj") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "can2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
 181 ];;
 182
 183 (* Finalization of the section Bijections *)
 184 let bij_inj = finalize_theorem bij_inj;;
 185 let bij_can_sym = finalize_theorem bij_can_sym;;
 186 let bij_can_eq = finalize_theorem bij_can_eq;;
 187 end_section "Bijections";;
 188
 189 (* Section BijectionsTheory *)
 190 begin_section "BijectionsTheory";;
 191 (add_section_var (mk_var ("f", (`:BB -> AA`))));;
 192 (add_section_var (mk_var ("h", (`:CC -> BB`))));;
 193
 194 (* Lemma eq_bij *)
 195 let eq_bij = section_proof [] `bijective f ==> !g. (!x. f x = g x) ==> bijective g` [
 196    (((((use_arg_then "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));
 197 ];;
 198
 199 (* Lemma bij_comp *)
 200 let bij_comp = section_proof [] `bijective f ==> bijective h ==> bijective (f o h)` [
 201    ((repeat_tactic 3 0 (((use_arg_then "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"]))))));
 202    (((fun arg_tac -> arg_tac (Arg_term (`r o g`))) (term_tac exists_tac)) THEN (split_tac));
 203    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "can_comp") (fun fst_arg -> (use_arg_then "f") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "h") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "g") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "r") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
 204    ((((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then "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));
 205    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "can_comp") (fun fst_arg -> (use_arg_then "r") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "g") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "h") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "f") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
 206    ((((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then "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));
 207 ];;
 208
 209 (* Lemma bij_can_bij *)
 210 let bij_can_bij = section_proof [] `bijective f ==> !f'. cancel f f' ==> bijective f'` [
 211    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "bijective")(thm_tac (new_rewrite [] [])))));
 212    (((use_arg_then "f") (term_tac exists_tac)) THEN (((use_arg_then "can_sym")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 213 ];;
 214
 215 (* Finalization of the section BijectionsTheory *)
 216 let eq_bij = finalize_theorem eq_bij;;
 217 let bij_comp = finalize_theorem bij_comp;;
 218 let bij_can_bij = finalize_theorem bij_can_bij;;
 219 end_section "BijectionsTheory";;
 220
 221 (* Section Involutions *)
 222 begin_section "Involutions";;
 223 (add_section_var (mk_var ("f", (`:A -> A`))));;
 224 let involutive = new_definition `involutive f <=> cancel f f`;;
 225 (add_section_hyp "Hf" (`involutive f`));;
 226
 227 (* Lemma inv_inj *)
 228 let inv_inj = section_proof [] `injective f` [
 229    ((((use_arg_then "Hf") (disch_tac [])) THEN (clear_assumption "Hf") THEN BETA_TAC) THEN ((((use_arg_then "involutive")(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then "can_inj") (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
 230 ];;
 231
 232 (* Lemma inv_bij *)
 233 let inv_bij = section_proof [] `bijective f` [
 234    ((((use_arg_then "bijective")(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then "f") (term_tac exists_tac)) THEN (((use_arg_then "Hf") (disch_tac [])) THEN (clear_assumption "Hf") THEN BETA_TAC) THEN (((use_arg_then "involutive")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 235 ];;
 236
 237 (* Finalization of the section Involutions *)
 238 let inv_inj = finalize_theorem inv_inj;;
 239 let inv_bij = finalize_theorem inv_bij;;
 240 end_section "Involutions";;
 241
 242 (* Section OperationProperties *)
 243 begin_section "OperationProperties";;
 244
 245 (* Section SopTisR *)
 246 begin_section "SopTisR";;
 247 let left_inverse = new_definition `left_inverse e inv op = !x. op (inv x) x = e`;;
 248 let right_inverse = new_definition `right_inverse e inv op = !x. op x (inv x) = e`;;
 249 let left_injective = new_definition `left_injective op = !x. injective (\y. op y x)`;;
 250 let right_injective = new_definition `right_injective op = !y. injective (op y)`;;
 251
 252 (* Finalization of the section SopTisR *)
 253 end_section "SopTisR";;
 254
 255 (* Section SopTisS *)
 256 begin_section "SopTisS";;
 257 let right_id = new_definition `right_id e op = !x. op x e = x`;;
 258 let left_zero = new_definition `left_zero z op = !x. op z x = z`;;
 259 let right_commutative = new_definition
 260         `right_commutative op = !x y z. op (op x y) z = op (op x z) y`;;
 261 let left_distributive = new_definition
 262         `left_distributive op add = !x y z. op (add x y) z = add (op x z) (op y z)`;;
 263 let right_loop = new_definition
 264         `right_loop inv op = !y. cancel (\x. op x y) (\x. op x (inv y))`;;
 265 let rev_right_loop = new_definition
 266         `rev_right_loop inv op = !y. cancel (\x. op x (inv y)) (\x. op x y)`;;
 267
 268 (* Finalization of the section SopTisS *)
 269 end_section "SopTisS";;
 270
 271 (* Section SopTisT *)
 272 begin_section "SopTisT";;
 273 let left_id = new_definition `left_id e op = !x. op e x = x`;;
 274 let right_zero = new_definition `right_zero z op = !x. op x z = z`;;
 275 let left_commutative = new_definition
 276         `left_commutative op = !x y z. op x (op y z) = op y (op x z)`;;
 277 let right_distributive = new_definition
 278         `right_distributive op add = !x y z. op x (add y z) = add (op x y) (op x z)`;;
 279 let left_loop = new_definition
 280         `left_loop inv op = !x. cancel (op x) (op (inv x))`;;
 281 let rev_left_loop = new_definition
 282         `rev_left_loop inv op = !x. cancel (op (inv x)) (op x)`;;
 283
 284 (* Finalization of the section SopTisT *)
 285 end_section "SopTisT";;
 286
 287 (* Section SopSisT *)
 288 begin_section "SopSisT";;
 289 let self_inverse = new_definition `self_inverse e op = !x. op x x = e`;;
 290 let commutative = new_definition `commutative op = !x y. op x y = op y x`;;
 291
 292 (* Finalization of the section SopSisT *)
 293 end_section "SopSisT";;
 294
 295 (* Section SopSisS *)
 296 begin_section "SopSisS";;
 297 let idempotent = new_definition `idempotent op = !x. op x x = x`;;
 298 let associative = new_definition `associative op = !x y z. op x (op y z) = op (op x y) z`;;
 299
 300 (* Finalization of the section SopSisS *)
 301 end_section "SopSisS";;
 302
 303 (* Finalization of the section OperationProperties *)
 304 end_section "OperationProperties";;