itab.ml

   1 (* ========================================================================= *)
   2 (* Intuitionistic theorem prover (complete for propositional fragment).      *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "tactics.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Accept a theorem modulo unification.                                      *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let UNIFY_ACCEPT_TAC mvs th (asl,w) =
  17   let insts = term_unify mvs (concl th) w in
  18   ([],insts),[],
  19   let th' = INSTANTIATE insts th in
  20   fun i [] -> INSTANTIATE i th';;
  21
  22 (* ------------------------------------------------------------------------- *)
  23 (* The actual prover, as a tactic.                                           *)
  24 (* ------------------------------------------------------------------------- *)
  25
  26 let ITAUT_TAC =
  27   let CONJUNCTS_THEN' ttac cth =
  28     ttac(CONJUNCT1 cth) THEN ttac(CONJUNCT2 cth) in
  29   let IMPLICATE t =
  30     let th1 = AP_THM NOT_DEF (dest_neg t) in
  31     CONV_RULE (RAND_CONV BETA_CONV) th1 in
  32   let RIGHT_REVERSIBLE_TAC = FIRST
  33    [CONJ_TAC;                                                     (* and     *)
  34     GEN_TAC;                                                      (* forall  *)
  35     DISCH_TAC;                                                    (* implies *)
  36     (fun gl -> CONV_TAC(K(IMPLICATE(snd gl))) gl);                (* not     *)
  37     EQ_TAC]                                                       (* iff     *)
  38   and LEFT_REVERSIBLE_TAC th gl = tryfind (fun ttac -> ttac th gl)
  39    [CONJUNCTS_THEN' ASSUME_TAC;                                   (* and    *)
  40     DISJ_CASES_TAC;                                               (* or     *)
  41     CHOOSE_TAC;                                                   (* exists *)
  42     (fun th -> ASSUME_TAC (EQ_MP (IMPLICATE (concl th)) th));     (* not    *)
  43     (CONJUNCTS_THEN' MP_TAC o uncurry CONJ  o EQ_IMP_RULE)]       (* iff    *)
  44   in
  45   let rec ITAUT_TAC mvs n gl =
  46     if n <= 0 then failwith "ITAUT_TAC: Too deep" else
  47     ((FIRST_ASSUM (UNIFY_ACCEPT_TAC mvs)) ORELSE
  48      (ACCEPT_TAC TRUTH) ORELSE
  49      (FIRST_ASSUM CONTR_TAC) ORELSE
  50      (RIGHT_REVERSIBLE_TAC THEN TRY (ITAUT_TAC mvs n)) ORELSE
  51      (FIRST_X_ASSUM LEFT_REVERSIBLE_TAC THEN TRY(ITAUT_TAC mvs n)) ORELSE
  52      (FIRST_X_ASSUM(fun th -> ASSUME_TAC th THEN
  53        (let gv = genvar(type_of(fst(dest_forall(concl th)))) in
  54         META_SPEC_TAC gv th THEN
  55         ITAUT_TAC (gv::mvs) (n - 2) THEN NO_TAC))) ORELSE
  56      (DISJ1_TAC THEN ITAUT_TAC mvs n THEN NO_TAC) ORELSE
  57      (DISJ2_TAC THEN ITAUT_TAC mvs n THEN NO_TAC) ORELSE
  58      (fun gl -> let gv = genvar(type_of(fst(dest_exists(snd gl)))) in
  59                 (X_META_EXISTS_TAC gv THEN
  60                  ITAUT_TAC (gv::mvs) (n - 2) THEN NO_TAC) gl) ORELSE
  61      (FIRST_ASSUM(fun th -> SUBGOAL_THEN (fst(dest_imp(concl th)))
  62                                       (fun ath -> ASSUME_TAC (MP th ath)) THEN
  63                            ITAUT_TAC mvs (n - 1) THEN NO_TAC))) gl in
  64   let rec ITAUT_ITERDEEP_TAC n gl =
  65     remark ("Searching with limit "^(string_of_int n));
  66     ((ITAUT_TAC [] n THEN NO_TAC) ORELSE ITAUT_ITERDEEP_TAC (n + 1)) gl in
  67   ITAUT_ITERDEEP_TAC 0;;
  68
  69 (* ------------------------------------------------------------------------- *)
  70 (* Alternative interface.                                                    *)
  71 (* ------------------------------------------------------------------------- *)
  72
  73 let ITAUT tm = prove(tm,ITAUT_TAC);;