metis now available in PreList
authorpaulson
Tue Sep 18 17:53:37 2007 +0200 (2007-09-18)
changeset 24632779fc4fcbf8b
parent 24631 c7da302a0346
child 24633 0a3a02066244
metis now available in PreList
src/HOL/List.thy
src/HOL/Main.thy
src/HOL/MetisExamples/Abstraction.thy
src/HOL/PreList.thy
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_reconstruct.ML
     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