author paulson Wed, 01 Nov 2006 15:49:43 +0100 changeset 21135 07549f79d19c parent 21134 cf9fe3c408b7 child 21136 85fd05aaf737
Numerous cosmetic changes. Use of ---> notation for types. Added rules for the introduction of the iff connective, but they are too prolific to be useful.
```--- a/src/HOL/Tools/res_hol_clause.ML	Wed Nov 01 15:45:44 2006 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Wed Nov 01 15:49:43 2006 +0100
@@ -22,7 +22,6 @@
val fequal_imp_equal = thm "Reconstruction.fequal_imp_equal";
val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";

-
(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
combinators appear to work best.*)
val use_Turner = ref false;
@@ -81,17 +80,6 @@
| is_free _ _ = false;

-exception BND of term;
-
-fun decre_bndVar (Bound n) = Bound (n-1)
-  | decre_bndVar (P \$ Q) = (decre_bndVar P) \$ (decre_bndVar Q)
-  | decre_bndVar t =
-    case t of Const(_,_) => t
-	    | Free(_,_) => t
-	    | Var(_,_) => t
-	    | Abs(_,_,_) => raise BND(t); (*should not occur*)
-
-
(*******************************************)
fun mk_compact_comb (tm as (Const("Reconstruction.COMBB",_)\$p) \$ (Const("Reconstruction.COMBB",_)\$q\$r)) Bnds count_comb =
let val tp_p = Term.type_of1(Bnds,p)
@@ -134,54 +122,47 @@
if !use_Turner then mk_compact_comb t Bnds count_comb else t;

fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb =
-      let val tpI = Type("fun",[tp,tp])
-	  val _ = increI count_comb
+      let val _ = increI count_comb
in
-	  Const("Reconstruction.COMBI",tpI)
+	  Const("Reconstruction.COMBI",tp-->tp)
end
| lam2comb (Abs(x,tp,Bound n)) Bnds count_comb =
-      let val (Bound n') = decre_bndVar (Bound n)
-	  val tb = List.nth(Bnds,n')
-	  val tK = Type("fun",[tb,Type("fun",[tp,tb])])
+      let val tb = List.nth(Bnds,n-1)
val _ = increK count_comb
in
-	  Const("Reconstruction.COMBK",tK) \$ (Bound n')
+	  Const("Reconstruction.COMBK", [tb,tp] ---> tb) \$ (Bound (n-1))
end
| lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb =
-      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
-	  val _ = increK count_comb
+      let val _ = increK count_comb
in
-	  Const("Reconstruction.COMBK",tK) \$ Const(c,t2)
+	  Const("Reconstruction.COMBK",[t2,t1] ---> t2) \$ Const(c,t2)
end
| lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
-      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
-	  val _ = increK count_comb
+      let val _ = increK count_comb
in
-	  Const("Reconstruction.COMBK",tK) \$ Free(v,t2)
+	  Const("Reconstruction.COMBK",[t2,t1] ---> t2) \$ Free(v,t2)
end
| lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
-      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
-	  val _ = increK count_comb
+      let val _ = increK count_comb
in
-	  Const("Reconstruction.COMBK",tK) \$ Var(ind,t2)
+	  Const("Reconstruction.COMBK", [t2,t1] ---> t2) \$ Var(ind,t2)
end
| lam2comb (t as (Abs(x,t1,P\$(Bound 0)))) Bnds count_comb =
-      let val nfreeP = not(is_free P 0)
-	  val tr = Term.type_of1(t1::Bnds,P)
+      let val tr = Term.type_of1(t1::Bnds,P)
in
-	  if nfreeP then (decre_bndVar P)
+	  if not(is_free P 0) then (incr_boundvars ~1 P)
else
-	  let val tI = Type("fun",[t1,t1])
+	  let val tI = [t1] ---> t1
val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
val tp' = Term.type_of1(Bnds,P')
-	      val tS = Type("fun",[tp',Type("fun",[tI,tr])])
+	      val tS = [tp',tI] ---> tr
val _ = increI count_comb
val _ = increS count_comb
in
-	      compact_comb (Const("Reconstruction.COMBS",tS) \$ P' \$ Const("Reconstruction.COMBI",tI)) Bnds count_comb
+	      compact_comb (Const("Reconstruction.COMBS",tS) \$ P' \$
+	                     Const("Reconstruction.COMBI",tI)) Bnds count_comb
end
-      end
-
+      end
| lam2comb (t as (Abs(x,t1,P\$Q))) Bnds count_comb =
let val nfreeP = not(is_free P 0)
and nfreeQ = not(is_free Q 0)
@@ -189,28 +170,28 @@
in
if nfreeP andalso nfreeQ
then
-	    let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])])
-		val PQ' = decre_bndVar(P \$ Q)
+	    let val tK = [tpq,t1] ---> tpq
+		val PQ' = incr_boundvars ~1(P \$ Q)
val _ = increK count_comb
in
Const("Reconstruction.COMBK",tK) \$ PQ'
end
else if nfreeP then
let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
-		val P' = decre_bndVar P
+		val P' = incr_boundvars ~1 P
val tp = Term.type_of1(Bnds,P')
val tq' = Term.type_of1(Bnds, Q')
-		val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
+		val tB = [tp,tq',t1] ---> tpq
val _ = increB count_comb
in
compact_comb (Const("Reconstruction.COMBB",tB) \$ P' \$ Q') Bnds count_comb
end
else if nfreeQ then
let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
-		val Q' = decre_bndVar Q
+		val Q' = incr_boundvars ~1 Q
val tq = Term.type_of1(Bnds,Q')
val tp' = Term.type_of1(Bnds, P')
-		val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
+		val tC = [tp',tq,t1] ---> tpq
val _ = increC count_comb
in
compact_comb (Const("Reconstruction.COMBC",tC) \$ P' \$ Q') Bnds count_comb
@@ -220,7 +201,7 @@
val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
val tp' = Term.type_of1(Bnds,P')
val tq' = Term.type_of1(Bnds,Q')
-		val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
+		val tS = [tp',tq',t1] ---> tpq
val _ = increS count_comb
in
compact_comb (Const("Reconstruction.COMBS",tS) \$ P' \$ Q') Bnds count_comb
@@ -444,15 +425,13 @@
fun too_general_terms (CombVar(v,_), t) = not (occurs v t)
| too_general_terms _ = false;

-fun too_general_lit (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
+fun too_general_equality (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
too_general_terms (t1,t2) orelse too_general_terms (t2,t1)
-  | too_general_lit _ = false;
+  | too_general_equality _ = false;

-(* forbid a clause that contains hBOOL(V) *)
-fun too_general [] = false
-  | too_general (lit::lits) =
-    case lit of Literal(_,Bool(CombVar(_,_))) => true
-	      | _ => too_general lits;
+(* forbid the literal hBOOL(V) *)
+fun too_general_bool (Literal(_,Bool(CombVar _))) = true
+  | too_general_bool _ = false;

(* making axiom and conjecture clauses *)
exception MAKE_CLAUSE
@@ -464,12 +443,9 @@
in
if forall isFalse lits
then error "Problem too trivial for resolution (empty clause)"
-	else if too_general lits
-	then (Output.debug ("Omitting " ^ axiom_name ^ ": clause contains universal predicates");
-	     raise MAKE_CLAUSE)
-	else
-	    if (!typ_level <> T_FULL) andalso kind=Axiom andalso forall too_general_lit lits
-	    then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general");
+	else if (!typ_level <> T_FULL) andalso kind=Axiom andalso
+	        (forall too_general_equality lits orelse exists too_general_bool lits)
+	    then (Output.debug ("Omitting " ^ axiom_name ^ ": clause is too prolific");
raise MAKE_CLAUSE)
else
Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
@@ -512,7 +488,7 @@
val type_wrapper = "typeinfo";

fun wrap_type (c,t) =
-    case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [c,t])
+    case !typ_level of T_FULL => type_wrapper ^ ResClause.paren_pack [c,t]
| _ => c;

@@ -545,19 +521,18 @@
let val (s1,tp1) = string_of_combterm1_aux is_pred t1
val (s2,tp2) = string_of_combterm1_aux is_pred t2
val tp' = ResClause.string_of_fol_type tp
-	val r =	case !typ_level of T_FULL => type_wrapper ^  (ResClause.paren_pack [(app_str ^ (ResClause.paren_pack [s1,s2])),tp'])
-				 | T_PARTIAL => app_str ^ (ResClause.paren_pack [s1,s2,tp1])
-				 | T_NONE => app_str ^ (ResClause.paren_pack [s1,s2])
-				 | T_CONST => raise STRING_OF_COMBTERM (1) (*should not happen, if happened may be a bug*)
-    in	(r,tp')
-
-    end
+	val r =	case !typ_level of
+	            T_FULL => type_wrapper ^ ResClause.paren_pack [(app_str ^ ResClause.paren_pack [s1,s2]),tp']
+		  | T_PARTIAL => app_str ^ ResClause.paren_pack [s1,s2,tp1]
+		  | T_NONE => app_str ^ ResClause.paren_pack [s1,s2]
+		  | T_CONST => raise STRING_OF_COMBTERM 1 (*should not happen, if happened may be a bug*)
+    in	(r,tp')   end
| string_of_combterm1_aux is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
if is_pred then
let val (s1,_) = string_of_combterm1_aux false t1
val (s2,_) = string_of_combterm1_aux false t2
in
-	    ("equal" ^ (ResClause.paren_pack [s1,s2]),bool_tp)
+	    ("equal" ^ ResClause.paren_pack [s1,s2], bool_tp)
end
else
let val (t,_) = string_of_combterm1_aux false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
@@ -566,7 +541,7 @@
end
| string_of_combterm1_aux is_pred (Bool(t)) =
let val (t',_) = string_of_combterm1_aux false t
-	val r = if is_pred then bool_str ^ (ResClause.paren_pack [t'])
+	val r = if is_pred then bool_str ^ ResClause.paren_pack [t']
else t'
in
(r,bool_tp)
@@ -578,7 +553,7 @@
let val tvars' = map string_of_ctyp tvars
val c' = if c = "equal" then "c_fequal" else c
in
-	c' ^ (ResClause.paren_pack tvars')
+	c' ^ ResClause.paren_pack tvars'
end
| string_of_combterm2 _ (CombFree(v,tp)) = v
| string_of_combterm2 _ (CombVar(v,tp)) = v
@@ -586,14 +561,14 @@
let val s1 = string_of_combterm2 is_pred t1
val s2 = string_of_combterm2 is_pred t2
in
-	app_str ^ (ResClause.paren_pack [s1,s2])
+	app_str ^ ResClause.paren_pack [s1,s2]
end
| string_of_combterm2 is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
if is_pred then
let val s1 = string_of_combterm2 false t1
val s2 = string_of_combterm2 false t2
in
-	    ("equal" ^ (ResClause.paren_pack [s1,s2]))
+	    ("equal" ^ ResClause.paren_pack [s1,s2])
end
else
string_of_combterm2 false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
@@ -601,17 +576,14 @@
| string_of_combterm2 is_pred (Bool(t)) =
let val t' = string_of_combterm2 false t
in
-	if is_pred then bool_str ^ (ResClause.paren_pack [t'])
+	if is_pred then bool_str ^ ResClause.paren_pack [t']
else t'
end;

-
-
fun string_of_combterm is_pred term =
case !typ_level of T_CONST => string_of_combterm2 is_pred term
| _ => string_of_combterm1 is_pred term;

-
fun string_of_clausename (cls_id,ax_name) =
ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;

@@ -737,24 +709,39 @@
(* write clauses to files                                             *)
(**********************************************************************)

-local
-
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)

-in
+(*Simulate the result of conversion to CNF*)
+fun pretend_cnf s = (thm s, (s,0));
+
+(*These theorems allow the proof of P=Q from P-->Q and Q-->P, so they are necessary for
+  completeness. Unfortunately, they are very prolific, causing greatly increased runtimes.
+  They also lead to many unsound proofs. Thus it is well that the "exists too_general_bool"
+  test deletes them except with the full-typed translation.*)
+val iff_thms = [pretend_cnf "Reconstruction.iff_positive",
+                pretend_cnf "Reconstruction.iff_negative"];

fun get_helper_clauses () =
-    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 []
-	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 []
-	val S = if !combS_count > 0 then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) else []
-	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 []
-	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) else []
+    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 []
+	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 []
+	val S = if !combS_count > 0
+	        then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S])
+	        else []
+	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 []
+	val S' = if !combS'_count > 0
+	         then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S'])
+	         else []
val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
in
-	make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') []
+	make_axiom_clauses (iff_thms @ other @ IK @ BC @ S @ B'C' @ S') []
end

-end

(* tptp format *)
```