needs "Examples/ssrfun-compiled.hl";;

(* Module Ssrbool*)
module Ssrbool = struct


(* Section ApplyIff *)
Sections.begin_section "ApplyIff";;
(Sections.add_section_var (mk_var ("P", (`:bool`))); Sections.add_section_var (mk_var ("Q", (`:bool`))));;
(Sections.add_section_hyp "eqPQ" (`P <=> Q`));;

(* Lemma iffLR *)
let iffLR = Sections.section_proof []
`P ==> Q`
[
   (done_tac);
];;

(* Lemma iffRL *)
let iffRL = Sections.section_proof []
`Q ==> P`
[
   (done_tac);
];;

(* Lemma iffLRn *)
let iffLRn = Sections.section_proof []
`~P ==> ~Q`
[
   (done_tac);
];;

(* Lemma iffRLn *)
let iffRLn = Sections.section_proof []
`~Q ==> ~P`
[
   (done_tac);
];;

(* Finalization of the section ApplyIff *)
let iffLR = Sections.finalize_theorem iffLR;;
let iffRL = Sections.finalize_theorem iffRL;;
let iffLRn = Sections.finalize_theorem iffLRn;;
let iffRLn = Sections.finalize_theorem iffRLn;;
Sections.end_section "ApplyIff";;

(* Lemma is_true_true *)
let is_true_true = Sections.section_proof []
`T`
[
   (done_tac);
];;

(* Lemma not_false_is_true *)
let not_false_is_true = Sections.section_proof []
`~F`
[
   (done_tac);
];;
let isT = is_true_true;;
let notF = not_false_is_true;;

(* Lemma negbT *)
let negbT = Sections.section_proof ["b"]
`(b = F) ==> ~b`
[
   (done_tac);
];;

(* Lemma negbTE *)
let negbTE = Sections.section_proof ["b"]
`~b ==> b = F`
[
   (done_tac);
];;

(* Lemma negbF *)
let negbF = Sections.section_proof ["b"]
`b ==> ~b = F`
[
   (done_tac);
];;

(* Lemma negbFE *)
let negbFE = Sections.section_proof ["b"]
`~b = F ==> b`
[
   (done_tac);
];;

(* Lemma negbK *)
let negbK = Sections.section_proof ["b"]
`~ ~b = b`
[
   (done_tac);
];;

(* Lemma negbNE *)
let negbNE = Sections.section_proof ["b"]
`~ ~ b ==> b`
[
   (done_tac);
];;

