anchor.diff:  limitations under the License.
   
   *)
  -
   /// Intuitionistic theorem prover (complete for propositional fragment).
   module NHol.itab
   
  
positive.code: open drule
  open tactics
  
  (*
  
  (* ------------------------------------------------------------------------- *)
  (* 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);;
  
  *)
  
negative.code: (*
  
  Copyright 1998 University of Cambridge
  Copyright 1998-2007 John Harrison
  Copyright 2013 Jack Pappas, Eric Taucher
  
  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  