# HG changeset patch # User paulson # Date 1162392583 -3600 # Node ID 07549f79d19c107d9941ca38eebe663279d3650c # Parent cf9fe3c408b765fe55fac6e5337c7d7772081187 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. diff -r cf9fe3c408b7 -r 07549f79d19c src/HOL/Tools/res_hol_clause.ML --- 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 *)