(* Lemma negb_inj *)
let negb_inj = Sections.section_proof ["b1";"b2"]
`~b1 = ~b2 ==> b1 = b2`
[
   ((((use_arg_then2 ("b1", [])) (disch_tac [])) THEN (clear_assumption "b1") THEN case) THEN (((use_arg_then2 ("b2", [])) (disch_tac [])) THEN (clear_assumption "b2") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma negbLR *)
let negbLR = Sections.section_proof ["b";"c"]
`b = ~c ==> ~b = c`
[
   ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma negbRL *)
let negbRL = Sections.section_proof ["b";"c"]
`~b = c ==> b = ~c`
[
   ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma contra *)
let contra = Sections.section_proof ["c";"b"]
`(c ==> b) ==> ~b ==> ~c`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
];;
let contraNN = contra;;

(* Lemma contraL *)
let contraL = Sections.section_proof ["c";"b"]
`(c ==> ~b) ==> b ==> ~c`
[
   (BETA_TAC THEN (move ["h"]));
   ((((fun arg_tac -> (use_arg_then2 ("contra", [contra])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma contraR *)
let contraR = Sections.section_proof ["c";"b"]
`(~c ==> b) ==> ~b ==> c`
[
   (BETA_TAC THEN (move ["h"]));
   ((((fun arg_tac -> (use_arg_then2 ("contra", [contra])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma contraLR *)
let contraLR = Sections.section_proof ["c";"b"]
`(~c ==> ~b) ==> b ==> c`
[
   (BETA_TAC THEN (move ["h"]));
   ((((fun arg_tac -> (use_arg_then2 ("contra", [contra])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma contraT *)
let contraT = Sections.section_proof ["b"]
`(~b ==> F) ==> b`
[
   (done_tac);
];;

(* Lemma wlog_neg *)
let wlog_neg = Sections.section_proof ["b"]
`(~b ==> b) ==> b`
[
   (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac));
];;

(* Lemma contraFT *)
let contraFT = Sections.section_proof ["c";"b"]
`(~c ==> b) ==> b = F ==> c`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
];;

(* Lemma contraFN *)
let contraFN = Sections.section_proof ["c";"b"]
`(c ==> b) ==> b = F ==> ~c`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
];;

(* Lemma contraTF *)
let contraTF = Sections.section_proof ["c";"b"]
`(c ==> ~b) ==> b ==> c = F`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
];;

(* Lemma contraNF *)
let contraNF = Sections.section_proof ["c";"b"]
`(c ==> b) ==> ~b ==> c = F`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
];;

(* Lemma contraFF *)
let contraFF = Sections.section_proof ["c";"b"]
`(c ==> b) ==> b = F ==> c = F`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
];;
let isSome = define `isSome NONE = F /\ (!x. isSome (SOME x) = T)`;;

(* Section BoolIf *)
Sections.begin_section "BoolIf";;
(Sections.add_section_var (mk_var ("vT", (`:A`))); Sections.add_section_var (mk_var ("vF", (`:A`))));;
(Sections.add_section_var (mk_var ("f", (`:A -> B`))));;
(Sections.add_section_var (mk_var ("b", (`:bool`))));;

(* Lemma if_same *)
let if_same = Sections.section_proof []
`(if b then vT else vT) = vT`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma if_neg *)
let if_neg = Sections.section_proof []
`(if ~b then vT else vF) = if b then vF else vT`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma fun_if *)
let fun_if = Sections.section_proof []
`f (if b then vT else vF) = if b then f vT else f vF`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma if_arg *)
let if_arg = Sections.section_proof ["fT";"fF";"x"]
`(if b then (fT:A->B) else fF) x = if b then fT x else fF x`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Finalization of the section BoolIf *)
let if_same = Sections.finalize_theorem if_same;;
let if_neg = Sections.finalize_theorem if_neg;;
let fun_if = Sections.finalize_theorem fun_if;;
let if_arg = Sections.finalize_theorem if_arg;;
Sections.end_section "BoolIf";;

(* Lemma andTb *)
let andTb = Sections.section_proof ["b"]
`(T /\ b) = b`
[
   (done_tac);
];;

(* Lemma andFb *)
let andFb = Sections.section_proof ["b"]
`(F /\ b) = F`
[
   (done_tac);
];;

(* Lemma andbT *)
let andbT = Sections.section_proof ["b"]
`(b /\ T) = b`
[
   (done_tac);
];;

(* Lemma andbF *)
let andbF = Sections.section_proof ["b"]
`(b /\ F) = F`
[
   (done_tac);
];;

(* Lemma andbb *)
let andbb = Sections.section_proof ["b"]
`(b /\ b) = b`
[
   (done_tac);
];;

(* Lemma andbC *)
let andbC = Sections.section_proof ["b";"c"]
`(b /\ c) = (c /\ b)`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andbA *)
let andbA = Sections.section_proof ["b";"c";"p"]
`b /\ (c /\ p) <=> (b /\ c) /\ p`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andbCA *)
let andbCA = Sections.section_proof ["b";"c";"p"]
`b /\ (c /\ p) <=> c /\ (b /\ p)`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andbAC *)
let andbAC = Sections.section_proof ["b";"c";"p"]
`(b /\ c) /\ p <=> (b /\ p) /\ c`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orTb *)
let orTb = Sections.section_proof ["b"]
`T \/ b <=> T`
[
   (done_tac);
];;

(* Lemma orFb *)
let orFb = Sections.section_proof ["b"]
`F \/ b <=> b`
[
   (done_tac);
];;

(* Lemma orbT *)
let orbT = Sections.section_proof ["b"]
`b \/ T <=> T`
[
   (done_tac);
];;

(* Lemma orbF *)
let orbF = Sections.section_proof ["b"]
`b \/ F <=> b`
[
   (done_tac);
];;

(* Lemma orbb *)
let orbb = Sections.section_proof ["b"]
`b \/ b <=> b`
[
   (done_tac);
];;

(* Lemma orbC *)
let orbC = Sections.section_proof ["b";"c"]
`b \/ c <=> c \/ b`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orbA *)
let orbA = Sections.section_proof ["b";"c";"p"]
`b \/ (c \/ p) <=> (b \/ c) \/ p`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orbCA *)
let orbCA = Sections.section_proof ["b";"c";"p"]
`b \/ (c \/ p) <=> c \/ (b \/ p)`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orbAC *)
let orbAC = Sections.section_proof ["b";"c";"p"]
`(b \/ c) \/ p <=> (b \/ p) \/ c`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andbN *)
let andbN = Sections.section_proof ["b"]
`b /\ ~b <=> F`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andNb *)
let andNb = Sections.section_proof ["b"]
`~b /\ b <=> F`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orbN *)
let orbN = Sections.section_proof ["b"]
`b \/ ~b`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orNb *)
let orNb = Sections.section_proof ["b"]
`~b \/ b`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andb_orl *)
let andb_orl = Sections.section_proof ["b";"c";"p"]
`(b \/ c) /\ p <=> (b /\ p) \/ (c /\ p)`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andb_orr *)
let andb_orr = Sections.section_proof ["b";"c";"p"]
`b /\ (c \/ p) <=> (b /\ c) \/ (b /\ p)`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orb_andl *)
let orb_andl = Sections.section_proof ["b";"c";"p"]
`(b /\ c) \/ p <=> (b \/ p) /\ (c \/ p)`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orb_andr *)
let orb_andr = Sections.section_proof ["b";"c";"p"]
`b \/ (c /\ p) <=> (b \/ c) /\ (b \/ p)`
[
   ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andb_idl *)
