# HG changeset patch
# User webertj
# Date 1110553701 -3600
# Node ID 27a706e3a53dc6ea2321996c5b0e6517ce03c94c
# Parent  83c0bf275b0fa864fb7c20e442a7205aac11241a
code reformatted

diff -r 83c0bf275b0f -r 27a706e3a53d src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Mar 11 00:45:07 2005 +0100
+++ b/src/HOL/Tools/res_atp.ML	Fri Mar 11 16:08:21 2005 +0100
@@ -1,6 +1,7 @@
-(*  Author: Jia Meng, Cambridge University Computer Laboratory
-    ID: $Id$
-    Copyright 2004 University of Cambridge
+(*  Title:      HOL/Tools/res_atp.ML
+    ID:         $Id$
+    Author:     Jia Meng, Cambridge University Computer Laboratory
+    Copyright   2004 University of Cambridge
 
 ATPs with TPTP format input.
 *)
@@ -10,217 +11,207 @@
 signature RES_ATP = 
 sig
 
-val trace_res : bool ref
-val axiom_file : Path.T
-val hyps_file : Path.T
-val isar_atp : ProofContext.context * Thm.thm -> unit
-val prob_file : Path.T
-val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
-val atp_tac : int -> Tactical.tactic
-val debug: bool ref
+	val trace_res  : bool ref
+	val axiom_file : Path.T
+	val hyps_file  : Path.T
+	val isar_atp   : ProofContext.context * Thm.thm -> unit
+	val prob_file  : Path.T
+	val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
+	val atp_tac    : int -> Tactical.tactic
+	val debug      : bool ref
 
 end;
 
 structure ResAtp : RES_ATP =
-
 struct
 
-(* used for debug *)
-val debug = ref false;
+	(* used for debug *)
+	val debug = ref false;
 
-fun debug_tac tac = (warning "testing";tac);
-(* default value is false *)
+	fun debug_tac tac =
+		(warning "testing"; tac);
+	(* default value is false *)
 
-val trace_res = ref false;
+	val trace_res = ref false;
 
-val skolem_tac = skolemize_tac;
-
+	val skolem_tac = skolemize_tac;
 
-val atomize_tac =
-    SUBGOAL
-     (fn (prop,_) =>
-	 let val ts = Logic.strip_assums_hyp prop
-	 in EVERY1 
-		[METAHYPS
-		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
-	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
-     end);
+	val atomize_tac =
+		SUBGOAL (fn (prop, _) =>
+			let
+				val ts = Logic.strip_assums_hyp prop
+			in
+				EVERY1
+					[METAHYPS (fn hyps => cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1),
+					 REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+			end);
 
-(* temporarily use these files, which will be loaded by Vampire *)
-val prob_file = File.tmp_path (Path.basic "prob");
-val axiom_file = File.tmp_path (Path.basic "axioms");
-val hyps_file = File.tmp_path (Path.basic "hyps");
-val dummy_tac = PRIMITIVE(fn thm => thm );
-
-
+	(* temporarily use these files, which will be loaded by Vampire *)
+	val prob_file  = File.tmp_path (Path.basic "prob");
+	val axiom_file = File.tmp_path (Path.basic "axioms");
+	val hyps_file  = File.tmp_path (Path.basic "hyps");
+	val dummy_tac  = PRIMITIVE (fn thm => thm );
 
-fun tptp_inputs thms n = 
-    let val clss = map (ResClause.make_conjecture_clause_thm) thms
-	val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss) 
-        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
-	val out = TextIO.openOut(probfile)
-    in
-	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
-    end;
+	fun tptp_inputs thms n =
+	let
+		val clss      = map (ResClause.make_conjecture_clause_thm) thms
+		val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
+		val probfile  = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
+		val out       = TextIO.openOut probfile
+	in
+		ResLib.writeln_strs out tptp_clss;
+		TextIO.closeOut out;
+		if !trace_res then warning probfile else ()
+	end;
 
 
 (**** for Isabelle/ML interface  ****)
 
-fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
-
-
-
+	fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
 
-fun atp_tac n = SELECT_GOAL
-  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
-  METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n;
-
+	fun atp_tac n =
+		SELECT_GOAL (EVERY1
+			[rtac ccontr,atomize_tac, skolemize_tac,
+			 METAHYPS (fn negs => call_atp_tac (make_clauses negs) n)]
+		) n;
 
-fun atp_ax_tac axioms n = 
-    let val axcls = ResLib.flat_noDup(map ResAxioms.clausify_axiom axioms)
-	val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup(map ResClause.tptp_clause axcls))
-	val axiomfile = File.sysify_path axiom_file
-	val out = TextIO.openOut (axiomfile)
-    in
-	(TextIO.output(out,axcls_str);TextIO.closeOut out; if !trace_res then (warning axiomfile) else (); atp_tac n)
-    end;
+	fun atp_ax_tac axioms n =
+	let
+		val axcls     = ResLib.flat_noDup (map ResAxioms.clausify_axiom axioms)
+		val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup (map ResClause.tptp_clause axcls))
+		val axiomfile = File.sysify_path axiom_file
+		val out       = TextIO.openOut axiomfile
+	in
+		TextIO.output (out, axcls_str);
+		TextIO.closeOut out;
+		if !trace_res then warning axiomfile else ();
+		atp_tac n
+	end;
 
