src/HOL/Tools/res_hol_clause.ML
changeset 20791 497e1c9d4a9f
parent 20660 8606ddd42554
child 20864 bb75b876b260
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Sat Sep 30 14:31:41 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Sat Sep 30 14:32:36 2006 +0200
     1.3 @@ -9,6 +9,20 @@
     1.4  
     1.5  struct
     1.6  
     1.7 +(* theorems for combinators and function extensionality *)
     1.8 +val ext = thm "HOL.ext";
     1.9 +val comb_I = thm "Reconstruction.COMBI_def";
    1.10 +val comb_K = thm "Reconstruction.COMBK_def";
    1.11 +val comb_B = thm "Reconstruction.COMBB_def";
    1.12 +val comb_C = thm "Reconstruction.COMBC_def";
    1.13 +val comb_S = thm "Reconstruction.COMBS_def";
    1.14 +val comb_B' = thm "Reconstruction.COMBB'_def";
    1.15 +val comb_C' = thm "Reconstruction.COMBC'_def";
    1.16 +val comb_S' = thm "Reconstruction.COMBS'_def";
    1.17 +val fequal_imp_equal = thm "Reconstruction.fequal_imp_equal";
    1.18 +val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
    1.19 +
    1.20 +
    1.21  (* a flag to set if we use extra combinators B',C',S' *)
    1.22  val use_combB'C'S' = ref true;
    1.23  
    1.24 @@ -56,8 +70,6 @@
    1.25    | is_free _ _ = false;
    1.26  
    1.27  
    1.28 -exception LAM2COMB of term;
    1.29 -
    1.30  exception BND of term;
    1.31  
    1.32  fun decre_bndVar (Bound n) = Bound (n-1)
    1.33 @@ -202,7 +214,7 @@
    1.34  			     compact_comb (Const("COMBS",tS) $ P' $ Q') Bnds count_comb
    1.35  			 end)))
    1.36      end
    1.37 -  | lam2comb (t as (Abs(x,t1,_))) _ _ = raise LAM2COMB (t);
    1.38 +  | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
    1.39  
    1.40  (*********************)
    1.41  
    1.42 @@ -841,37 +853,26 @@
    1.43  (* write clauses to files                                             *)
    1.44  (**********************************************************************)
    1.45  
    1.46 -(* tptp format *)
    1.47 -
    1.48 -fun read_in fs = map (File.read o File.unpack_platform_path) fs; 
    1.49 +local
    1.50  
    1.51 -fun get_helper_tptp () =
    1.52 -    let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.tptp"]) else []
    1.53 -	val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.tptp"]) else []
    1.54 -	val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.tptp"]) else []
    1.55 -	val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.tptp"]) else []
    1.56 -	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.tptp"]) else []
    1.57 -    in
    1.58 -	("helper1.tptp") :: (IK @ BC @ S @ B'C' @ S')
    1.59 -    end;
    1.60 +val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
    1.61  
    1.62 +in
    1.63  
    1.64 -fun get_helper_clauses_tptp () =
    1.65 -  let val tlevel = case !typ_level of 
    1.66 -		       T_FULL => (Output.debug "Fully-typed HOL"; 
    1.67 -				  "~~/src/HOL/Tools/atp-inputs/full_")
    1.68 -		     | T_PARTIAL => (Output.debug "Partially-typed HOL"; 
    1.69 -				     "~~/src/HOL/Tools/atp-inputs/par_")
    1.70 -		     | T_CONST => (Output.debug "Const-only-typed HOL"; 
    1.71 -				   "~~/src/HOL/Tools/atp-inputs/const_")
    1.72 -		     | T_NONE => (Output.debug "Untyped HOL"; 
    1.73 -				  "~~/src/HOL/Tools/atp-inputs/u_")
    1.74 -      val helpers = get_helper_tptp ()
    1.75 -      val t_helpers = map (curry (op ^) tlevel) helpers
    1.76 -  in
    1.77 -      read_in t_helpers
    1.78 -  end;
    1.79 -	
    1.80 +fun get_helper_clauses () =
    1.81 +    let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) else []
    1.82 +	val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) else []
    1.83 +	val S = if !combS_count > 0 then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) else []
    1.84 +	val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) else []
    1.85 +	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) else []
    1.86 +	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
    1.87 +    in
    1.88 +	make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') []
    1.89 +    end
    1.90 +
    1.91 +end
    1.92 +
    1.93 +(* tptp format *)
    1.94  						  
    1.95  (* write TPTP format to a single file *)
    1.96  (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *)
    1.97 @@ -881,47 +882,21 @@
    1.98  	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
    1.99  	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.100  	val out = TextIO.openOut filename
   1.101 -	val helper_clauses = get_helper_clauses_tptp ()
   1.102 +	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
   1.103      in
   1.104  	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses';
   1.105  	ResClause.writeln_strs out tfree_clss;
   1.106  	ResClause.writeln_strs out tptp_clss;
   1.107  	List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses;
   1.108  	List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses;
   1.109 -	List.app (curry TextIO.output out) helper_clauses;
   1.110 +	List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   1.111  	TextIO.closeOut out;
   1.112  	clnames
   1.113      end;
   1.114  
   1.115  
   1.116 -fun get_helper_dfg () =
   1.117 -    let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.dfg"]) else []
   1.118 -	val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.dfg"]) else []
   1.119 -	val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.dfg"]) else []
   1.120 -	val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.dfg"]) else []
   1.121 -	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.dfg"]) else []
   1.122 -    in
   1.123 -	("helper1.dfg") :: (IK @ BC @ S @ B'C' @ S')
   1.124 -    end;
   1.125 -
   1.126  
   1.127  (* dfg format *)
   1.128 -fun get_helper_clauses_dfg () = 
   1.129 - let val tlevel = case !typ_level of 
   1.130 -                      T_FULL => (Output.debug "Fully-typed HOL"; 
   1.131 -                                 "~~/src/HOL/Tools/atp-inputs/full_")
   1.132 -		    | T_PARTIAL => (Output.debug "Partially-typed HOL"; 
   1.133 -		                    "~~/src/HOL/Tools/atp-inputs/par_")
   1.134 -		    | T_CONST => (Output.debug "Const-only-typed HOL"; 
   1.135 -		                  "~~/src/HOL/Tools/atp-inputs/const_")
   1.136 -		    | T_NONE => (Output.debug "Untyped HOL"; 
   1.137 -		                 "~~/src/HOL/Tools/atp-inputs/u_")
   1.138 -     val helpers = get_helper_dfg ()
   1.139 -     val t_helpers = map (curry (op ^) tlevel) helpers
   1.140 - in
   1.141 -     read_in t_helpers
   1.142 - end;
   1.143 -
   1.144  
   1.145  fun dfg_write_file  thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas =
   1.146      let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) 
   1.147 @@ -935,7 +910,8 @@
   1.148  	val (axstrs,_) =  ListPair.unzip (map clause2dfg axclauses')
   1.149  	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
   1.150  	val out = TextIO.openOut filename
   1.151 -	val helper_clauses = get_helper_clauses_dfg ()
   1.152 +	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
   1.153 +	val helper_clauses_strs = (#1 o ListPair.unzip o (map clause2dfg)) helper_clauses
   1.154      in
   1.155  	TextIO.output (out, ResClause.string_of_start probname); 
   1.156  	TextIO.output (out, ResClause.string_of_descrip probname); 
   1.157 @@ -944,7 +920,7 @@
   1.158  	ResClause.writeln_strs out axstrs;
   1.159  	List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses;
   1.160  	List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses;
   1.161 -	ResClause.writeln_strs out helper_clauses;
   1.162 +	ResClause.writeln_strs out helper_clauses_strs;
   1.163  	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   1.164  	ResClause.writeln_strs out tfree_clss;
   1.165  	ResClause.writeln_strs out dfg_clss;