let andb_idl = Sections.section_proof ["a";"b"]
`(b ==> a) ==> (a /\ b <=> b)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andb_idr *)
let andb_idr = Sections.section_proof ["a";"b"]
`(a ==> b) ==> (a /\ b <=> a)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andb_id2l *)
let andb_id2l = Sections.section_proof ["a";"b";"c"]
`(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andb_id2r *)
let andb_id2r = Sections.section_proof ["a";"b";"c"]
`(b ==> (a <=> c)) ==> (a /\ b <=> c /\ b)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orb_idl *)
let orb_idl = Sections.section_proof ["a";"b"]
`(a ==> b) ==> (a \/ b <=> b)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orbb_idr *)
let orbb_idr = Sections.section_proof ["a";"b"]
`(b ==> a) ==> (a \/ b <=> a)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orb_id2l *)
let orb_id2l = Sections.section_proof ["a";"b";"c"]
`(~ a ==> (b <=> c)) ==> (a \/ b <=> a \/ c)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orb_id2r *)
let orb_id2r = Sections.section_proof ["a";"b";"c"]
`(~ b ==> (a <=> c)) ==> (a \/ b <=> c \/ b)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma negb_and *)
let negb_and = Sections.section_proof ["a";"b"]
`~ (a /\ b) <=> ~ a \/ ~ b`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma negb_or *)
let negb_or = Sections.section_proof ["a";"b"]
`~ (a \/ b) <=> ~ a /\ ~ b`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andbK *)
let andbK = Sections.section_proof ["a";"b"]
`((a /\ b) \/ a) = a`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma andKb *)
let andKb = Sections.section_proof ["a";"b"]
`a \/ b /\ a <=> a`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orbK *)
let orbK = Sections.section_proof ["a";"b"]
`(a \/ b) /\ a <=> a`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma orKb *)
let orKb = Sections.section_proof ["a";"b"]
`a /\ (b \/ a) <=> a`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implybT *)
let implybT = Sections.section_proof ["b"]
`b ==> T`
[
   (done_tac);
];;

(* Lemma implybF *)
let implybF = Sections.section_proof ["b"]
`(b ==> F) <=> ~ b`
[
   (done_tac);
];;

(* Lemma implyFb *)
let implyFb = Sections.section_proof ["b"]
`F ==> b`
[
   (done_tac);
];;

(* Lemma implyTb *)
let implyTb = Sections.section_proof ["b"]
`(T ==> b) <=> b`
[
   (done_tac);
];;

(* Lemma implybb *)
let implybb = Sections.section_proof ["b"]
`b ==> b`
[
   (done_tac);
];;