-
-fun atp thm =
-    let val prems = prems_of thm
-    in
-	case prems of [] => () 
-		    | _ => (atp_tac 1 thm; ())
-    end;
+	fun atp thm =
+	let
+		val prems = prems_of thm
+	in
+		case prems of [] => ()
+		            | _  => (atp_tac 1 thm; ())
+	end;
 
 
 (**** For running in Isar ****)
 
-(* same function as that in res_axioms.ML *)
-fun repeat_RS thm1 thm2 =
-    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
-    in
-	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
-    end;
-
-(* a special version of repeat_RS *)
-fun repeat_someI_ex thm = repeat_RS thm someI_ex;
-
+	(* same function as that in res_axioms.ML *)
+	fun repeat_RS thm1 thm2 =
+	let
+		val thm1' = thm1 RS thm2 handle THM _ => thm1
+	in
+		if eq_thm (thm1, thm1') then thm1' else (repeat_RS thm1' thm2)
+	end;
 
-(* convert clauses from "assume" to conjecture. write to file "hyps" *)
-fun isar_atp_h thms =
-    let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
-	val prems' = map repeat_someI_ex prems
-	val prems'' = make_clauses prems'
-	val prems''' = ResAxioms.rm_Eps [] prems''
-	val clss = map ResClause.make_conjecture_clause prems'''
-	val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
-        val hypsfile = File.sysify_path hyps_file
-	val out = TextIO.openOut(hypsfile)
-    in
-	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; if !trace_res then (warning hypsfile) else ())
-    end;
-
-
+	(* a special version of repeat_RS *)
+	fun repeat_someI_ex thm =
+		repeat_RS thm someI_ex;
 
-
-val isar_atp_g = atp_tac;
-
+	(* convert clauses from "assume" to conjecture. write to file "hyps" *)
+	fun isar_atp_h thms =
+	let
+		val prems     = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
+		val prems'    = map repeat_someI_ex prems
+		val prems''   = make_clauses prems'
+		val prems'''  = ResAxioms.rm_Eps [] prems''
+		val clss      = map ResClause.make_conjecture_clause prems'''
+		val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
+		val hypsfile  = File.sysify_path hyps_file
+		val out       = TextIO.openOut hypsfile
+	in
+		ResLib.writeln_strs out tptp_clss;
+		TextIO.closeOut out;
+		if !trace_res then warning hypsfile else ()
+	end;
 
-fun isar_atp_goal' thm k n = 
-    if (k > n) then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
-
-
-fun isar_atp_goal thm n_subgoals = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals));
-
-
+	val isar_atp_g = atp_tac;
 
