--- a/src/HOL/List.thy Tue Sep 18 16:08:08 2007 +0200
+++ b/src/HOL/List.thy Tue Sep 18 17:53:37 2007 +0200
@@ -689,10 +689,7 @@
"map f xs = map f ys ==> length xs = length ys"
apply (induct ys arbitrary: xs)
apply simp
-apply(simp (no_asm_use))
-apply clarify
-apply(simp (no_asm_use))
-apply fast
+apply (metis Suc_length_conv length_map)
done
lemma map_inj_on:
@@ -1091,7 +1088,7 @@
lemma list_eq_iff_nth_eq:
"(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
apply(induct xs arbitrary: ys)
- apply simp apply blast
+ apply force
apply(case_tac ys)
apply simp
apply(simp add:nth_Cons split:nat.split)apply blast
@@ -1100,11 +1097,10 @@
lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
apply (induct xs, simp, simp)
apply safe
-apply (rule_tac x = 0 in exI, simp)
- apply (rule_tac x = "Suc i" in exI, simp)
+apply (metis nat_case_0 nth.simps zero_less_Suc)
+apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
apply (case_tac i, simp)
-apply (rename_tac j)
-apply (rule_tac x = j in exI, simp)
+apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
done
lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
@@ -1926,10 +1922,7 @@
by simp
lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
-apply(rule trans)
-apply(subst upt_rec)
- prefer 2 apply (rule refl, simp)
-done
+by (metis upt_rec)
lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
-- {* LOOPS as a simprule, since @{text "j <= j"}. *}
@@ -2046,13 +2039,7 @@
by (induct xs) auto
lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
-proof -
- assume "finite A"
- then obtain xs where "set xs = A" by(auto dest!:finite_list)
- hence "set(remdups xs) = A & distinct(remdups xs)" by simp
- thus ?thesis ..
-qed
-(* by (metis distinct_remdups finite_list set_remdups) *)
+by (metis distinct_remdups finite_list set_remdups)
lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
by (induct x, auto)
@@ -2128,11 +2115,8 @@
apply (case_tac j)
apply (clarsimp simp add: set_conv_nth, simp)
apply (rule conjI)
- apply (clarsimp simp add: set_conv_nth)
- apply (erule_tac x = 0 in allE, simp)
- apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
-apply (erule_tac x = "Suc i" in allE, simp)
-apply (erule_tac x = "Suc j" in allE, simp)
+apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
+apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
done
lemma nth_eq_iff_index_eq:
@@ -2798,7 +2782,7 @@
apply (case_tac xa, erule ssubst)
apply (erule allE, erule allE) -- {* avoid simp recursion *}
apply (case_tac x, simp, simp)
- apply (case_tac x, erule allE, erule allE, simp)
+ apply (case_tac x, erule allE, erule allE, simp)
apply (erule_tac x = listb in allE)
apply (erule_tac x = lista in allE, simp)
apply (unfold trans_def)
--- a/src/HOL/Main.thy Tue Sep 18 16:08:08 2007 +0200
+++ b/src/HOL/Main.thy Tue Sep 18 17:53:37 2007 +0200
@@ -5,7 +5,7 @@
header {* Main HOL *}
theory Main
-imports Map Hilbert_Choice ATP_Linkup
+imports Map
begin
text {*
@@ -13,10 +13,11 @@
PreList} already includes most HOL theories.
\medskip Late clause setup: installs \emph{all} known theorems
- into the clause cache; cf.\ theory @{text ATP_Linkup}.
+ into the clause cache; cf.\ theory @{text ATP_Linkup}.
+ FIXME: delete once end_theory actions are installed!
*}
-setup ResAxioms.setup
+setup ResAxioms.clause_cache_setup
ML {* val HOL_proofs = !proofs *}
--- a/src/HOL/MetisExamples/Abstraction.thy Tue Sep 18 16:08:08 2007 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy Tue Sep 18 17:53:37 2007 +0200
@@ -93,8 +93,7 @@
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"proof (neg_clausify)
assume 0: "(cl, f) \<in> CLF"
assume 1: "CLF = Sigma CL llabs_subgoal_1"
-assume 2: "\<And>cl. llabs_subgoal_1 cl =
- Collect (llabs_List_Xlists_def_1_ (pset cl))"
+assume 2: "\<And>cl. llabs_subgoal_1 cl = Collect (llabs_Predicate_Xsup_Un_eq_1_ (pset cl))"
assume 3: "f \<notin> pset cl"
show "False"
by (metis 0 1 SigmaD2 3 2 Collect_mem_eq)
@@ -109,15 +108,17 @@
lemma
"(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
- f \<in> pset cl \<rightarrow> pset cl"
+ f \<in> pset cl \<rightarrow> pset cl"
proof (neg_clausify)
assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1"
assume 1: "\<And>cl. llabs_subgoal_1 cl =
Collect
- (llabs_List_Xlists_def_1_ (Pi (pset cl) (COMBK (pset cl))))"
+ (llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))))"
assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
+have 3: "\<not> llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))) f"
+ by (metis Collect_mem_eq 2)
show "False"
- by (metis Collect_mem_eq 1 2 SigmaD2 0)
+ by (metis acc_def 0 Collect_mem_eq SigmaD2 3 1 Collect_mem_eq)
qed finish_clausify
(*Hack to prevent the "Additional hypotheses" error*)
--- a/src/HOL/PreList.thy Tue Sep 18 16:08:08 2007 +0200
+++ b/src/HOL/PreList.thy Tue Sep 18 17:53:37 2007 +0200
@@ -7,7 +7,7 @@
header {* A Basis for Building the Theory of Lists *}
theory PreList
-imports Presburger Relation_Power SAT Recdef Extraction Record
+imports Presburger Relation_Power SAT Recdef Extraction Record ATP_Linkup
uses "Tools/function_package/lexicographic_order.ML"
"Tools/function_package/fundef_datatype.ML"
begin
@@ -21,5 +21,8 @@
setup LexicographicOrder.setup
setup FundefDatatype.setup
+(*Sledgehammer*)
+setup ResAxioms.setup
+
end
--- a/src/HOL/Tools/res_axioms.ML Tue Sep 18 16:08:08 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue Sep 18 17:53:37 2007 +0200
@@ -15,6 +15,7 @@
val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
val meson_method_setup : theory -> theory
val setup : theory -> theory
+ val clause_cache_setup : theory -> theory
val assume_abstract_list: string -> thm list -> thm list
val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
--- a/src/HOL/Tools/res_reconstruct.ML Tue Sep 18 16:08:08 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Sep 18 17:53:37 2007 +0200
@@ -523,11 +523,14 @@
get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract));
(*String contains multiple lines. We want those of the form
- "*********** [448, input] ***********".
+ "*********** [448, input] ***********"
+ or possibly those of the form
+ "cnf(108, axiom, ..."
A list consisting of the first number in each line is returned. *)
fun get_vamp_linenums proofextract =
let val toks = String.tokens (not o Char.isAlphaNum)
fun inputno [ntok,"input"] = Int.fromString ntok
+ | inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
| inputno _ = NONE
val lines = String.tokens (fn c => c = #"\n") proofextract
in List.mapPartial (inputno o toks) lines end