(* ========================================================================= *)
(* Intuitionistic theorem prover (complete for propositional fragment).      *)
(*                                                                           *)
(*       John Harrison, University of Cambridge Computer Laboratory          *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

needs "tactics.ml";;

(* ------------------------------------------------------------------------- *)
(* Accept a theorem modulo unification.                                      *)
(* ------------------------------------------------------------------------- *)

let UNIFY_ACCEPT_TAC mvs th (asl,w) =
  let insts = term_unify mvs (concl th) w in
  ([],insts),[],
  let th' = INSTANTIATE insts th in
  fun i [] -> INSTANTIATE i th';;

(* ------------------------------------------------------------------------- *)
(* The actual prover, as a tactic.                                           *)
(* ------------------------------------------------------------------------- *)

let ITAUT_TAC =
  let CONJUNCTS_THEN' ttac cth =
    ttac(CONJUNCT1 cth) THEN ttac(CONJUNCT2 cth) in
  let IMPLICATE t =
    let th1 = AP_THM NOT_DEF (dest_neg t) in
    CONV_RULE (RAND_CONV BETA_CONV) th1 in
  let RIGHT_REVERSIBLE_TAC = FIRST
   [CONJ_TAC;                                                     (* and     *)
    GEN_TAC;                                                      (* forall  *)
    DISCH_TAC;                                                    (* implies *)
    (fun gl -> CONV_TAC(K(IMPLICATE(snd gl))) gl);                (* not     *)
    EQ_TAC]                                                       (* iff     *)
  and LEFT_REVERSIBLE_TAC th gl = tryfind (fun ttac -> ttac th gl)
   [CONJUNCTS_THEN' ASSUME_TAC;                                   (* and    *)
    DISJ_CASES_TAC;                                               (* or     *)
    CHOOSE_TAC;                                                   (* exists *)
    (fun th -> ASSUME_TAC (EQ_MP (IMPLICATE (concl th)) th));     (* not    *)
    (CONJUNCTS_THEN' MP_TAC o uncurry CONJ  o EQ_IMP_RULE)]       (* iff    *)
  in
  let rec ITAUT_TAC mvs n gl =
    if n <= 0 then failwith "ITAUT_TAC: Too deep" else
    ((FIRST_ASSUM (UNIFY_ACCEPT_TAC mvs)) ORELSE
     (ACCEPT_TAC TRUTH) ORELSE
     (FIRST_ASSUM CONTR_TAC) ORELSE
     (RIGHT_REVERSIBLE_TAC THEN TRY (ITAUT_TAC mvs n)) ORELSE
     (FIRST_X_ASSUM LEFT_REVERSIBLE_TAC THEN TRY(ITAUT_TAC mvs n)) ORELSE
     (FIRST_X_ASSUM(fun th -> ASSUME_TAC th THEN
       (let gv = genvar(type_of(fst(dest_forall(concl th)))) in
        META_SPEC_TAC gv th THEN
        ITAUT_TAC (gv::mvs) (n - 2) THEN NO_TAC))) ORELSE
     (DISJ1_TAC THEN ITAUT_TAC mvs n THEN NO_TAC) ORELSE
     (DISJ2_TAC THEN ITAUT_TAC mvs n THEN NO_TAC) ORELSE
     (fun gl -> let gv = genvar(type_of(fst(dest_exists(snd gl)))) in
                (X_META_EXISTS_TAC gv THEN
                 ITAUT_TAC (gv::mvs) (n - 2) THEN NO_TAC) gl) ORELSE
     (FIRST_ASSUM(fun th -> SUBGOAL_THEN (fst(dest_imp(concl th)))
                                      (fun ath -> ASSUME_TAC (MP th ath)) THEN
                           ITAUT_TAC mvs (n - 1) THEN NO_TAC))) gl in
  let rec ITAUT_ITERDEEP_TAC n gl =
    remark ("Searching with limit "^(string_of_int n));
    ((ITAUT_TAC [] n THEN NO_TAC) ORELSE ITAUT_ITERDEEP_TAC (n + 1)) gl in
  ITAUT_ITERDEEP_TAC 0;;

(* ------------------------------------------------------------------------- *)
(* Alternative interface.                                                    *)
(* ------------------------------------------------------------------------- *)

let ITAUT tm = prove(tm,ITAUT_TAC);;