src/HOL/Tools/res_atp.ML
author paulson
Fri Jan 21 18:00:18 2005 +0100 (2005-01-21 ago)
changeset 15452 e2a721567f67
parent 15347 14585bc8fa09
child 15572 9c89b1adf573
permissions -rw-r--r--
Jia Meng: delta simpsets and clasets
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@15452
     7
paulson@15452
     8
(*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
paulson@15452
     9
paulson@15347
    10
signature RES_ATP = 
paulson@15347
    11
sig
paulson@15347
    12
paulson@15347
    13
val trace_res : bool ref
paulson@15347
    14
val axiom_file : Path.T
paulson@15347
    15
val hyps_file : Path.T
paulson@15452
    16
val isar_atp : ProofContext.context * Thm.thm -> unit
paulson@15347
    17
val prob_file : Path.T
paulson@15347
    18
val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
paulson@15347
    19
val atp_tac : int -> Tactical.tactic
paulson@15452
    20
val debug: bool ref
paulson@15347
    21
paulson@15347
    22
end;
paulson@15347
    23
paulson@15347
    24
structure ResAtp : RES_ATP =
paulson@15347
    25
paulson@15347
    26
struct
paulson@15347
    27
paulson@15452
    28
(* used for debug *)
paulson@15452
    29
val debug = ref false;
paulson@15452
    30
paulson@15452
    31
fun debug_tac tac = (warning "testing";tac);
paulson@15347
    32
(* default value is false *)
paulson@15347
    33
paulson@15347
    34
val trace_res = ref false;
paulson@15347
    35
paulson@15347
    36
val skolem_tac = skolemize_tac;
paulson@15347
    37
paulson@15347
    38
paulson@15347
    39
val atomize_tac =
paulson@15347
    40
    SUBGOAL
paulson@15347
    41
     (fn (prop,_) =>
paulson@15347
    42
	 let val ts = Logic.strip_assums_hyp prop
paulson@15347
    43
	 in EVERY1 
paulson@15347
    44
		[METAHYPS
paulson@15347
    45
		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
paulson@15347
    46
	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
paulson@15347
    47
     end);
paulson@15347
    48
paulson@15347
    49
(* temporarily use these files, which will be loaded by Vampire *)
paulson@15347
    50
val prob_file = File.tmp_path (Path.basic "prob");
paulson@15347
    51
val axiom_file = File.tmp_path (Path.basic "axioms");
paulson@15347
    52
val hyps_file = File.tmp_path (Path.basic "hyps");
paulson@15347
    53
val dummy_tac = PRIMITIVE(fn thm => thm );
paulson@15347
    54
paulson@15347
    55
paulson@15347
    56
paulson@15452
    57
fun tptp_inputs thms n = 
paulson@15347
    58
    let val clss = map (ResClause.make_conjecture_clause_thm) thms
paulson@15347
    59
	val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss) 
paulson@15452
    60
        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
paulson@15347
    61
	val out = TextIO.openOut(probfile)
paulson@15347
    62
    in
paulson@15347
    63
	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
paulson@15347
    64
    end;
paulson@15347
    65
paulson@15347
    66
paulson@15347
    67
(**** for Isabelle/ML interface  ****)
paulson@15347
    68
paulson@15452
    69
fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
paulson@15452
    70
paulson@15347
    71
paulson@15347
    72
paulson@15452
    73
paulson@15452
    74
fun atp_tac n = SELECT_GOAL
paulson@15452
    75
  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
paulson@15452
    76
  METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n;
paulson@15347
    77
paulson@15347
    78
paulson@15347
    79
fun atp_ax_tac axioms n = 
paulson@15347
    80
    let val axcls = ResLib.flat_noDup(map ResAxioms.clausify_axiom axioms)
paulson@15347
    81
	val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup(map ResClause.tptp_clause axcls))
paulson@15347
    82
	val axiomfile = File.sysify_path axiom_file
paulson@15347
    83
	val out = TextIO.openOut (axiomfile)
paulson@15347
    84
    in
paulson@15347
    85
	(TextIO.output(out,axcls_str);TextIO.closeOut out; if !trace_res then (warning axiomfile) else (); atp_tac n)
paulson@15347
    86
    end;
paulson@15347
    87
paulson@15347
    88
paulson@15347
    89
fun atp thm =
paulson@15347
    90
    let val prems = prems_of thm
paulson@15347
    91
    in
paulson@15347
    92
	case prems of [] => () 
paulson@15347
    93
		    | _ => (atp_tac 1 thm; ())
paulson@15347
    94
    end;
paulson@15347
    95
paulson@15347
    96
paulson@15347
    97
(**** For running in Isar ****)
paulson@15347
    98
paulson@15347
    99
(* same function as that in res_axioms.ML *)
paulson@15347
   100
fun repeat_RS thm1 thm2 =
paulson@15347
   101
    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
paulson@15347
   102
    in
paulson@15347
   103
	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
paulson@15347
   104
    end;
paulson@15347
   105
paulson@15347
   106
(* a special version of repeat_RS *)
paulson@15347
   107
fun repeat_someI_ex thm = repeat_RS thm someI_ex;
paulson@15347
   108
paulson@15347
   109
paulson@15452
   110
(* convert clauses from "assume" to conjecture. write to file "hyps" *)
paulson@15347
   111
fun isar_atp_h thms =
paulson@15347
   112
    let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
paulson@15347
   113
	val prems' = map repeat_someI_ex prems
paulson@15347
   114
	val prems'' = make_clauses prems'
