src/HOL/Tools/res_hol_clause.ML
changeset 20360 8c8c824dccdc
parent 20281 16733b31e1cf
child 20421 d9606c64bc23
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Aug 08 12:28:00 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Aug 08 18:40:04 2006 +0200
     1.3 @@ -158,14 +158,9 @@
     1.4  
     1.5  fun string_of_term (Const(c,t)) = c
     1.6    | string_of_term (Free(v,t)) = v
     1.7 -  | string_of_term (Var((x,n),t)) =
     1.8 -    let val xn = x ^ "_" ^ (string_of_int n)
     1.9 -    in xn end
    1.10 +  | string_of_term (Var((x,n),t)) = x ^ "_" ^ (string_of_int n)
    1.11    | string_of_term (P $ Q) =
    1.12 -    let val P' = string_of_term P
    1.13 -	val Q' = string_of_term Q
    1.14 -    in
    1.15 -	"(" ^ P' ^ " " ^ Q' ^ ")" end
    1.16 +      "(" ^ string_of_term P ^ " " ^ string_of_term Q ^ ")" 
    1.17    | string_of_term t =  raise TERM_COMB (t);
    1.18  
    1.19  
    1.20 @@ -189,6 +184,7 @@
    1.21  
    1.22  type axiom_name = string;
    1.23  datatype kind = Axiom | Conjecture;
    1.24 +
    1.25  fun name_of_kind Axiom = "axiom"
    1.26    | name_of_kind Conjecture = "conjecture";
    1.27  
    1.28 @@ -210,10 +206,9 @@
    1.29  		  | CombVar of string * ctyp
    1.30  		  | CombApp of combterm * combterm * ctyp
    1.31  		  | Bool of combterm;
    1.32 +		  
    1.33  datatype literal = Literal of polarity * combterm;
    1.34  
    1.35 -
    1.36 -
    1.37  datatype clause = 
    1.38  	 Clause of {clause_id: clause_id,
    1.39  		    axiom_name: axiom_name,
    1.40 @@ -225,7 +220,6 @@
    1.41                      ctfree_type_literals: ctype_literal list};
    1.42  
    1.43  
    1.44 -
    1.45  fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
    1.46  fun get_axiomName (Clause cls) = #axiom_name cls;
    1.47  fun get_clause_id (Clause cls) = #clause_id cls;
    1.48 @@ -238,8 +232,8 @@
    1.49  (*********************************************************************)
    1.50  
    1.51  fun isFalse (Literal(pol,Bool(CombConst(c,_,_)))) =
    1.52 -    (pol andalso c = "c_False") orelse
    1.53 -    (not pol andalso c = "c_True")
    1.54 +      (pol andalso c = "c_False") orelse
    1.55 +      (not pol andalso c = "c_True")
    1.56    | isFalse _ = false;
    1.57  
    1.58  
    1.59 @@ -429,7 +423,8 @@
    1.60  fun too_general_terms (CombVar(v,_), t) = not (occurs v t)
    1.61    | too_general_terms _ = false;
    1.62  
    1.63 -fun too_general_lit (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) = too_general_terms (t1,t2) orelse too_general_terms (t2,t1)
    1.64 +fun too_general_lit (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
    1.65 +      too_general_terms (t1,t2) orelse too_general_terms (t2,t1)
    1.66    | too_general_lit _ = false;
    1.67  
    1.68  (* forbid a clause that contains hBOOL(V) *)
    1.69 @@ -448,10 +443,13 @@
    1.70      in
    1.71  	if forall isFalse lits
    1.72  	then error "Problem too trivial for resolution (empty clause)"
    1.73 -	else if too_general lits then (Output.debug ("Omitting " ^ axiom_name ^ ": clause contains universal predicates"); raise MAKE_CLAUSE)
    1.74 +	else if too_general lits 
    1.75 +	then (Output.debug ("Omitting " ^ axiom_name ^ ": clause contains universal predicates"); 
    1.76 +	     raise MAKE_CLAUSE)
    1.77  	else
    1.78  	    if (!typ_level <> T_FULL) andalso kind=Axiom andalso forall too_general_lit lits 
    1.79 -	    then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); raise MAKE_CLAUSE) 
    1.80 +	    then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); 
    1.81 +	          raise MAKE_CLAUSE) 
    1.82  	else
    1.83  	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
    1.84  		    literals = lits, ctypes_sorts = ctypes_sorts, 
    1.85 @@ -460,20 +458,24 @@
    1.86      end;
    1.87  
    1.88  
    1.89 -fun make_axiom_clause thm (ax_name,cls_id,is_user) = make_clause(cls_id,ax_name,Axiom,thm,is_user);
    1.90 +fun make_axiom_clause thm (ax_name,cls_id,is_user) = 
    1.91 +      make_clause(cls_id,ax_name,Axiom,thm,is_user);
    1.92   
    1.93  fun make_axiom_clauses [] user_lemmas = []
    1.94    | make_axiom_clauses ((thm,(name,id))::thms) user_lemmas =
    1.95      let val is_user = name mem user_lemmas
    1.96 -	val cls = SOME (make_axiom_clause thm (name,id,is_user)) handle MAKE_CLAUSE => NONE
    1.97 +	val cls = SOME (make_axiom_clause thm (name,id,is_user)) 
    1.98 +	          handle MAKE_CLAUSE => NONE
    1.99  	val clss = make_axiom_clauses thms user_lemmas
   1.100      in
   1.101  	case cls of NONE => clss
   1.102 -		  | SOME(cls') => if isTaut cls' then clss else (name,cls')::clss
   1.103 +		  | SOME(cls') => if isTaut cls' then clss 
   1.104 +		                  else (name,cls')::clss
   1.105      end;
   1.106  
   1.107  
   1.108 -fun make_conjecture_clause n thm = make_clause(n,"conjecture",Conjecture,thm,true);
   1.109 +fun make_conjecture_clause n thm = 
   1.110 +    make_clause(n,"conjecture",Conjecture,thm,true);
   1.111   
   1.112  
   1.113  fun make_conjecture_clauses_aux _ [] = []
   1.114 @@ -613,10 +615,10 @@
   1.115      let val lits = map tptp_literal (#literals cls)
   1.116  	val ctvar_lits_strs =
   1.117  	    case !typ_level of T_NONE => []
   1.118 -			     | _ => (map ResClause.tptp_of_typeLit (#ctvar_type_literals cls)) 
   1.119 +	      | _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls)
   1.120  	val ctfree_lits = 
   1.121  	    case !typ_level of T_NONE => []
   1.122 -			     | _ => (map ResClause.tptp_of_typeLit (#ctfree_type_literals cls)) 
   1.123 +	      | _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls)
   1.124      in
   1.125  	(ctvar_lits_strs @ lits, ctfree_lits)
   1.126      end; 
   1.127 @@ -642,10 +644,10 @@
   1.128        val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts
   1.129        val tvar_lits_strs = 
   1.130  	  case !typ_level of T_NONE => [] 
   1.131 -			    | _ => map ResClause.dfg_of_typeLit tvar_lits
   1.132 +	      | _ => map ResClause.dfg_of_typeLit tvar_lits
   1.133        val tfree_lits =
   1.134            case !typ_level of T_NONE => []
   1.135 -			    | _ => map ResClause.dfg_of_typeLit tfree_lits 
   1.136 +	      | _ => map ResClause.dfg_of_typeLit tfree_lits 
   1.137    in
   1.138        (tvar_lits_strs @ lits, tfree_lits)
   1.139    end; 
   1.140 @@ -673,13 +675,13 @@
   1.141  
   1.142  fun init_combs (comb,funcs) =
   1.143      case !typ_level of T_CONST => 
   1.144 -		       (case comb of "c_COMBK" => Symtab.update (comb,2) funcs
   1.145 -				   | "c_COMBS" => Symtab.update (comb,3) funcs
   1.146 -				   | "c_COMBI" => Symtab.update (comb,1) funcs
   1.147 -				   | "c_COMBB" => Symtab.update (comb,3) funcs
   1.148 -				   | "c_COMBC" => Symtab.update (comb,3) funcs
   1.149 -				   | _ => funcs)
   1.150 -		     | _ => Symtab.update (comb,0) funcs;
   1.151 +	    (case comb of "c_COMBK" => Symtab.update (comb,2) funcs
   1.152 +			| "c_COMBS" => Symtab.update (comb,3) funcs
   1.153 +			| "c_COMBI" => Symtab.update (comb,1) funcs
   1.154 +			| "c_COMBB" => Symtab.update (comb,3) funcs
   1.155 +			| "c_COMBC" => Symtab.update (comb,3) funcs
   1.156 +			| _ => funcs)
   1.157 +	  | _ => Symtab.update (comb,0) funcs;
   1.158  
   1.159  fun init_funcs_tab funcs = 
   1.160      let val tp = !typ_level