author paulson Tue Sep 18 17:53:37 2007 +0200 (2007-09-18) changeset 24632 779fc4fcbf8b parent 24631 c7da302a0346 child 24633 0a3a02066244
metis now available in PreList
 src/HOL/List.thy file | annotate | diff | revisions src/HOL/Main.thy file | annotate | diff | revisions src/HOL/MetisExamples/Abstraction.thy file | annotate | diff | revisions src/HOL/PreList.thy file | annotate | diff | revisions src/HOL/Tools/res_axioms.ML file | annotate | diff | revisions src/HOL/Tools/res_reconstruct.ML file | annotate | diff | revisions
     1.1 --- a/src/HOL/List.thy	Tue Sep 18 16:08:08 2007 +0200
1.2 +++ b/src/HOL/List.thy	Tue Sep 18 17:53:37 2007 +0200
1.3 @@ -689,10 +689,7 @@
1.4    "map f xs = map f ys ==> length xs = length ys"
1.5  apply (induct ys arbitrary: xs)
1.6   apply simp
1.7 -apply(simp (no_asm_use))
1.8 -apply clarify
1.9 -apply(simp (no_asm_use))
1.10 -apply fast
1.11 +apply (metis Suc_length_conv length_map)
1.12  done
1.13
1.14  lemma map_inj_on:
1.15 @@ -1091,7 +1088,7 @@
1.16  lemma list_eq_iff_nth_eq:
1.17   "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
1.18  apply(induct xs arbitrary: ys)
1.19 - apply simp apply blast
1.20 + apply force
1.21  apply(case_tac ys)
1.22   apply simp
1.23  apply(simp add:nth_Cons split:nat.split)apply blast
1.24 @@ -1100,11 +1097,10 @@
1.25  lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
1.26  apply (induct xs, simp, simp)
1.27  apply safe
1.28 -apply (rule_tac x = 0 in exI, simp)
1.29 - apply (rule_tac x = "Suc i" in exI, simp)
1.30 +apply (metis nat_case_0 nth.simps zero_less_Suc)
1.31 +apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
1.32  apply (case_tac i, simp)
1.33 -apply (rename_tac j)
1.34 -apply (rule_tac x = j in exI, simp)
1.35 +apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
1.36  done
1.37
1.38  lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
1.39 @@ -1926,10 +1922,7 @@
1.40  by simp
1.41
1.42  lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
1.43 -apply(rule trans)
1.44 -apply(subst upt_rec)
1.45 - prefer 2 apply (rule refl, simp)
1.46 -done
1.47 +by (metis upt_rec)
1.48
1.49  lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
1.50  -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
1.51 @@ -2046,13 +2039,7 @@
1.52  by (induct xs) auto
1.53
1.54  lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
1.55 -proof -
1.56 -  assume "finite A"
1.57 -  then obtain xs where "set xs = A" by(auto dest!:finite_list)
1.58 -  hence "set(remdups xs) = A & distinct(remdups xs)" by simp
1.59 -  thus ?thesis ..
1.60 -qed
1.61 -(* by (metis distinct_remdups finite_list set_remdups) *)
1.62 +by (metis distinct_remdups finite_list set_remdups)
1.63
1.64  lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
1.65  by (induct x, auto)
1.66 @@ -2128,11 +2115,8 @@
1.67   apply (case_tac j)
1.68  apply (clarsimp simp add: set_conv_nth, simp)
1.69  apply (rule conjI)
1.70 - apply (clarsimp simp add: set_conv_nth)
1.71 - apply (erule_tac x = 0 in allE, simp)
1.72 - apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
1.73 -apply (erule_tac x = "Suc i" in allE, simp)
1.74 -apply (erule_tac x = "Suc j" in allE, simp)
1.75 +apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
1.76 +apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
1.77  done
1.78
1.79  lemma nth_eq_iff_index_eq:
1.80 @@ -2798,7 +2782,7 @@
1.81    apply (case_tac xa, erule ssubst)
1.82    apply (erule allE, erule allE) -- {* avoid simp recursion *}
1.83    apply (case_tac x, simp, simp)
1.84 -  apply (case_tac x, erule allE, erule allE, simp)
1.85 +  apply (case_tac x, erule allE, erule allE, simp)
1.86    apply (erule_tac x = listb in allE)
1.87    apply (erule_tac x = lista in allE, simp)
1.88    apply (unfold trans_def)

     2.1 --- a/src/HOL/Main.thy	Tue Sep 18 16:08:08 2007 +0200
