src/HOL/Tools/res_hol_clause.ML
changeset 21135 07549f79d19c
parent 21108 04d8e6eb9a2e
child 21254 d53f76357f41
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Nov 01 15:45:44 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Nov 01 15:49:43 2006 +0100
     1.3 @@ -22,7 +22,6 @@
     1.4  val fequal_imp_equal = thm "Reconstruction.fequal_imp_equal";
     1.5  val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
     1.6  
     1.7 -
     1.8  (*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
     1.9    combinators appear to work best.*)
    1.10  val use_Turner = ref false;
    1.11 @@ -81,17 +80,6 @@
    1.12    | is_free _ _ = false;
    1.13  
    1.14  
    1.15 -exception BND of term;
    1.16 -
    1.17 -fun decre_bndVar (Bound n) = Bound (n-1)
    1.18 -  | decre_bndVar (P $ Q) = (decre_bndVar P) $ (decre_bndVar Q)
    1.19 -  | decre_bndVar t =
    1.20 -    case t of Const(_,_) => t
    1.21 -	    | Free(_,_) => t
    1.22 -	    | Var(_,_) => t
    1.23 -	    | Abs(_,_,_) => raise BND(t); (*should not occur*)
    1.24 -
    1.25 -
    1.26  (*******************************************)
    1.27  fun mk_compact_comb (tm as (Const("Reconstruction.COMBB",_)$p) $ (Const("Reconstruction.COMBB",_)$q$r)) Bnds count_comb =
    1.28      let val tp_p = Term.type_of1(Bnds,p)
    1.29 @@ -134,54 +122,47 @@
    1.30    if !use_Turner then mk_compact_comb t Bnds count_comb else t;
    1.31  
    1.32  fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = 
    1.33 -      let val tpI = Type("fun",[tp,tp])
    1.34 -	  val _ = increI count_comb
    1.35 +      let val _ = increI count_comb
    1.36        in 
    1.37 -	  Const("Reconstruction.COMBI",tpI) 
    1.38 +	  Const("Reconstruction.COMBI",tp-->tp) 
    1.39        end
    1.40    | lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = 
    1.41 -      let val (Bound n') = decre_bndVar (Bound n)
    1.42 -	  val tb = List.nth(Bnds,n')
    1.43 -	  val tK = Type("fun",[tb,Type("fun",[tp,tb])])
    1.44 +      let val tb = List.nth(Bnds,n-1)
    1.45  	  val _ = increK count_comb 
    1.46        in
    1.47 -	  Const("Reconstruction.COMBK",tK) $ (Bound n')
    1.48 +	  Const("Reconstruction.COMBK", [tb,tp] ---> tb) $ (Bound (n-1))
    1.49        end
    1.50    | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = 
    1.51 -      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.52 -	  val _ = increK count_comb 
    1.53 +      let val _ = increK count_comb 
    1.54        in 
    1.55 -	  Const("Reconstruction.COMBK",tK) $ Const(c,t2) 
    1.56 +	  Const("Reconstruction.COMBK",[t2,t1] ---> t2) $ Const(c,t2) 
    1.57        end
    1.58    | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
    1.59 -      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.60 -	  val _ = increK count_comb
    1.61 +      let val _ = increK count_comb
    1.62        in
    1.63 -	  Const("Reconstruction.COMBK",tK) $ Free(v,t2)
    1.64 +	  Const("Reconstruction.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
    1.65        end
    1.66    | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
    1.67 -      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.68 -	  val _ = increK count_comb 
    1.69 +      let val _ = increK count_comb 
    1.70        in
    1.71 -	  Const("Reconstruction.COMBK",tK) $ Var(ind,t2)
    1.72 +	  Const("Reconstruction.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
    1.73        end
    1.74    | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb =
    1.75 -      let val nfreeP = not(is_free P 0)
    1.76 -	  val tr = Term.type_of1(t1::Bnds,P)
    1.77 +      let val tr = Term.type_of1(t1::Bnds,P)
    1.78        in
    1.79 -	  if nfreeP then (decre_bndVar P)
    1.80 +	  if not(is_free P 0) then (incr_boundvars ~1 P)
    1.81  	  else 
    1.82 -	  let val tI = Type("fun",[t1,t1])
    1.83 +	  let val tI = [t1] ---> t1
    1.84  	      val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
    1.85  	      val tp' = Term.type_of1(Bnds,P')
    1.86 -	      val tS = Type("fun",[tp',Type("fun",[tI,tr])])
    1.87 +	      val tS = [tp',tI] ---> tr
    1.88  	      val _ = increI count_comb
    1.89  	      val _ = increS count_comb
    1.90  	  in
    1.91 -	      compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb
    1.92 +	      compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ 
    1.93 +	                     Const("Reconstruction.COMBI",tI)) Bnds count_comb
    1.94  	  end
    1.95 -      end
    1.96 -	    
    1.97 +      end	    
    1.98    | lam2comb (t as (Abs(x,t1,P$Q))) Bnds count_comb =
    1.99        let val nfreeP = not(is_free P 0)
   1.100  	  and nfreeQ = not(is_free Q 0)
   1.101 @@ -189,28 +170,28 @@
   1.102        in
   1.103  	  if nfreeP andalso nfreeQ 
   1.104  	  then 
   1.105 -	    let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])])
   1.106 -		val PQ' = decre_bndVar(P $ Q)
   1.107 +	    let val tK = [tpq,t1] ---> tpq
   1.108 +		val PQ' = incr_boundvars ~1(P $ Q)
   1.109  		val _ = increK count_comb
   1.110  	    in 
   1.111  		Const("Reconstruction.COMBK",tK) $ PQ'
   1.112  	    end
   1.113  	  else if nfreeP then 
   1.114  	    let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
   1.115 -		val P' = decre_bndVar P
   1.116 +		val P' = incr_boundvars ~1 P
   1.117  		val tp = Term.type_of1(Bnds,P')
   1.118  		val tq' = Term.type_of1(Bnds, Q')
   1.119 -		val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.120 +		val tB = [tp,tq',t1] ---> tpq
   1.121  		val _ = increB count_comb
   1.122  	    in
   1.123  		compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb 
   1.124  	    end
   1.125  	  else if nfreeQ then 
   1.126  	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.127 -		val Q' = decre_bndVar Q
   1.128 +		val Q' = incr_boundvars ~1 Q
   1.129  		val tq = Term.type_of1(Bnds,Q')
   1.130  		val tp' = Term.type_of1(Bnds, P')
   1.131 -		val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
   1.132 +		val tC = [tp',tq,t1] ---> tpq
   1.133  		val _ = increC count_comb
   1.134  	    in
   1.135  		compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
   1.136 @@ -220,7 +201,7 @@
   1.137  		val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb 
   1.138  		val tp' = Term.type_of1(Bnds,P')
   1.139  		val tq' = Term.type_of1(Bnds,Q')
   1.140 -		val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.141 +		val tS = [tp',tq',t1] ---> tpq
   1.142  		val _ = increS count_comb
   1.143  	    in
   1.144  		compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
   1.145 @@ -444,15 +425,13 @@
   1.146  fun too_general_terms (CombVar(v,_), t) = not (occurs v t)
   1.147    | too_general_terms _ = false;
   1.148  
   1.149 -fun too_general_lit (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
   1.150 +fun too_general_equality (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
   1.151        too_general_terms (t1,t2) orelse too_general_terms (t2,t1)
   1.152 -  | too_general_lit _ = false;
   1.153 +  | too_general_equality _ = false;
   1.154  
   1.155 -(* forbid a clause that contains hBOOL(V) *)
   1.156 -fun too_general [] = false
   1.157 -  | too_general (lit::lits) = 
   1.158 -    case lit of Literal(_,Bool(CombVar(_,_))) => true
   1.159 -	      | _ => too_general lits;
   1.160 +(* forbid the literal hBOOL(V) *)
   1.161 +fun too_general_bool (Literal(_,Bool(CombVar _))) = true
   1.162 +  | too_general_bool _ = false;
   1.163  
   1.164  (* making axiom and conjecture clauses *)
   1.165  exception MAKE_CLAUSE
   1.166 @@ -464,12 +443,9 @@
   1.167      in
   1.168  	if forall isFalse lits
   1.169  	then error "Problem too trivial for resolution (empty clause)"
   1.170 -	else if too_general lits 
   1.171 -	then (Output.debug ("Omitting " ^ axiom_name ^ ": clause contains universal predicates"); 
   1.172 -	     raise MAKE_CLAUSE)
   1.173 -	else
   1.174 -	    if (!typ_level <> T_FULL) andalso kind=Axiom andalso forall too_general_lit lits 
   1.175 -	    then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); 
   1.176 +	else if (!typ_level <> T_FULL) andalso kind=Axiom andalso 
   1.177 +	        (forall too_general_equality lits orelse exists too_general_bool lits)
   1.178 +	    then (Output.debug ("Omitting " ^ axiom_name ^ ": clause is too prolific"); 
   1.179  	          raise MAKE_CLAUSE) 
   1.180  	else
   1.181  	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
   1.182 @@ -512,7 +488,7 @@
   1.183  val type_wrapper = "typeinfo";
   1.184  
   1.185  fun wrap_type (c,t) = 
   1.186 -    case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [c,t])
   1.187 +    case !typ_level of T_FULL => type_wrapper ^ ResClause.paren_pack [c,t]
   1.188  		     | _ => c;
   1.189      
   1.190  
   1.191 @@ -545,19 +521,18 @@
   1.192      let val (s1,tp1) = string_of_combterm1_aux is_pred t1
   1.193  	val (s2,tp2) = string_of_combterm1_aux is_pred t2
   1.194  	val tp' = ResClause.string_of_fol_type tp
   1.195 -	val r =	case !typ_level of T_FULL => type_wrapper ^  (ResClause.paren_pack [(app_str ^ (ResClause.paren_pack [s1,s2])),tp'])
   1.196 -				 | T_PARTIAL => app_str ^ (ResClause.paren_pack [s1,s2,tp1])
   1.197 -				 | T_NONE => app_str ^ (ResClause.paren_pack [s1,s2])
   1.198 -				 | T_CONST => raise STRING_OF_COMBTERM (1) (*should not happen, if happened may be a bug*)
   1.199 -    in	(r,tp')
   1.200 -
   1.201 -    end
   1.202 +	val r =	case !typ_level of
   1.203 +	            T_FULL => type_wrapper ^ ResClause.paren_pack [(app_str ^ ResClause.paren_pack [s1,s2]),tp']
   1.204 +		  | T_PARTIAL => app_str ^ ResClause.paren_pack [s1,s2,tp1]
   1.205 +		  | T_NONE => app_str ^ ResClause.paren_pack [s1,s2]
   1.206 +		  | T_CONST => raise STRING_OF_COMBTERM 1 (*should not happen, if happened may be a bug*)
   1.207 +    in	(r,tp')   end
   1.208    | string_of_combterm1_aux is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   1.209      if is_pred then 
   1.210  	let val (s1,_) = string_of_combterm1_aux false t1
   1.211  	    val (s2,_) = string_of_combterm1_aux false t2
   1.212  	in
   1.213 -	    ("equal" ^ (ResClause.paren_pack [s1,s2]),bool_tp)
   1.214 +	    ("equal" ^ ResClause.paren_pack [s1,s2], bool_tp)
   1.215  	end
   1.216      else
   1.217  	let val (t,_) = string_of_combterm1_aux false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   1.218 @@ -566,7 +541,7 @@
   1.219  	end
   1.220    | string_of_combterm1_aux is_pred (Bool(t)) = 
   1.221      let val (t',_) = string_of_combterm1_aux false t
   1.222 -	val r = if is_pred then bool_str ^ (ResClause.paren_pack [t'])
   1.223 +	val r = if is_pred then bool_str ^ ResClause.paren_pack [t']
   1.224  		else t'
   1.225      in
   1.226  	(r,bool_tp)
   1.227 @@ -578,7 +553,7 @@
   1.228      let val tvars' = map string_of_ctyp tvars
   1.229  	val c' = if c = "equal" then "c_fequal" else c
   1.230      in
   1.231 -	c' ^ (ResClause.paren_pack tvars')
   1.232 +	c' ^ ResClause.paren_pack tvars'
   1.233      end
   1.234    | string_of_combterm2 _ (CombFree(v,tp)) = v
   1.235    | string_of_combterm2 _ (CombVar(v,tp)) = v
   1.236 @@ -586,14 +561,14 @@
   1.237      let val s1 = string_of_combterm2 is_pred t1
   1.238  	val s2 = string_of_combterm2 is_pred t2
   1.239      in
   1.240 -	app_str ^ (ResClause.paren_pack [s1,s2])
   1.241 +	app_str ^ ResClause.paren_pack [s1,s2]
   1.242      end
   1.243    | string_of_combterm2 is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   1.244      if is_pred then 
   1.245  	let val s1 = string_of_combterm2 false t1
   1.246  	    val s2 = string_of_combterm2 false t2
   1.247  	in
   1.248 -	    ("equal" ^ (ResClause.paren_pack [s1,s2]))
   1.249 +	    ("equal" ^ ResClause.paren_pack [s1,s2])
   1.250  	end
   1.251      else
   1.252  	string_of_combterm2 false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   1.253 @@ -601,17 +576,14 @@
   1.254    | string_of_combterm2 is_pred (Bool(t)) = 
   1.255      let val t' = string_of_combterm2 false t
   1.256      in
   1.257 -	if is_pred then bool_str ^ (ResClause.paren_pack [t'])
   1.258 +	if is_pred then bool_str ^ ResClause.paren_pack [t']
   1.259  	else t'
   1.260      end;
   1.261  
   1.262 -
   1.263 -
   1.264  fun string_of_combterm is_pred term = 
   1.265      case !typ_level of T_CONST => string_of_combterm2 is_pred term
   1.266  		     | _ => string_of_combterm1 is_pred term;
   1.267  
   1.268 -
   1.269  fun string_of_clausename (cls_id,ax_name) = 
   1.270      ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.271  
   1.272 @@ -737,24 +709,39 @@
   1.273  (* write clauses to files                                             *)
   1.274  (**********************************************************************)
   1.275  
   1.276 -local
   1.277 -
   1.278  val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   1.279  
   1.280 -in
   1.281 +(*Simulate the result of conversion to CNF*)
   1.282 +fun pretend_cnf s = (thm s, (s,0));
   1.283 +
   1.284 +(*These theorems allow the proof of P=Q from P-->Q and Q-->P, so they are necessary for
   1.285 +  completeness. Unfortunately, they are very prolific, causing greatly increased runtimes.
   1.286 +  They also lead to many unsound proofs. Thus it is well that the "exists too_general_bool"
   1.287 +  test deletes them except with the full-typed translation.*)
   1.288 +val iff_thms = [pretend_cnf "Reconstruction.iff_positive", 
   1.289 +                pretend_cnf "Reconstruction.iff_negative"];
   1.290  
   1.291  fun get_helper_clauses () =
   1.292 -    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.293 -	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.294 -	val S = if !combS_count > 0 then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) else []
   1.295 -	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.296 -	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) else []
   1.297 +    let val IK = if !combI_count > 0 orelse !combK_count > 0 
   1.298 +                 then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) 
   1.299 +                 else []
   1.300 +	val BC = if !combB_count > 0 orelse !combC_count > 0 
   1.301 +	         then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) 
   1.302 +	         else []
   1.303 +	val S = if !combS_count > 0 
   1.304 +	        then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) 
   1.305 +	        else []
   1.306 +	val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 
   1.307 +	           then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) 
   1.308 +	           else []
   1.309 +	val S' = if !combS'_count > 0 
   1.310 +	         then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) 
   1.311 +	         else []
   1.312  	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   1.313      in
   1.314 -	make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') []
   1.315 +	make_axiom_clauses (iff_thms @ other @ IK @ BC @ S @ B'C' @ S') []
   1.316      end
   1.317  
   1.318 -end
   1.319  
   1.320  (* tptp format *)
   1.321