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