jHOLLight/Examples/ssrfun-compiled.hl

   1
   2 (* Module Ssrfun*)
   3 module Ssrfun = struct
   4
   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)`;;
  10
  11 (* Lemma odflt_alt *)
  12 let odflt_alt = Sections.section_proof ["x"]
  13 `(!y. odflt x (SOME y) = y) /\ odflt x NONE = x`
  14 [
  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));
  16 ];;
  17
  18 (* Lemma obind_alt *)
  19 let obind_alt = Sections.section_proof ["f"]
  20 `obind f NONE = NONE /\ (!x. obind f (SOME x) = f x)`
  21 [
  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));
  23 ];;
  24
  25 (* Lemma omap_alt *)
  26 let omap_alt = Sections.section_proof ["f"]
  27 `omap f NONE = NONE /\ (!x. omap f (SOME x) = SOME (f x))`
  28 [
  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));
  30 ];;
  31
  32 (* Lemma eq_sym *)
  33 let eq_sym = Sections.section_proof ["x";"y"]
  34 `x = y ==> y = x`
  35 [
  36    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  37 ];;
  38
  39 (* Lemma eq_trans *)
  40 let eq_trans = Sections.section_proof ["x";"y";"z"]
  41 `x = y ==> y = z ==> x = z`
  42 [
  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));
  44 ];;
  45
  46 (* Lemma f_equal *)
  47 let f_equal = Sections.section_proof ["f";"x";"y"]
  48 `x = y ==> f x = f y`
  49 [
  50    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  51 ];;
  52
  53 (* Lemma f_equal2 *)
  54 let f_equal2 = Sections.section_proof ["f";"x1";"y1";"x2";"y2"]
  55 `x1 = y1 ==> x2 = y2 ==> f x1 x2 = f y1 y2`
  56 [
  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));
  58 ];;
  59 let erefl = eq_sym;;
  60 let esym = eq_sym;;
  61 let etrans = eq_trans;;
  62 let congr1 = f_equal;;
  63 let congr2 = f_equal2;;
  64
  65 (* Lemma eq_ext *)
  66 let eq_ext = Sections.section_proof ["f";"g"]
  67 `(!x. f x = g x) <=> f = g`
  68 [
  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));
  70 ];;
  71
  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`;;
  79
  80 (* Lemma can_pcan *)
  81 let can_pcan = Sections.section_proof ["g"]
  82 `cancel f g ==> pcancel f (\y. SOME (g y))`
  83 [
  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));
  85 ];;
  86
  87 (* Lemma pcan_inj *)
  88 let pcan_inj = Sections.section_proof ["g"]
  89 `pcancel f g ==> injective f`
  90 [
  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));
  93 ];;
  94
  95 (* Lemma can_inj *)
  96 let can_inj = Sections.section_proof ["g"]
  97 `cancel f g ==> injective f`
  98 [
  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));
 101 ];;
 102
 103 (* Lemma canLR *)
 104 let canLR = Sections.section_proof ["g";"x";"y"]
 105 `cancel f g ==> x = f y ==> g x = y`
 106 [
 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));
 108 ];;
 109
 110 (* Lemma canRL *)
 111 let canRL = Sections.section_proof ["g";"x";"y"]
 112 `cancel f g ==> f x = y ==> x = g y`
 113 [
 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));
 115 ];;
 116
 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";;
 124
 125 (* Lemma some_inj *)
 126 let some_inj = Sections.section_proof []
 127 `injective SOME`
 128 [
 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));
 130 ];;
 131
 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`))));;
 136
 137 (* Lemma inj_id *)
 138 let inj_id = Sections.section_proof []
 139 `injective I`
 140 [
 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));
 142 ];;
 143
 144 (* Lemma inj_can_sym *)
 145 let inj_can_sym = Sections.section_proof ["f'"]
 146 `cancel f f' ==> injective f' ==> cancel f' f`
 147 [
 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));
 150 ];;
 151
 152 (* Lemma inj_comp *)
 153 let inj_comp = Sections.section_proof []
 154 `injective f ==> injective h ==> injective (f o h)`
 155 [
 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));
 158 ];;
 159
 160 (* Lemma can_comp *)
 161 let can_comp = Sections.section_proof ["f'";"h'"]
 162 `cancel f f' ==> cancel h h' ==> cancel (f o h) (h' o f')`
 163 [
 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));
 165 ];;
 166
 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')`
 170 [
 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));
 172 ];;
 173
 174 (* Lemma eq_inj *)
 175 let eq_inj = Sections.section_proof []
 176 `injective f ==> (!x. f x = g x) ==> injective g`
 177 [
 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));
 179 ];;
 180
 181 (* Lemma eq_can *)
 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'`
 184 [
 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));
 186 ];;
 187
 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`
 191 [
 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));
 194 ];;
 195
 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";;
 206
 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`));;
 212
 213 (* Lemma bij_inj *)
 214 let bij_inj = Sections.section_proof []
 215 `injective f`
 216 [
 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));
 218 ];;
 219
 220 (* Lemma bij_can_sym *)
 221 let bij_can_sym = Sections.section_proof ["f'"]
 222 `cancel f' f <=> cancel f f'`
 223 [
 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));
 227 ];;
 228
 229 (* Lemma bij_can_eq *)
 230 let bij_can_eq = Sections.section_proof ["f'";"f''"]
 231 `cancel f f' ==> cancel f f'' ==> f' = f''`
 232 [
 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));
 235 ];;
 236
 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";;
 242
 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`))));;
 247
 248 (* Lemma eq_bij *)
 249 let eq_bij = Sections.section_proof []
 250 `bijective f ==> !g. (!x. f x = g x) ==> bijective g`
 251 [
 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));
 253 ];;
 254
 255 (* Lemma bij_comp *)
 256 let bij_comp = Sections.section_proof []
 257 `bijective f ==> bijective h ==> bijective (f o h)`
 258 [
 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));
 265 ];;
 266
 267 (* Lemma bij_can_bij *)
 268 let bij_can_bij = Sections.section_proof []
 269 `bijective f ==> !f'. cancel f f' ==> bijective f'`
 270 [
 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));
 273 ];;
 274
 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";;
 280
 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`));;
 286
 287 (* Lemma inv_inj *)
 288 let inv_inj = Sections.section_proof []
 289 `injective f`
 290 [
 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));
 292 ];;
 293
 294 (* Lemma inv_bij *)
 295 let inv_bij = Sections.section_proof []
 296 `bijective f`
 297 [
 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));
 299 ];;
 300
 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";;
 305
 306 (* Section OperationProperties *)
 307 Sections.begin_section "OperationProperties";;
 308
 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)`;;
 315
 316 (* Finalization of the section SopTisR *)
 317 Sections.end_section "SopTisR";;
 318
 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)`;;
 331
 332 (* Finalization of the section SopTisS *)
 333 Sections.end_section "SopTisS";;
 334
 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)`;;
 347
 348 (* Finalization of the section SopTisT *)
 349 Sections.end_section "SopTisT";;
 350
 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`;;
 355
 356 (* Finalization of the section SopSisT *)
 357 Sections.end_section "SopSisT";;
 358
 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`;;
 363
 364 (* Finalization of the section SopSisS *)
 365 Sections.end_section "SopSisS";;
 366
 367 (* Finalization of the section OperationProperties *)
 368 Sections.end_section "OperationProperties";;
 369
 370 (* Close the module *)
 371 end;;