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