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.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.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.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;
```