-fun isar_atp_aux thms thm n_subgoals = 
-    (isar_atp_h thms; isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
+	fun isar_atp_goal' thm k n =
+		if k > n then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
 
+	fun isar_atp_goal thm n_subgoals =
+		if !debug then warning (string_of_thm thm) else isar_atp_goal' thm 1 n_subgoals;
+
+	fun isar_atp_aux thms thm n_subgoals =
+		(isar_atp_h thms;
+		 isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
 
-fun isar_atp' (thms, thm) =
-    let val prems = prems_of thm
-    in
-	case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())
-		    | _ => (isar_atp_aux thms thm (length prems))
-    end;
+	fun isar_atp' (thms, thm) =
+	let
+		val prems = prems_of thm
+	in
+		case prems of [] => if !debug then warning "entering forward, no goal" else ()
+		            | _  => isar_atp_aux thms thm (length prems)
+	end;
 
-
-
-
-local
+	local
 
-fun get_thms_cs claset =
-    let val clsset = rep_cs claset
-	val safeEs = #safeEs clsset
-	val safeIs = #safeIs clsset
-	val hazEs = #hazEs clsset
-	val hazIs = #hazIs clsset
-    in
-	safeEs @ safeIs @ hazEs @ hazIs
-    end;
-
-
-
-fun append_name name [] _ = []
-  | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
+		fun get_thms_cs claset =
+		let
+			val clsset = rep_cs claset
+			val safeEs = #safeEs clsset
+			val safeIs = #safeIs clsset
+			val hazEs  = #hazEs clsset
+			val hazIs  = #hazIs clsset
+		in
+			safeEs @ safeIs @ hazEs @ hazIs
+		end;
 
-fun append_names (name::names) (thms::thmss) =
-    let val thms' = append_name name thms 0
-    in
-	thms'::(append_names names thmss)
-    end;
-
+		fun append_name name []          _ = []
+		  | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)), thm)) :: (append_name name thms (k+1));
 
-fun get_thms_ss [] = []
-  | get_thms_ss thms =
-    let val names = map Thm.name_of_thm thms 
-        val thms' = map (mksimps mksimps_pairs) thms
-        val thms'' = append_names names thms'
-    in
-	ResLib.flat_noDup thms''
-    end;
-
-
-
+		fun append_names (name::names) (thms::thmss) =
+		let
+			val thms' = append_name name thms 0
+		in
+			thms'::(append_names names thmss)
+		end;
 
-in
-
+		fun get_thms_ss []   =
+			[]
+		  | get_thms_ss thms =
+			let
+				val names = map Thm.name_of_thm thms
+				val thms' = map (mksimps mksimps_pairs) thms
+				val thms'' = append_names names thms'
+			in
+				ResLib.flat_noDup thms''
+			end;
 
-(* convert locally declared rules to axiom clauses *)
-(* write axiom clauses to ax_file *)
-fun isar_local_thms (delta_cs, delta_ss_thms) =
-    let val thms_cs = get_thms_cs delta_cs
-	val thms_ss = get_thms_ss delta_ss_thms
-	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
-	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
-	val ax_file = File.sysify_path axiom_file
-	val out = TextIO.openOut ax_file
-    in
-	(ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)
-    end;
-
+	in
 
-
-
+		(* convert locally declared rules to axiom clauses *)
+		(* write axiom clauses to ax_file *)
+		fun isar_local_thms (delta_cs, delta_ss_thms) =
+		let
+			val thms_cs      = get_thms_cs delta_cs
+			val thms_ss      = get_thms_ss delta_ss_thms
+			val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
+			val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
+			val ax_file      = File.sysify_path axiom_file
+			val out          = TextIO.openOut ax_file
+		in
+			ResLib.writeln_strs out clauses_strs;
+			TextIO.closeOut out
+		end;
 
-(* called in Isar automatically *)
-fun isar_atp (ctxt,thm) =
-    let val prems = ProofContext.prems_of ctxt
-      val d_cs = Classical.get_delta_claset ctxt
-      val d_ss_thms = Simplifier.get_delta_simpset ctxt
-    in
-	(isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))
-    end;
+		(* called in Isar automatically *)
+		fun isar_atp (ctxt, thm) =
+		let
+			val prems     = ProofContext.prems_of ctxt
+			val d_cs      = Classical.get_delta_claset ctxt
+			val d_ss_thms = Simplifier.get_delta_simpset ctxt
+		in
+			isar_local_thms (d_cs, d_ss_thms);
+			isar_atp' (prems, thm)
+		end;
 
-end
-
-
-
+	end  (* local *)
 
 end;
 
 Proof.atp_hook := ResAtp.isar_atp;
-
-