# HG changeset patch
# User paulson
# Date 1110816250 -3600
# Node ID f161fa6f8fd55e624ee216672352fec5e7480d1c
# Parent  30576c645e91e83428446a630756c0636c8ba4ba
bug fixes involving typechecking clauses

diff -r 30576c645e91 -r f161fa6f8fd5 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sat Mar 12 00:07:05 2005 +0100
+++ b/src/HOL/Tools/res_atp.ML	Mon Mar 14 17:04:10 2005 +0100
@@ -1,7 +1,6 @@
-(*  Title:      HOL/Tools/res_atp.ML
-    ID:         $Id$
-    Author:     Jia Meng, Cambridge University Computer Laboratory
-    Copyright   2004 University of Cambridge
+(*  Author: Jia Meng, Cambridge University Computer Laboratory
+    ID: $Id$
+    Copyright 2004 University of Cambridge
 
 ATPs with TPTP format input.
 *)
@@ -11,207 +10,237 @@
 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;
+(* 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;
+
 
-	(* a special version of repeat_RS *)
-	fun repeat_someI_ex thm =
-		repeat_RS thm someI_ex;
+(* 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,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss) 
+	val tfree_lits = ResLib.flat_noDup tfree_litss
+	val tfree_clss = map ResClause.tfree_clause tfree_lits 
+        val hypsfile = File.sysify_path hyps_file
+	val out = TextIO.openOut(hypsfile)
+    in
+	((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 
+    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;
+fun tptp_inputs_tfrees thms n tfrees = 
+    let val clss = map (ResClause.make_conjecture_clause_thm) thms
+	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
+	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
+        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
+	val out = TextIO.openOut(probfile)
+    in
+	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
+    end;
 
-	val isar_atp_g = atp_tac;
+
+fun call_atp_tac_tfrees thms n tfrees = (tptp_inputs_tfrees thms n tfrees; dummy_tac);
+
+
+fun atp_tac_tfrees tfrees n  = SELECT_GOAL
+  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
+  METAHYPS(fn negs => (call_atp_tac_tfrees (make_clauses negs) n tfrees))]) n;
+
+
+fun isar_atp_g tfrees = atp_tac_tfrees tfrees;
 
-	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 k n tfree_lits = 
+    if (k > n) then () else (isar_atp_g tfree_lits k thm; isar_atp_goal' thm (k+1) n tfree_lits);
+
 
-	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_goal thm n_subgoals tfree_lits = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals tfree_lits));
 
-	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_aux thms thm n_subgoals = 
+    let val tfree_lits = isar_atp_h thms 
+    in
+	isar_atp_goal thm n_subgoals tfree_lits
+    end;
+   
 
-	local
+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 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;
+
+
+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 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 append_names (name::names) (thms::thmss) =
+    let val thms' = append_name name thms 0
+    in
+	thms'::(append_names names thmss)
+    end;
+
 
-		fun append_names (name::names) (thms::thmss) =
-		let
-			val thms' = append_name name thms 0
-		in
-			thms'::(append_names names thmss)
-		end;
+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 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;
+
+
+in
+
 
-	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;
 
-		(* 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  (* local *)
+end
+
+
+
 
 end;
 
 Proof.atp_hook := ResAtp.isar_atp;
+
+
diff -r 30576c645e91 -r f161fa6f8fd5 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sat Mar 12 00:07:05 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Mon Mar 14 17:04:10 2005 +0100
@@ -262,7 +262,7 @@
     let val thm' = transfer_to_Reconstruction thm
 	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
     in
-	rm_redundant_cls thm''
+	map Thm.varifyT (rm_redundant_cls thm'')
     end;
 
 fun meta_cnf_axiom thm = 
diff -r 30576c645e91 -r f161fa6f8fd5 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Sat Mar 12 00:07:05 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Mon Mar 14 17:04:10 2005 +0100
@@ -33,6 +33,8 @@
     val tptp_clauses2str : string list -> string
     val typed : unit -> unit
     val untyped : unit -> unit
+    val clause2tptp : clause -> string * string list
+    val tfree_clause : string -> string
   end;
 
 structure ResClause : RES_CLAUSE =
@@ -612,7 +614,7 @@
 	(tvar_lits_strs @ lits,tfree_lits)
     end; 
 
-    
+
 fun tptp_clause cls =
     let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
 	val cls_id = string_of_clauseID cls
@@ -627,6 +629,20 @@
     end;
 
 
+fun clause2tptp cls =
+    let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
+	val cls_id = string_of_clauseID cls
+	val ax_name = string_of_axiomName cls
+	val knd = string_of_kind cls
+	val lits_str = ResLib.list_to_string' lits
+	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
+    in
+	(cls_str,tfree_lits) 
+    end;
+
+
+fun tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
+
 val delim = "\n";
 val tptp_clauses2str = ResLib.list2str_sep delim;