# HG changeset patch # User paulson # Date 1190908528 -7200 # Node ID 73b8b42a36b67054f5daa090ecf5ee65964426ec # Parent a53f5db5acbb040d71aec6c8460af43b5cea3f3d removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/ATP_Linkup.thy Thu Sep 27 17:55:28 2007 +0200 @@ -7,7 +7,8 @@ header{* The Isabelle-ATP Linkup *} theory ATP_Linkup -imports Divides Record Hilbert_Choice +imports Divides Record Hilbert_Choice Presburger Relation_Power SAT Recdef Extraction + (*It must be a parent or a child of every other theory, to prevent theory-merge errors.*) uses "Tools/polyhash.ML" "Tools/res_clause.ML" @@ -110,4 +111,11 @@ use "Tools/metis_tools.ML" setup MetisTools.setup +(*Sledgehammer*) +setup ResAxioms.setup + +setup {* + Theory.at_end ResAxioms.clause_cache_endtheory +*} + end diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Algebra/Exponent.thy Thu Sep 27 17:55:28 2007 +0200 @@ -205,15 +205,10 @@ apply (rule notnotD) apply (rule notI) apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption) -apply (drule_tac m = a in less_imp_le) +apply (drule less_imp_le [of a]) apply (drule le_imp_power_dvd) apply (drule_tac n = "p ^ r" in dvd_trans, assumption) -apply (frule_tac m = k in less_imp_le) -apply (drule_tac c = m in le_extend_mult, assumption) -apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1) -prefer 2 apply assumption -apply (rule dvd_refl [THEN dvd_mult2]) -apply (drule_tac n = k in dvd_imp_le, auto) +apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less) done lemma p_fac_forw: "[| 0 < (m::nat); 0 deg (p + q) < deg r" - apply (rule_tac j = "deg r - 1" in le_less_trans) + apply (rule le_less_trans [of _ "deg r - 1"]) prefer 2 apply arith apply (rule deg_aboveI) @@ -248,13 +248,8 @@ f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2" apply (subgoal_tac "q1 = q2") - apply clarify - apply (rule_tac a = "q2 * g + r1 - q2 * g" and b = "q2 * g + r2 - q2 * g" in box_equals) - apply simp - apply (simp (no_asm)) - apply (simp (no_asm)) - apply (rule long_div_quo_unique) - apply assumption+ + apply (metis a_comm a_lcancel m_comm) + apply (metis a_comm l_zero long_div_quo_unique m_comm conc) done end diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Complex/ex/NSPrimes.thy --- a/src/HOL/Complex/ex/NSPrimes.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Complex/ex/NSPrimes.thy Thu Sep 27 17:55:28 2007 +0200 @@ -215,8 +215,7 @@ apply (rule inj_onI) apply (rule ccontr, auto) apply (drule injf_max_order_preserving2) -apply (cut_tac m = x and n = y in less_linear, auto) -apply (auto dest!: spec) +apply (metis linorder_antisym_conv3 order_less_le) done lemma infinite_set_has_order_preserving_inj: diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/HoareParallel/Gar_Coll.thy --- a/src/HOL/HoareParallel/Gar_Coll.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/HoareParallel/Gar_Coll.thy Thu Sep 27 17:55:28 2007 +0200 @@ -185,7 +185,7 @@ apply (erule_tac x=i in allE , erule (1) notE impE) apply simp apply clarify - apply (drule le_imp_less_or_eq) + apply (drule Nat.le_imp_less_or_eq) apply (erule disjE) apply (subgoal_tac "Suc (ind x)\r") apply fast @@ -276,7 +276,7 @@ apply (erule_tac x=i in allE , erule (1) notE impE) apply simp apply clarify - apply (drule le_imp_less_or_eq) + apply (drule Nat.le_imp_less_or_eq) apply (erule disjE) apply (subgoal_tac "Suc (ind x)\r") apply fast @@ -309,7 +309,7 @@ apply (erule_tac x=i in allE , erule (1) notE impE) apply simp apply clarify - apply (drule le_imp_less_or_eq) + apply (drule Nat.le_imp_less_or_eq) apply (erule disjE) apply (subgoal_tac "Suc (ind x)\r") apply fast diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/HoareParallel/Graph.thy --- a/src/HOL/HoareParallel/Graph.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/HoareParallel/Graph.thy Thu Sep 27 17:55:28 2007 +0200 @@ -1,4 +1,3 @@ - header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms} \section {Formalization of the Memory} *} @@ -337,7 +336,7 @@ apply(erule_tac P = "\i. i < Suc nat \ ?P i" and x = "nat" in allE) apply simp apply(case_tac "j\R") - apply(drule le_imp_less_or_eq) + apply(drule Nat.le_imp_less_or_eq) apply(erule disjE) apply(erule allE , erule (1) notE impE) apply force diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/HoareParallel/Mul_Gar_Coll.thy --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Thu Sep 27 17:55:28 2007 +0200 @@ -383,8 +383,7 @@ apply force --{* 1 subgoal left *} apply clarify -apply(drule le_imp_less_or_eq) -apply(disjE_tac) +apply(drule Nat.le_imp_less_or_eq) apply (simp_all add:Blacks_def) done diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Hyperreal/Integration.thy --- a/src/HOL/Hyperreal/Integration.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Hyperreal/Integration.thy Thu Sep 27 17:55:28 2007 +0200 @@ -553,18 +553,15 @@ done lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n" -apply (cut_tac m = n and n = "psize D" in less_linear, auto) -apply (cut_tac m = m and n = n in less_linear) -apply (cut_tac m = m and n = "psize D" in less_linear) +apply (cut_tac less_linear [of n "psize D"], auto) +apply (cut_tac less_linear [of m n]) +apply (cut_tac less_linear [of m "psize D"]) apply (auto dest: partition_gt) apply (drule_tac n = m in partition_lt_gen, auto) apply (frule partition_eq_bound) apply (drule_tac [2] partition_gt, auto) -apply (rule ccontr, drule leI, drule le_imp_less_or_eq) -apply (auto dest: partition_eq_bound) -apply (rule ccontr, drule leI, drule le_imp_less_or_eq) -apply (frule partition_eq_bound, assumption) -apply (drule_tac m = m in partition_eq_bound, auto) +apply (metis dense_linear_order_class.dlo_simps(8) le_def partition_rhs partition_rhs2) +apply (metis Nat.le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2) done lemma lemma_additivity4_psize_eq: @@ -577,7 +574,7 @@ apply (auto intro: partition_lt_Suc) apply (drule_tac n = n in partition_lt_gen, assumption) apply (arith, arith) -apply (cut_tac m = na and n = "psize D" in less_linear) +apply (cut_tac m = na and n = "psize D" in Nat.less_linear) apply (auto dest: partition_lt_cancel) apply (rule_tac x=N and y=n in linorder_cases) apply (drule_tac x = n and P="%m. N \ m --> ?f m = ?g m" in spec, simp) @@ -609,12 +606,8 @@ "[| partition(a,b) D; D na < D n; D n < D (Suc na); n < psize D |] ==> False" -apply (cut_tac m = n and n = "Suc na" in less_linear, auto) -apply (drule_tac [2] n = n in partition_lt_gen, auto) -apply (cut_tac m = "psize D" and n = na in less_linear) -apply (auto simp add: partition_rhs2 less_Suc_eq) -apply (drule_tac n = na in partition_lt_gen, auto) -done +by (metis not_less_eq partition_lt_cancel real_of_nat_less_iff) + lemma psize_const [simp]: "psize (%x. k) = 0" by (auto simp add: psize_def) diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Hyperreal/Poly.thy --- a/src/HOL/Hyperreal/Poly.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Hyperreal/Poly.thy Thu Sep 27 17:55:28 2007 +0200 @@ -739,10 +739,7 @@ ==> EX! n. ([-a, 1] %^ n) divides p & ~(([-a, 1] %^ (Suc n)) divides p)" apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc) -apply (cut_tac m = y and n = n in less_linear) -apply (drule_tac m = n in poly_exp_divides) -apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides] - simp del: pmult_Cons pexp_Suc) +apply (metis Suc_leI Nat.less_linear poly_exp_divides) done text{*Order*} diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Hyperreal/StarClasses.thy --- a/src/HOL/Hyperreal/StarClasses.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Hyperreal/StarClasses.thy Thu Sep 27 17:55:28 2007 +0200 @@ -348,8 +348,8 @@ instance star :: (semiring_0_cancel) semiring_0_cancel .. -instance star :: (comm_semiring) comm_semiring -by (intro_classes, transfer, rule distrib) +instance star :: (comm_semiring) comm_semiring +by (intro_classes, transfer, rule left_distrib) instance star :: (comm_semiring_0) comm_semiring_0 .. instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/IOA/IOA.thy --- a/src/HOL/IOA/IOA.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/IOA/IOA.thy Thu Sep 27 17:55:28 2007 +0200 @@ -251,9 +251,7 @@ apply (rule_tac x = "Suc n" in exI) apply (simp (no_asm)) apply simp - apply (rule allI) - apply (cut_tac m = "na" and n = "n" in less_linear) - apply auto + apply (metis ioa_triple_proj less_antisym) done diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Main.thy --- a/src/HOL/Main.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Main.thy Thu Sep 27 17:55:28 2007 +0200 @@ -11,14 +11,8 @@ text {* Theory @{text Main} includes everything. Note that theory @{text PreList} already includes most HOL theories. - - \medskip Late clause setup: installs \emph{all} known theorems - into the clause cache; cf.\ theory @{text ATP_Linkup}. - FIXME: delete once @{text end_theory} actions are installed! *} -setup ResAxioms.clause_cache_setup - ML {* val HOL_proofs = !proofs *} end diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/MetisExamples/Abstraction.thy --- a/src/HOL/MetisExamples/Abstraction.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/MetisExamples/Abstraction.thy Thu Sep 27 17:55:28 2007 +0200 @@ -90,13 +90,20 @@ apply (metis Collect_mem_eq SigmaD2); done -lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL.{f. f \ pset cl}) ==> f \ pset cl"proof (neg_clausify) -assume 0: "(cl, f) \ CLF" -assume 1: "CLF = Sigma CL llabs_subgoal_1" -assume 2: "\cl. llabs_subgoal_1 cl = Collect (llabs_Predicate_Xsup_Un_eq_1_ (pset cl))" -assume 3: "f \ pset cl" +lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL.{f. f \ pset cl}) ==> f \ pset cl" +proof (neg_clausify) +assume 0: "\cl\'a\type set. + (llabs_subgoal_1\'a\type set \ 'a\type set) cl = + Collect (llabs_Set_XCollect_ex_eq_3_ op \ (pset cl))" +assume 1: "(f\'a\type) \ pset (cl\'a\type set)" +assume 2: "(cl\'a\type set, f\'a\type) \ (CLF\('a\type set \ 'a\type) set)" +have 3: "llabs_Predicate_Xsup_Un_eq2_1_ (CLF\('a\type set \ 'a\type) set) + (cl\'a\type set) (f\'a\type)" + by (metis acc_def 2) +assume 4: "(CLF\('a\type set \ 'a\type) set) = +Sigma (CL\'a\type set set) (llabs_subgoal_1\'a\type set \ 'a\type set)" show "False" - by (metis 0 1 SigmaD2 3 2 Collect_mem_eq) + by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2) qed finish_clausify (*ugly hack: combinators??*) ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*} @@ -110,15 +117,16 @@ "(cl,f) \ (SIGMA cl::'a set : CL. {f. f \ pset cl \ pset cl}) ==> f \ pset cl \ pset cl" proof (neg_clausify) -assume 0: "(cl, f) \ Sigma CL llabs_subgoal_1" -assume 1: "\cl. llabs_subgoal_1 cl = - Collect - (llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))))" -assume 2: "f \ Pi (pset cl) (COMBK (pset cl))" -have 3: "\ llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))) f" - by (metis Collect_mem_eq 2) +assume 0: "\cl\'a\type set. + (llabs_subgoal_1\'a\type set \ ('a\type \ 'a\type) set) cl = + Collect + (llabs_Set_XCollect_ex_eq_3_ op \ (Pi (pset cl) (COMBK (pset cl))))" +assume 1: "(f\'a\type \ 'a\type) \ Pi (pset (cl\'a\type set)) (COMBK (pset cl))" +assume 2: "(cl\'a\type set, f\'a\type \ 'a\type) +\ Sigma (CL\'a\type set set) + (llabs_subgoal_1\'a\type set \ ('a\type \ 'a\type) set)" show "False" - by (metis acc_def 0 Collect_mem_eq SigmaD2 3 1 Collect_mem_eq) + by (metis 1 Collect_mem_eq 0 SigmaD2 2) qed finish_clausify (*Hack to prevent the "Additional hypotheses" error*) diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/MetisExamples/set.thy --- a/src/HOL/MetisExamples/set.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/MetisExamples/set.thy Thu Sep 27 17:55:28 2007 +0200 @@ -11,7 +11,7 @@ lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & (S(x,y) | ~S(y,z) | Q(Z,Z)) & - (Q(X,y) | ~Q(y,Z) | S(X,X))" + (Q(X,y) | ~Q(y,Z) | S(X,X))" by metis (*??But metis can't prove the single-step version...*) diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/PreList.thy --- a/src/HOL/PreList.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/PreList.thy Thu Sep 27 17:55:28 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 ATP_Linkup +imports ATP_Linkup uses "Tools/function_package/lexicographic_order.ML" "Tools/function_package/fundef_datatype.ML" begin @@ -21,7 +21,4 @@ setup LexicographicOrder.setup setup FundefDatatype.setup -(*Sledgehammer*) -setup ResAxioms.setup - end diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Tools/meson.ML Thu Sep 27 17:55:28 2007 +0200 @@ -209,10 +209,10 @@ (*** The basic CNF transformation ***) -val max_clauses = ref 40; +val max_clauses = 40; -fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses; -fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses; +fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses; +fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses; (*Estimate the number of clauses in order to detect infeasible theorems*) fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t @@ -239,7 +239,7 @@ val nclauses = signed_nclauses true; -fun too_many_clauses t = nclauses t >= !max_clauses; +fun too_many_clauses t = nclauses t >= max_clauses; (*Replaces universally quantified variables by FREE variables -- because assumptions may not contain scheme variables. Later, we call "generalize". *) @@ -396,7 +396,7 @@ [] => false (*not a function type, OK*) | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts; -(*Raises an exception if any Vars in the theorem mention type bool. +(*Returns false if any Vars in the theorem mention type bool. Also rejects functions whose arguments are Booleans or other functions.*) fun is_fol_term thy t = Term.is_first_order ["all","All","Ex"] t andalso diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Sep 27 17:55:28 2007 +0200 @@ -21,19 +21,13 @@ val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) val atpset_rules_of: Proof.context -> (string * thm) list val meson_method_setup: theory -> theory - val clause_cache_setup: theory -> theory + val clause_cache_endtheory: theory -> theory option val setup: theory -> theory end; structure ResAxioms: RES_AXIOMS = struct -(*For running the comparison between combinators and abstractions. - CANNOT be a ref, as the setting is used while Isabelle is built. - Currently TRUE: the combinator code cannot be used with proof reconstruction - because it is not performed by inference!!*) -val abstract_lambdas = true; - (* FIXME legacy *) fun freeze_thm th = #1 (Drule.freeze_thaw th); @@ -74,22 +68,19 @@ Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th | _ => th; -(**** Transformation of Clasets and Simpsets into First-Order Axioms ****) - -(*Transfer a theorem into theory ATP_Linkup.thy if it is not already - inside that theory -- because it's needed for Skolemization *) - -(*This will refer to the final version of theory ATP_Linkup.*) -val recon_thy_ref = Theory.check_thy @{theory} - -(*If called while ATP_Linkup is being created, it will transfer to the - current version. If called afterward, it will transfer to the final version.*) -fun transfer_to_ATP_Linkup th = - transfer (Theory.deref recon_thy_ref) th handle THM _ => th; - +(*To enforce single-threading*) +exception Clausify_failure of theory; (**** SKOLEMIZATION BY INFERENCE (lcp) ****) +fun rhs_extra_types lhsT rhs = + let val lhs_vars = Term.add_tfreesT lhsT [] + fun add_new_TFrees (TFree v) = + if member (op =) lhs_vars v then I else insert (op =) (TFree v) + | add_new_TFrees _ = I + val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs [] + in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; + (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested prefix for the Skolem constant. Result is a new theory*) fun declare_skofuns s th thy = @@ -97,18 +88,26 @@ fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = (*Existential: declare a Skolem function, then insert into body and continue*) let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref)) - val args = term_frees xtp (*get the formal parameter list*) - val Ts = map type_of args - val cT = Ts ---> T + val args0 = term_frees xtp (*get the formal parameter list*) + val Ts = map type_of args0 + val extraTs = rhs_extra_types (Ts ---> T) xtp + val _ = if null extraTs then () else + warning ("Skolemization: extra type vars: " ^ + commas_quote (map (Sign.string_of_typ thy) extraTs)); + val argsx = map (fn T => Free(gensym"vsk", T)) extraTs + val args = argsx @ args0 + val cT = extraTs ---> Ts ---> T val c = Const (Sign.full_name thy cname, cT) val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) (*Forms a lambda-abstraction over the formal parameters*) + val _ = Output.debug (fn () => "declaring the constant " ^ cname) val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy (*Theory is augmented with the constant, then its def*) val cdef = cname ^ "_def" val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' + handle ERROR _ => raise Clausify_failure thy' in dec_sko (subst_bound (list_comb(c,args), p)) - (thy'', get_axiom thy'' cdef :: axs) + (thy'', get_axiom thy'' cdef :: axs) end | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx = (*Universal quant: insert a free variable into body and continue*) @@ -280,6 +279,7 @@ val cdef = cname ^ "_def" val thy = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy + handle ERROR _ => raise Clausify_failure thy val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef)); val ax = get_axiom thy cdef |> freeze_thm |> mk_object_eq |> strip_lambdas (length args) @@ -402,6 +402,17 @@ |> Thm.varifyT end; + +(*This will refer to the final version of theory ATP_Linkup.*) +val atp_linkup_thy_ref = Theory.check_thy @{theory} + +(*Transfer a theorem into theory ATP_Linkup.thy if it is not already + inside that theory -- because it's needed for Skolemization. + If called while ATP_Linkup is being created, it will transfer to the + current version. If called afterward, it will transfer to the final version.*) +fun transfer_to_ATP_Linkup th = + transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th; + (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) fun to_nnf th = th |> transfer_to_ATP_Linkup @@ -423,26 +434,21 @@ |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") (*Replace lambdas by assumed function definitions in the theorems*) -fun assume_abstract_list s ths = - if abstract_lambdas then List.concat (map (assume_abstract s) ths) - else map Drule.eta_contraction_rule ths; +fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths); (*Replace lambdas by declared function definitions in the theorems*) -fun declare_abstract' s (thy, []) = (thy, []) - | declare_abstract' s (thy, th::ths) = +fun declare_abstract s (thy, []) = (thy, []) + | declare_abstract s (thy, th::ths) = let val (thy', th_defs) = if lambda_free (prop_of th) then (thy, [th]) else th |> zero_var_indexes |> freeze_thm |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s + handle Clausify_failure thy_e => (thy_e,[]) val _ = assert_lambda_free th_defs "declare_abstract: lambdas" - val (thy'', ths') = declare_abstract' s (thy', ths) + val (thy'', ths') = declare_abstract (s^"'") (thy', ths) in (thy'', th_defs @ ths') end; -fun declare_abstract s (thy, ths) = - if abstract_lambdas then declare_abstract' s (thy, ths) - else (thy, map Drule.eta_contraction_rule ths); - (*Keep the full complexity of the original name*) fun flatten_name s = space_implode "_X" (NameSpace.explode s); @@ -450,6 +456,10 @@ if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th) else gensym "unknown_thm_"; +fun name_or_string th = + if PureThy.has_name_hint th then PureThy.get_name_hint th + else string_of_thm th; + (*Skolemize a named theorem, with Skolem functions as additional premises.*) fun skolem_thm th = let val nnfth = to_nnf th and s = fake_name th @@ -461,62 +471,51 @@ It returns a modified theory, unless skolemization fails.*) fun skolem thy th = Option.map - (fn (nnfth, s) => - let val _ = Output.debug (fn () => "skolemizing " ^ s ^ ": ") + (fn nnfth => + let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ") + val _ = Output.debug (fn () => string_of_thm nnfth) + val s = fake_name th val (thy',defs) = declare_skofuns s nnfth thy val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth + val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") val (thy'',cnfs') = declare_abstract s (thy',cnfs) - in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') - end) - (SOME (to_nnf th, fake_name th) handle THM _ => NONE); + in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end + handle Clausify_failure thy_e => ([],thy_e) + ) + (try to_nnf th); +(*The cache prevents repeated clausification of a theorem, and also repeated declaration of + Skolem functions.*) structure ThmCache = TheoryDataFun ( - type T = (thm list) Thmtab.table ref; - val empty : T = ref Thmtab.empty; - fun copy (ref tab) : T = ref tab; + type T = (thm list) Thmtab.table; + val empty = Thmtab.empty; + fun copy tab : T = tab; val extend = copy; - fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2)); + fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2); ); -(*The cache prevents repeated clausification of a theorem, and also repeated declaration of - Skolem functions. The global one holds theorems proved prior to this point. Theory data - holds the remaining ones.*) -val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table); - (*Populate the clause cache using the supplied theorem. Return the clausal form and modified theory.*) -fun skolem_cache_thm clause_cache th thy = - case Thmtab.lookup (!clause_cache) th of +fun skolem_cache_thm th thy = + case Thmtab.lookup (ThmCache.get thy) th of NONE => (case skolem thy (Thm.transfer thy th) of NONE => ([th],thy) | SOME (cls,thy') => - (if null cls - then warning ("skolem_cache: empty clause set for " ^ string_of_thm th) - else (); - change clause_cache (Thmtab.update (th, cls)); - (cls,thy'))) + (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ + " clauses inserted into cache: " ^ name_or_string th); + (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy'))) | SOME cls => (cls,thy); (*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom th = - let val cache = ThmCache.get (Thm.theory_of_thm th) - handle ERROR _ => global_clause_cache - val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th + let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th) in - case in_cache of - NONE => - (case Thmtab.lookup (!global_clause_cache) th of - NONE => - let val cls = map Goal.close_result (skolem_thm th) - in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^ - (if PureThy.has_name_hint th then PureThy.get_name_hint th - else string_of_thm th)); - change cache (Thmtab.update (th, cls)); cls - end - | SOME cls => cls) - | SOME cls => cls + case Thmtab.lookup (ThmCache.get thy) th of + NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th); + map Goal.close_result (skolem_thm th)) + | SOME cls => cls end; fun pairname th = (PureThy.get_name_hint th, th); @@ -572,14 +571,23 @@ (*Setup function: takes a theory and installs ALL known theorems into the clause cache*) -fun skolem_cache clause_cache th thy = #2 (skolem_cache_thm clause_cache th thy); +val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)]; + +fun skolem_cache th thy = #2 (skolem_cache_thm th thy); + +fun skolem_cache_all thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy; + +fun skolem_cache_new thy = fold skolem_cache (map #2 (PureThy.thms_of thy)) thy; (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are lambda_free, but then the individual theory caches become much bigger.*) -fun clause_cache_setup thy = - fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy; - +(*The new constant is a hack to prevent multiple execution*) +fun clause_cache_endtheory thy = + let val _ = Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy) + in + Option.map skolem_cache_new (try mark_skolemized thy) + end; (*** meson proof methods ***) @@ -672,7 +680,7 @@ | conj_rule ths = foldr1 conj2_rule ths; fun skolem_attr (Context.Theory thy, th) = - let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy + let val (cls, thy') = skolem_cache_thm th thy in (Context.Theory thy', conj_rule cls) end | skolem_attr (context, th) = (context, th) @@ -684,6 +692,6 @@ [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), "conversion of goal to conjecture clauses")]; -val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods; +val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods; end; diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/W0/W0.thy --- a/src/HOL/W0/W0.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/W0/W0.thy Thu Sep 27 17:55:28 2007 +0200 @@ -208,11 +208,8 @@ addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *}) -- {* @{text \} *} apply (unfold free_tv_subst cod_def dom_def) - apply (tactic "safe_tac set_cs") - apply (cut_tac m = m and n = n in less_linear) - apply (tactic "fast_tac (HOL_cs addSIs [@{thm less_or_eq_imp_le}]) 1") - apply (cut_tac m = ma and n = n in less_linear) - apply (fast intro!: less_or_eq_imp_le) + apply safe + apply (metis linorder_not_less)+ done lemma new_tv_list: "new_tv n x = (\y \ set x. new_tv n y)" diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/ex/Primrec.thy --- a/src/HOL/ex/Primrec.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/ex/Primrec.thy Thu Sep 27 17:55:28 2007 +0200 @@ -219,7 +219,7 @@ text {* PROPERTY A 11 *} lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (4 + (i1 + i2), j)" - apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans) + apply (rule less_trans [of _ "ack (Suc (Suc 0), ack (i1 + i2, j))" _]) prefer 2 apply (rule ack_nest_bound [THEN less_le_trans]) apply (simp add: Suc3_eq_add_3) @@ -235,11 +235,10 @@ "\k'. \i j. ..."} *} lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (4 + k, j)" - apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans) - prefer 2 + apply (rule less_trans [of _ "ack (k, j) + ack (0, j)" _]) + apply (blast intro: add_less_mono less_ack2) apply (rule ack_add_bound [THEN less_le_trans]) apply simp - apply (rule add_less_mono less_ack2 | assumption)+ done @@ -333,7 +332,7 @@ lemma ack_not_PRIMREC: "\ PRIMREC (\l. case l of [] => 0 | x # l' => ack (x, x))" apply (rule notI) apply (erule ack_bounds_PRIMREC [THEN exE]) - apply (rule less_irrefl) + apply (rule Nat.less_irrefl) apply (drule_tac x = "[x]" in spec) apply simp done