src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15697 681bcb7f0389
parent 15684 5ec4d21889d6
child 15700 970e0293dfb3
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Apr 11 12:34:34 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Apr 11 16:25:31 2005 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  (* Versions that include type information *)
     1.5   
     1.6  fun string_of_thm thm = let val _ = set show_sorts
     1.7 -                                val str = Sign.string_of_term Mainsign (prop_of thm)
     1.8 +                                val str = string_of_thm thm
     1.9                                  val no_returns =List.filter not_newline (explode str)
    1.10                                  val _ = reset show_sorts
    1.11                              in 
    1.12 @@ -149,28 +149,6 @@
    1.13                                        add_if_not_inlist ys xs (y::newlist)
    1.14                                          else add_if_not_inlist ys xs (newlist)
    1.15  
    1.16 -(*
    1.17 -fun is_alpha_space_neg_eq_colon ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse  ( ch = ";") orelse( ch = "=")
    1.18 -
    1.19 -(* replace | by ; here *)
    1.20 -fun change_or [] = []
    1.21 -|   change_or (x::xs) = if x = "|" 
    1.22 -                          then 
    1.23 -                             [";"]@(change_or xs)
    1.24 -                          else (x::(change_or xs))
    1.25 -
    1.26 -
    1.27 -fun clause_lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
    1.28 -                              val exp_term = explode termstr
    1.29 -                              val colon_term = change_or exp_term
    1.30 -                   in
    1.31 -                             implode(List.filter is_alpha_space_neg_eq_colon colon_term)
    1.32 -                   end
    1.33 -
    1.34 -fun get_clause_lits thm =  clause_lit_string (prop_of thm)
    1.35 -*)
    1.36 -
    1.37 -
    1.38  fun onestr [] str = str
    1.39  |   onestr (x::xs) str = onestr xs (str^(concat x))
    1.40  
    1.41 @@ -181,83 +159,10 @@
    1.42  |   onelist (x::xs) newlist = onelist xs (newlist@x)
    1.43  
    1.44  
    1.45 -(**** Code to support ordinary resolution, rather than Model Elimination ****)
    1.46 -
    1.47 -(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
    1.48 -  with no contrapositives, for ordinary resolution.*)
    1.49 -
    1.50 -(*raises exception if no rules apply -- unlike RL*)
    1.51 -fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    1.52 -  | tryres (th, []) = raise THM("tryres", 0, [th]);
    1.53  
    1.54  val prop_of = #prop o rep_thm;
    1.55  
    1.56  
    1.57 -(*For ordinary resolution. *)
    1.58 -val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
    1.59 -(*Use "theorem naming" to label the clauses*)
    1.60 -fun name_thms label =
    1.61 -    let fun name1 (th, (k,ths)) =
    1.62 -	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
    1.63 -
    1.64 -    in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    1.65 -
    1.66 -(*Find an all-negative support clause*)
    1.67 -fun is_negative th = forall (not o #1) (literals (prop_of th));
    1.68 -
    1.69 -val neg_clauses = List.filter is_negative;
    1.70 -
    1.71 -
    1.72 -
    1.73 -(*True if the given type contains bool anywhere*)
    1.74 -fun has_bool (Type("bool",_)) = true
    1.75 -  | has_bool (Type(_, Ts)) = exists has_bool Ts
    1.76 -  | has_bool _ = false;
    1.77 -  
    1.78 -
    1.79 -(*Create a meta-level Horn clause*)
    1.80 -fun make_horn crules th = make_horn crules (tryres(th,crules))
    1.81 -			  handle THM _ => th;
    1.82 -
    1.83 -
    1.84 -(*Raises an exception if any Vars in the theorem mention type bool. That would mean
    1.85 -  they are higher-order, and in addition, they could cause make_horn to loop!*)
    1.86 -fun check_no_bool th =
    1.87 -  if exists (has_bool o fastype_of) (term_vars (#prop (rep_thm th)))
    1.88 -  then raise THM ("check_no_bool", 0, [th]) else th;
    1.89 -
    1.90 -
    1.91 -(*Rules to convert the head literal into a negated assumption. If the head
    1.92 -  literal is already negated, then using notEfalse instead of notEfalse'
    1.93 -  prevents a double negation.*)
    1.94 -val notEfalse = read_instantiate [("R","False")] notE;
    1.95 -val notEfalse' = rotate_prems 1 notEfalse;
    1.96 -
    1.97 -fun negated_asm_of_head th = 
    1.98 -    th RS notEfalse handle THM _ => th RS notEfalse';
    1.99 -
   1.100 -(*Converting one clause*)
   1.101 -fun make_meta_clause th = 
   1.102 -	negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th));
   1.103 -
   1.104 -fun make_meta_clauses ths =
   1.105 -    name_thms "MClause#"
   1.106 -      (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
   1.107 -
   1.108 -(*Permute a rule's premises to move the i-th premise to the last position.*)
   1.109 -fun make_last i th =
   1.110 -  let val n = nprems_of th 
   1.111 -  in  if 1 <= i andalso i <= n 
   1.112 -      then Thm.permute_prems (i-1) 1 th
   1.113 -      else raise THM("select_literal", i, [th])
   1.114 -  end;
   1.115 -
   1.116 -(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   1.117 -  double-negations.*)
   1.118 -val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   1.119 -
   1.120 -(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   1.121 -fun select_literal i cl = negate_head (make_last i cl);
   1.122  
   1.123   fun get_axioms_used proof_steps thmstring = let 
   1.124                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
   1.125 @@ -281,7 +186,7 @@
   1.126  
   1.127                                              val distfrees = distinct frees
   1.128  
   1.129 -                                            val metas = map make_meta_clause clauses
   1.130 +                                            val metas = map Meson.make_meta_clause clauses
   1.131                                              val ax_strs = map #3 axioms
   1.132  
   1.133                                              (* literals of -all- axioms, not just those used by spass *)