type fp = X of int | Vrai | Faux | Et of fp * fp | Ou of fp * fp | Imp of fp * fp | Equiv of fp * fp | Non of fp ;; exception Undefined;; let rec elim_equiv f = match f with | Et (f1,f2) -> Et (elim_equiv f1, elim_equiv f2) | Ou (f1,f2) -> Ou (elim_equiv f1, elim_equiv f2) | Imp (f1,f2) -> Imp (elim_equiv f1, elim_equiv f2) | Equiv (f1,f2) -> let f1' = elim_equiv f1 in let f2' = elim_equiv f2 in Et (Imp (f1',f2'), Imp (f1',f2')) | Non f' -> Non (elim_equiv f') | f -> f ;; let rec elim_imp f = match f with | Et (f1,f2) -> Et (elim_imp f1, elim_imp f2) | Ou (f1,f2) -> Ou (elim_imp f1, elim_imp f2) | Imp (f1,f2) -> Ou (Non (elim_imp f1), elim_imp f2) | Equiv (f1,f2) -> raise Undefined | Non f' -> Non (elim_imp f') | f -> f ;; let rec repousse_neg f = match f with | Et (f1,f2) -> Et (repousse_neg f1, repousse_neg f2) | Ou (f1,f2) -> Ou (repousse_neg f1, repousse_neg f2) | Imp (f1,f2) -> raise Undefined | Equiv (f1,f2) -> raise Undefined | Non f' -> repousse_neg_non f' | f -> f and repousse_neg_non f = match f with | Et (f1,f2) -> Ou (repousse_neg_non f1, repousse_neg_non f2) | Ou (f1,f2) -> Et (repousse_neg_non f1, repousse_neg_non f2) | Non f' -> repousse_neg f' | Vrai -> Faux | Faux -> Vrai | X n -> Non (X n) | f -> raise Undefined ;; let rec repousse_neg2 f = match f with | Et (f1,f2) -> Et (repousse_neg f1, repousse_neg f2) | Ou (f1,f2) -> Ou (repousse_neg f1, repousse_neg f2) | Imp (f1,f2) -> raise Undefined | Equiv (f1,f2) -> raise Undefined | Non (Et (f1,f2)) -> Ou (repousse_neg (Non f1), repousse_neg (Non f2)) | Non (Ou (f1,f2)) -> Et (repousse_neg (Non f1), repousse_neg (Non f2)) | Non (Non f' ) -> repousse_neg f' | Non (Vrai ) -> Faux | Non (Faux ) -> Vrai | Non (X n ) -> Non (X n) | Non (f' ) -> raise Undefined | f -> f ;; let rec inverse_ou_et f = match f with | Et (f1,f2) -> Et (inverse_ou_et f1, inverse_ou_et f2) | Ou (f1,f2) -> inverse_aux (inverse_ou_et f1) (inverse_ou_et f2) | Imp (f1,f2) -> raise Undefined | Equiv (f1,f2) -> raise Undefined | f -> f and inverse_aux f1 f2 = match (f1,f2) with | (f1, Et (f21,f22)) -> Et (inverse_aux f1 f21, inverse_aux f1 f22) | (Et (f11,f12), f2) -> Et (inverse_aux f11 f2, inverse_aux f12 f2) | (f1,f2) -> Ou (f1,f2) ;;