src/HOL/Tools/res_atp.ML
changeset 20661 46832fee1215
parent 20643 267f30cbe2cb
child 20757 fe84fe0dfd30
equal deleted inserted replaced
20660:8606ddd42554 20661:46832fee1215
   454    "Set.UnionI",
   454    "Set.UnionI",
   455 *)
   455 *)
   456 
   456 
   457 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   457 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   458 
   458 
   459 fun fake_thm_name th = 
       
   460     Context.theory_name (theory_of_thm th) ^ "." ^ gensym"";
       
   461 
       
   462 fun put_name_pair ("",th) = (fake_thm_name th, th)
       
   463   | put_name_pair (a,th)  = (a,th);
       
   464 
       
   465 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   459 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   466 
   460 
   467 exception HASH_CLAUSE and HASH_STRING;
   461 exception HASH_CLAUSE and HASH_STRING;
   468 
   462 
   469 (*Catches (for deletion) theorems automatically generated from other theorems*)
   463 (*Catches (for deletion) theorems automatically generated from other theorems*)
   499 
   493 
   500 (** a hash function from Term.term to int, and also a hash table **)
   494 (** a hash function from Term.term to int, and also a hash table **)
   501 val xor_words = List.foldl Word.xorb 0w0;
   495 val xor_words = List.foldl Word.xorb 0w0;
   502 
   496 
   503 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   497 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   504   | hashw_term ((Free(_,_)), w) = w
   498   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   505   | hashw_term ((Var(_,_)), w) = w
   499   | hashw_term ((Var(_,_)), w) = w
   506   | hashw_term ((Bound _), w) = w
   500   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   507   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   501   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   508   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   502   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   509 
   503 
   510 fun hashw_pred (P,w) = 
   504 fun hashw_pred (P,w) = 
   511     let val (p,args) = strip_comb P
   505     let val (p,args) = strip_comb P
   521   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   515   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   522   | get_literals lit lits = (lit::lits);
   516   | get_literals lit lits = (lit::lits);
   523 
   517 
   524 
   518 
   525 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   519 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
       
   520 
       
   521 (*Versions ONLY for "faking" a theorem name. Here we take variable names into account
       
   522   so that similar theorems don't collide.  FIXME: this entire business of "faking" 
       
   523   theorem names must end!*)
       
   524 fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
       
   525   | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
       
   526   | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);
       
   527 
       
   528 fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
       
   529   | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
       
   530   | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
       
   531   | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
       
   532   | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
       
   533   | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));
       
   534 
       
   535 fun full_hashw_thm (th,w) = 
       
   536   let val {prop,hyps,...} = rep_thm th
       
   537   in List.foldl full_hashw_term w (prop::hyps) end
       
   538 
       
   539 fun full_hash_thm th = full_hashw_thm (th,0w0);
   526 
   540 
   527 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   541 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   528 
   542 
   529 (*Create a hash table for clauses, of the given size*)
   543 (*Create a hash table for clauses, of the given size*)
   530 fun mk_clause_table n =
   544 fun mk_clause_table n =
   554 
   568 
   555 (* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
   569 (* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
   556 fun get_relevant_clauses thy cls_thms white_cls goals =
   570 fun get_relevant_clauses thy cls_thms white_cls goals =
   557   insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   571   insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   558 
   572 
       
   573 (*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
       
   574 fun fake_thm_name th = 
       
   575     Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
       
   576 
       
   577 fun put_name_pair ("",th) = (fake_thm_name th, th)
       
   578   | put_name_pair (a,th)  = (a,th);
   559 
   579 
   560 fun display_thms [] = ()
   580 fun display_thms [] = ()
   561   | display_thms ((name,thm)::nthms) = 
   581   | display_thms ((name,thm)::nthms) = 
   562       let val nthm = name ^ ": " ^ (string_of_thm thm)
   582       let val nthm = name ^ ": " ^ (string_of_thm thm)
   563       in Output.debug nthm; display_thms nthms  end;
   583       in Output.debug nthm; display_thms nthms  end;