Some work on the new waldmeister integration
authorsteckerm
Tue Sep 02 16:38:26 2014 +0200 (2014-09-02)
changeset 58142d6a2e3567f95
parent 58141 182f89d83432
child 58143 7f7026ae9dc5
Some work on the new waldmeister integration
src/HOL/ATP.thy
src/HOL/Tools/ATP/atp_waldmeister.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     1.1 --- a/src/HOL/ATP.thy	Tue Sep 02 14:40:32 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue Sep 02 16:38:26 2014 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4  
     1.5  (* Has all needed simplification lemmas for logic.
     1.6     "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
     1.7 -lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
     1.8 +lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
     1.9    eq_ac disj_comms disj_assoc conj_comms conj_assoc
    1.10  
    1.11  
     2.1 --- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Tue Sep 02 14:40:32 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Tue Sep 02 16:38:26 2014 +0200
     2.3 @@ -5,21 +5,202 @@
     2.4  General-purpose functions used by the Sledgehammer modules.
     2.5  *)
     2.6  
     2.7 +exception FailureMessage of string
     2.8 +exception FailureTerm of term * term
     2.9 +exception FailureWM of (term * term list * (string * string) list)
    2.10 +
    2.11 +signature ATP_WALDMEISTER_SKOLEMIZER =
    2.12 +sig
    2.13 +  val skolemize : bool -> Proof.context -> term -> (Proof.context * (term list * term))
    2.14 +end;
    2.15 +
    2.16 +signature ATP_WALDMEISTER_TYPE_ENCODER =
    2.17 +sig
    2.18 +  val encode_type : typ -> string
    2.19 +  val decode_type_string : string -> typ
    2.20 +  val encode_types : typ list -> string
    2.21 +  val decode_types : string -> typ list
    2.22 +  val encode_const : string * typ list -> string
    2.23 +  val decode_const : string -> string * typ list
    2.24 +end;
    2.25 +
    2.26  signature ATP_WALDMEISTER =
    2.27  sig
    2.28    type 'a atp_problem = 'a ATP_Problem.atp_problem
    2.29    type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
    2.30    type 'a atp_proof = 'a ATP_Proof.atp_proof
    2.31    type stature = ATP_Problem_Generate.stature
    2.32 -
    2.33 -  val generate_waldmeister_problem: Proof.context -> term list -> term ->
    2.34 +  type waldmeister_info =  (string * (term list * (term option * term))) list
    2.35 +  
    2.36 +  val waldmeister_skolemize_rule : string
    2.37 +  
    2.38 +  val generate_waldmeister_problem : Proof.context -> term list -> term ->
    2.39      ((string * stature) * term) list ->
    2.40 -    string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
    2.41 +    string atp_problem * string Symtab.table * (string * term) list * int Symtab.table * 
    2.42 +    waldmeister_info
    2.43    val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof ->
    2.44      (term, string) atp_step list
    2.45 +  val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list -> 
    2.46 +    (term, string) atp_step list
    2.47  end;
    2.48  
    2.49 -structure ATP_Waldmeister : ATP_WALDMEISTER =
    2.50 +structure ATP_Waldmeister_Skolemizer : ATP_WALDMEISTER_SKOLEMIZER =
    2.51 +struct
    2.52 +
    2.53 +open HOLogic
    2.54 +
    2.55 +fun contains_quantor (Const (@{const_name Ex},_) $ _) = true
    2.56 +  | contains_quantor (Const (@{const_name All},_) $ _) = true
    2.57 +  | contains_quantor (t1 $ t2) = contains_quantor t1 orelse contains_quantor t2
    2.58 +  | contains_quantor _ = false
    2.59 +
    2.60 +fun mk_fun_for_bvar ctxt1 ctxt2 arg_trms (bound_name,ty) =
    2.61 +  let
    2.62 +    val fun_type = (map type_of arg_trms) ---> ty
    2.63 +    val (fun_name,_) = singleton (Variable.variant_frees ctxt2 []) ("sko_" ^ bound_name,fun_type)
    2.64 +    val (_,ctxt1_new) = Variable.add_fixes [fun_name] ctxt1
    2.65 +    val (_,ctxt2_new) = Variable.add_fixes [fun_name] ctxt2
    2.66 +  in
    2.67 +    (Term.list_comb (Free (fun_name,fun_type),arg_trms),ctxt1_new,ctxt2_new)
    2.68 +  end
    2.69 +
    2.70 +fun skolem_free ctxt1 ctxt2 vars (bound_name,ty,trm) =
    2.71 +    let
    2.72 +      val (fun_trm,ctxt1_new,ctxt2_new) = mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty)
    2.73 +    in
    2.74 +      (Term.subst_bounds ([fun_trm],trm),ctxt1_new,ctxt2_new)
    2.75 +    end
    2.76 +
    2.77 +fun skolem_var ctxt (bound_name,ty,trm) =
    2.78 +    let
    2.79 +      val (var_name,_) = singleton (Variable.variant_frees ctxt []) (bound_name,ty)
    2.80 +      val (_,ctxt') = Variable.add_fixes [var_name] ctxt
    2.81 +      val var = Var ((var_name,0),ty)
    2.82 +    in
    2.83 +     (Term.subst_bounds ([var],trm),ctxt',var)
    2.84 +    end
    2.85 +
    2.86 +fun skolem_bound is_free ctxt1 ctxt2 spets vars x =
    2.87 +    if is_free then
    2.88 +      let 
    2.89 +        val (trm',ctxt1',ctxt2') = skolem_free ctxt1 ctxt2 vars x
    2.90 +      in
    2.91 +        (ctxt1',ctxt2',spets,trm',vars)
    2.92 +      end
    2.93 +    else
    2.94 +      let
    2.95 +        val (trm',ctxt2',var) = skolem_var ctxt2 x
    2.96 +      in
    2.97 +        (ctxt1,ctxt2',spets,trm',var::vars)
    2.98 +      end
    2.99 +
   2.100 +fun skolemize' pos ctxt1 ctxt2 spets vars (Const (@{const_name Not},_) $ trm') =
   2.101 +    let
   2.102 +      val (ctxt1',ctxt2',spets',trm'') = skolemize' (not pos) ctxt1 ctxt2 spets vars trm'
   2.103 +    in
   2.104 +      (ctxt1',ctxt2',map mk_not spets',mk_not trm'')
   2.105 +    end
   2.106 +  | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (@{const_name HOL.eq},_) $ a $ b)) =
   2.107 +    if contains_quantor trm then
   2.108 +      skolemize' pos ctxt1 ctxt2 (trm::spets) vars (mk_conj (mk_imp (a,b), mk_imp (b,a)))
   2.109 +    else
   2.110 +      (ctxt1,ctxt2,spets,trm)
   2.111 +  | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name,_) $ Abs x)) =
   2.112 +    if name = @{const_name Ex} orelse name = @{const_name All} then
   2.113 +      let
   2.114 +        val is_free =  (name = @{const_name Ex} andalso pos) 
   2.115 +          orelse (name = @{const_name All} andalso not pos)
   2.116 +        val (ctxt1',ctxt2',spets',trm',vars') = 
   2.117 +          skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x
   2.118 +      in
   2.119 +        skolemize' pos ctxt1' ctxt2' spets' vars' trm'
   2.120 +      end
   2.121 +    else
   2.122 +      (ctxt1,ctxt2,spets,trm)
   2.123 +  | skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name,_)) $ a $ b) =
   2.124 +    if name = @{const_name conj} orelse name = @{const_name disj} orelse 
   2.125 +       name = @{const_name implies} then
   2.126 +      let
   2.127 +        val pos_a = if name = @{const_name implies} then not pos else pos
   2.128 +        val (ctxt1',ctxt2',spets',a') = skolemize'  pos_a ctxt1 ctxt2 [] vars a
   2.129 +        val (ctxt1'',ctxt2'',spets'',b') = skolemize' pos ctxt1' ctxt2' [] vars b
   2.130 +      in
   2.131 +        (ctxt1'',ctxt2'',
   2.132 +         map (fn trm => c $ a' $ trm) spets'' @ map (fn trm => c $ trm $ b) spets' @ spets,
   2.133 +         c $ a' $ b')
   2.134 +      end
   2.135 +    else
   2.136 +      (ctxt1,ctxt2,spets,c $ a $ b)
   2.137 +  | skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1,ctxt2,spets,trm)
   2.138 +
   2.139 +  fun skolemize positve ctxt trm = 
   2.140 +    let
   2.141 +      val (ctxt1,_,spets,skolemized_trm) = skolemize' positve ctxt ctxt [] [] trm
   2.142 +    in
   2.143 +        (ctxt1,(trm :: List.rev spets,skolemized_trm))
   2.144 +    end
   2.145 +
   2.146 +end;
   2.147 +
   2.148 +structure ATP_Waldmeister_Type_Encoder : ATP_WALDMEISTER_TYPE_ENCODER =
   2.149 +struct
   2.150 +
   2.151 +val delimiter = ";"
   2.152 +val open_paranthesis = "["
   2.153 +val close_parathesis = "]"
   2.154 +val type_prefix = "Type"
   2.155 +val tfree_prefix = "TFree"
   2.156 +val tvar_prefix = "TVar"
   2.157 +
   2.158 +val identifier_character = not o member (op =) [delimiter,open_paranthesis,close_parathesis]
   2.159 +
   2.160 +fun encode_type (Type (name,types)) = 
   2.161 +type_prefix ^ open_paranthesis ^ name ^ delimiter ^ 
   2.162 +  (map encode_type types |> String.concatWith delimiter) ^ close_parathesis
   2.163 +| encode_type (TFree (name,sorts)) = 
   2.164 +tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ (String.concatWith delimiter sorts) ^ delimiter
   2.165 +| encode_type (TVar ((name,i),sorts)) =
   2.166 +tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ 
   2.167 +  close_parathesis ^ delimiter ^ (String.concatWith delimiter sorts) ^ close_parathesis
   2.168 +
   2.169 +fun encode_types types = (String.concatWith delimiter (map encode_type types))
   2.170 +
   2.171 +fun parse_identifier x =
   2.172 +  (Scan.many identifier_character >> implode) x
   2.173 +  
   2.174 +fun parse_star delim scanner x = (Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x
   2.175 +  
   2.176 +fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --|
   2.177 +  $$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x
   2.178 +and parse_tfree x = (Scan.this_string tfree_prefix |-- $$ open_paranthesis |-- parse_identifier --|
   2.179 +  $$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TFree) x
   2.180 +and parse_tvar x = (Scan.this_string tvar_prefix |-- $$ open_paranthesis |-- $$ open_paranthesis
   2.181 +  |-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$ 
   2.182 +  close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --| 
   2.183 +  $$ close_parathesis >> TVar) x
   2.184 +and parse_any_type x = (parse_type || parse_tfree || parse_tvar) x
   2.185 +
   2.186 +fun parse_types x = parse_star delimiter parse_any_type x
   2.187 +  
   2.188 +fun decode_type_string s = Scan.finite Symbol.stopper
   2.189 +           (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^
   2.190 +                                                quote s)) parse_type))  (Symbol.explode s) |> fst
   2.191 +
   2.192 +fun decode_types s = Scan.finite Symbol.stopper
   2.193 +           (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^
   2.194 +           quote s))) parse_types) (Symbol.explode s) |> fst
   2.195 +
   2.196 +fun encode_const (name,tys) = name ^ delimiter ^ encode_types tys
   2.197 +
   2.198 +fun parse_const s = (parse_identifier --| $$ delimiter -- parse_types) s
   2.199 +
   2.200 +fun decode_const s = Scan.finite Symbol.stopper
   2.201 +           (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized const encoding" ^
   2.202 +           quote s))) parse_const) (Symbol.explode s) |> fst
   2.203 +
   2.204 +end;
   2.205 +
   2.206 +structure ATP_Waldmeister : ATP_WALDMEISTER  =
   2.207  struct
   2.208  
   2.209  open ATP_Util
   2.210 @@ -27,6 +208,9 @@
   2.211  open ATP_Problem_Generate
   2.212  open ATP_Proof
   2.213  open ATP_Proof_Reconstruct
   2.214 +open ATP_Waldmeister_Skolemizer
   2.215 +open ATP_Waldmeister_Type_Encoder
   2.216 +open HOLogic
   2.217  
   2.218  type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
   2.219  type atp_connective = ATP_Problem.atp_connective
   2.220 @@ -34,103 +218,129 @@
   2.221  type atp_format = ATP_Problem.atp_format
   2.222  type atp_formula_role = ATP_Problem.atp_formula_role
   2.223  type 'a atp_problem = 'a ATP_Problem.atp_problem
   2.224 +type waldmeister_info =  (string * (term list * (term option * term))) list
   2.225  
   2.226  val const_prefix = #"c"
   2.227  val var_prefix = #"V"
   2.228 -val free_prefix = #"f"
   2.229 +val free_prefix = #"v"
   2.230  val conjecture_condition_name = "condition"
   2.231 +val waldmeister_equals = "eq"
   2.232 +val waldmeister_true = "true"
   2.233 +val waldmeister_false = "false"
   2.234 +val waldmeister_skolemize_rule = "waldmeister_skolemize"
   2.235  
   2.236  val factsN = "Relevant facts"
   2.237  val helpersN = "Helper facts"
   2.238  val conjN = "Conjecture"
   2.239 +val conj_identifier = conjecture_prefix ^ "0"
   2.240  
   2.241 -exception Failure
   2.242 -exception FailureMessage of string
   2.243 +val WM_ERROR_MSG = "Waldmeister problem generator failed: "
   2.244  
   2.245  (*
   2.246  Some utilitary functions for translation.
   2.247  *)
   2.248  
   2.249 -fun is_eq (Const (@{const_name "HOL.eq"}, _) $ _ $ _) = true
   2.250 -  | is_eq _ = false
   2.251 +fun gen_ascii_tuple str = (str, ascii_of str)
   2.252  
   2.253 -fun gen_ascii_tuple str = (str, ascii_of str)
   2.254 +fun mk_eq_true (trm as (Const (@{const_name HOL.eq}, _) $ _ $ _)) = (NONE,trm)
   2.255 +  | mk_eq_true trm = (SOME trm,HOLogic.mk_eq (trm, @{term True}))
   2.256  
   2.257  (*
   2.258  Translation from Isabelle theorms and terms to ATP terms.
   2.259  *)
   2.260  
   2.261 -fun trm_to_atp'' (Const (x, _)) args = [ATerm ((gen_ascii_tuple (String.str const_prefix ^ x), []), args)]
   2.262 -  | trm_to_atp'' (Free (x, _)) args = ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), [])::args
   2.263 -  | trm_to_atp'' (Var ((x, _), _)) args = ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), [])::args
   2.264 -  | trm_to_atp'' (trm1 $ trm2) args = trm_to_atp'' trm1 (trm_to_atp'' trm2 [] @ args)
   2.265 -  | trm_to_atp'' _ args = args
   2.266 -
   2.267 -fun trm_to_atp' trm = trm_to_atp'' trm [] |> hd
   2.268 +fun trm_to_atp'' thy (Const (x, ty)) args =
   2.269 +    let
   2.270 +      val ty_args = Sign.const_typargs thy (x,ty)
   2.271 +    in
   2.272 +      [ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x,ty_args)), []), args)]
   2.273 +    end
   2.274 +  | trm_to_atp'' _ (Free (x, _)) args = 
   2.275 +    [ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)]
   2.276 +  | trm_to_atp'' _ (Var ((x, _), _)) args = 
   2.277 +    [ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)]
   2.278 +  | trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args)
   2.279 +  | trm_to_atp'' _ trm _ = raise FailureTerm (trm,trm)
   2.280  
   2.281 -fun eq_trm_to_atp (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =
   2.282 -    ATerm ((("equal", "equal"), []), [trm_to_atp' lhs, trm_to_atp' rhs])
   2.283 -  | eq_trm_to_atp _ = raise Failure
   2.284 +fun trm_to_atp' thy trm = trm_to_atp'' thy trm [] |> hd
   2.285 +
   2.286 +fun eq_trm_to_atp thy (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =
   2.287 +    ATerm ((("equal", "equal"), []), [trm_to_atp' thy lhs, trm_to_atp' thy rhs])
   2.288 +  | eq_trm_to_atp _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Non-eq term")
   2.289  
   2.290 -fun trm_to_atp trm =
   2.291 -  if is_eq trm then eq_trm_to_atp trm
   2.292 -  else HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp
   2.293 +fun thm_to_atps thy split_conj prop_term =
   2.294 +  if split_conj then map (eq_trm_to_atp thy) (prop_term |> HOLogic.dest_conj)
   2.295 +  else [prop_term |> eq_trm_to_atp thy]
   2.296  
   2.297 -fun thm_to_atps split_conj prop_term =
   2.298 -  if split_conj then map trm_to_atp (prop_term |> HOLogic.dest_conj)
   2.299 -  else [prop_term |> trm_to_atp]
   2.300 -
   2.301 -fun prepare_conjecture conj_term =
   2.302 +fun split_conjecture _ conj_term =
   2.303    let
   2.304      fun split_conj_trm (Const (@{const_name Pure.imp}, _) $ condition $ consequence) =
   2.305          (SOME condition, consequence)
   2.306        | split_conj_trm conj = (NONE, conj)
   2.307      val (condition, consequence) = split_conj_trm conj_term
   2.308    in
   2.309 -    (case condition of SOME x => HOLogic.dest_conj x |> map trm_to_atp | NONE => []
   2.310 -    , trm_to_atp consequence)
   2.311 +    (case condition of SOME x => HOLogic.dest_conj x | NONE => []
   2.312 +    , consequence)
   2.313    end
   2.314  
   2.315  (* Translation from ATP terms to Isabelle terms. *)
   2.316  
   2.317 -fun construct_term (ATerm ((name, _), _)) =
   2.318 +fun construct_term (name, args) =
   2.319    let
   2.320      val prefix = String.sub (name, 0)
   2.321 +    val encoded_name = String.extract(name,1,NONE)
   2.322 +    fun dummy_fun_type () = replicate (length args) dummyT ---> dummyT
   2.323    in
   2.324      if prefix = const_prefix then
   2.325 -      Const (String.extract (name, 1, NONE), Type ("", []))
   2.326 +      let
   2.327 +        val (const_name,ty_args) = decode_const encoded_name
   2.328 +      in
   2.329 +        Const (const_name,Sign.const_instance @{theory } (* FIXME? *) (const_name, ty_args))
   2.330 +      end
   2.331      else if prefix = free_prefix then
   2.332 -      Free (String.extract (name, 1, NONE), TFree ("", []))
   2.333 +      Free (encoded_name, dummy_fun_type ())
   2.334      else if Char.isUpper prefix then
   2.335 -      Var ((name, 0), TVar (("", 0), []))
   2.336 +      Var ((name, 0), dummy_fun_type ()) 
   2.337 +      (* Use name instead of encoded_name because Waldmeister renames free variables. *)
   2.338 +    else if name = waldmeister_equals then
   2.339 +      case args of 
   2.340 +        [_, _] => 
   2.341 +          eq_const dummyT
   2.342 +      | _ => raise FailureMessage 
   2.343 +        (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ 
   2.344 +         Int.toString (length args))
   2.345 +    else if name = waldmeister_true then
   2.346 +      @{term "True"}
   2.347 +    else if name = waldmeister_false then
   2.348 +      @{term "False"}
   2.349      else
   2.350 -      raise Failure
   2.351 +      raise FailureMessage 
   2.352 +        (WM_ERROR_MSG ^ "Unknown name prefix when parsing Waldmeister proof: name = " ^ name)
   2.353    end
   2.354 -  | construct_term _ = raise Failure
   2.355  
   2.356 -fun atp_to_trm' (ATerm (descr, args)) =
   2.357 +and atp_to_trm' (ATerm ((name,_), args)) =
   2.358      (case args of
   2.359 -      [] => construct_term (ATerm (descr, args))
   2.360 -     | _ => Term.list_comb (construct_term (ATerm (descr, args)), map atp_to_trm' args))
   2.361 -     | atp_to_trm' _ = raise Failure
   2.362 +      [] => construct_term (name, args)
   2.363 +     | _ => Term.list_comb (construct_term (name, args), map atp_to_trm' args))
   2.364 +     | atp_to_trm' _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm' expects ATerm")
   2.365  
   2.366  fun atp_to_trm (ATerm (("equal", _), [lhs, rhs])) =
   2.367 -    Const (@{const_name HOL.eq}, Type ("", [])) $ atp_to_trm' lhs $ atp_to_trm' rhs
   2.368 -  | atp_to_trm (ATerm (("$true", _), _)) = Const ("HOL.True", Type ("", []))
   2.369 -  | atp_to_trm _ = raise Failure
   2.370 +    mk_eq (atp_to_trm' lhs, atp_to_trm' rhs)
   2.371 +  | atp_to_trm (ATerm (("$true", _), _)) = @{term True}
   2.372 +  | atp_to_trm _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm expects ATerm")
   2.373  
   2.374 -fun formula_to_trm (AAtom aterm) = atp_to_trm aterm
   2.375 +fun formula_to_trm (AAtom aterm) = aterm |> atp_to_trm
   2.376    | formula_to_trm (AConn (ANot, [aterm])) =
   2.377 -    Const (@{const_name HOL.Not}, @{typ "bool \<Rightarrow> bool"}) $ formula_to_trm aterm
   2.378 -  | formula_to_trm _ = raise Failure
   2.379 +    mk_not (formula_to_trm aterm)
   2.380 +  | formula_to_trm _ = raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn")
   2.381  
   2.382  (* Abstract translation *)
   2.383  
   2.384  fun mk_formula prefix_name name atype aterm =
   2.385    Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
   2.386  
   2.387 -fun problem_lines_of_fact prefix ((s, _), t) =
   2.388 -  map (mk_formula prefix s Axiom) (thm_to_atps false t)
   2.389 +fun problem_lines_of_fact thy prefix (s,(_,(_,t))) =
   2.390 +  map (mk_formula prefix s Axiom) (thm_to_atps thy false t)
   2.391  
   2.392  fun make_nice problem = nice_atp_problem true CNF problem
   2.393  
   2.394 @@ -138,49 +348,94 @@
   2.395    let
   2.396      val formula = mk_anot (AAtom aterm)
   2.397    in
   2.398 -    Formula ((conjecture_prefix ^ "0", ""), Hypothesis, formula, NONE, [])
   2.399 +    Formula ((conj_identifier, ""), Hypothesis, formula, NONE, [])
   2.400    end
   2.401  
   2.402 -fun atp_proof_step_to_term (name, role, formula, formula_name, step_names) =
   2.403 -  (name, role, formula_to_trm formula, formula_name, step_names)
   2.404 -
   2.405 -fun generate_waldmeister_problem ctxt hyp_ts0 concl_t0 facts0 =
   2.406 +fun generate_waldmeister_problem ctxt _ concl_t0 facts0 =
   2.407    let
   2.408      val thy = Proof_Context.theory_of ctxt
   2.409  
   2.410      val preproc = Object_Logic.atomize_term thy
   2.411  
   2.412 -    val hyp_ts = map preproc hyp_ts0
   2.413 -    val concl_t = preproc concl_t0
   2.414 -    val facts = map (apsnd preproc) facts0
   2.415 +    (*val hyp_ts = map preproc hyp_ts0 : term list *)
   2.416 +    val concl_t = preproc concl_t0 : term
   2.417 +    val facts = map (apsnd preproc #> apfst fst) facts0 : (string * term) list
   2.418 +    val (conditions, consequence) = split_conjecture thy concl_t : term list * term
   2.419 +    
   2.420 +    fun map_ctxt' _ ctxt [] ys = (ctxt,ys)
   2.421 +      | map_ctxt' f ctxt (x :: xs) ys =
   2.422 +        let
   2.423 +          val (ctxt',x') = f ctxt x
   2.424 +        in
   2.425 +          map_ctxt' f ctxt' xs (x'::ys)
   2.426 +        end
   2.427 +
   2.428 +    fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs []
   2.429 +      
   2.430 +    fun skolemize_fact ctxt (name,trm) = 
   2.431 +      let 
   2.432 +        val (ctxt',(steps,trm')) = skolemize true ctxt trm 
   2.433 +      in 
   2.434 +        (ctxt',(name,(steps,trm')))
   2.435 +      end
   2.436 +    
   2.437 +    fun name_list' _ [] _ = []
   2.438 +      | name_list' prefix (x :: xs) i = (prefix ^ Int.toString i,x) :: name_list' prefix xs (i+1)
   2.439 +      
   2.440 +    fun name_list prefix xs = name_list' prefix xs 0 
   2.441  
   2.442 -    val (conditions, consequence) = prepare_conjecture concl_t
   2.443 -    val fact_lines = maps (problem_lines_of_fact (fact_prefix ^ "0_" (* FIXME *))) facts
   2.444 +    val (ctxt',sko_facts) = map_ctxt skolemize_fact ctxt facts : 
   2.445 +      Proof.context * (string * (term list * term)) list
   2.446 +    val (ctxt'',sko_conditions) = map_ctxt (skolemize false) ctxt' conditions : 
   2.447 +      Proof.context * (term list * term) list
   2.448 +
   2.449 +    val sko_eq_facts = map (apsnd (apsnd mk_eq_true)) sko_facts : 
   2.450 +      (string * (term list * (term option * term))) list
   2.451 +    val sko_eq_conditions = map (apsnd mk_eq_true) sko_conditions 
   2.452 +            |> name_list conjecture_condition_name : 
   2.453 +      (string * (term list * (term option * term))) list
   2.454 +    val (_,eq_conseq as (_,(non_eq_consequence,eq_consequence))) = 
   2.455 +      skolemize false ctxt'' consequence |> apsnd (apsnd mk_eq_true) :
   2.456 +      (Proof.context * (term list * (term option * term)))
   2.457 +
   2.458 +    val sko_eq_info =
   2.459 +      (((conj_identifier,eq_conseq) :: sko_eq_conditions) @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts) : 
   2.460 +      (string * (term list * (term option * term))) list
   2.461 +
   2.462 +    val fact_lines = maps (problem_lines_of_fact thy (fact_prefix ^ "0_" (* FIXME *))) sko_eq_facts
   2.463      val condition_lines =
   2.464 -      map (mk_formula fact_prefix conjecture_condition_name Hypothesis) conditions
   2.465 +      map (fn (name,(_,(_,trm))) => mk_formula fact_prefix name Hypothesis (eq_trm_to_atp thy trm)) sko_eq_conditions
   2.466      val axiom_lines = fact_lines @ condition_lines
   2.467 -    val conj_line = mk_conjecture consequence
   2.468 +
   2.469 +    val conj_line = mk_conjecture (eq_trm_to_atp thy eq_consequence)
   2.470 +    
   2.471 +    fun is_some (SOME _) = true
   2.472 +      | is_some NONE = false
   2.473 +    
   2.474 +    val helper_lemmas_needed = List.exists (snd #> snd #> fst #> is_some) sko_eq_facts
   2.475 +      orelse List.exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse
   2.476 +      is_some non_eq_consequence
   2.477  
   2.478      val helper_lines =
   2.479 -      if List.exists (is_eq o snd) facts orelse not (is_eq concl_t) then
   2.480 +      if helper_lemmas_needed then
   2.481          [(helpersN,
   2.482            @{thms waldmeister_fol}
   2.483            |> map (fn th => (("", (Global, General)), preproc (prop_of th)))
   2.484 -          |> maps (problem_lines_of_fact helper_prefix))]
   2.485 +          |> maps 
   2.486 +            (fn ((s,_),t) => map (mk_formula helper_prefix s Axiom) (thm_to_atps thy false t)))]
   2.487        else
   2.488          []
   2.489 +
   2.490      val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])]
   2.491  
   2.492 -    val (nice_problem, symtabs) = make_nice problem
   2.493 +    val (nice_problem, pool) = make_nice (@{print} problem)
   2.494    in
   2.495 -    (nice_problem, Symtab.empty, [], Symtab.empty)
   2.496 +    (nice_problem, Option.map snd pool |> the_default Symtab.empty, [], Symtab.empty, sko_eq_info)
   2.497    end
   2.498  
   2.499 -fun termify_line ctxt (name, role, AAtom u, rule, deps) =
   2.500 +fun termify_line ctxt (name, role, u, rule, deps) =
   2.501    let
   2.502 -    val thy = Proof_Context.theory_of ctxt
   2.503 -    val t = u
   2.504 -      |> atp_to_trm
   2.505 +    val t = u |> formula_to_trm
   2.506        |> singleton (infer_formulas_types ctxt)
   2.507        |> HOLogic.mk_Trueprop
   2.508    in
   2.509 @@ -192,4 +447,38 @@
   2.510    #> map (termify_line ctxt)
   2.511    #> repair_waldmeister_endgame
   2.512  
   2.513 -end;
   2.514 +fun lookup table k = 
   2.515 +  List.find (fn (key, _) => key = k) table
   2.516 +  
   2.517 +fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of
   2.518 +  SOME x => x |
   2.519 +  NONE => NONE
   2.520 +  
   2.521 +fun fix_name name = 
   2.522 +  if String.isPrefix "fact" name then 
   2.523 +    String.extract(name,7,NONE) |> unascii_of |> curry (op ^) "fact_0_"
   2.524 +  else
   2.525 +    name
   2.526 +
   2.527 +fun skolemization_steps info 
   2.528 +  (proof_step as ((waldmeister_name,isabelle_names), _, trm, rule, _)) =
   2.529 +  case get_skolem_info info (map fix_name isabelle_names |> @{print}) of
   2.530 +    NONE => [proof_step] |
   2.531 +    SOME (_,([],_)) => [proof_step] |
   2.532 +    SOME (_,(step :: steps,_)) =>
   2.533 +      let
   2.534 +        fun mk_steps _ [] = []
   2.535 +          | mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^  Int.toString i),[]),Plain,
   2.536 +            mk_Trueprop x,waldmeister_skolemize_rule,[(waldmeister_name ^ "_" ^  Int.toString (i-1),if i = 1 then isabelle_names else [])]) :: mk_steps (i+1) xs
   2.537 +        val skolem_steps = ((waldmeister_name ^ "_0",isabelle_names),Unknown,mk_Trueprop step,rule,[]) :: 
   2.538 +          mk_steps 1 steps
   2.539 +      in
   2.540 +        skolem_steps @ [((waldmeister_name,[]), Unknown, trm, waldmeister_skolemize_rule,
   2.541 +            [(waldmeister_name ^ "_" ^ Int.toString (length skolem_steps - 1),if length skolem_steps = 1 then isabelle_names else [])])]
   2.542 +      end
   2.543 +  
   2.544 +fun introduce_waldmeister_skolems info (proof_steps : (term, string) atp_step list) = (@{print} info; proof_steps |> tap (map @{print})
   2.545 +      |> map (skolemization_steps info) |> List.concat |> tap (map @{print}))
   2.546 +
   2.547 +
   2.548 +end;
   2.549 \ No newline at end of file
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Sep 02 14:40:32 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Sep 02 16:38:26 2014 +0200
     3.3 @@ -56,6 +56,7 @@
     3.4  val veriT_simp_arith_rule = "simp_arith"
     3.5  val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
     3.6  val veriT_tmp_skolemize_rule = "tmp_skolemize"
     3.7 +val waldmeister_skolemize_rule = ATP_Waldmeister.waldmeister_skolemize_rule
     3.8  val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
     3.9  val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
    3.10  val zipperposition_cnf_rule = "cnf"
    3.11 @@ -63,7 +64,7 @@
    3.12  val skolemize_rules =
    3.13    [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
    3.14     spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
    3.15 -   veriT_tmp_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
    3.16 +   veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
    3.17  
    3.18  val is_skolemize_rule = member (op =) skolemize_rules
    3.19  fun is_arith_rule rule =
    3.20 @@ -167,7 +168,7 @@
    3.21            | SOME n => n)
    3.22  
    3.23          fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
    3.24 -        fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
    3.25 +        fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev |> @{print}
    3.26  
    3.27          fun get_role keep_role ((num, _), role, t, rule, _) =
    3.28            if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 02 14:40:32 2014 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 02 16:38:26 2014 +0200
     4.3 @@ -256,7 +256,7 @@
     4.4              val readable_names = not (Config.get ctxt atp_full_names)
     4.5              val lam_trans = lam_trans |> the_default best_lam_trans
     4.6              val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
     4.7 -            val value as (atp_problem, _, _, _) =
     4.8 +            val value as (atp_problem, _, _, _, _) =
     4.9                if cache_key = SOME key then
    4.10                  cache_value
    4.11                else
    4.12 @@ -267,9 +267,11 @@
    4.13                  |> map (apsnd prop_of)
    4.14                  |> (if waldmeister_new then
    4.15                        generate_waldmeister_problem ctxt hyp_ts concl_t
    4.16 +                        #> (fn (a,b,c,d,e) => (a,b,c,d,SOME e))
    4.17                      else
    4.18                        generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
    4.19 -                        uncurried_aliases readable_names true hyp_ts concl_t)
    4.20 +                        uncurried_aliases readable_names true hyp_ts concl_t
    4.21 +                        #> (fn (a,b,c,d) => (a,b,c,d,NONE)))
    4.22  
    4.23              fun sel_weights () = atp_problem_selection_weights atp_problem
    4.24              fun ord_info () = atp_problem_term_order_info atp_problem
    4.25 @@ -332,7 +334,7 @@
    4.26              end
    4.27            | maybe_run_slice _ result = result
    4.28        in
    4.29 -        ((NONE, ([], Symtab.empty, [], Symtab.empty)),
    4.30 +        ((NONE, ([], Symtab.empty, [], Symtab.empty,NONE)),
    4.31           ("", Time.zeroTime, [], [], SOME InternalError), NONE)
    4.32          |> fold maybe_run_slice actual_slices
    4.33        end
    4.34 @@ -344,7 +346,7 @@
    4.35        if dest_dir = "" then ()
    4.36        else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
    4.37  
    4.38 -    val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome),
    4.39 +    val ((_, (_, pool, lifted, sym_tab,wm_info)), (output, run_time, used_from, atp_proof, outcome),
    4.40           SOME (format, type_enc)) =
    4.41        with_cleanup clean_up run () |> tap export
    4.42  
    4.43 @@ -378,8 +380,10 @@
    4.44                        if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE
    4.45                      val atp_proof =
    4.46                        atp_proof
    4.47 -                      |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
    4.48 +                      |> (if waldmeister_new then termify_waldmeister_proof ctxt pool
    4.49 +                          else termify_atp_proof ctxt name format type_enc pool lifted sym_tab)
    4.50                        |> spass ? introduce_spass_skolems
    4.51 +                      |> waldmeister_new ? introduce_waldmeister_skolems (the wm_info)
    4.52                        |> factify_atp_proof (map fst used_from) hyp_ts concl_t
    4.53                    in
    4.54                      (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
    4.55 @@ -404,4 +408,4 @@
    4.56       preferred_methss = preferred_methss, run_time = run_time, message = message}
    4.57    end
    4.58  
    4.59 -end;
    4.60 +end;
    4.61 \ No newline at end of file