2.2 +++ b/src/HOL/Main.thy	Tue Sep 18 17:53:37 2007 +0200
2.3 @@ -5,7 +5,7 @@
2.4  header {* Main HOL *}
2.5
2.6  theory Main
2.7 -imports Map Hilbert_Choice ATP_Linkup
2.8 +imports Map
2.9  begin
2.10
2.11  text {*
2.12 @@ -13,10 +13,11 @@
2.13    PreList} already includes most HOL theories.
2.14
2.15    \medskip Late clause setup: installs \emph{all} known theorems
2.16 -  into the clause cache; cf.\ theory @{text ATP_Linkup}.
2.17 +  into the clause cache; cf.\ theory @{text ATP_Linkup}.
2.18 +  FIXME: delete once end_theory actions are installed!
2.19  *}
2.20
2.21 -setup ResAxioms.setup
2.22 +setup ResAxioms.clause_cache_setup
2.23
2.24  ML {* val HOL_proofs = !proofs *}
2.25

     3.1 --- a/src/HOL/MetisExamples/Abstraction.thy	Tue Sep 18 16:08:08 2007 +0200
3.2 +++ b/src/HOL/MetisExamples/Abstraction.thy	Tue Sep 18 17:53:37 2007 +0200
3.3 @@ -93,8 +93,7 @@
3.4  lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"proof (neg_clausify)
3.5  assume 0: "(cl, f) \<in> CLF"
3.6  assume 1: "CLF = Sigma CL llabs_subgoal_1"
3.7 -assume 2: "\<And>cl. llabs_subgoal_1 cl =
3.8 -     Collect (llabs_List_Xlists_def_1_ (pset cl))"
3.9 +assume 2: "\<And>cl. llabs_subgoal_1 cl = Collect (llabs_Predicate_Xsup_Un_eq_1_ (pset cl))"
3.10  assume 3: "f \<notin> pset cl"
3.11  show "False"
3.12    by (metis 0 1 SigmaD2 3 2 Collect_mem_eq)
3.13 @@ -109,15 +108,17 @@
3.14
3.15  lemma
3.16      "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
3.17 -    f \<in> pset cl \<rightarrow> pset cl"
3.18 +    f \<in> pset cl \<rightarrow> pset cl"
3.19  proof (neg_clausify)
3.20  assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1"
3.21  assume 1: "\<And>cl. llabs_subgoal_1 cl =
3.22       Collect
3.23 -      (llabs_List_Xlists_def_1_ (Pi (pset cl) (COMBK (pset cl))))"
3.24 +      (llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))))"
3.25  assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
3.26 +have 3: "\<not> llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))) f"
3.27 +  by (metis Collect_mem_eq 2)
3.28  show "False"
3.29 -  by (metis Collect_mem_eq 1 2 SigmaD2 0)
3.30 +  by (metis acc_def 0 Collect_mem_eq SigmaD2 3 1 Collect_mem_eq)
3.31  qed finish_clausify
3.32      (*Hack to prevent the "Additional hypotheses" error*)
3.33

     4.1 --- a/src/HOL/PreList.thy	Tue Sep 18 16:08:08 2007 +0200
4.2 +++ b/src/HOL/PreList.thy	Tue Sep 18 17:53:37 2007 +0200
4.3 @@ -7,7 +7,7 @@
4.4  header {* A Basis for Building the Theory of Lists *}
4.5
4.6  theory PreList
4.7 -imports Presburger Relation_Power SAT Recdef Extraction Record
4.8 +imports Presburger Relation_Power SAT Recdef Extraction Record ATP_Linkup
4.9  uses "Tools/function_package/lexicographic_order.ML"
4.10       "Tools/function_package/fundef_datatype.ML"
4.11  begin
4.12 @@ -21,5 +21,8 @@
4.13  setup LexicographicOrder.setup
4.14  setup FundefDatatype.setup
4.15
4.16 +(*Sledgehammer*)
4.17 +setup ResAxioms.setup
4.18 +
4.19  end
4.20

     5.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Sep 18 16:08:08 2007 +0200
5.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Sep 18 17:53:37 2007 +0200
5.3 @@ -15,6 +15,7 @@
5.4    val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
5.5    val meson_method_setup : theory -> theory
5.6    val setup : theory -> theory
5.7 +  val clause_cache_setup : theory -> theory
5.8    val assume_abstract_list: string -> thm list -> thm list
5.9    val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
5.10    val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)

     6.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Sep 18 16:08:08 2007 +0200
6.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Sep 18 17:53:37 2007 +0200
6.3 @@ -523,11 +523,14 @@
6.4     get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract));
6.5
6.6   (*String contains multiple lines. We want those of the form
6.7 -     "*********** [448, input] ***********".
6.8 +     "*********** [448, input] ***********"
6.9 +   or possibly those of the form
6.10 +     "cnf(108, axiom, ..."
6.11    A list consisting of the first number in each line is returned. *)
6.12  fun get_vamp_linenums proofextract =
6.13    let val toks = String.tokens (not o Char.isAlphaNum)
6.14        fun inputno [ntok,"input"] = Int.fromString ntok
6.15 +        | inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
6.16          | inputno _ = NONE
6.17        val lines = String.tokens (fn c => c = #"\n") proofextract
6.18    in  List.mapPartial (inputno o toks) lines  end