(* Lemma negb_imply *)
let negb_imply = Sections.section_proof ["a";"b"]
`~ (a ==> b) <=> a /\ ~ b`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implybE *)
let implybE = Sections.section_proof ["a";"b"]
`(a ==> b) <=> ~ a \/ b`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implyNb *)
let implyNb = Sections.section_proof ["a";"b"]
`(~ a ==> b) <=> a \/ b`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implybN *)
let implybN = Sections.section_proof ["a";"b"]
`(a ==> ~ b) <=> (b ==> ~ a)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implybNN *)
let implybNN = Sections.section_proof ["a";"b"]
`(~ a ==> ~ b) <=> b ==> a`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implyb_idl *)
let implyb_idl = Sections.section_proof ["a";"b"]
`(~ a ==> b) ==> ((a ==> b) <=> b)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implyb_idr *)
let implyb_idr = Sections.section_proof ["a";"b"]
`(b ==> ~ a) ==> ((a ==> b) <=> ~ a)`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma implyb_id2l *)
let implyb_id2l = Sections.section_proof ["a";"b";"c"]
`(a ==> (b <=> c)) ==> ((a ==> b) <=> (a ==> c))`
[
   ((((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
];;
let XOR_DEF = new_definition `XOR p q = if p then ~q else q`;;
overload_interface("+", `XOR`);;

(* Lemma addFb *)
let addFb = Sections.section_proof ["b"]
`F + b <=> b`
[
   ((((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma addbF *)
let addbF = Sections.section_proof ["b"]
`b + F <=> b`
[
   ((((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma addbb *)
let addbb = Sections.section_proof ["b"]
`b + b <=> F`
[
   ((((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma addbC *)
let addbC = Sections.section_proof ["b";"c"]
`b + c <=> c + b`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma addbA *)
let addbA = Sections.section_proof ["a";"b";"c"]
`a + (b + c) <=> (a + b) + c`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
];;

(* Lemma addbCA *)
let addbCA = Sections.section_proof ["a";"b";"c"]
`(a + b) + c <=> (a + c) + b`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
];;

(* Lemma addbAC *)
let addbAC = Sections.section_proof ["a";"b";"c"]
`a + (b + c) <=> b + (a + c)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
];;

(* Lemma andb_addl *)
let andb_addl = Sections.section_proof ["a";"b";"c"]
`(a + b) /\ c <=> (a /\ c) + (b /\ c)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
];;

(* Lemma andb_addr *)
let andb_addr = Sections.section_proof ["a";"b";"c"]
`a /\ (b + c) <=> (a /\ b) + (a /\ c)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
];;

(* Lemma addKb *)
let addKb = Sections.section_proof ["x";"y"]
`x + (x + y) <=> y`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN case) THEN (((use_arg_then2 ("y", [])) (disch_tac [])) THEN (clear_assumption "y") THEN case THEN (simp_tac)));
];;

(* Lemma addbK *)
let addbK = Sections.section_proof ["x";"y"]
`(y + x) + x <=> y`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN case) THEN (((use_arg_then2 ("y", [])) (disch_tac [])) THEN (clear_assumption "y") THEN case THEN (simp_tac)));
];;

(* Lemma addIb *)
let addIb = Sections.section_proof ["x";"y1";"y2"]
`(y1 + x <=> y2 + x) ==> (y1 = y2)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("y1", [])) (disch_tac [])) THEN (clear_assumption "y1") THEN case) THEN (((use_arg_then2 ("y2", [])) (disch_tac [])) THEN (clear_assumption "y2") THEN case) THEN (((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN case THEN (simp_tac)));
];;

(* Lemma addbI *)
let addbI = Sections.section_proof ["x";"y1";"y2"]
`(x + y1 <=> x + y2) ==> (y1 = y2)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN case) THEN (((use_arg_then2 ("y1", [])) (disch_tac [])) THEN (clear_assumption "y1") THEN case) THEN (((use_arg_then2 ("y2", [])) (disch_tac [])) THEN (clear_assumption "y2") THEN case THEN (simp_tac)));
];;

(* Lemma addTb *)
let addTb = Sections.section_proof ["b"]
`T + b <=> ~b`
[
   (((((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
];;

(* Lemma addbT *)
let addbT = Sections.section_proof ["b"]
`b + T <=> ~ b`
[
   ((((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma addbN *)
let addbN = Sections.section_proof ["a";"b"]
`a + ~ b <=> ~ (a + b)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)));
];;

(* Lemma addNb *)
let addNb = Sections.section_proof ["a";"b"]
`~ a + b <=> ~ (a + b)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("XOR_DEF", [XOR_DEF]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a", [])) (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)));
];;
let subpred = new_definition `subpred p1 p2 <=> (!x. p1 x ==> p2 x)`;;
let subrel = new_definition `subrel r1 r2 <=> (!x y. r1 x y ==> r2 x y)`;;
let pred0 = new_definition `pred0 = (\x. F)`;;
let predT = new_definition `predT = (\x. T)`;;
let predI = new_definition `predI p1 p2 = (\x. p1 x /\ p2 x)`;;
let predU = new_definition `predU p1 p2 = (\x. p1 x \/ p2 x)`;;
let predC = new_definition `predC p = (\x. ~p x)`;;
let predD = new_definition `predD p1 p2 = (\x. ~p2 x /\ p1 x)`;;
let preim = new_definition `preim f (d:A->bool) = (\x. d (f x))`;;
let relU = new_definition `relU r1 r2 = (\x y. r1 x y \/ r2 x y)`;;

(* Lemma subrelUl *)
let subrelUl = Sections.section_proof ["r1";"r2"]
`subrel r1 (relU r1 r2)`
[
   (((((use_arg_then2 ("relU", [relU]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subrel", [subrel]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma subrelUr *)
let subrelUr = Sections.section_proof ["r1";"r2"]
`subrel r2 (relU r1 r2)`
[
   (((((use_arg_then2 ("relU", [relU]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subrel", [subrel]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
];;

(* Close the module *)
end;;