# HG changeset patch
# User steckerm
# Date 1411202664 -7200
# Node ID 539cc471186f0ddddd213274c1a62d5cddceab06
# Parent  c3c7a09a3adaaaf36b6de336500d90d9f0828c2c
Minor fixes in ATP_Waldmeister

diff -r c3c7a09a3ada -r 539cc471186f src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Sat Sep 20 10:44:23 2014 +0200
+++ b/src/HOL/ATP.thy	Sat Sep 20 10:44:24 2014 +0200
@@ -133,10 +133,15 @@
 
 subsection {* Waldmeister helpers *}
 
-(* Has all needed simplification lemmas for logic.
-   "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
-lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
-  eq_ac disj_comms disj_assoc conj_comms conj_assoc
+(* Has all needed simplification lemmas for logic. *)
+lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
+  by simp
+
+lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
+  by metis
+
+lemmas waldmeister_fol = boolean_equality boolean_comm
+  simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc
 
 
 subsection {* Basic connection between ATPs and HOL *}
@@ -148,6 +153,6 @@
 ML_file "Tools/ATP/atp_systems.ML"
 ML_file "Tools/ATP/atp_waldmeister.ML"
 
-hide_fact (open) waldmeister_fol
+hide_fact (open) waldmeister_fol boolean_equality boolean_comm
 
 end
diff -r c3c7a09a3ada -r 539cc471186f src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:44:23 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:44:24 2014 +0200
@@ -304,7 +304,8 @@
       val resT = dest_funT funT |> snd
       val newT = funT --> argT --> resT
     in
-      mk_waldmeister_app (Const (waldmeister_apply ^ encode_type resT, newT) $ function $ a) args
+      mk_waldmeister_app (Const (waldmeister_apply ^ "," ^ 
+        encode_types [resT, argT], newT) $ function $ a) args
     end
 
 fun hide_partial_applications info (trm as (_ $ _)) =
@@ -335,7 +336,7 @@
   | remove_waldmeister_app x = x
 
 (*
-  Translation from Isabelle theorms and terms to ATP terms.
+  Translation from Isabelle terms to ATP terms.
 *)
 
 fun trm_to_atp'' thy (Const (x, ty)) args =
@@ -425,8 +426,8 @@
 fun mk_formula prefix_name name atype aterm =
   Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
 
-fun problem_lines_of_fact thy prefix (s, (_, (_, t))) fact_number =
-  mk_formula (prefix ^ Int.toString fact_number ^ "_") s Axiom (eq_trm_to_atp thy t)
+fun problem_lines_of_fact thy prefix (s, (_, (_, t))) =
+  mk_formula (prefix ^ "0_") s Axiom (eq_trm_to_atp thy t)
 
 fun make_nice problem = nice_atp_problem true CNF problem
 
@@ -468,7 +469,8 @@
       | name_list' prefix (x :: xs) i = (prefix ^ Int.toString i, x) :: name_list' prefix xs (i + 1)
 
     fun name_list prefix xs = name_list' prefix xs 0
-
+    
+    (* Skolemization, hiding lambdas and translating formulas to equations *)
     val (ctxt', sko_facts) = map_ctxt skolemize_fact ctxt facts
     val (ctxt'', sko_conditions) = map_ctxt (skolemize true) ctxt' conditions
 
@@ -484,6 +486,7 @@
       (((conj_identifier, eq_conseq) :: sko_eq_conditions0) 
       @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts0)
 
+    (* Translation of partial function applications *)
     val fun_app_info = map_minimal_app (map (snd o snd o snd) sko_eq_info)
 
     fun hide_partial_apps_in_last (x, (y, (z, term))) = 
@@ -493,10 +496,8 @@
     val sko_eq_conditions = map hide_partial_apps_in_last sko_eq_conditions0
     val eq_consequence = hide_partial_applications fun_app_info eq_consequence0
 
-    fun map_enum _ _ [] = []
-      | map_enum f i (x :: xs) = f x i :: map_enum f (i + 1) xs
-
-    val fact_lines = map_enum (problem_lines_of_fact thy fact_prefix) 0 sko_eq_facts
+    (* Problem creation *)
+    val fact_lines = map (problem_lines_of_fact thy fact_prefix) sko_eq_facts
     val condition_lines =
       map (fn (name, (_, (_, trm))) =>
         mk_formula fact_prefix name Hypothesis (eq_trm_to_atp thy trm)) sko_eq_conditions
@@ -543,19 +544,12 @@
   SOME x => x |
   NONE => NONE
 
-fun fix_name name =
-  let
-    fun drop_digits' xs [] = (xs, [])
-      | drop_digits' xs (c :: cs) = if Char.isDigit c then drop_digits' (c :: xs) cs else
-        (xs, (c :: cs))
-    fun drop_digits xs = drop_digits' [] xs
-  in
-    if String.isPrefix fact_prefix name then 
-      String.extract(name,size fact_prefix,NONE) |> String.explode |> drop_digits ||> tl 
-        ||> String.implode ||> unascii_of |> (fn (x,y) => fact_prefix ^ String.implode x ^ "_" ^ y)
-    else
-      name
-  end
+fun fix_name name = 
+  if  String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then
+    String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |> 
+    (fn x => fact_prefix ^ "0_" ^ x)
+  else
+    name
 
 fun skolemization_steps info
   (proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) =