# HG changeset patch # User wenzelm # Date 1223992896 -7200 # Node ID 824f8390aaa2b03895d281c5446b33d48102b827 # Parent 790d1863be2863130fc6fbcc0eb81de70e28fe89 renamed AtpThread to AtpWrapper; diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/ATP_Linkup.thy Tue Oct 14 16:01:36 2008 +0200 @@ -17,7 +17,7 @@ ("Tools/res_reconstruct.ML") ("Tools/res_atp.ML") ("Tools/atp_manager.ML") - ("Tools/atp_thread.ML") + ("Tools/atp_wrapper.ML") "~~/src/Tools/Metis/metis.ML" ("Tools/metis_tools.ML") begin @@ -97,25 +97,25 @@ use "Tools/res_atp.ML" use "Tools/atp_manager.ML" -use "Tools/atp_thread.ML" +use "Tools/atp_wrapper.ML" text {* basic provers *} -setup {* AtpManager.add_prover "spass" AtpThread.spass *} -setup {* AtpManager.add_prover "vampire" AtpThread.vampire *} -setup {* AtpManager.add_prover "e" AtpThread.eprover *} +setup {* AtpManager.add_prover "spass" AtpWrapper.spass *} +setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *} +setup {* AtpManager.add_prover "e" AtpWrapper.eprover *} text {* provers with stuctured output *} -setup {* AtpManager.add_prover "vampire_full" AtpThread.vampire_full *} -setup {* AtpManager.add_prover "e_full" AtpThread.eprover_full *} +setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *} +setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *} text {* on some problems better results *} -setup {* AtpManager.add_prover "spass_no_tc" (AtpThread.spass_filter_opts 40 false) *} +setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_filter_opts 40 false) *} text {* remote provers via SystemOnTPTP *} setup {* AtpManager.add_prover "remote_vamp9" - (AtpThread.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *} + (AtpWrapper.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *} setup {* AtpManager.add_prover "remote_vamp10" - (AtpThread.remote_prover "Vampire---10.0" "drakosha.pl 60") *} + (AtpWrapper.remote_prover "Vampire---10.0" "drakosha.pl 60") *} subsection {* The Metis prover *} diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/IsaMakefile Tue Oct 14 16:01:36 2008 +0200 @@ -217,7 +217,7 @@ Tools/Groebner_Basis/normalizer_data.ML \ Tools/Groebner_Basis/normalizer.ML \ Tools/atp_manager.ML \ - Tools/atp_thread.ML \ + Tools/atp_wrapper.ML \ Tools/meson.ML \ Tools/metis_tools.ML \ Tools/numeral.ML \ diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/Abstraction.thy --- a/src/HOL/MetisExamples/Abstraction.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/MetisExamples/Abstraction.thy Tue Oct 14 16:01:36 2008 +0200 @@ -22,7 +22,7 @@ pset :: "'a set => 'a set" order :: "'a set => ('a * 'a) set" -ML{*AtpThread.problem_name := "Abstraction__Collect_triv"*} +ML{*AtpWrapper.problem_name := "Abstraction__Collect_triv"*} lemma (*Collect_triv:*) "a \ {x. P x} ==> P a" proof (neg_clausify) assume 0: "(a\'a\type) \ Collect (P\'a\type \ bool)" @@ -37,12 +37,12 @@ by (metis mem_Collect_eq) -ML{*AtpThread.problem_name := "Abstraction__Collect_mp"*} +ML{*AtpWrapper.problem_name := "Abstraction__Collect_mp"*} lemma "a \ {x. P x --> Q x} ==> a \ {x. P x} ==> a \ {x. Q x}" by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq); --{*34 secs*} -ML{*AtpThread.problem_name := "Abstraction__Sigma_triv"*} +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_triv"*} lemma "(a,b) \ Sigma A B ==> a \ A & b \ B a" proof (neg_clausify) assume 0: "(a\'a\type, b\'b\type) \ Sigma (A\'a\type set) (B\'a\type \ 'b\type set)" @@ -60,7 +60,7 @@ lemma Sigma_triv: "(a,b) \ Sigma A B ==> a \ A & b \ B a" by (metis SigmaD1 SigmaD2) -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect"*} +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect"*} lemma "(a,b) \ (SIGMA x: A. {y. x = f y}) ==> a \ A & a = f b" (*???metis cannot prove this by (metis CollectD SigmaD1 SigmaD2 UN_eq) @@ -112,7 +112,7 @@ qed -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_in_pp"*} +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_in_pp"*} lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL.{f. f \ pset cl}) ==> f \ pset cl" by (metis Collect_mem_eq SigmaD2) @@ -131,7 +131,7 @@ by (metis 5 0) qed -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect_Pi"*} +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect_Pi"*} lemma "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> f \ pset cl \ pset cl" @@ -147,7 +147,7 @@ qed -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect_Int"*} +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect_Int"*} lemma "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" @@ -170,13 +170,13 @@ qed -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*} +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*} lemma "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl & monotone f (pset cl) (order cl)}) ==> (f \ pset cl \ pset cl) & (monotone f (pset cl) (order cl))" by auto -ML{*AtpThread.problem_name := "Abstraction__CLF_subset_Collect_Int"*} +ML{*AtpWrapper.problem_name := "Abstraction__CLF_subset_Collect_Int"*} lemma "(cl,f) \ CLF ==> CLF \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" @@ -187,7 +187,7 @@ --{*@{text Int_def} is redundant*} *) -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_Collect_Int"*} +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_Collect_Int"*} lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" @@ -196,7 +196,7 @@ by (metis Collect_mem_eq Int_commute SigmaD2) *) -ML{*AtpThread.problem_name := "Abstraction__CLF_subset_Collect_Pi"*} +ML{*AtpWrapper.problem_name := "Abstraction__CLF_subset_Collect_Pi"*} lemma "(cl,f) \ CLF ==> CLF \ (SIGMA cl': CL. {f. f \ pset cl' \ pset cl'}) ==> @@ -206,7 +206,7 @@ by (metis Collect_mem_eq SigmaD2 subsetD) *) -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_Collect_Pi"*} +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_Collect_Pi"*} lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> @@ -216,21 +216,21 @@ by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE) *) -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*} +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*} lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl & monotone f (pset cl) (order cl)}) ==> (f \ pset cl \ pset cl) & (monotone f (pset cl) (order cl))" by auto -ML{*AtpThread.problem_name := "Abstraction__map_eq_zipA"*} +ML{*AtpWrapper.problem_name := "Abstraction__map_eq_zipA"*} lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)" apply (induct xs) (*sledgehammer*) apply auto done -ML{*AtpThread.problem_name := "Abstraction__map_eq_zipB"*} +ML{*AtpWrapper.problem_name := "Abstraction__map_eq_zipB"*} lemma "map (%w. (w -> w, w \ w)) xs = zip (map (%w. w -> w) xs) (map (%w. w \ w) xs)" apply (induct xs) @@ -238,28 +238,28 @@ apply auto done -ML{*AtpThread.problem_name := "Abstraction__image_evenA"*} +ML{*AtpWrapper.problem_name := "Abstraction__image_evenA"*} lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\x. even x --> Suc(f x) \ A)"; (*sledgehammer*) by auto -ML{*AtpThread.problem_name := "Abstraction__image_evenB"*} +ML{*AtpWrapper.problem_name := "Abstraction__image_evenB"*} lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A ==> (\x. even x --> f (f (Suc(f x))) \ A)"; (*sledgehammer*) by auto -ML{*AtpThread.problem_name := "Abstraction__image_curry"*} +ML{*AtpWrapper.problem_name := "Abstraction__image_curry"*} lemma "f \ (%u v. b \ u \ v) ` A ==> \u v. P (b \ u \ v) ==> P(f y)" (*sledgehammer*) by auto -ML{*AtpThread.problem_name := "Abstraction__image_TimesA"*} +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesA"*} lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \ B) = (f`A) \ (g`B)" (*sledgehammer*) apply (rule equalityI) (***Even the two inclusions are far too difficult -ML{*AtpThread.problem_name := "Abstraction__image_TimesA_simpler"*} +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesA_simpler"*} ***) apply (rule subsetI) apply (erule imageE) @@ -282,13 +282,13 @@ (*Given the difficulty of the previous problem, these two are probably impossible*) -ML{*AtpThread.problem_name := "Abstraction__image_TimesB"*} +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesB"*} lemma image_TimesB: "(%(x,y,z). (f x, g y, h z)) ` (A \ B \ C) = (f`A) \ (g`B) \ (h`C)" (*sledgehammer*) by force -ML{*AtpThread.problem_name := "Abstraction__image_TimesC"*} +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesC"*} lemma image_TimesC: "(%(x,y). (x \ x, y \ y)) ` (A \ B) = ((%x. x \ x) ` A) \ ((%y. y \ y) ` B)" diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/BT.thy --- a/src/HOL/MetisExamples/BT.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/MetisExamples/BT.thy Tue Oct 14 16:01:36 2008 +0200 @@ -66,21 +66,21 @@ text {* \medskip BT simplification *} -ML {*AtpThread.problem_name := "BT__n_leaves_reflect"*} +ML {*AtpWrapper.problem_name := "BT__n_leaves_reflect"*} lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" apply (induct t) apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1)) apply (metis add_commute n_leaves.simps(2) reflect.simps(2)) done -ML {*AtpThread.problem_name := "BT__n_nodes_reflect"*} +ML {*AtpWrapper.problem_name := "BT__n_nodes_reflect"*} lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" apply (induct t) apply (metis reflect.simps(1)) apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2)) done -ML {*AtpThread.problem_name := "BT__depth_reflect"*} +ML {*AtpWrapper.problem_name := "BT__depth_reflect"*} lemma depth_reflect: "depth (reflect t) = depth t" apply (induct t) apply (metis depth.simps(1) reflect.simps(1)) @@ -91,21 +91,21 @@ The famous relationship between the numbers of leaves and nodes. *} -ML {*AtpThread.problem_name := "BT__n_leaves_nodes"*} +ML {*AtpWrapper.problem_name := "BT__n_leaves_nodes"*} lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" apply (induct t) apply (metis n_leaves.simps(1) n_nodes.simps(1)) apply auto done -ML {*AtpThread.problem_name := "BT__reflect_reflect_ident"*} +ML {*AtpWrapper.problem_name := "BT__reflect_reflect_ident"*} lemma reflect_reflect_ident: "reflect (reflect t) = t" apply (induct t) apply (metis add_right_cancel reflect.simps(1)); apply (metis reflect.simps(2)) done -ML {*AtpThread.problem_name := "BT__bt_map_ident"*} +ML {*AtpWrapper.problem_name := "BT__bt_map_ident"*} lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" apply (rule ext) apply (induct_tac y) @@ -116,7 +116,7 @@ done -ML {*AtpThread.problem_name := "BT__bt_map_appnd"*} +ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*} lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)" apply (induct t) apply (metis appnd.simps(1) bt_map.simps(1)) @@ -124,7 +124,7 @@ done -ML {*AtpThread.problem_name := "BT__bt_map_compose"*} +ML {*AtpWrapper.problem_name := "BT__bt_map_compose"*} lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" apply (induct t) apply (metis bt_map.simps(1)) @@ -134,42 +134,42 @@ done -ML {*AtpThread.problem_name := "BT__bt_map_reflect"*} +ML {*AtpWrapper.problem_name := "BT__bt_map_reflect"*} lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" apply (induct t) apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1)) apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2)) done -ML {*AtpThread.problem_name := "BT__preorder_bt_map"*} +ML {*AtpWrapper.problem_name := "BT__preorder_bt_map"*} lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" apply (induct t) apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) apply simp done -ML {*AtpThread.problem_name := "BT__inorder_bt_map"*} +ML {*AtpWrapper.problem_name := "BT__inorder_bt_map"*} lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" apply (induct t) apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1)) apply simp done -ML {*AtpThread.problem_name := "BT__postorder_bt_map"*} +ML {*AtpWrapper.problem_name := "BT__postorder_bt_map"*} lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" apply (induct t) apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1)) apply simp done -ML {*AtpThread.problem_name := "BT__depth_bt_map"*} +ML {*AtpWrapper.problem_name := "BT__depth_bt_map"*} lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" apply (induct t) apply (metis bt_map.simps(1) depth.simps(1)) apply simp done -ML {*AtpThread.problem_name := "BT__n_leaves_bt_map"*} +ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*} lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" apply (induct t) apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1)) @@ -177,21 +177,21 @@ done -ML {*AtpThread.problem_name := "BT__preorder_reflect"*} +ML {*AtpWrapper.problem_name := "BT__preorder_reflect"*} lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" apply (induct t) apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv) apply (metis Cons_eq_append_conv monoid_append.add_0_left postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident) done -ML {*AtpThread.problem_name := "BT__inorder_reflect"*} +ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*} lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" apply (induct t) apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1)) apply simp done -ML {*AtpThread.problem_name := "BT__postorder_reflect"*} +ML {*AtpWrapper.problem_name := "BT__postorder_reflect"*} lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" apply (induct t) apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1)) @@ -202,7 +202,7 @@ Analogues of the standard properties of the append function for lists. *} -ML {*AtpThread.problem_name := "BT__appnd_assoc"*} +ML {*AtpWrapper.problem_name := "BT__appnd_assoc"*} lemma appnd_assoc [simp]: "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)" apply (induct t1) @@ -210,14 +210,14 @@ apply (metis appnd.simps(2)) done -ML {*AtpThread.problem_name := "BT__appnd_Lf2"*} +ML {*AtpWrapper.problem_name := "BT__appnd_Lf2"*} lemma appnd_Lf2 [simp]: "appnd t Lf = t" apply (induct t) apply (metis appnd.simps(1)) apply (metis appnd.simps(2)) done -ML {*AtpThread.problem_name := "BT__depth_appnd"*} +ML {*AtpWrapper.problem_name := "BT__depth_appnd"*} declare max_add_distrib_left [simp] lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2" apply (induct t1) @@ -225,7 +225,7 @@ apply (simp add: ); done -ML {*AtpThread.problem_name := "BT__n_leaves_appnd"*} +ML {*AtpWrapper.problem_name := "BT__n_leaves_appnd"*} lemma n_leaves_appnd [simp]: "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2" apply (induct t1) @@ -233,7 +233,7 @@ apply (simp add: left_distrib) done -ML {*AtpThread.problem_name := "BT__bt_map_appnd"*} +ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*} lemma (*bt_map_appnd:*) "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)" apply (induct t1) diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/BigO.thy --- a/src/HOL/MetisExamples/BigO.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/MetisExamples/BigO.thy Tue Oct 14 16:01:36 2008 +0200 @@ -18,7 +18,7 @@ bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set" ("(1O'(_'))") "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" -ML_command{*AtpThread.problem_name := "BigO__bigo_pos_const"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_pos_const"*} lemma bigo_pos_const: "(EX (c::'a::ordered_idom). ALL x. (abs (h x)) <= (c * (abs (f x)))) = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" @@ -215,7 +215,7 @@ {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}" by (auto simp add: bigo_def bigo_pos_const) -ML_command{*AtpThread.problem_name := "BigO__bigo_elt_subset"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_elt_subset"*} lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)" apply (auto simp add: bigo_alt_def) apply (rule_tac x = "ca * c" in exI) @@ -233,7 +233,7 @@ done -ML_command{*AtpThread.problem_name := "BigO__bigo_refl"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_refl"*} lemma bigo_refl [intro]: "f : O(f)" apply(auto simp add: bigo_def) proof (neg_clausify) @@ -247,7 +247,7 @@ by (metis 0 2) qed -ML_command{*AtpThread.problem_name := "BigO__bigo_zero"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_zero"*} lemma bigo_zero: "0 : O(g)" apply (auto simp add: bigo_def func_zero) proof (neg_clausify) @@ -337,7 +337,7 @@ apply (auto del: subsetI simp del: bigo_plus_idemp) done -ML_command{*AtpThread.problem_name := "BigO__bigo_plus_eq"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq"*} lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> O(f + g) = O(f) \ O(g)" apply (rule equalityI) @@ -360,13 +360,13 @@ apply (rule abs_triangle_ineq) apply (metis add_nonneg_nonneg) apply (rule add_mono) -ML_command{*AtpThread.problem_name := "BigO__bigo_plus_eq_simpler"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq_simpler"*} (*Found by SPASS; SLOW*) apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right order_trans) apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans) done -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded_alt"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt"*} lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" apply (auto simp add: bigo_def) @@ -426,7 +426,7 @@ text{*So here is the easier (and more natural) problem using transitivity*} -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded_alt_trans"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt_trans"*} lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" apply (auto simp add: bigo_def) (*Version 1: one-shot proof*) @@ -434,7 +434,7 @@ done text{*So here is the easier (and more natural) problem using transitivity*} -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded_alt_trans"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt_trans"*} lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" apply (auto simp add: bigo_def) (*Version 2: single-step proof*) @@ -473,7 +473,7 @@ apply simp done -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded2"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded2"*} lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==> f : lb +o O(g)" apply (rule set_minus_imp_plus) @@ -496,7 +496,7 @@ by (metis 4 2 0) qed -ML_command{*AtpThread.problem_name := "BigO__bigo_abs"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_abs"*} lemma bigo_abs: "(%x. abs(f x)) =o O(f)" apply (unfold bigo_def) apply auto @@ -511,7 +511,7 @@ by (metis 0 2) qed -ML_command{*AtpThread.problem_name := "BigO__bigo_abs2"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_abs2"*} lemma bigo_abs2: "f =o O(%x. abs(f x))" apply (unfold bigo_def) apply auto @@ -583,7 +583,7 @@ by (simp add: bigo_abs3 [symmetric]) qed -ML_command{*AtpThread.problem_name := "BigO__bigo_mult"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult"*} lemma bigo_mult [intro]: "O(f)\O(g) <= O(f * g)" apply (rule subsetI) apply (subst bigo_def) @@ -595,7 +595,7 @@ apply(erule_tac x = x in allE)+ apply(subgoal_tac "c * ca * abs(f x * g x) = (c * abs(f x)) * (ca * abs(g x))") -ML_command{*AtpThread.problem_name := "BigO__bigo_mult_simpler"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult_simpler"*} prefer 2 apply (metis mult_assoc mult_left_commute OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute @@ -660,14 +660,14 @@ qed -ML_command{*AtpThread.problem_name := "BigO__bigo_mult2"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult2"*} lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)" apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) (*sledgehammer*); apply (rule_tac x = c in exI) apply clarify apply (drule_tac x = x in spec) -ML_command{*AtpThread.problem_name := "BigO__bigo_mult2_simpler"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult2_simpler"*} (*sledgehammer [no luck]*); apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))") apply (simp add: mult_ac) @@ -675,11 +675,11 @@ apply (rule abs_ge_zero) done -ML_command{*AtpThread.problem_name:="BigO__bigo_mult3"*} +ML_command{*AtpWrapper.problem_name:="BigO__bigo_mult3"*} lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)" by (metis bigo_mult set_times_intro subset_iff) -ML_command{*AtpThread.problem_name:="BigO__bigo_mult4"*} +ML_command{*AtpWrapper.problem_name:="BigO__bigo_mult4"*} lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)" by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib) @@ -713,13 +713,13 @@ qed qed -ML_command{*AtpThread.problem_name := "BigO__bigo_mult6"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult6"*} lemma bigo_mult6: "ALL x. f x ~= 0 ==> O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)" by (metis bigo_mult2 bigo_mult5 order_antisym) (*proof requires relaxing relevance: 2007-01-25*) -ML_command{*AtpThread.problem_name := "BigO__bigo_mult7"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult7"*} declare bigo_mult6 [simp] lemma bigo_mult7: "ALL x. f x ~= 0 ==> O(f * g) <= O(f::'a => ('b::ordered_field)) \ O(g)" @@ -731,7 +731,7 @@ done declare bigo_mult6 [simp del] -ML_command{*AtpThread.problem_name := "BigO__bigo_mult8"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult8"*} declare bigo_mult7[intro!] lemma bigo_mult8: "ALL x. f x ~= 0 ==> O(f * g) = O(f::'a => ('b::ordered_field)) \ O(g)" @@ -782,7 +782,7 @@ qed qed -ML_command{*AtpThread.problem_name:="BigO__bigo_plus_absorb"*} +ML_command{*AtpWrapper.problem_name:="BigO__bigo_plus_absorb"*} lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)" by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff); @@ -809,7 +809,7 @@ lemma bigo_const1: "(%x. c) : O(%x. 1)" by (auto simp add: bigo_def mult_ac) -ML_command{*AtpThread.problem_name:="BigO__bigo_const2"*} +ML_command{*AtpWrapper.problem_name:="BigO__bigo_const2"*} lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)" by (metis bigo_const1 bigo_elt_subset); @@ -832,7 +832,7 @@ apply (rule bigo_const1) done -ML_command{*AtpThread.problem_name := "BigO__bigo_const3"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const3"*} lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" apply (simp add: bigo_def) proof (neg_clausify) @@ -856,7 +856,7 @@ O(%x. c) = O(%x. 1)" by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult1"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult1"*} lemma bigo_const_mult1: "(%x. c * f x) : O(f)" apply (simp add: bigo_def abs_mult) proof (neg_clausify) @@ -872,7 +872,7 @@ lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)" by (rule bigo_elt_subset, rule bigo_const_mult1) -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult3"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult3"*} lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)" apply (simp add: bigo_def) (*sledgehammer [no luck]*); @@ -890,7 +890,7 @@ O(%x. c * f x) = O(f)" by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult5"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult5"*} lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> (%x. c) *o O(f) = O(f)" apply (auto del: subsetI) @@ -910,7 +910,7 @@ done -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult6"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult6"*} lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)" apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times @@ -967,7 +967,7 @@ apply (blast intro: order_trans mult_right_mono abs_ge_self) done -ML_command{*AtpThread.problem_name := "BigO__bigo_setsum1"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum1"*} lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> EX c. ALL x y. abs(f x y) <= c * (h x y) ==> (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)" @@ -984,7 +984,7 @@ (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)" by (rule bigo_setsum1, auto) -ML_command{*AtpThread.problem_name := "BigO__bigo_setsum3"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum3"*} lemma bigo_setsum3: "f =o O(h) ==> (%x. SUM y : A x. (l x y) * f(k x y)) =o O(%x. SUM y : A x. abs(l x y * h(k x y)))" @@ -1015,7 +1015,7 @@ apply (erule set_plus_imp_minus) done -ML_command{*AtpThread.problem_name := "BigO__bigo_setsum5"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum5"*} lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> ALL x. 0 <= h x ==> (%x. SUM y : A x. (l x y) * f(k x y)) =o @@ -1072,7 +1072,7 @@ apply (simp add: func_times) done -ML_command{*AtpThread.problem_name := "BigO__bigo_fix"*} +ML_command{*AtpWrapper.problem_name := "BigO__bigo_fix"*} lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==> f =o O(h)" apply (simp add: bigo_alt_def) @@ -1137,7 +1137,7 @@ apply (erule spec)+ done -ML_command{*AtpThread.problem_name:="BigO__bigo_lesso1"*} +ML_command{*AtpWrapper.problem_name:="BigO__bigo_lesso1"*} lemma bigo_lesso1: "ALL x. f x <= g x ==> f ALL x. 0 <= k x ==> ALL x. k x <= f x ==> k ALL x. 0 <= k x ==> ALL x. g x <= k x ==> f EX C. ALL x. f x <= g x + C * abs(h x)" apply (simp only: lesso_def bigo_alt_def) diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/Message.thy --- a/src/HOL/MetisExamples/Message.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/MetisExamples/Message.thy Tue Oct 14 16:01:36 2008 +0200 @@ -78,7 +78,7 @@ | Body: "Crypt K X \ parts H ==> X \ parts H" -ML{*AtpThread.problem_name := "Message__parts_mono"*} +ML{*AtpWrapper.problem_name := "Message__parts_mono"*} lemma parts_mono: "G \ H ==> parts(G) \ parts(H)" apply auto apply (erule parts.induct) @@ -102,7 +102,7 @@ subsubsection{*Inverse of keys *} -ML{*AtpThread.problem_name := "Message__invKey_eq"*} +ML{*AtpWrapper.problem_name := "Message__invKey_eq"*} lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')" by (metis invKey) @@ -203,7 +203,7 @@ apply (simp only: parts_Un) done -ML{*AtpThread.problem_name := "Message__parts_insert_two"*} +ML{*AtpWrapper.problem_name := "Message__parts_insert_two"*} lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \ parts {Y} \ parts H" by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un) @@ -240,7 +240,7 @@ lemma parts_idem [simp]: "parts (parts H) = parts H" by blast -ML{*AtpThread.problem_name := "Message__parts_subset_iff"*} +ML{*AtpWrapper.problem_name := "Message__parts_subset_iff"*} lemma parts_subset_iff [simp]: "(parts G \ parts H) = (G \ parts H)" apply (rule iffI) apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing) @@ -251,7 +251,7 @@ by (blast dest: parts_mono); -ML{*AtpThread.problem_name := "Message__parts_cut"*} +ML{*AtpWrapper.problem_name := "Message__parts_cut"*} lemma parts_cut: "[|Y\ parts(insert X G); X\ parts H|] ==> Y\ parts(G \ H)" by (metis Un_subset_iff insert_subset parts_increasing parts_trans) @@ -316,7 +316,7 @@ done -ML{*AtpThread.problem_name := "Message__msg_Nonce_supply"*} +ML{*AtpWrapper.problem_name := "Message__msg_Nonce_supply"*} lemma msg_Nonce_supply: "\N. \n. N\n --> Nonce n \ parts {msg}" apply (induct_tac "msg") apply (simp_all add: parts_insert2) @@ -368,7 +368,7 @@ lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard] -ML{*AtpThread.problem_name := "Message__parts_analz"*} +ML{*AtpWrapper.problem_name := "Message__parts_analz"*} lemma parts_analz [simp]: "parts (analz H) = parts H" apply (rule equalityI) apply (metis analz_subset_parts parts_subset_iff) @@ -520,7 +520,7 @@ by (drule analz_mono, blast) -ML{*AtpThread.problem_name := "Message__analz_cut"*} +ML{*AtpWrapper.problem_name := "Message__analz_cut"*} declare analz_trans[intro] lemma analz_cut: "[| Y\ analz (insert X H); X\ analz H |] ==> Y\ analz H" (*TOO SLOW @@ -538,7 +538,7 @@ text{*A congruence rule for "analz" *} -ML{*AtpThread.problem_name := "Message__analz_subset_cong"*} +ML{*AtpWrapper.problem_name := "Message__analz_subset_cong"*} lemma analz_subset_cong: "[| analz G \ analz G'; analz H \ analz H' |] ==> analz (G \ H) \ analz (G' \ H')" @@ -616,7 +616,7 @@ by (intro Un_least synth_mono Un_upper1 Un_upper2) -ML{*AtpThread.problem_name := "Message__synth_insert"*} +ML{*AtpWrapper.problem_name := "Message__synth_insert"*} lemma synth_insert: "insert X (synth H) \ synth(insert X H)" by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono) @@ -638,7 +638,7 @@ lemma synth_trans: "[| X\ synth G; G \ synth H |] ==> X\ synth H" by (drule synth_mono, blast) -ML{*AtpThread.problem_name := "Message__synth_cut"*} +ML{*AtpWrapper.problem_name := "Message__synth_cut"*} lemma synth_cut: "[| Y\ synth (insert X H); X\ synth H |] ==> Y\ synth H" (*TOO SLOW by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono) @@ -670,7 +670,7 @@ subsubsection{*Combinations of parts, analz and synth *} -ML{*AtpThread.problem_name := "Message__parts_synth"*} +ML{*AtpWrapper.problem_name := "Message__parts_synth"*} lemma parts_synth [simp]: "parts (synth H) = parts H \ synth H" apply (rule equalityI) apply (rule subsetI) @@ -685,14 +685,14 @@ -ML{*AtpThread.problem_name := "Message__analz_analz_Un"*} +ML{*AtpWrapper.problem_name := "Message__analz_analz_Un"*} lemma analz_analz_Un [simp]: "analz (analz G \ H) = analz (G \ H)" apply (rule equalityI); apply (metis analz_idem analz_subset_cong order_eq_refl) apply (metis analz_increasing analz_subset_cong order_eq_refl) done -ML{*AtpThread.problem_name := "Message__analz_synth_Un"*} +ML{*AtpWrapper.problem_name := "Message__analz_synth_Un"*} declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro] lemma analz_synth_Un [simp]: "analz (synth G \ H) = analz (G \ H) \ synth G" apply (rule equalityI) @@ -706,7 +706,7 @@ done -ML{*AtpThread.problem_name := "Message__analz_synth"*} +ML{*AtpWrapper.problem_name := "Message__analz_synth"*} lemma analz_synth [simp]: "analz (synth H) = analz H \ synth H" proof (neg_clausify) assume 0: "analz (synth H) \ analz H \ synth H" @@ -729,7 +729,7 @@ subsubsection{*For reasoning about the Fake rule in traces *} -ML{*AtpThread.problem_name := "Message__parts_insert_subset_Un"*} +ML{*AtpWrapper.problem_name := "Message__parts_insert_subset_Un"*} lemma parts_insert_subset_Un: "X\ G ==> parts(insert X H) \ parts G \ parts H" proof (neg_clausify) assume 0: "X \ G" @@ -748,7 +748,7 @@ by (metis 6 0) qed -ML{*AtpThread.problem_name := "Message__Fake_parts_insert"*} +ML{*AtpWrapper.problem_name := "Message__Fake_parts_insert"*} lemma Fake_parts_insert: "X \ synth (analz H) ==> parts (insert X H) \ synth (analz H) \ parts H" @@ -791,14 +791,14 @@ ==> Z \ synth (analz H) \ parts H"; by (blast dest: Fake_parts_insert [THEN subsetD, dest]) -ML{*AtpThread.problem_name := "Message__Fake_analz_insert"*} +ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert"*} declare analz_mono [intro] synth_mono [intro] lemma Fake_analz_insert: "X\ synth (analz G) ==> analz (insert X H) \ synth (analz G) \ analz (G \ H)" by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12)) -ML{*AtpThread.problem_name := "Message__Fake_analz_insert_simpler"*} +ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert_simpler"*} (*simpler problems? BUT METIS CAN'T PROVE lemma Fake_analz_insert_simpler: "X\ synth (analz G) ==> diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/Tarski.thy --- a/src/HOL/MetisExamples/Tarski.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/MetisExamples/Tarski.thy Tue Oct 14 16:01:36 2008 +0200 @@ -416,7 +416,7 @@ (*never proved, 2007-01-22: Tarski__CLF_unnamed_lemma NOT PROVABLE because of the conjunction used in the definition: we don't allow reasoning with rules like conjE, which is essential here.*) -ML_command{*AtpThread.problem_name:="Tarski__CLF_unnamed_lemma"*} +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_unnamed_lemma"*} lemma (in CLF) [simp]: "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" apply (insert f_cl) @@ -433,7 +433,7 @@ by (simp add: A_def r_def) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__CLF_CLF_dual"*} +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_CLF_dual"*} declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp] lemma (in CLF) CLF_dual: "(dual cl, f) \ CLF_set" @@ -461,7 +461,7 @@ subsection {* lemmas for Tarski, lub *} (*never proved, 2007-01-22*) -ML{*AtpThread.problem_name:="Tarski__CLF_lubH_le_flubH"*} +ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_le_flubH"*} declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] lemma (in CLF) lubH_le_flubH: "H = {x. (x, f x) \ r & x \ A} ==> (lub H cl, f (lub H cl)) \ r" @@ -471,7 +471,7 @@ -- {* @{text "\x:H. (x, f (lub H r)) \ r"} *} apply (rule ballI) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__CLF_lubH_le_flubH_simpler"*} +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_le_flubH_simpler"*} apply (rule transE) -- {* instantiates @{text "(x, ?z) \ order cl to (x, f x)"}, *} -- {* because of the def of @{text H} *} @@ -489,7 +489,7 @@ CLF.monotone_f[rule del] CL.lub_upper[rule del] (*never proved, 2007-01-22*) -ML{*AtpThread.problem_name:="Tarski__CLF_flubH_le_lubH"*} +ML{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH"*} declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] CLF.lubH_le_flubH[simp] @@ -499,7 +499,7 @@ apply (rule_tac t = "H" in ssubst, assumption) apply (rule CollectI) apply (rule conjI) -ML_command{*AtpThread.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} (*??no longer terminates, with combinators apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2) *) @@ -513,7 +513,7 @@ (*never proved, 2007-01-22*) -ML{*AtpThread.problem_name:="Tarski__CLF_lubH_is_fixp"*} +ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp"*} (*Single-step version fails. The conjecture clauses refer to local abstraction functions (Frees), which prevents expand_defs_tac from removing those "definitions" at the end of the proof. *) @@ -588,7 +588,7 @@ "H = {x. (x, f x) \ r & x \ A} ==> lub H cl \ fix f A" apply (simp add: fix_def) apply (rule conjI) -ML_command{*AtpThread.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} apply (metis CO_refl lubH_le_flubH reflD1) apply (metis antisymE flubH_le_lubH lubH_le_flubH) done @@ -607,7 +607,7 @@ apply (simp_all add: P_def) done -ML{*AtpThread.problem_name:="Tarski__CLF_lubH_least_fixf"*} +ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_least_fixf"*} lemma (in CLF) lubH_least_fixf: "H = {x. (x, f x) \ r & x \ A} ==> \L. (\y \ fix f A. (y,L) \ r) --> (lub H cl, L) \ r" @@ -615,7 +615,7 @@ done subsection {* Tarski fixpoint theorem 1, first part *} -ML{*AtpThread.problem_name:="Tarski__CLF_T_thm_1_lub"*} +ML{*AtpWrapper.problem_name:="Tarski__CLF_T_thm_1_lub"*} declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp] lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \ r & x \ A} cl" @@ -623,7 +623,7 @@ apply (rule sym) apply (simp add: P_def) apply (rule lubI) -ML_command{*AtpThread.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*} +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*} apply (metis P_def fix_subset) apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) (*??no longer terminates, with combinators @@ -638,7 +638,7 @@ (*never proved, 2007-01-22*) -ML{*AtpThread.problem_name:="Tarski__CLF_glbH_is_fixp"*} +ML{*AtpWrapper.problem_name:="Tarski__CLF_glbH_is_fixp"*} declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp] lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \ r & x \ A} ==> glb H cl \ P" @@ -662,13 +662,13 @@ (*never proved, 2007-01-22*) -ML{*AtpThread.problem_name:="Tarski__T_thm_1_glb"*} (*ALL THEOREMS*) +ML{*AtpWrapper.problem_name:="Tarski__T_thm_1_glb"*} (*ALL THEOREMS*) lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \ r & x \ A} cl" (*sledgehammer;*) apply (simp add: glb_dual_lub P_def A_def r_def) apply (rule dualA_iff [THEN subst]) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__T_thm_1_glb_simpler"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__T_thm_1_glb_simpler"*} (*ALL THEOREMS*) (*sledgehammer;*) apply (simp add: CLF.T_thm_1_lub [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff) @@ -677,13 +677,13 @@ subsection {* interval *} -ML{*AtpThread.problem_name:="Tarski__rel_imp_elem"*} +ML{*AtpWrapper.problem_name:="Tarski__rel_imp_elem"*} declare (in CLF) CO_refl[simp] refl_def [simp] lemma (in CLF) rel_imp_elem: "(x, y) \ r ==> x \ A" by (metis CO_refl reflD1) declare (in CLF) CO_refl[simp del] refl_def [simp del] -ML{*AtpThread.problem_name:="Tarski__interval_subset"*} +ML{*AtpWrapper.problem_name:="Tarski__interval_subset"*} declare (in CLF) rel_imp_elem[intro] declare interval_def [simp] lemma (in CLF) interval_subset: "[| a \ A; b \ A |] ==> interval r a b \ A" @@ -718,7 +718,7 @@ "[| a \ A; b \ A; S \ interval r a b |]==> S \ A" by (simp add: subset_trans [OF _ interval_subset]) -ML{*AtpThread.problem_name:="Tarski__L_in_interval"*} (*ALL THEOREMS*) +ML{*AtpWrapper.problem_name:="Tarski__L_in_interval"*} (*ALL THEOREMS*) lemma (in CLF) L_in_interval: "[| a \ A; b \ A; S \ interval r a b; S \ {}; isLub S cl L; interval r a b \ {} |] ==> L \ interval r a b" @@ -737,7 +737,7 @@ done (*never proved, 2007-01-22*) -ML{*AtpThread.problem_name:="Tarski__G_in_interval"*} (*ALL THEOREMS*) +ML{*AtpWrapper.problem_name:="Tarski__G_in_interval"*} (*ALL THEOREMS*) lemma (in CLF) G_in_interval: "[| a \ A; b \ A; interval r a b \ {}; S \ interval r a b; isGlb S cl G; S \ {} |] ==> G \ interval r a b" @@ -746,7 +746,7 @@ dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub) done -ML{*AtpThread.problem_name:="Tarski__intervalPO"*} (*ALL THEOREMS*) +ML{*AtpWrapper.problem_name:="Tarski__intervalPO"*} (*ALL THEOREMS*) lemma (in CLF) intervalPO: "[| a \ A; b \ A; interval r a b \ {} |] ==> (| pset = interval r a b, order = induced (interval r a b) r |) @@ -819,7 +819,7 @@ lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual] (*never proved, 2007-01-22*) -ML{*AtpThread.problem_name:="Tarski__interval_is_sublattice"*} (*ALL THEOREMS*) +ML{*AtpWrapper.problem_name:="Tarski__interval_is_sublattice"*} (*ALL THEOREMS*) lemma (in CLF) interval_is_sublattice: "[| a \ A; b \ A; interval r a b \ {} |] ==> interval r a b <<= cl" @@ -827,7 +827,7 @@ apply (rule sublatticeI) apply (simp add: interval_subset) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__interval_is_sublattice_simpler"*} +ML_command{*AtpWrapper.problem_name:="Tarski__interval_is_sublattice_simpler"*} (*sledgehammer *) apply (rule CompleteLatticeI) apply (simp add: intervalPO) @@ -846,7 +846,7 @@ lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)" by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) -ML_command{*AtpThread.problem_name:="Tarski__Bot_in_lattice"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_in_lattice"*} (*ALL THEOREMS*) lemma (in CLF) Bot_in_lattice: "Bot cl \ A" (*sledgehammer; *) apply (simp add: Bot_def least_def) @@ -856,12 +856,12 @@ done (*first proved 2007-01-25 after relaxing relevance*) -ML_command{*AtpThread.problem_name:="Tarski__Top_in_lattice"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__Top_in_lattice"*} (*ALL THEOREMS*) lemma (in CLF) Top_in_lattice: "Top cl \ A" (*sledgehammer;*) apply (simp add: Top_dual_Bot A_def) (*first proved 2007-01-25 after relaxing relevance*) -ML_command{*AtpThread.problem_name:="Tarski__Top_in_lattice_simpler"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__Top_in_lattice_simpler"*} (*ALL THEOREMS*) (*sledgehammer*) apply (rule dualA_iff [THEN subst]) apply (blast intro!: CLF.Bot_in_lattice [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] dualPO CL_dualCL CLF_dual) @@ -876,7 +876,7 @@ done (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__Bot_prop"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_prop"*} (*ALL THEOREMS*) lemma (in CLF) Bot_prop: "x \ A ==> (Bot cl, x) \ r" (*sledgehammer*) apply (simp add: Bot_dual_Top r_def) @@ -885,12 +885,12 @@ dualA_iff A_def dualPO CL_dualCL CLF_dual) done -ML_command{*AtpThread.problem_name:="Tarski__Bot_in_lattice"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_in_lattice"*} (*ALL THEOREMS*) lemma (in CLF) Top_intv_not_empty: "x \ A ==> interval r x (Top cl) \ {}" apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE) done -ML_command{*AtpThread.problem_name:="Tarski__Bot_intv_not_empty"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_intv_not_empty"*} (*ALL THEOREMS*) lemma (in CLF) Bot_intv_not_empty: "x \ A ==> interval r (Bot cl) x \ {}" apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem) done @@ -902,7 +902,7 @@ by (simp add: P_def fix_subset po_subset_po) (*first proved 2007-01-25 after relaxing relevance*) -ML_command{*AtpThread.problem_name:="Tarski__Y_subset_A"*} +ML_command{*AtpWrapper.problem_name:="Tarski__Y_subset_A"*} declare (in Tarski) P_def[simp] Y_ss [simp] declare fix_subset [intro] subset_trans [intro] lemma (in Tarski) Y_subset_A: "Y \ A" @@ -918,7 +918,7 @@ by (rule Y_subset_A [THEN lub_in_lattice]) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__lubY_le_flubY"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY"*} (*ALL THEOREMS*) lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \ r" (*sledgehammer*) apply (rule lub_least) @@ -927,12 +927,12 @@ apply (rule lubY_in_A) -- {* @{text "Y \ P ==> f x = x"} *} apply (rule ballI) -ML_command{*AtpThread.problem_name:="Tarski__lubY_le_flubY_simpler"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY_simpler"*} (*ALL THEOREMS*) (*sledgehammer *) apply (rule_tac t = "x" in fix_imp_eq [THEN subst]) apply (erule Y_ss [simplified P_def, THEN subsetD]) -- {* @{text "reduce (f x, f (lub Y cl)) \ r to (x, lub Y cl) \ r"} by monotonicity *} -ML_command{*AtpThread.problem_name:="Tarski__lubY_le_flubY_simplest"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY_simplest"*} (*ALL THEOREMS*) (*sledgehammer*) apply (rule_tac f = "f" in monotoneE) apply (rule monotone_f) @@ -942,7 +942,7 @@ done (*first proved 2007-01-25 after relaxing relevance*) -ML_command{*AtpThread.problem_name:="Tarski__intY1_subset"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_subset"*} (*ALL THEOREMS*) lemma (in Tarski) intY1_subset: "intY1 \ A" (*sledgehammer*) apply (unfold intY1_def) @@ -954,7 +954,7 @@ lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD] (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__intY1_f_closed"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_f_closed"*} (*ALL THEOREMS*) lemma (in Tarski) intY1_f_closed: "x \ intY1 \ f x \ intY1" (*sledgehammer*) apply (simp add: intY1_def interval_def) @@ -962,7 +962,7 @@ apply (rule transE) apply (rule lubY_le_flubY) -- {* @{text "(f (lub Y cl), f x) \ r"} *} -ML_command{*AtpThread.problem_name:="Tarski__intY1_f_closed_simpler"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_f_closed_simpler"*} (*ALL THEOREMS*) (*sledgehammer [has been proved before now...]*) apply (rule_tac f=f in monotoneE) apply (rule monotone_f) @@ -975,13 +975,13 @@ apply (simp add: intY1_def interval_def intY1_elem) done -ML_command{*AtpThread.problem_name:="Tarski__intY1_func"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_func"*} (*ALL THEOREMS*) lemma (in Tarski) intY1_func: "(%x: intY1. f x) \ intY1 -> intY1" apply (rule restrict_in_funcset) apply (metis intY1_f_closed restrict_in_funcset) done -ML_command{*AtpThread.problem_name:="Tarski__intY1_mono"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_mono"*} (*ALL THEOREMS*) lemma (in Tarski) intY1_mono: "monotone (%x: intY1. f x) intY1 (induced intY1 r)" (*sledgehammer *) @@ -990,7 +990,7 @@ done (*proof requires relaxing relevance: 2007-01-25*) -ML_command{*AtpThread.problem_name:="Tarski__intY1_is_cl"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_is_cl"*} (*ALL THEOREMS*) lemma (in Tarski) intY1_is_cl: "(| pset = intY1, order = induced intY1 r |) \ CompleteLattice" (*sledgehammer*) @@ -1003,7 +1003,7 @@ done (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__v_in_P"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__v_in_P"*} (*ALL THEOREMS*) lemma (in Tarski) v_in_P: "v \ P" (*sledgehammer*) apply (unfold P_def) @@ -1013,7 +1013,7 @@ v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono) done -ML_command{*AtpThread.problem_name:="Tarski__z_in_interval"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__z_in_interval"*} (*ALL THEOREMS*) lemma (in Tarski) z_in_interval: "[| z \ P; \y\Y. (y, z) \ induced P r |] ==> z \ intY1" (*sledgehammer *) @@ -1027,14 +1027,14 @@ apply (simp add: induced_def) done -ML_command{*AtpThread.problem_name:="Tarski__fz_in_int_rel"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__fz_in_int_rel"*} (*ALL THEOREMS*) lemma (in Tarski) f'z_in_int_rel: "[| z \ P; \y\Y. (y, z) \ induced P r |] ==> ((%x: intY1. f x) z, z) \ induced intY1 r" apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval) done (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__tarski_full_lemma"*} (*ALL THEOREMS*) +ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma"*} (*ALL THEOREMS*) lemma (in Tarski) tarski_full_lemma: "\L. isLub Y (| pset = P, order = induced P r |) L" apply (rule_tac x = "v" in exI) @@ -1064,12 +1064,12 @@ prefer 2 apply (simp add: v_in_P) apply (unfold v_def) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__tarski_full_lemma_simpler"*} +ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma_simpler"*} (*sledgehammer*) apply (rule indE) apply (rule_tac [2] intY1_subset) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__tarski_full_lemma_simplest"*} +ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma_simplest"*} (*sledgehammer*) apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) apply (simp add: CL_imp_PO intY1_is_cl) @@ -1087,7 +1087,7 @@ (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__Tarski_full"*} +ML_command{*AtpWrapper.problem_name:="Tarski__Tarski_full"*} declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp] Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro] CompleteLatticeI_simp [intro] @@ -1097,7 +1097,7 @@ apply (rule CompleteLatticeI_simp) apply (rule fixf_po, clarify) (*never proved, 2007-01-22*) -ML_command{*AtpThread.problem_name:="Tarski__Tarski_full_simpler"*} +ML_command{*AtpWrapper.problem_name:="Tarski__Tarski_full_simpler"*} (*sledgehammer*) apply (simp add: P_def A_def r_def) apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro, diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/TransClosure.thy --- a/src/HOL/MetisExamples/TransClosure.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/MetisExamples/TransClosure.thy Tue Oct 14 16:01:36 2008 +0200 @@ -22,7 +22,7 @@ consts f:: "addr \ val" -ML {*AtpThread.problem_name := "TransClosure__test"*} +ML {*AtpWrapper.problem_name := "TransClosure__test"*} lemma "\ f c = Intg x; \ y. f b = Intg y \ y \ x; (a,b) \ R\<^sup>*; (b,c) \ R\<^sup>* \ \ \ c. (b,c) \ R \ (a,c) \ R\<^sup>*" by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl) @@ -51,7 +51,7 @@ by (metis 10 3) qed -ML {*AtpThread.problem_name := "TransClosure__test_simpler"*} +ML {*AtpWrapper.problem_name := "TransClosure__test_simpler"*} lemma "\ f c = Intg x; \ y. f b = Intg y \ y \ x; (a,b) \ R\<^sup>*; (b,c) \ R\<^sup>* \ \ \ c. (b,c) \ R \ (a,c) \ R\<^sup>*" apply (erule_tac x="b" in converse_rtranclE) diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/set.thy --- a/src/HOL/MetisExamples/set.thy Tue Oct 14 15:45:46 2008 +0200 +++ b/src/HOL/MetisExamples/set.thy Tue Oct 14 16:01:36 2008 +0200 @@ -198,7 +198,7 @@ by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq) qed -ML {*AtpThread.problem_name := "set__equal_union"*} +ML {*AtpWrapper.problem_name := "set__equal_union"*} lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -206,12 +206,12 @@ by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) -ML {*AtpThread.problem_name := "set__equal_inter"*} +ML {*AtpWrapper.problem_name := "set__equal_inter"*} lemma "(X = Y \ Z) = (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))" by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset) -ML {*AtpThread.problem_name := "set__fixedpoint"*} +ML {*AtpWrapper.problem_name := "set__fixedpoint"*} lemma fixedpoint: "\!x. f (g x) = x \ \!y. g (f y) = y" by metis @@ -230,7 +230,7 @@ by (metis 4 0) qed -ML {*AtpThread.problem_name := "set__singleton_example"*} +ML {*AtpWrapper.problem_name := "set__singleton_example"*} lemma (*singleton_example_2:*) "\x \ S. \S \ x \ \z. S \ {z}" by (metis Set.subsetI Union_upper insertCI set_eq_subset) @@ -260,7 +260,7 @@ 293-314. *} -ML {*AtpThread.problem_name := "set__Bledsoe_Fung"*} +ML {*AtpWrapper.problem_name := "set__Bledsoe_Fung"*} (*Notes: 1, the numbering doesn't completely agree with the paper. 2, we must rename set variables to avoid type clashes.*) lemma "\B. (\x \ B. x \ (0::int))" diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/Tools/atp_thread.ML --- a/src/HOL/Tools/atp_thread.ML Tue Oct 14 15:45:46 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,150 +0,0 @@ -(* Title: HOL/Tools/atp_thread.ML - ID: $Id$ - Author: Fabian Immler, TU Muenchen - -Automatic provers as managed threads. -*) - -signature ATP_THREAD = -sig - (* hooks for writing problemfiles *) - val destdir: string ref - val problem_name: string ref - (* basic template *) - val external_prover: - ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) -> - Path.T * string -> - (string * int -> bool) -> - (string * string vector * Proof.context * thm * int -> string) -> - int -> Proof.state -> Thread.thread - (* provers as functions returning threads *) - val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread - val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread - val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread - val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread - val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread - val remote_prover: string -> string -> int -> Proof.state -> Thread.thread - val full_prover: Path.T * string -> int -> Proof.state -> Thread.thread - val spass_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread - val eprover_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread - val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread - val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread - val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread - val spass: int -> Proof.state -> Thread.thread - val eprover: int -> Proof.state -> Thread.thread - val eprover_full: int -> Proof.state -> Thread.thread - val vampire: int -> Proof.state -> Thread.thread - val vampire_full: int -> Proof.state -> Thread.thread -end; - -structure AtpThread : ATP_THREAD = -struct - - (* preferences for path and filename to problemfiles *) - val destdir = ref ""; (*Empty means write files to /tmp*) - val problem_name = ref "prob"; - - (*Setting up a Thread for an external prover*) - fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state = - let - val destdir' = ! destdir - val problem_name' = ! problem_name - val (ctxt, (chain_ths, goal)) = Proof.get_goal state - (* path to unique problem file *) - fun prob_pathname nr = - let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr) - in if destdir' = "" then File.tmp_path probfile - else if File.exists (Path.explode (destdir')) - then Path.append (Path.explode (destdir')) probfile - else error ("No such directory: " ^ destdir') - end - (* write out problem file and call prover *) - fun call_prover () = - let - val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths - val (filenames, thm_names_list) = - write_problem_files prob_pathname (ctxt, chain_ths, goal) - val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*) - - val cmdline = - if File.exists cmd then File.shell_path cmd ^ " " ^ args - else error ("Bad executable: " ^ Path.implode cmd); - val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1)) - val _ = - if rc <> 0 - then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc) - else () - (* remove *temporary* files *) - val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else () - in - if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno) - else NONE - end - in - AtpManager.atp_thread call_prover produce_answer - end; - - - (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*) - - fun tptp_prover_filter_opts_full max_new theory_const full command sg = - external_prover - (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const) - command - ResReconstruct.check_success_e_vamp_spass - (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) - sg - - (* arbitrary atp with tptp input/output and problemfile as last argument*) - fun tptp_prover_filter_opts max_new theory_const = - tptp_prover_filter_opts_full max_new theory_const false; - (* default settings*) - val tptp_prover = tptp_prover_filter_opts 60 true; - - (* for structured proofs: prover must support TSTP *) - fun full_prover_filter_opts max_new theory_const = - tptp_prover_filter_opts_full max_new theory_const true; - (* default settings*) - val full_prover = full_prover_filter_opts 60 true; - - fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts - max_new theory_const - (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*) - (* default settings*) - val vampire = vampire_filter_opts 60 false; - - (* a vampire for full proof output *) - fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts - max_new theory_const - (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*) - (* default settings*) - val vampire_full = vampire_filter_opts 60 false; - - fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts - max_new theory_const - (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent") - (* default settings *) - val eprover = eprover_filter_opts 100 false; - - (* an E for full proof output*) - fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts - max_new theory_const - (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent") - (* default settings *) - val eprover_full = eprover_filter_opts_full 100 false; - - fun spass_filter_opts max_new theory_const = external_prover - (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const) - (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof") - ResReconstruct.check_success_e_vamp_spass - ResReconstruct.lemma_list_dfg - (* default settings*) - val spass = spass_filter_opts 40 true; - - (* remote prover invocation via SystemOnTPTP *) - fun remote_prover_filter_opts max_new theory_const name command = - tptp_prover_filter_opts max_new theory_const - (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command) - val remote_prover = remote_prover_filter_opts 60 false - -end; diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/Tools/atp_wrapper.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/atp_wrapper.ML Tue Oct 14 16:01:36 2008 +0200 @@ -0,0 +1,150 @@ +(* Title: HOL/Tools/atp_wrapper.ML + ID: $Id$ + Author: Fabian Immler, TU Muenchen + +Wrapper functions for external ATPs. +*) + +signature ATP_WRAPPER = +sig + (* hooks for writing problemfiles *) + val destdir: string ref + val problem_name: string ref + (* basic template *) + val external_prover: + ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) -> + Path.T * string -> + (string * int -> bool) -> + (string * string vector * Proof.context * thm * int -> string) -> + int -> Proof.state -> Thread.thread + (* provers as functions returning threads *) + val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread + val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread + val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread + val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread + val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread + val remote_prover: string -> string -> int -> Proof.state -> Thread.thread + val full_prover: Path.T * string -> int -> Proof.state -> Thread.thread + val spass_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread + val eprover_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread + val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread + val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread + val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread + val spass: int -> Proof.state -> Thread.thread + val eprover: int -> Proof.state -> Thread.thread + val eprover_full: int -> Proof.state -> Thread.thread + val vampire: int -> Proof.state -> Thread.thread + val vampire_full: int -> Proof.state -> Thread.thread +end; + +structure AtpWrapper: ATP_WRAPPER = +struct + + (* preferences for path and filename to problemfiles *) + val destdir = ref ""; (*Empty means write files to /tmp*) + val problem_name = ref "prob"; + + (*Setting up a Thread for an external prover*) + fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state = + let + val destdir' = ! destdir + val problem_name' = ! problem_name + val (ctxt, (chain_ths, goal)) = Proof.get_goal state + (* path to unique problem file *) + fun prob_pathname nr = + let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr) + in if destdir' = "" then File.tmp_path probfile + else if File.exists (Path.explode (destdir')) + then Path.append (Path.explode (destdir')) probfile + else error ("No such directory: " ^ destdir') + end + (* write out problem file and call prover *) + fun call_prover () = + let + val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths + val (filenames, thm_names_list) = + write_problem_files prob_pathname (ctxt, chain_ths, goal) + val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*) + + val cmdline = + if File.exists cmd then File.shell_path cmd ^ " " ^ args + else error ("Bad executable: " ^ Path.implode cmd); + val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1)) + val _ = + if rc <> 0 + then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc) + else () + (* remove *temporary* files *) + val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else () + in + if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno) + else NONE + end + in + AtpManager.atp_thread call_prover produce_answer + end; + + + (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*) + + fun tptp_prover_filter_opts_full max_new theory_const full command sg = + external_prover + (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const) + command + ResReconstruct.check_success_e_vamp_spass + (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) + sg + + (* arbitrary atp with tptp input/output and problemfile as last argument*) + fun tptp_prover_filter_opts max_new theory_const = + tptp_prover_filter_opts_full max_new theory_const false; + (* default settings*) + val tptp_prover = tptp_prover_filter_opts 60 true; + + (* for structured proofs: prover must support TSTP *) + fun full_prover_filter_opts max_new theory_const = + tptp_prover_filter_opts_full max_new theory_const true; + (* default settings*) + val full_prover = full_prover_filter_opts 60 true; + + fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts + max_new theory_const + (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*) + (* default settings*) + val vampire = vampire_filter_opts 60 false; + + (* a vampire for full proof output *) + fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts + max_new theory_const + (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*) + (* default settings*) + val vampire_full = vampire_filter_opts 60 false; + + fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts + max_new theory_const + (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent") + (* default settings *) + val eprover = eprover_filter_opts 100 false; + + (* an E for full proof output*) + fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts + max_new theory_const + (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent") + (* default settings *) + val eprover_full = eprover_filter_opts_full 100 false; + + fun spass_filter_opts max_new theory_const = external_prover + (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const) + (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof") + ResReconstruct.check_success_e_vamp_spass + ResReconstruct.lemma_list_dfg + (* default settings*) + val spass = spass_filter_opts 40 true; + + (* remote prover invocation via SystemOnTPTP *) + fun remote_prover_filter_opts max_new theory_const name command = + tptp_prover_filter_opts max_new theory_const + (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command) + val remote_prover = remote_prover_filter_opts 60 false + +end;