src/HOL/Tools/res_atp.ML
author paulson
Tue Nov 30 18:25:55 2004 +0100 (2004-11-30 ago)
changeset 15347 14585bc8fa09
child 15452 e2a721567f67
permissions -rw-r--r--
resolution package tools by Jia Meng
paulson@15347
     1
(*  Author: Jia Meng, Cambridge University Computer Laboratory
paulson@15347
     2
    ID: $Id$
paulson@15347
     3
    Copyright 2004 University of Cambridge
paulson@15347
     4
paulson@15347
     5
ATPs with TPTP format input.
paulson@15347
     6
*)
paulson@15347
     7
signature RES_ATP = 
paulson@15347
     8
sig
paulson@15347
     9
paulson@15347
    10
val trace_res : bool ref
paulson@15347
    11
val axiom_file : Path.T
paulson@15347
    12
val hyps_file : Path.T
paulson@15347
    13
val isar_atp : Thm.thm list * Thm.thm -> unit
paulson@15347
    14
val prob_file : Path.T
paulson@15347
    15
val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
paulson@15347
    16
val atp_tac : int -> Tactical.tactic
paulson@15347
    17
paulson@15347
    18
end;
paulson@15347
    19
paulson@15347
    20
structure ResAtp : RES_ATP =
paulson@15347
    21
paulson@15347
    22
struct
paulson@15347
    23
paulson@15347
    24
(* default value is false *)
paulson@15347
    25
paulson@15347
    26
val trace_res = ref false;
paulson@15347
    27
paulson@15347
    28
val skolem_tac = skolemize_tac;
paulson@15347
    29
paulson@15347
    30
paulson@15347
    31
val atomize_tac =
paulson@15347
    32
    SUBGOAL
paulson@15347
    33
     (fn (prop,_) =>
paulson@15347
    34
	 let val ts = Logic.strip_assums_hyp prop
paulson@15347
    35
	 in EVERY1 
paulson@15347
    36
		[METAHYPS
paulson@15347
    37
		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
paulson@15347
    38
	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
paulson@15347
    39
     end);
paulson@15347
    40
paulson@15347
    41
(* temporarily use these files, which will be loaded by Vampire *)
paulson@15347
    42
val prob_file = File.tmp_path (Path.basic "prob");
paulson@15347
    43
val axiom_file = File.tmp_path (Path.basic "axioms");
paulson@15347
    44
val hyps_file = File.tmp_path (Path.basic "hyps");
paulson@15347
    45
val dummy_tac = PRIMITIVE(fn thm => thm );
paulson@15347
    46
paulson@15347
    47
paulson@15347
    48
paulson@15347
    49
fun tptp_inputs thms = 
paulson@15347
    50
    let val clss = map (ResClause.make_conjecture_clause_thm) thms
paulson@15347
    51
	val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss) 
paulson@15347
    52
        val probfile = File.sysify_path prob_file
paulson@15347
    53
	val out = TextIO.openOut(probfile)
paulson@15347
    54
    in
paulson@15347
    55
	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
paulson@15347
    56
    end;
paulson@15347
    57
paulson@15347
    58
paulson@15347
    59
(**** for Isabelle/ML interface  ****)
paulson@15347
    60
paulson@15347
    61
fun call_atp_tac thms = (tptp_inputs thms; dummy_tac);
paulson@15347
    62
paulson@15347
    63
paulson@15347
    64
val atp_tac = SELECT_GOAL
paulson@15347
    65
  (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac, 
paulson@15347
    66
  METAHYPS(fn negs => (call_atp_tac(make_clauses negs)))]);
paulson@15347
    67
paulson@15347
    68
paulson@15347
    69
fun atp_ax_tac axioms n = 
paulson@15347
    70
    let val axcls = ResLib.flat_noDup(map ResAxioms.clausify_axiom axioms)
paulson@15347
    71
	val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup(map ResClause.tptp_clause axcls))
paulson@15347
    72
	val axiomfile = File.sysify_path axiom_file
paulson@15347
    73
	val out = TextIO.openOut (axiomfile)
paulson@15347
    74
    in
paulson@15347
    75
	(TextIO.output(out,axcls_str);TextIO.closeOut out; if !trace_res then (warning axiomfile) else (); atp_tac n)
paulson@15347
    76
    end;
paulson@15347
    77
paulson@15347
    78
paulson@15347
    79
fun atp thm =
paulson@15347
    80
    let val prems = prems_of thm
paulson@15347
    81
    in
paulson@15347
    82
	case prems of [] => () 
paulson@15347
    83
		    | _ => (atp_tac 1 thm; ())
paulson@15347
    84
    end;
paulson@15347
    85
paulson@15347
    86
paulson@15347
    87
(**** For running in Isar ****)
paulson@15347
    88
paulson@15347
    89
(* same function as that in res_axioms.ML *)
paulson@15347
    90
fun repeat_RS thm1 thm2 =
paulson@15347
    91
    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
paulson@15347
    92
    in
paulson@15347
    93
	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
paulson@15347
    94
    end;
paulson@15347
    95
paulson@15347
    96
(* a special version of repeat_RS *)
paulson@15347
    97
fun repeat_someI_ex thm = repeat_RS thm someI_ex;
paulson@15347
    98
paulson@15347
    99
paulson@15347
   100
paulson@15347
   101
fun isar_atp_h thms =
paulson@15347
   102
    let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
paulson@15347
   103
	val prems' = map repeat_someI_ex prems
paulson@15347
   104
	val prems'' = make_clauses prems'
paulson@15347
   105
	val prems''' = ResAxioms.rm_Eps [] prems''
paulson@15347
   106
	val clss = map ResClause.make_hypothesis_clause prems'''
paulson@15347
   107
	val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
paulson@15347
   108
        val hypsfile = File.sysify_path hyps_file
paulson@15347
   109
	val out = TextIO.openOut(hypsfile)
paulson@15347
   110
    in
paulson@15347
   111
	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; if !trace_res then (warning hypsfile) else ())
paulson@15347
   112
    end;
paulson@15347
   113
paulson@15347
   114
paulson@15347
   115
paulson@15347
   116
paulson@15347
   117
val isar_atp_g = atp_tac;
paulson@15347
   118
paulson@15347
   119
fun isar_atp_aux thms thm = 
paulson@15347
   120
    (isar_atp_h thms; isar_atp_g 1 thm;());
paulson@15347
   121
paulson@15347
   122
paulson@15347
   123
paulson@15347
   124
paulson@15347
   125
paulson@15347
   126
(* called in Isar automatically *)
paulson@15347
   127
fun isar_atp (thms, thm) =
paulson@15347
   128
    let val prems = prems_of thm
paulson@15347
   129
    in
paulson@15347
   130
	case prems of [] => () 
paulson@15347
   131
		    | _ => (isar_atp_aux thms thm)
paulson@15347
   132
    end;
paulson@15347
   133
paulson@15347
   134
end;
paulson@15347
   135
paulson@15347
   136
Proof.atp_hook := ResAtp.isar_atp;
paulson@15347
   137
paulson@15347
   138