paulson@15347
   115
	val prems''' = ResAxioms.rm_Eps [] prems''
paulson@15452
   116
	val clss = map ResClause.make_conjecture_clause prems'''
paulson@15347
   117
	val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
paulson@15347
   118
        val hypsfile = File.sysify_path hyps_file
paulson@15347
   119
	val out = TextIO.openOut(hypsfile)
paulson@15347
   120
    in
paulson@15347
   121
	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; if !trace_res then (warning hypsfile) else ())
paulson@15347
   122
    end;
paulson@15347
   123
paulson@15347
   124
paulson@15347
   125
paulson@15347
   126
paulson@15347
   127
val isar_atp_g = atp_tac;
paulson@15347
   128
paulson@15452
   129
paulson@15452
   130
fun isar_atp_goal' thm k n = 
paulson@15452
   131
    if (k > n) then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
paulson@15452
   132
paulson@15452
   133
paulson@15452
   134
fun isar_atp_goal thm n_subgoals = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals));
paulson@15452
   135
paulson@15452
   136
paulson@15452
   137
paulson@15452
   138
fun isar_atp_aux thms thm n_subgoals = 
paulson@15452
   139
    (isar_atp_h thms; isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
paulson@15452
   140
paulson@15452
   141
paulson@15452
   142
fun isar_atp' (thms, thm) =
paulson@15452
   143
    let val prems = prems_of thm
paulson@15452
   144
    in
paulson@15452
   145
	case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())
paulson@15452
   146
		    | _ => (isar_atp_aux thms thm (length prems))
paulson@15452
   147
    end;
paulson@15452
   148
paulson@15452
   149
paulson@15452
   150
paulson@15452
   151
paulson@15452
   152
local
paulson@15452
   153
paulson@15452
   154
fun retr_thms ([]:MetaSimplifier.rrule list) = []
paulson@15452
   155
	  | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
paulson@15452
   156
paulson@15452
   157
paulson@15452
   158
fun snds [] = []
paulson@15452
   159
  |   snds ((x,y)::l) = y::(snds l);
paulson@15452
   160
paulson@15452
   161
paulson@15452
   162
paulson@15452
   163
paulson@15452
   164
fun get_thms_cs claset =
paulson@15452
   165
    let val clsset = rep_cs claset
paulson@15452
   166
	val safeEs = #safeEs clsset
paulson@15452
   167
	val safeIs = #safeIs clsset
paulson@15452
   168
	val hazEs = #hazEs clsset
paulson@15452
   169
	val hazIs = #hazIs clsset
paulson@15452
   170
    in
paulson@15452
   171
	safeEs @ safeIs @ hazEs @ hazIs
paulson@15452
   172
    end;
paulson@15452
   173
paulson@15452
   174
paulson@15452
   175
paulson@15452
   176
fun append_name name [] _ = []
paulson@15452
   177
  | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
paulson@15452
   178
paulson@15452
   179
fun append_names (name::names) (thms::thmss) =
paulson@15452
   180
    let val thms' = append_name name thms 0
paulson@15452
   181
    in
paulson@15452
   182
	thms'::(append_names names thmss)
paulson@15452
   183
    end;
paulson@15452
   184
paulson@15452
   185
paulson@15452
   186
fun get_thms_ss [] = []
paulson@15452
   187
  | get_thms_ss thms =
paulson@15452
   188
    let val names = map Thm.name_of_thm thms 
paulson@15452
   189
        val thms' = map (mksimps mksimps_pairs) thms
paulson@15452
   190
        val thms'' = append_names names thms'
paulson@15452
   191
    in
paulson@15452
   192
	ResLib.flat_noDup thms''
paulson@15452
   193
    end;
paulson@15452
   194
paulson@15452
   195
paulson@15452
   196
paulson@15452
   197
paulson@15452
   198
in
paulson@15452
   199
paulson@15452
   200
paulson@15452
   201
(* convert locally declared rules to axiom clauses *)
paulson@15452
   202
(* write axiom clauses to ax_file *)
paulson@15452
   203
fun isar_local_thms (delta_cs, delta_ss_thms) =
paulson@15452
   204
    let val thms_cs = get_thms_cs delta_cs
paulson@15452
   205
	val thms_ss = get_thms_ss delta_ss_thms
paulson@15452
   206
	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
paulson@15452
   207
	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
paulson@15452
   208
	val ax_file = File.sysify_path axiom_file
paulson@15452
   209
	val out = TextIO.openOut ax_file
paulson@15452
   210
    in
paulson@15452
   211
	(ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)
paulson@15452
   212
    end;
paulson@15347
   213
paulson@15347
   214
paulson@15347
   215
paulson@15347
   216
paulson@15347
   217
paulson@15347
   218
(* called in Isar automatically *)
paulson@15452
   219
fun isar_atp (ctxt,thm) =
paulson@15452
   220
    let val prems = ProofContext.prems_of ctxt
paulson@15452
   221
      val d_cs = Classical.get_delta_claset ctxt
paulson@15452
   222
      val d_ss_thms = Simplifier.get_delta_simpset ctxt
paulson@15347
   223
    in
paulson@15452
   224
	(isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))
paulson@15347
   225
    end;
paulson@15347
   226
paulson@15452
   227
end
paulson@15452
   228
paulson@15452
   229
paulson@15452
   230
paulson@15452
   231
paulson@15347
   232
end;
paulson@15347
   233
paulson@15347
   234
Proof.atp_hook := ResAtp.isar_atp;
paulson@15347
   235
paulson@15347
   236