renamed AtpThread to AtpWrapper;
authorwenzelm
Tue Oct 14 16:01:36 2008 +0200 (2008-10-14)
changeset 28592824f8390aaa2
parent 28591 790d1863be28
child 28593 f087237af65d
renamed AtpThread to AtpWrapper;
src/HOL/ATP_Linkup.thy
src/HOL/IsaMakefile
src/HOL/MetisExamples/Abstraction.thy
src/HOL/MetisExamples/BT.thy
src/HOL/MetisExamples/BigO.thy
src/HOL/MetisExamples/Message.thy
src/HOL/MetisExamples/Tarski.thy
src/HOL/MetisExamples/TransClosure.thy
src/HOL/MetisExamples/set.thy
src/HOL/Tools/atp_thread.ML
src/HOL/Tools/atp_wrapper.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Tue Oct 14 15:45:46 2008 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Tue Oct 14 16:01:36 2008 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    ("Tools/res_reconstruct.ML")
     1.5    ("Tools/res_atp.ML")
     1.6    ("Tools/atp_manager.ML")
     1.7 -  ("Tools/atp_thread.ML")
     1.8 +  ("Tools/atp_wrapper.ML")
     1.9    "~~/src/Tools/Metis/metis.ML"
    1.10    ("Tools/metis_tools.ML")
    1.11  begin
    1.12 @@ -97,25 +97,25 @@
    1.13  use "Tools/res_atp.ML"
    1.14  
    1.15  use "Tools/atp_manager.ML"
    1.16 -use "Tools/atp_thread.ML"
    1.17 +use "Tools/atp_wrapper.ML"
    1.18  
    1.19  text {* basic provers *}
    1.20 -setup {* AtpManager.add_prover "spass" AtpThread.spass *}
    1.21 -setup {* AtpManager.add_prover "vampire" AtpThread.vampire *}
    1.22 -setup {* AtpManager.add_prover "e" AtpThread.eprover *}
    1.23 +setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}
    1.24 +setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *}
    1.25 +setup {* AtpManager.add_prover "e" AtpWrapper.eprover *}
    1.26  
    1.27  text {* provers with stuctured output *}
    1.28 -setup {* AtpManager.add_prover "vampire_full" AtpThread.vampire_full *}
    1.29 -setup {* AtpManager.add_prover "e_full" AtpThread.eprover_full *}
    1.30 +setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *}
    1.31 +setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *}
    1.32  
    1.33  text {* on some problems better results *}
    1.34 -setup {* AtpManager.add_prover "spass_no_tc" (AtpThread.spass_filter_opts 40 false) *}
    1.35 +setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_filter_opts 40 false) *}
    1.36  
    1.37  text {* remote provers via SystemOnTPTP *}
    1.38  setup {* AtpManager.add_prover "remote_vamp9"
    1.39 -  (AtpThread.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
    1.40 +  (AtpWrapper.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
    1.41  setup {* AtpManager.add_prover "remote_vamp10"
    1.42 -  (AtpThread.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
    1.43 +  (AtpWrapper.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
    1.44  
    1.45  
    1.46  subsection {* The Metis prover *}
     2.1 --- a/src/HOL/IsaMakefile	Tue Oct 14 15:45:46 2008 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Oct 14 16:01:36 2008 +0200
     2.3 @@ -217,7 +217,7 @@
     2.4    Tools/Groebner_Basis/normalizer_data.ML \
     2.5    Tools/Groebner_Basis/normalizer.ML \
     2.6    Tools/atp_manager.ML \
     2.7 -  Tools/atp_thread.ML \
     2.8 +  Tools/atp_wrapper.ML \
     2.9    Tools/meson.ML \
    2.10    Tools/metis_tools.ML \
    2.11    Tools/numeral.ML \
     3.1 --- a/src/HOL/MetisExamples/Abstraction.thy	Tue Oct 14 15:45:46 2008 +0200
     3.2 +++ b/src/HOL/MetisExamples/Abstraction.thy	Tue Oct 14 16:01:36 2008 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4    pset  :: "'a set => 'a set"
     3.5    order :: "'a set => ('a * 'a) set"
     3.6  
     3.7 -ML{*AtpThread.problem_name := "Abstraction__Collect_triv"*}
     3.8 +ML{*AtpWrapper.problem_name := "Abstraction__Collect_triv"*}
     3.9  lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
    3.10  proof (neg_clausify)
    3.11  assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
    3.12 @@ -37,12 +37,12 @@
    3.13  by (metis mem_Collect_eq)
    3.14  
    3.15  
    3.16 -ML{*AtpThread.problem_name := "Abstraction__Collect_mp"*}
    3.17 +ML{*AtpWrapper.problem_name := "Abstraction__Collect_mp"*}
    3.18  lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
    3.19    by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq);
    3.20    --{*34 secs*}
    3.21  
    3.22 -ML{*AtpThread.problem_name := "Abstraction__Sigma_triv"*}
    3.23 +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_triv"*}
    3.24  lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
    3.25  proof (neg_clausify)
    3.26  assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type) \<in> Sigma (A\<Colon>'a\<Colon>type set) (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set)"
    3.27 @@ -60,7 +60,7 @@
    3.28  lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
    3.29  by (metis SigmaD1 SigmaD2)
    3.30  
    3.31 -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect"*}
    3.32 +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect"*}
    3.33  lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
    3.34  (*???metis cannot prove this
    3.35  by (metis CollectD SigmaD1 SigmaD2 UN_eq)
    3.36 @@ -112,7 +112,7 @@
    3.37  qed
    3.38  
    3.39  
    3.40 -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_in_pp"*}
    3.41 +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_in_pp"*}
    3.42  lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
    3.43  by (metis Collect_mem_eq SigmaD2)
    3.44  
    3.45 @@ -131,7 +131,7 @@
    3.46    by (metis 5 0)
    3.47  qed
    3.48  
    3.49 -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect_Pi"*}
    3.50 +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect_Pi"*}
    3.51  lemma
    3.52      "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
    3.53      f \<in> pset cl \<rightarrow> pset cl"
    3.54 @@ -147,7 +147,7 @@
    3.55  qed
    3.56  
    3.57  
    3.58 -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect_Int"*}
    3.59 +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect_Int"*}
    3.60  lemma
    3.61      "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
    3.62     f \<in> pset cl \<inter> cl"
    3.63 @@ -170,13 +170,13 @@
    3.64  qed
    3.65  
    3.66  
    3.67 -ML{*AtpThread.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
    3.68 +ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
    3.69  lemma
    3.70      "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
    3.71     (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
    3.72  by auto
    3.73  
    3.74 -ML{*AtpThread.problem_name := "Abstraction__CLF_subset_Collect_Int"*}
    3.75 +ML{*AtpWrapper.problem_name := "Abstraction__CLF_subset_Collect_Int"*}
    3.76  lemma "(cl,f) \<in> CLF ==> 
    3.77     CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
    3.78     f \<in> pset cl \<inter> cl"
    3.79 @@ -187,7 +187,7 @@
    3.80    --{*@{text Int_def} is redundant*}
    3.81  *)
    3.82  
    3.83 -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
    3.84 +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
    3.85  lemma "(cl,f) \<in> CLF ==> 
    3.86     CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
    3.87     f \<in> pset cl \<inter> cl"
    3.88 @@ -196,7 +196,7 @@
    3.89  by (metis Collect_mem_eq Int_commute SigmaD2)
    3.90  *)
    3.91  
    3.92 -ML{*AtpThread.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
    3.93 +ML{*AtpWrapper.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
    3.94  lemma 
    3.95     "(cl,f) \<in> CLF ==> 
    3.96      CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
    3.97 @@ -206,7 +206,7 @@
    3.98  by (metis Collect_mem_eq SigmaD2 subsetD)
    3.99  *)
   3.100  
   3.101 -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
   3.102 +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
   3.103  lemma 
   3.104    "(cl,f) \<in> CLF ==> 
   3.105     CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   3.106 @@ -216,21 +216,21 @@
   3.107  by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
   3.108  *)
   3.109  
   3.110 -ML{*AtpThread.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
   3.111 +ML{*AtpWrapper.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
   3.112  lemma 
   3.113    "(cl,f) \<in> CLF ==> 
   3.114     CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
   3.115     (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
   3.116  by auto
   3.117  
   3.118 -ML{*AtpThread.problem_name := "Abstraction__map_eq_zipA"*}
   3.119 +ML{*AtpWrapper.problem_name := "Abstraction__map_eq_zipA"*}
   3.120  lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
   3.121  apply (induct xs)
   3.122  (*sledgehammer*)  
   3.123  apply auto
   3.124  done
   3.125  
   3.126 -ML{*AtpThread.problem_name := "Abstraction__map_eq_zipB"*}
   3.127 +ML{*AtpWrapper.problem_name := "Abstraction__map_eq_zipB"*}
   3.128  lemma "map (%w. (w -> w, w \<times> w)) xs = 
   3.129         zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
   3.130  apply (induct xs)
   3.131 @@ -238,28 +238,28 @@
   3.132  apply auto
   3.133  done
   3.134  
   3.135 -ML{*AtpThread.problem_name := "Abstraction__image_evenA"*}
   3.136 +ML{*AtpWrapper.problem_name := "Abstraction__image_evenA"*}
   3.137  lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
   3.138  (*sledgehammer*)  
   3.139  by auto
   3.140  
   3.141 -ML{*AtpThread.problem_name := "Abstraction__image_evenB"*}
   3.142 +ML{*AtpWrapper.problem_name := "Abstraction__image_evenB"*}
   3.143  lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
   3.144         ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
   3.145  (*sledgehammer*)  
   3.146  by auto
   3.147  
   3.148 -ML{*AtpThread.problem_name := "Abstraction__image_curry"*}
   3.149 +ML{*AtpWrapper.problem_name := "Abstraction__image_curry"*}
   3.150  lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 
   3.151  (*sledgehammer*)  
   3.152  by auto
   3.153  
   3.154 -ML{*AtpThread.problem_name := "Abstraction__image_TimesA"*}
   3.155 +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesA"*}
   3.156  lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
   3.157  (*sledgehammer*) 
   3.158  apply (rule equalityI)
   3.159  (***Even the two inclusions are far too difficult
   3.160 -ML{*AtpThread.problem_name := "Abstraction__image_TimesA_simpler"*}
   3.161 +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesA_simpler"*}
   3.162  ***)
   3.163  apply (rule subsetI)
   3.164  apply (erule imageE)
   3.165 @@ -282,13 +282,13 @@
   3.166  (*Given the difficulty of the previous problem, these two are probably
   3.167  impossible*)
   3.168  
   3.169 -ML{*AtpThread.problem_name := "Abstraction__image_TimesB"*}
   3.170 +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesB"*}
   3.171  lemma image_TimesB:
   3.172      "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" 
   3.173  (*sledgehammer*) 
   3.174  by force
   3.175  
   3.176 -ML{*AtpThread.problem_name := "Abstraction__image_TimesC"*}
   3.177 +ML{*AtpWrapper.problem_name := "Abstraction__image_TimesC"*}
   3.178  lemma image_TimesC:
   3.179      "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
   3.180       ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
     4.1 --- a/src/HOL/MetisExamples/BT.thy	Tue Oct 14 15:45:46 2008 +0200
     4.2 +++ b/src/HOL/MetisExamples/BT.thy	Tue Oct 14 16:01:36 2008 +0200
     4.3 @@ -66,21 +66,21 @@
     4.4  
     4.5  text {* \medskip BT simplification *}
     4.6  
     4.7 -ML {*AtpThread.problem_name := "BT__n_leaves_reflect"*}
     4.8 +ML {*AtpWrapper.problem_name := "BT__n_leaves_reflect"*}
     4.9  lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
    4.10    apply (induct t)
    4.11    apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1))
    4.12    apply (metis add_commute n_leaves.simps(2) reflect.simps(2))
    4.13    done
    4.14  
    4.15 -ML {*AtpThread.problem_name := "BT__n_nodes_reflect"*}
    4.16 +ML {*AtpWrapper.problem_name := "BT__n_nodes_reflect"*}
    4.17  lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
    4.18    apply (induct t)
    4.19    apply (metis reflect.simps(1))
    4.20    apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2))
    4.21    done
    4.22  
    4.23 -ML {*AtpThread.problem_name := "BT__depth_reflect"*}
    4.24 +ML {*AtpWrapper.problem_name := "BT__depth_reflect"*}
    4.25  lemma depth_reflect: "depth (reflect t) = depth t"
    4.26    apply (induct t)
    4.27    apply (metis depth.simps(1) reflect.simps(1))
    4.28 @@ -91,21 +91,21 @@
    4.29    The famous relationship between the numbers of leaves and nodes.
    4.30  *}
    4.31  
    4.32 -ML {*AtpThread.problem_name := "BT__n_leaves_nodes"*}
    4.33 +ML {*AtpWrapper.problem_name := "BT__n_leaves_nodes"*}
    4.34  lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
    4.35    apply (induct t)
    4.36    apply (metis n_leaves.simps(1) n_nodes.simps(1))
    4.37    apply auto
    4.38    done
    4.39  
    4.40 -ML {*AtpThread.problem_name := "BT__reflect_reflect_ident"*}
    4.41 +ML {*AtpWrapper.problem_name := "BT__reflect_reflect_ident"*}
    4.42  lemma reflect_reflect_ident: "reflect (reflect t) = t"
    4.43    apply (induct t)
    4.44    apply (metis add_right_cancel reflect.simps(1));
    4.45    apply (metis reflect.simps(2))
    4.46    done
    4.47  
    4.48 -ML {*AtpThread.problem_name := "BT__bt_map_ident"*}
    4.49 +ML {*AtpWrapper.problem_name := "BT__bt_map_ident"*}
    4.50  lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
    4.51  apply (rule ext) 
    4.52  apply (induct_tac y)
    4.53 @@ -116,7 +116,7 @@
    4.54  done
    4.55  
    4.56  
    4.57 -ML {*AtpThread.problem_name := "BT__bt_map_appnd"*}
    4.58 +ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*}
    4.59  lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
    4.60  apply (induct t)
    4.61    apply (metis appnd.simps(1) bt_map.simps(1))
    4.62 @@ -124,7 +124,7 @@
    4.63  done
    4.64  
    4.65  
    4.66 -ML {*AtpThread.problem_name := "BT__bt_map_compose"*}
    4.67 +ML {*AtpWrapper.problem_name := "BT__bt_map_compose"*}
    4.68  lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
    4.69  apply (induct t) 
    4.70    apply (metis bt_map.simps(1))
    4.71 @@ -134,42 +134,42 @@
    4.72  done
    4.73  
    4.74  
    4.75 -ML {*AtpThread.problem_name := "BT__bt_map_reflect"*}
    4.76 +ML {*AtpWrapper.problem_name := "BT__bt_map_reflect"*}
    4.77  lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
    4.78    apply (induct t)
    4.79    apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1))
    4.80    apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2))
    4.81    done
    4.82  
    4.83 -ML {*AtpThread.problem_name := "BT__preorder_bt_map"*}
    4.84 +ML {*AtpWrapper.problem_name := "BT__preorder_bt_map"*}
    4.85  lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
    4.86    apply (induct t)
    4.87    apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
    4.88     apply simp
    4.89    done
    4.90  
    4.91 -ML {*AtpThread.problem_name := "BT__inorder_bt_map"*}
    4.92 +ML {*AtpWrapper.problem_name := "BT__inorder_bt_map"*}
    4.93  lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
    4.94    apply (induct t)
    4.95    apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1))
    4.96    apply simp
    4.97    done
    4.98  
    4.99 -ML {*AtpThread.problem_name := "BT__postorder_bt_map"*}
   4.100 +ML {*AtpWrapper.problem_name := "BT__postorder_bt_map"*}
   4.101  lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
   4.102    apply (induct t)
   4.103    apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1))
   4.104     apply simp
   4.105    done
   4.106  
   4.107 -ML {*AtpThread.problem_name := "BT__depth_bt_map"*}
   4.108 +ML {*AtpWrapper.problem_name := "BT__depth_bt_map"*}
   4.109  lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
   4.110    apply (induct t)
   4.111    apply (metis bt_map.simps(1) depth.simps(1))
   4.112     apply simp
   4.113    done
   4.114  
   4.115 -ML {*AtpThread.problem_name := "BT__n_leaves_bt_map"*}
   4.116 +ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*}
   4.117  lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
   4.118    apply (induct t)
   4.119    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))
   4.120 @@ -177,21 +177,21 @@
   4.121    done
   4.122  
   4.123  
   4.124 -ML {*AtpThread.problem_name := "BT__preorder_reflect"*}
   4.125 +ML {*AtpWrapper.problem_name := "BT__preorder_reflect"*}
   4.126  lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   4.127    apply (induct t)
   4.128    apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
   4.129    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)
   4.130    done
   4.131  
   4.132 -ML {*AtpThread.problem_name := "BT__inorder_reflect"*}
   4.133 +ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*}
   4.134  lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
   4.135    apply (induct t)
   4.136    apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1))
   4.137    apply simp
   4.138    done
   4.139  
   4.140 -ML {*AtpThread.problem_name := "BT__postorder_reflect"*}
   4.141 +ML {*AtpWrapper.problem_name := "BT__postorder_reflect"*}
   4.142  lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
   4.143    apply (induct t)
   4.144    apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
   4.145 @@ -202,7 +202,7 @@
   4.146   Analogues of the standard properties of the append function for lists.
   4.147  *}
   4.148  
   4.149 -ML {*AtpThread.problem_name := "BT__appnd_assoc"*}
   4.150 +ML {*AtpWrapper.problem_name := "BT__appnd_assoc"*}
   4.151  lemma appnd_assoc [simp]:
   4.152       "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
   4.153    apply (induct t1)
   4.154 @@ -210,14 +210,14 @@
   4.155    apply (metis appnd.simps(2))
   4.156    done
   4.157  
   4.158 -ML {*AtpThread.problem_name := "BT__appnd_Lf2"*}
   4.159 +ML {*AtpWrapper.problem_name := "BT__appnd_Lf2"*}
   4.160  lemma appnd_Lf2 [simp]: "appnd t Lf = t"
   4.161    apply (induct t)
   4.162    apply (metis appnd.simps(1))
   4.163    apply (metis appnd.simps(2))
   4.164    done
   4.165  
   4.166 -ML {*AtpThread.problem_name := "BT__depth_appnd"*}
   4.167 +ML {*AtpWrapper.problem_name := "BT__depth_appnd"*}
   4.168    declare max_add_distrib_left [simp]
   4.169  lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
   4.170    apply (induct t1)
   4.171 @@ -225,7 +225,7 @@
   4.172  apply (simp add: ); 
   4.173    done
   4.174  
   4.175 -ML {*AtpThread.problem_name := "BT__n_leaves_appnd"*}
   4.176 +ML {*AtpWrapper.problem_name := "BT__n_leaves_appnd"*}
   4.177  lemma n_leaves_appnd [simp]:
   4.178       "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
   4.179    apply (induct t1)
   4.180 @@ -233,7 +233,7 @@
   4.181    apply (simp add: left_distrib)
   4.182    done
   4.183  
   4.184 -ML {*AtpThread.problem_name := "BT__bt_map_appnd"*}
   4.185 +ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*}
   4.186  lemma (*bt_map_appnd:*)
   4.187       "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
   4.188    apply (induct t1)
     5.1 --- a/src/HOL/MetisExamples/BigO.thy	Tue Oct 14 15:45:46 2008 +0200
     5.2 +++ b/src/HOL/MetisExamples/BigO.thy	Tue Oct 14 16:01:36 2008 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4    bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
     5.5    "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
     5.6  
     5.7 -ML_command{*AtpThread.problem_name := "BigO__bigo_pos_const"*}
     5.8 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_pos_const"*}
     5.9  lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
    5.10      ALL x. (abs (h x)) <= (c * (abs (f x))))
    5.11        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    5.12 @@ -215,7 +215,7 @@
    5.13      {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
    5.14  by (auto simp add: bigo_def bigo_pos_const)
    5.15  
    5.16 -ML_command{*AtpThread.problem_name := "BigO__bigo_elt_subset"*}
    5.17 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_elt_subset"*}
    5.18  lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
    5.19    apply (auto simp add: bigo_alt_def)
    5.20    apply (rule_tac x = "ca * c" in exI)
    5.21 @@ -233,7 +233,7 @@
    5.22  done
    5.23  
    5.24  
    5.25 -ML_command{*AtpThread.problem_name := "BigO__bigo_refl"*}
    5.26 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_refl"*}
    5.27  lemma bigo_refl [intro]: "f : O(f)"
    5.28    apply(auto simp add: bigo_def)
    5.29  proof (neg_clausify)
    5.30 @@ -247,7 +247,7 @@
    5.31    by (metis 0 2)
    5.32  qed
    5.33  
    5.34 -ML_command{*AtpThread.problem_name := "BigO__bigo_zero"*}
    5.35 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_zero"*}
    5.36  lemma bigo_zero: "0 : O(g)"
    5.37    apply (auto simp add: bigo_def func_zero)
    5.38  proof (neg_clausify)
    5.39 @@ -337,7 +337,7 @@
    5.40    apply (auto del: subsetI simp del: bigo_plus_idemp)
    5.41  done
    5.42  
    5.43 -ML_command{*AtpThread.problem_name := "BigO__bigo_plus_eq"*}
    5.44 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq"*}
    5.45  lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
    5.46    O(f + g) = O(f) \<oplus> O(g)"
    5.47    apply (rule equalityI)
    5.48 @@ -360,13 +360,13 @@
    5.49    apply (rule abs_triangle_ineq)
    5.50    apply (metis add_nonneg_nonneg)
    5.51    apply (rule add_mono)
    5.52 -ML_command{*AtpThread.problem_name := "BigO__bigo_plus_eq_simpler"*} 
    5.53 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq_simpler"*} 
    5.54  (*Found by SPASS; SLOW*)
    5.55  apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right order_trans)
    5.56  apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
    5.57  done
    5.58  
    5.59 -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded_alt"*}
    5.60 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt"*}
    5.61  lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
    5.62      f : O(g)" 
    5.63    apply (auto simp add: bigo_def)
    5.64 @@ -426,7 +426,7 @@
    5.65  
    5.66  
    5.67  text{*So here is the easier (and more natural) problem using transitivity*}
    5.68 -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded_alt_trans"*}
    5.69 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt_trans"*}
    5.70  lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
    5.71    apply (auto simp add: bigo_def)
    5.72    (*Version 1: one-shot proof*) 
    5.73 @@ -434,7 +434,7 @@
    5.74    done
    5.75  
    5.76  text{*So here is the easier (and more natural) problem using transitivity*}
    5.77 -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded_alt_trans"*}
    5.78 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt_trans"*}
    5.79  lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
    5.80    apply (auto simp add: bigo_def)
    5.81  (*Version 2: single-step proof*)
    5.82 @@ -473,7 +473,7 @@
    5.83    apply simp
    5.84  done
    5.85  
    5.86 -ML_command{*AtpThread.problem_name := "BigO__bigo_bounded2"*}
    5.87 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded2"*}
    5.88  lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
    5.89      f : lb +o O(g)"
    5.90    apply (rule set_minus_imp_plus)
    5.91 @@ -496,7 +496,7 @@
    5.92    by (metis 4 2 0)
    5.93  qed
    5.94  
    5.95 -ML_command{*AtpThread.problem_name := "BigO__bigo_abs"*}
    5.96 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_abs"*}
    5.97  lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
    5.98    apply (unfold bigo_def)
    5.99    apply auto
   5.100 @@ -511,7 +511,7 @@
   5.101    by (metis 0 2)
   5.102  qed
   5.103  
   5.104 -ML_command{*AtpThread.problem_name := "BigO__bigo_abs2"*}
   5.105 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_abs2"*}
   5.106  lemma bigo_abs2: "f =o O(%x. abs(f x))"
   5.107    apply (unfold bigo_def)
   5.108    apply auto
   5.109 @@ -583,7 +583,7 @@
   5.110      by (simp add: bigo_abs3 [symmetric])
   5.111  qed
   5.112  
   5.113 -ML_command{*AtpThread.problem_name := "BigO__bigo_mult"*}
   5.114 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult"*}
   5.115  lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
   5.116    apply (rule subsetI)
   5.117    apply (subst bigo_def)
   5.118 @@ -595,7 +595,7 @@
   5.119    apply(erule_tac x = x in allE)+
   5.120    apply(subgoal_tac "c * ca * abs(f x * g x) = 
   5.121        (c * abs(f x)) * (ca * abs(g x))")
   5.122 -ML_command{*AtpThread.problem_name := "BigO__bigo_mult_simpler"*}
   5.123 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult_simpler"*}
   5.124  prefer 2 
   5.125  apply (metis mult_assoc mult_left_commute
   5.126    OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute
   5.127 @@ -660,14 +660,14 @@
   5.128  qed
   5.129  
   5.130  
   5.131 -ML_command{*AtpThread.problem_name := "BigO__bigo_mult2"*}
   5.132 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult2"*}
   5.133  lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
   5.134    apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
   5.135  (*sledgehammer*); 
   5.136    apply (rule_tac x = c in exI)
   5.137    apply clarify
   5.138    apply (drule_tac x = x in spec)
   5.139 -ML_command{*AtpThread.problem_name := "BigO__bigo_mult2_simpler"*}
   5.140 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult2_simpler"*}
   5.141  (*sledgehammer [no luck]*); 
   5.142    apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
   5.143    apply (simp add: mult_ac)
   5.144 @@ -675,11 +675,11 @@
   5.145    apply (rule abs_ge_zero)
   5.146  done
   5.147  
   5.148 -ML_command{*AtpThread.problem_name:="BigO__bigo_mult3"*}
   5.149 +ML_command{*AtpWrapper.problem_name:="BigO__bigo_mult3"*}
   5.150  lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
   5.151  by (metis bigo_mult set_times_intro subset_iff)
   5.152  
   5.153 -ML_command{*AtpThread.problem_name:="BigO__bigo_mult4"*}
   5.154 +ML_command{*AtpWrapper.problem_name:="BigO__bigo_mult4"*}
   5.155  lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
   5.156  by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
   5.157  
   5.158 @@ -713,13 +713,13 @@
   5.159    qed
   5.160  qed
   5.161  
   5.162 -ML_command{*AtpThread.problem_name := "BigO__bigo_mult6"*}
   5.163 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult6"*}
   5.164  lemma bigo_mult6: "ALL x. f x ~= 0 ==>
   5.165      O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"
   5.166  by (metis bigo_mult2 bigo_mult5 order_antisym)
   5.167  
   5.168  (*proof requires relaxing relevance: 2007-01-25*)
   5.169 -ML_command{*AtpThread.problem_name := "BigO__bigo_mult7"*}
   5.170 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult7"*}
   5.171    declare bigo_mult6 [simp]
   5.172  lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   5.173      O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   5.174 @@ -731,7 +731,7 @@
   5.175  done
   5.176    declare bigo_mult6 [simp del]
   5.177  
   5.178 -ML_command{*AtpThread.problem_name := "BigO__bigo_mult8"*}
   5.179 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult8"*}
   5.180    declare bigo_mult7[intro!]
   5.181  lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   5.182      O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   5.183 @@ -782,7 +782,7 @@
   5.184    qed
   5.185  qed
   5.186  
   5.187 -ML_command{*AtpThread.problem_name:="BigO__bigo_plus_absorb"*}
   5.188 +ML_command{*AtpWrapper.problem_name:="BigO__bigo_plus_absorb"*}
   5.189  lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
   5.190  by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff);
   5.191  
   5.192 @@ -809,7 +809,7 @@
   5.193  lemma bigo_const1: "(%x. c) : O(%x. 1)"
   5.194  by (auto simp add: bigo_def mult_ac)
   5.195  
   5.196 -ML_command{*AtpThread.problem_name:="BigO__bigo_const2"*}
   5.197 +ML_command{*AtpWrapper.problem_name:="BigO__bigo_const2"*}
   5.198  lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
   5.199  by (metis bigo_const1 bigo_elt_subset);
   5.200  
   5.201 @@ -832,7 +832,7 @@
   5.202    apply (rule bigo_const1)
   5.203  done
   5.204  
   5.205 -ML_command{*AtpThread.problem_name := "BigO__bigo_const3"*}
   5.206 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const3"*}
   5.207  lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
   5.208  apply (simp add: bigo_def)
   5.209  proof (neg_clausify)
   5.210 @@ -856,7 +856,7 @@
   5.211      O(%x. c) = O(%x. 1)"
   5.212  by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   5.213  
   5.214 -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult1"*}
   5.215 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult1"*}
   5.216  lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   5.217    apply (simp add: bigo_def abs_mult)
   5.218  proof (neg_clausify)
   5.219 @@ -872,7 +872,7 @@
   5.220  lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
   5.221  by (rule bigo_elt_subset, rule bigo_const_mult1)
   5.222  
   5.223 -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult3"*}
   5.224 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult3"*}
   5.225  lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
   5.226    apply (simp add: bigo_def)
   5.227  (*sledgehammer [no luck]*); 
   5.228 @@ -890,7 +890,7 @@
   5.229      O(%x. c * f x) = O(f)"
   5.230  by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   5.231  
   5.232 -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult5"*}
   5.233 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult5"*}
   5.234  lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   5.235      (%x. c) *o O(f) = O(f)"
   5.236    apply (auto del: subsetI)
   5.237 @@ -910,7 +910,7 @@
   5.238  done
   5.239  
   5.240  
   5.241 -ML_command{*AtpThread.problem_name := "BigO__bigo_const_mult6"*}
   5.242 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult6"*}
   5.243  lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
   5.244    apply (auto intro!: subsetI
   5.245      simp add: bigo_def elt_set_times_def func_times
   5.246 @@ -967,7 +967,7 @@
   5.247  apply (blast intro: order_trans mult_right_mono abs_ge_self) 
   5.248  done
   5.249  
   5.250 -ML_command{*AtpThread.problem_name := "BigO__bigo_setsum1"*}
   5.251 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum1"*}
   5.252  lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> 
   5.253      EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
   5.254        (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
   5.255 @@ -984,7 +984,7 @@
   5.256        (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
   5.257  by (rule bigo_setsum1, auto)  
   5.258  
   5.259 -ML_command{*AtpThread.problem_name := "BigO__bigo_setsum3"*}
   5.260 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum3"*}
   5.261  lemma bigo_setsum3: "f =o O(h) ==>
   5.262      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   5.263        O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   5.264 @@ -1015,7 +1015,7 @@
   5.265    apply (erule set_plus_imp_minus)
   5.266  done
   5.267  
   5.268 -ML_command{*AtpThread.problem_name := "BigO__bigo_setsum5"*}
   5.269 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum5"*}
   5.270  lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> 
   5.271      ALL x. 0 <= h x ==>
   5.272        (%x. SUM y : A x. (l x y) * f(k x y)) =o
   5.273 @@ -1072,7 +1072,7 @@
   5.274    apply (simp add: func_times) 
   5.275  done
   5.276  
   5.277 -ML_command{*AtpThread.problem_name := "BigO__bigo_fix"*}
   5.278 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_fix"*}
   5.279  lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
   5.280      f =o O(h)"
   5.281    apply (simp add: bigo_alt_def)
   5.282 @@ -1137,7 +1137,7 @@
   5.283    apply (erule spec)+
   5.284  done
   5.285  
   5.286 -ML_command{*AtpThread.problem_name:="BigO__bigo_lesso1"*}
   5.287 +ML_command{*AtpWrapper.problem_name:="BigO__bigo_lesso1"*}
   5.288  lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
   5.289    apply (unfold lesso_def)
   5.290    apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
   5.291 @@ -1149,7 +1149,7 @@
   5.292  done
   5.293  
   5.294  
   5.295 -ML_command{*AtpThread.problem_name := "BigO__bigo_lesso2"*}
   5.296 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso2"*}
   5.297  lemma bigo_lesso2: "f =o g +o O(h) ==>
   5.298      ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
   5.299        k <o g =o O(h)"
   5.300 @@ -1186,7 +1186,7 @@
   5.301    by (metis min_max.less_eq_less_sup.sup_commute min_max.less_eq_less_inf.inf_commute min_max.less_eq_less_inf_sup.sup_inf_absorb min_max.less_eq_less_inf.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
   5.302  qed
   5.303  
   5.304 -ML_command{*AtpThread.problem_name := "BigO__bigo_lesso3"*}
   5.305 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3"*}
   5.306  lemma bigo_lesso3: "f =o g +o O(h) ==>
   5.307      ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
   5.308        f <o k =o O(h)"
   5.309 @@ -1203,7 +1203,7 @@
   5.310    apply (simp del: compare_rls diff_minus);
   5.311    apply (subst abs_of_nonneg)
   5.312    apply (drule_tac x = x in spec) back
   5.313 -ML_command{*AtpThread.problem_name := "BigO__bigo_lesso3_simpler"*}
   5.314 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3_simpler"*}
   5.315  apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
   5.316  apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
   5.317  apply (metis abs_ge_zero linorder_linear min_max.less_eq_less_sup.sup_absorb1 min_max.less_eq_less_sup.sup_commute)
   5.318 @@ -1223,7 +1223,7 @@
   5.319      split: split_max abs_split)
   5.320  done
   5.321  
   5.322 -ML_command{*AtpThread.problem_name := "BigO__bigo_lesso5"*}
   5.323 +ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso5"*}
   5.324  lemma bigo_lesso5: "f <o g =o O(h) ==>
   5.325      EX C. ALL x. f x <= g x + C * abs(h x)"
   5.326    apply (simp only: lesso_def bigo_alt_def)
     6.1 --- a/src/HOL/MetisExamples/Message.thy	Tue Oct 14 15:45:46 2008 +0200
     6.2 +++ b/src/HOL/MetisExamples/Message.thy	Tue Oct 14 16:01:36 2008 +0200
     6.3 @@ -78,7 +78,7 @@
     6.4    | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
     6.5  
     6.6  
     6.7 -ML{*AtpThread.problem_name := "Message__parts_mono"*}
     6.8 +ML{*AtpWrapper.problem_name := "Message__parts_mono"*}
     6.9  lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
    6.10  apply auto
    6.11  apply (erule parts.induct) 
    6.12 @@ -102,7 +102,7 @@
    6.13  
    6.14  subsubsection{*Inverse of keys *}
    6.15  
    6.16 -ML{*AtpThread.problem_name := "Message__invKey_eq"*}
    6.17 +ML{*AtpWrapper.problem_name := "Message__invKey_eq"*}
    6.18  lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
    6.19  by (metis invKey)
    6.20  
    6.21 @@ -203,7 +203,7 @@
    6.22  apply (simp only: parts_Un)
    6.23  done
    6.24  
    6.25 -ML{*AtpThread.problem_name := "Message__parts_insert_two"*}
    6.26 +ML{*AtpWrapper.problem_name := "Message__parts_insert_two"*}
    6.27  lemma parts_insert2:
    6.28       "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
    6.29  by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
    6.30 @@ -240,7 +240,7 @@
    6.31  lemma parts_idem [simp]: "parts (parts H) = parts H"
    6.32  by blast
    6.33  
    6.34 -ML{*AtpThread.problem_name := "Message__parts_subset_iff"*}
    6.35 +ML{*AtpWrapper.problem_name := "Message__parts_subset_iff"*}
    6.36  lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
    6.37  apply (rule iffI) 
    6.38  apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
    6.39 @@ -251,7 +251,7 @@
    6.40  by (blast dest: parts_mono); 
    6.41  
    6.42  
    6.43 -ML{*AtpThread.problem_name := "Message__parts_cut"*}
    6.44 +ML{*AtpWrapper.problem_name := "Message__parts_cut"*}
    6.45  lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
    6.46  by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
    6.47  
    6.48 @@ -316,7 +316,7 @@
    6.49  done
    6.50  
    6.51  
    6.52 -ML{*AtpThread.problem_name := "Message__msg_Nonce_supply"*}
    6.53 +ML{*AtpWrapper.problem_name := "Message__msg_Nonce_supply"*}
    6.54  lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
    6.55  apply (induct_tac "msg") 
    6.56  apply (simp_all add: parts_insert2)
    6.57 @@ -368,7 +368,7 @@
    6.58  lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
    6.59  
    6.60  
    6.61 -ML{*AtpThread.problem_name := "Message__parts_analz"*}
    6.62 +ML{*AtpWrapper.problem_name := "Message__parts_analz"*}
    6.63  lemma parts_analz [simp]: "parts (analz H) = parts H"
    6.64  apply (rule equalityI)
    6.65  apply (metis analz_subset_parts parts_subset_iff)
    6.66 @@ -520,7 +520,7 @@
    6.67  by (drule analz_mono, blast)
    6.68  
    6.69  
    6.70 -ML{*AtpThread.problem_name := "Message__analz_cut"*}
    6.71 +ML{*AtpWrapper.problem_name := "Message__analz_cut"*}
    6.72      declare analz_trans[intro]
    6.73  lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
    6.74  (*TOO SLOW
    6.75 @@ -538,7 +538,7 @@
    6.76  
    6.77  text{*A congruence rule for "analz" *}
    6.78  
    6.79 -ML{*AtpThread.problem_name := "Message__analz_subset_cong"*}
    6.80 +ML{*AtpWrapper.problem_name := "Message__analz_subset_cong"*}
    6.81  lemma analz_subset_cong:
    6.82       "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
    6.83        ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
    6.84 @@ -616,7 +616,7 @@
    6.85  by (intro Un_least synth_mono Un_upper1 Un_upper2)
    6.86  
    6.87  
    6.88 -ML{*AtpThread.problem_name := "Message__synth_insert"*}
    6.89 +ML{*AtpWrapper.problem_name := "Message__synth_insert"*}
    6.90   
    6.91  lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
    6.92  by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
    6.93 @@ -638,7 +638,7 @@
    6.94  lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
    6.95  by (drule synth_mono, blast)
    6.96  
    6.97 -ML{*AtpThread.problem_name := "Message__synth_cut"*}
    6.98 +ML{*AtpWrapper.problem_name := "Message__synth_cut"*}
    6.99  lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   6.100  (*TOO SLOW
   6.101  by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
   6.102 @@ -670,7 +670,7 @@
   6.103  
   6.104  subsubsection{*Combinations of parts, analz and synth *}
   6.105  
   6.106 -ML{*AtpThread.problem_name := "Message__parts_synth"*}
   6.107 +ML{*AtpWrapper.problem_name := "Message__parts_synth"*}
   6.108  lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   6.109  apply (rule equalityI)
   6.110  apply (rule subsetI)
   6.111 @@ -685,14 +685,14 @@
   6.112  
   6.113  
   6.114  
   6.115 -ML{*AtpThread.problem_name := "Message__analz_analz_Un"*}
   6.116 +ML{*AtpWrapper.problem_name := "Message__analz_analz_Un"*}
   6.117  lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   6.118  apply (rule equalityI);
   6.119  apply (metis analz_idem analz_subset_cong order_eq_refl)
   6.120  apply (metis analz_increasing analz_subset_cong order_eq_refl)
   6.121  done
   6.122  
   6.123 -ML{*AtpThread.problem_name := "Message__analz_synth_Un"*}
   6.124 +ML{*AtpWrapper.problem_name := "Message__analz_synth_Un"*}
   6.125      declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
   6.126  lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   6.127  apply (rule equalityI)
   6.128 @@ -706,7 +706,7 @@
   6.129  done
   6.130  
   6.131  
   6.132 -ML{*AtpThread.problem_name := "Message__analz_synth"*}
   6.133 +ML{*AtpWrapper.problem_name := "Message__analz_synth"*}
   6.134  lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   6.135  proof (neg_clausify)
   6.136  assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
   6.137 @@ -729,7 +729,7 @@
   6.138  
   6.139  subsubsection{*For reasoning about the Fake rule in traces *}
   6.140  
   6.141 -ML{*AtpThread.problem_name := "Message__parts_insert_subset_Un"*}
   6.142 +ML{*AtpWrapper.problem_name := "Message__parts_insert_subset_Un"*}
   6.143  lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   6.144  proof (neg_clausify)
   6.145  assume 0: "X \<in> G"
   6.146 @@ -748,7 +748,7 @@
   6.147    by (metis 6 0)
   6.148  qed
   6.149  
   6.150 -ML{*AtpThread.problem_name := "Message__Fake_parts_insert"*}
   6.151 +ML{*AtpWrapper.problem_name := "Message__Fake_parts_insert"*}
   6.152  lemma Fake_parts_insert:
   6.153       "X \<in> synth (analz H) ==>  
   6.154        parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   6.155 @@ -791,14 +791,14 @@
   6.156        ==> Z \<in>  synth (analz H) \<union> parts H";
   6.157  by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   6.158  
   6.159 -ML{*AtpThread.problem_name := "Message__Fake_analz_insert"*}
   6.160 +ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert"*}
   6.161      declare analz_mono [intro] synth_mono [intro] 
   6.162  lemma Fake_analz_insert:
   6.163       "X\<in> synth (analz G) ==>  
   6.164        analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   6.165  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))
   6.166  
   6.167 -ML{*AtpThread.problem_name := "Message__Fake_analz_insert_simpler"*}
   6.168 +ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert_simpler"*}
   6.169  (*simpler problems?  BUT METIS CAN'T PROVE
   6.170  lemma Fake_analz_insert_simpler:
   6.171       "X\<in> synth (analz G) ==>  
     7.1 --- a/src/HOL/MetisExamples/Tarski.thy	Tue Oct 14 15:45:46 2008 +0200
     7.2 +++ b/src/HOL/MetisExamples/Tarski.thy	Tue Oct 14 16:01:36 2008 +0200
     7.3 @@ -416,7 +416,7 @@
     7.4  (*never proved, 2007-01-22: Tarski__CLF_unnamed_lemma
     7.5    NOT PROVABLE because of the conjunction used in the definition: we don't
     7.6    allow reasoning with rules like conjE, which is essential here.*)
     7.7 -ML_command{*AtpThread.problem_name:="Tarski__CLF_unnamed_lemma"*}
     7.8 +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_unnamed_lemma"*}
     7.9  lemma (in CLF) [simp]:
    7.10      "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" 
    7.11  apply (insert f_cl)
    7.12 @@ -433,7 +433,7 @@
    7.13  by (simp add: A_def r_def)
    7.14  
    7.15  (*never proved, 2007-01-22*)
    7.16 -ML_command{*AtpThread.problem_name:="Tarski__CLF_CLF_dual"*}
    7.17 +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_CLF_dual"*}
    7.18  declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp]
    7.19  
    7.20  lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" 
    7.21 @@ -461,7 +461,7 @@
    7.22  subsection {* lemmas for Tarski, lub *}
    7.23  
    7.24  (*never proved, 2007-01-22*)
    7.25 -ML{*AtpThread.problem_name:="Tarski__CLF_lubH_le_flubH"*}
    7.26 +ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_le_flubH"*}
    7.27    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] 
    7.28  lemma (in CLF) lubH_le_flubH:
    7.29       "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r"
    7.30 @@ -471,7 +471,7 @@
    7.31  -- {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *}
    7.32  apply (rule ballI)
    7.33  (*never proved, 2007-01-22*)
    7.34 -ML_command{*AtpThread.problem_name:="Tarski__CLF_lubH_le_flubH_simpler"*}
    7.35 +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_le_flubH_simpler"*}
    7.36  apply (rule transE)
    7.37  -- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *}
    7.38  -- {* because of the def of @{text H} *}
    7.39 @@ -489,7 +489,7 @@
    7.40            CLF.monotone_f[rule del] CL.lub_upper[rule del] 
    7.41  
    7.42  (*never proved, 2007-01-22*)
    7.43 -ML{*AtpThread.problem_name:="Tarski__CLF_flubH_le_lubH"*}
    7.44 +ML{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH"*}
    7.45    declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro]
    7.46         PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] 
    7.47         CLF.lubH_le_flubH[simp]
    7.48 @@ -499,7 +499,7 @@
    7.49  apply (rule_tac t = "H" in ssubst, assumption)
    7.50  apply (rule CollectI)
    7.51  apply (rule conjI)
    7.52 -ML_command{*AtpThread.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
    7.53 +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
    7.54  (*??no longer terminates, with combinators
    7.55  apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2) 
    7.56  *)
    7.57 @@ -513,7 +513,7 @@
    7.58  
    7.59  
    7.60  (*never proved, 2007-01-22*)
    7.61 -ML{*AtpThread.problem_name:="Tarski__CLF_lubH_is_fixp"*}
    7.62 +ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp"*}
    7.63  (*Single-step version fails. The conjecture clauses refer to local abstraction
    7.64  functions (Frees), which prevents expand_defs_tac from removing those 
    7.65  "definitions" at the end of the proof. *)
    7.66 @@ -588,7 +588,7 @@
    7.67       "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
    7.68  apply (simp add: fix_def)
    7.69  apply (rule conjI)
    7.70 -ML_command{*AtpThread.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} 
    7.71 +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} 
    7.72  apply (metis CO_refl lubH_le_flubH reflD1)
    7.73  apply (metis antisymE flubH_le_lubH lubH_le_flubH)
    7.74  done
    7.75 @@ -607,7 +607,7 @@
    7.76  apply (simp_all add: P_def)
    7.77  done
    7.78  
    7.79 -ML{*AtpThread.problem_name:="Tarski__CLF_lubH_least_fixf"*}
    7.80 +ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_least_fixf"*}
    7.81  lemma (in CLF) lubH_least_fixf:
    7.82       "H = {x. (x, f x) \<in> r & x \<in> A}
    7.83        ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r"
    7.84 @@ -615,7 +615,7 @@
    7.85  done
    7.86  
    7.87  subsection {* Tarski fixpoint theorem 1, first part *}
    7.88 -ML{*AtpThread.problem_name:="Tarski__CLF_T_thm_1_lub"*}
    7.89 +ML{*AtpWrapper.problem_name:="Tarski__CLF_T_thm_1_lub"*}
    7.90    declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] 
    7.91            CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp]
    7.92  lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl"
    7.93 @@ -623,7 +623,7 @@
    7.94  apply (rule sym)
    7.95  apply (simp add: P_def)
    7.96  apply (rule lubI)
    7.97 -ML_command{*AtpThread.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*}
    7.98 +ML_command{*AtpWrapper.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*}
    7.99  apply (metis P_def fix_subset) 
   7.100  apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
   7.101  (*??no longer terminates, with combinators
   7.102 @@ -638,7 +638,7 @@
   7.103  
   7.104  
   7.105  (*never proved, 2007-01-22*)
   7.106 -ML{*AtpThread.problem_name:="Tarski__CLF_glbH_is_fixp"*}
   7.107 +ML{*AtpWrapper.problem_name:="Tarski__CLF_glbH_is_fixp"*}
   7.108    declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] 
   7.109            PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp]
   7.110  lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P"
   7.111 @@ -662,13 +662,13 @@
   7.112  
   7.113  
   7.114  (*never proved, 2007-01-22*)
   7.115 -ML{*AtpThread.problem_name:="Tarski__T_thm_1_glb"*}  (*ALL THEOREMS*)
   7.116 +ML{*AtpWrapper.problem_name:="Tarski__T_thm_1_glb"*}  (*ALL THEOREMS*)
   7.117  lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl"
   7.118  (*sledgehammer;*)
   7.119  apply (simp add: glb_dual_lub P_def A_def r_def)
   7.120  apply (rule dualA_iff [THEN subst])
   7.121  (*never proved, 2007-01-22*)
   7.122 -ML_command{*AtpThread.problem_name:="Tarski__T_thm_1_glb_simpler"*}  (*ALL THEOREMS*)
   7.123 +ML_command{*AtpWrapper.problem_name:="Tarski__T_thm_1_glb_simpler"*}  (*ALL THEOREMS*)
   7.124  (*sledgehammer;*)
   7.125  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,
   7.126    OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff)
   7.127 @@ -677,13 +677,13 @@
   7.128  subsection {* interval *}
   7.129  
   7.130  
   7.131 -ML{*AtpThread.problem_name:="Tarski__rel_imp_elem"*}
   7.132 +ML{*AtpWrapper.problem_name:="Tarski__rel_imp_elem"*}
   7.133    declare (in CLF) CO_refl[simp] refl_def [simp]
   7.134  lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
   7.135  by (metis CO_refl reflD1)
   7.136    declare (in CLF) CO_refl[simp del]  refl_def [simp del]
   7.137  
   7.138 -ML{*AtpThread.problem_name:="Tarski__interval_subset"*}
   7.139 +ML{*AtpWrapper.problem_name:="Tarski__interval_subset"*}
   7.140    declare (in CLF) rel_imp_elem[intro] 
   7.141    declare interval_def [simp]
   7.142  lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
   7.143 @@ -718,7 +718,7 @@
   7.144       "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b |]==> S \<subseteq> A"
   7.145  by (simp add: subset_trans [OF _ interval_subset])
   7.146  
   7.147 -ML{*AtpThread.problem_name:="Tarski__L_in_interval"*}  (*ALL THEOREMS*)
   7.148 +ML{*AtpWrapper.problem_name:="Tarski__L_in_interval"*}  (*ALL THEOREMS*)
   7.149  lemma (in CLF) L_in_interval:
   7.150       "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b;
   7.151           S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} |] ==> L \<in> interval r a b" 
   7.152 @@ -737,7 +737,7 @@
   7.153  done
   7.154  
   7.155  (*never proved, 2007-01-22*)
   7.156 -ML{*AtpThread.problem_name:="Tarski__G_in_interval"*}  (*ALL THEOREMS*)
   7.157 +ML{*AtpWrapper.problem_name:="Tarski__G_in_interval"*}  (*ALL THEOREMS*)
   7.158  lemma (in CLF) G_in_interval:
   7.159       "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G;
   7.160           S \<noteq> {} |] ==> G \<in> interval r a b"
   7.161 @@ -746,7 +746,7 @@
   7.162                   dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
   7.163  done
   7.164  
   7.165 -ML{*AtpThread.problem_name:="Tarski__intervalPO"*}  (*ALL THEOREMS*)
   7.166 +ML{*AtpWrapper.problem_name:="Tarski__intervalPO"*}  (*ALL THEOREMS*)
   7.167  lemma (in CLF) intervalPO:
   7.168       "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
   7.169        ==> (| pset = interval r a b, order = induced (interval r a b) r |)
   7.170 @@ -819,7 +819,7 @@
   7.171  lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual]
   7.172  
   7.173  (*never proved, 2007-01-22*)
   7.174 -ML{*AtpThread.problem_name:="Tarski__interval_is_sublattice"*}  (*ALL THEOREMS*)
   7.175 +ML{*AtpWrapper.problem_name:="Tarski__interval_is_sublattice"*}  (*ALL THEOREMS*)
   7.176  lemma (in CLF) interval_is_sublattice:
   7.177       "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
   7.178          ==> interval r a b <<= cl"
   7.179 @@ -827,7 +827,7 @@
   7.180  apply (rule sublatticeI)
   7.181  apply (simp add: interval_subset)
   7.182  (*never proved, 2007-01-22*)
   7.183 -ML_command{*AtpThread.problem_name:="Tarski__interval_is_sublattice_simpler"*}  
   7.184 +ML_command{*AtpWrapper.problem_name:="Tarski__interval_is_sublattice_simpler"*}  
   7.185  (*sledgehammer *)
   7.186  apply (rule CompleteLatticeI)
   7.187  apply (simp add: intervalPO)
   7.188 @@ -846,7 +846,7 @@
   7.189  lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)"
   7.190  by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
   7.191  
   7.192 -ML_command{*AtpThread.problem_name:="Tarski__Bot_in_lattice"*}  (*ALL THEOREMS*)
   7.193 +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_in_lattice"*}  (*ALL THEOREMS*)
   7.194  lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A"
   7.195  (*sledgehammer; *)
   7.196  apply (simp add: Bot_def least_def)
   7.197 @@ -856,12 +856,12 @@
   7.198  done
   7.199  
   7.200  (*first proved 2007-01-25 after relaxing relevance*)
   7.201 -ML_command{*AtpThread.problem_name:="Tarski__Top_in_lattice"*}  (*ALL THEOREMS*)
   7.202 +ML_command{*AtpWrapper.problem_name:="Tarski__Top_in_lattice"*}  (*ALL THEOREMS*)
   7.203  lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
   7.204  (*sledgehammer;*)
   7.205  apply (simp add: Top_dual_Bot A_def)
   7.206  (*first proved 2007-01-25 after relaxing relevance*)
   7.207 -ML_command{*AtpThread.problem_name:="Tarski__Top_in_lattice_simpler"*}  (*ALL THEOREMS*)
   7.208 +ML_command{*AtpWrapper.problem_name:="Tarski__Top_in_lattice_simpler"*}  (*ALL THEOREMS*)
   7.209  (*sledgehammer*)
   7.210  apply (rule dualA_iff [THEN subst])
   7.211  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)
   7.212 @@ -876,7 +876,7 @@
   7.213  done
   7.214  
   7.215  (*never proved, 2007-01-22*)
   7.216 -ML_command{*AtpThread.problem_name:="Tarski__Bot_prop"*}  (*ALL THEOREMS*) 
   7.217 +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_prop"*}  (*ALL THEOREMS*) 
   7.218  lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r"
   7.219  (*sledgehammer*) 
   7.220  apply (simp add: Bot_dual_Top r_def)
   7.221 @@ -885,12 +885,12 @@
   7.222                   dualA_iff A_def dualPO CL_dualCL CLF_dual)
   7.223  done
   7.224  
   7.225 -ML_command{*AtpThread.problem_name:="Tarski__Bot_in_lattice"*}  (*ALL THEOREMS*)
   7.226 +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_in_lattice"*}  (*ALL THEOREMS*)
   7.227  lemma (in CLF) Top_intv_not_empty: "x \<in> A  ==> interval r x (Top cl) \<noteq> {}" 
   7.228  apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE)
   7.229  done
   7.230  
   7.231 -ML_command{*AtpThread.problem_name:="Tarski__Bot_intv_not_empty"*}  (*ALL THEOREMS*)
   7.232 +ML_command{*AtpWrapper.problem_name:="Tarski__Bot_intv_not_empty"*}  (*ALL THEOREMS*)
   7.233  lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}" 
   7.234  apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem)
   7.235  done
   7.236 @@ -902,7 +902,7 @@
   7.237  by (simp add: P_def fix_subset po_subset_po)
   7.238  
   7.239  (*first proved 2007-01-25 after relaxing relevance*)
   7.240 -ML_command{*AtpThread.problem_name:="Tarski__Y_subset_A"*}
   7.241 +ML_command{*AtpWrapper.problem_name:="Tarski__Y_subset_A"*}
   7.242    declare (in Tarski) P_def[simp] Y_ss [simp]
   7.243    declare fix_subset [intro] subset_trans [intro]
   7.244  lemma (in Tarski) Y_subset_A: "Y \<subseteq> A"
   7.245 @@ -918,7 +918,7 @@
   7.246    by (rule Y_subset_A [THEN lub_in_lattice])
   7.247  
   7.248  (*never proved, 2007-01-22*)
   7.249 -ML_command{*AtpThread.problem_name:="Tarski__lubY_le_flubY"*}  (*ALL THEOREMS*)
   7.250 +ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY"*}  (*ALL THEOREMS*)
   7.251  lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r"
   7.252  (*sledgehammer*) 
   7.253  apply (rule lub_least)
   7.254 @@ -927,12 +927,12 @@
   7.255  apply (rule lubY_in_A)
   7.256  -- {* @{text "Y \<subseteq> P ==> f x = x"} *}
   7.257  apply (rule ballI)
   7.258 -ML_command{*AtpThread.problem_name:="Tarski__lubY_le_flubY_simpler"*}  (*ALL THEOREMS*)
   7.259 +ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY_simpler"*}  (*ALL THEOREMS*)
   7.260  (*sledgehammer *)
   7.261  apply (rule_tac t = "x" in fix_imp_eq [THEN subst])
   7.262  apply (erule Y_ss [simplified P_def, THEN subsetD])
   7.263  -- {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *}
   7.264 -ML_command{*AtpThread.problem_name:="Tarski__lubY_le_flubY_simplest"*}  (*ALL THEOREMS*)
   7.265 +ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY_simplest"*}  (*ALL THEOREMS*)
   7.266  (*sledgehammer*)
   7.267  apply (rule_tac f = "f" in monotoneE)
   7.268  apply (rule monotone_f)
   7.269 @@ -942,7 +942,7 @@
   7.270  done
   7.271  
   7.272  (*first proved 2007-01-25 after relaxing relevance*)
   7.273 -ML_command{*AtpThread.problem_name:="Tarski__intY1_subset"*}  (*ALL THEOREMS*)
   7.274 +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_subset"*}  (*ALL THEOREMS*)
   7.275  lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A"
   7.276  (*sledgehammer*) 
   7.277  apply (unfold intY1_def)
   7.278 @@ -954,7 +954,7 @@
   7.279  lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD]
   7.280  
   7.281  (*never proved, 2007-01-22*)
   7.282 -ML_command{*AtpThread.problem_name:="Tarski__intY1_f_closed"*}  (*ALL THEOREMS*)
   7.283 +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_f_closed"*}  (*ALL THEOREMS*)
   7.284  lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1"
   7.285  (*sledgehammer*) 
   7.286  apply (simp add: intY1_def  interval_def)
   7.287 @@ -962,7 +962,7 @@
   7.288  apply (rule transE)
   7.289  apply (rule lubY_le_flubY)
   7.290  -- {* @{text "(f (lub Y cl), f x) \<in> r"} *}
   7.291 -ML_command{*AtpThread.problem_name:="Tarski__intY1_f_closed_simpler"*}  (*ALL THEOREMS*)
   7.292 +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_f_closed_simpler"*}  (*ALL THEOREMS*)
   7.293  (*sledgehammer [has been proved before now...]*)
   7.294  apply (rule_tac f=f in monotoneE)
   7.295  apply (rule monotone_f)
   7.296 @@ -975,13 +975,13 @@
   7.297  apply (simp add: intY1_def interval_def  intY1_elem)
   7.298  done
   7.299  
   7.300 -ML_command{*AtpThread.problem_name:="Tarski__intY1_func"*}  (*ALL THEOREMS*)
   7.301 +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_func"*}  (*ALL THEOREMS*)
   7.302  lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
   7.303  apply (rule restrict_in_funcset)
   7.304  apply (metis intY1_f_closed restrict_in_funcset)
   7.305  done
   7.306  
   7.307 -ML_command{*AtpThread.problem_name:="Tarski__intY1_mono"*}  (*ALL THEOREMS*)
   7.308 +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_mono"*}  (*ALL THEOREMS*)
   7.309  lemma (in Tarski) intY1_mono:
   7.310       "monotone (%x: intY1. f x) intY1 (induced intY1 r)"
   7.311  (*sledgehammer *)
   7.312 @@ -990,7 +990,7 @@
   7.313  done
   7.314  
   7.315  (*proof requires relaxing relevance: 2007-01-25*)
   7.316 -ML_command{*AtpThread.problem_name:="Tarski__intY1_is_cl"*}  (*ALL THEOREMS*)
   7.317 +ML_command{*AtpWrapper.problem_name:="Tarski__intY1_is_cl"*}  (*ALL THEOREMS*)
   7.318  lemma (in Tarski) intY1_is_cl:
   7.319      "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice"
   7.320  (*sledgehammer*) 
   7.321 @@ -1003,7 +1003,7 @@
   7.322  done
   7.323  
   7.324  (*never proved, 2007-01-22*)
   7.325 -ML_command{*AtpThread.problem_name:="Tarski__v_in_P"*}  (*ALL THEOREMS*)
   7.326 +ML_command{*AtpWrapper.problem_name:="Tarski__v_in_P"*}  (*ALL THEOREMS*)
   7.327  lemma (in Tarski) v_in_P: "v \<in> P"
   7.328  (*sledgehammer*) 
   7.329  apply (unfold P_def)
   7.330 @@ -1013,7 +1013,7 @@
   7.331                   v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono)
   7.332  done
   7.333  
   7.334 -ML_command{*AtpThread.problem_name:="Tarski__z_in_interval"*}  (*ALL THEOREMS*)
   7.335 +ML_command{*AtpWrapper.problem_name:="Tarski__z_in_interval"*}  (*ALL THEOREMS*)
   7.336  lemma (in Tarski) z_in_interval:
   7.337       "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1"
   7.338  (*sledgehammer *)
   7.339 @@ -1027,14 +1027,14 @@
   7.340  apply (simp add: induced_def)
   7.341  done
   7.342  
   7.343 -ML_command{*AtpThread.problem_name:="Tarski__fz_in_int_rel"*}  (*ALL THEOREMS*)
   7.344 +ML_command{*AtpWrapper.problem_name:="Tarski__fz_in_int_rel"*}  (*ALL THEOREMS*)
   7.345  lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
   7.346        ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" 
   7.347  apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval)
   7.348  done
   7.349  
   7.350  (*never proved, 2007-01-22*)
   7.351 -ML_command{*AtpThread.problem_name:="Tarski__tarski_full_lemma"*}  (*ALL THEOREMS*)
   7.352 +ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma"*}  (*ALL THEOREMS*)
   7.353  lemma (in Tarski) tarski_full_lemma:
   7.354       "\<exists>L. isLub Y (| pset = P, order = induced P r |) L"
   7.355  apply (rule_tac x = "v" in exI)
   7.356 @@ -1064,12 +1064,12 @@
   7.357   prefer 2 apply (simp add: v_in_P)
   7.358  apply (unfold v_def)
   7.359  (*never proved, 2007-01-22*)
   7.360 -ML_command{*AtpThread.problem_name:="Tarski__tarski_full_lemma_simpler"*} 
   7.361 +ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma_simpler"*} 
   7.362  (*sledgehammer*) 
   7.363  apply (rule indE)
   7.364  apply (rule_tac [2] intY1_subset)
   7.365  (*never proved, 2007-01-22*)
   7.366 -ML_command{*AtpThread.problem_name:="Tarski__tarski_full_lemma_simplest"*} 
   7.367 +ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma_simplest"*} 
   7.368  (*sledgehammer*) 
   7.369  apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
   7.370    apply (simp add: CL_imp_PO intY1_is_cl)
   7.371 @@ -1087,7 +1087,7 @@
   7.372  
   7.373  
   7.374  (*never proved, 2007-01-22*)
   7.375 -ML_command{*AtpThread.problem_name:="Tarski__Tarski_full"*}
   7.376 +ML_command{*AtpWrapper.problem_name:="Tarski__Tarski_full"*}
   7.377    declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp]
   7.378                 Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro]
   7.379                 CompleteLatticeI_simp [intro]
   7.380 @@ -1097,7 +1097,7 @@
   7.381  apply (rule CompleteLatticeI_simp)
   7.382  apply (rule fixf_po, clarify)
   7.383  (*never proved, 2007-01-22*)
   7.384 -ML_command{*AtpThread.problem_name:="Tarski__Tarski_full_simpler"*}
   7.385 +ML_command{*AtpWrapper.problem_name:="Tarski__Tarski_full_simpler"*}
   7.386  (*sledgehammer*) 
   7.387  apply (simp add: P_def A_def r_def)
   7.388  apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
     8.1 --- a/src/HOL/MetisExamples/TransClosure.thy	Tue Oct 14 15:45:46 2008 +0200
     8.2 +++ b/src/HOL/MetisExamples/TransClosure.thy	Tue Oct 14 16:01:36 2008 +0200
     8.3 @@ -22,7 +22,7 @@
     8.4  
     8.5  consts f:: "addr \<Rightarrow> val"
     8.6  
     8.7 -ML {*AtpThread.problem_name := "TransClosure__test"*}
     8.8 +ML {*AtpWrapper.problem_name := "TransClosure__test"*}
     8.9  lemma "\<lbrakk> f c = Intg x; \<forall> y. f b = Intg y \<longrightarrow> y \<noteq> x; (a,b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>* \<rbrakk> 
    8.10     \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"  
    8.11  by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
    8.12 @@ -51,7 +51,7 @@
    8.13    by (metis 10 3)
    8.14  qed
    8.15  
    8.16 -ML {*AtpThread.problem_name := "TransClosure__test_simpler"*}
    8.17 +ML {*AtpWrapper.problem_name := "TransClosure__test_simpler"*}
    8.18  lemma "\<lbrakk> f c = Intg x; \<forall> y. f b = Intg y \<longrightarrow> y \<noteq> x; (a,b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>* \<rbrakk> 
    8.19     \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
    8.20  apply (erule_tac x="b" in converse_rtranclE)
     9.1 --- a/src/HOL/MetisExamples/set.thy	Tue Oct 14 15:45:46 2008 +0200
     9.2 +++ b/src/HOL/MetisExamples/set.thy	Tue Oct 14 16:01:36 2008 +0200
     9.3 @@ -198,7 +198,7 @@
     9.4    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)
     9.5  qed 
     9.6  
     9.7 -ML {*AtpThread.problem_name := "set__equal_union"*}
     9.8 +ML {*AtpWrapper.problem_name := "set__equal_union"*}
     9.9  lemma (*equal_union: *)
    9.10     "(X = Y \<union> Z) =
    9.11      (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" 
    9.12 @@ -206,12 +206,12 @@
    9.13  by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
    9.14  
    9.15  
    9.16 -ML {*AtpThread.problem_name := "set__equal_inter"*}
    9.17 +ML {*AtpWrapper.problem_name := "set__equal_inter"*}
    9.18  lemma "(X = Y \<inter> Z) =
    9.19      (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
    9.20  by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset)
    9.21  
    9.22 -ML {*AtpThread.problem_name := "set__fixedpoint"*}
    9.23 +ML {*AtpWrapper.problem_name := "set__fixedpoint"*}
    9.24  lemma fixedpoint:
    9.25      "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
    9.26  by metis
    9.27 @@ -230,7 +230,7 @@
    9.28    by (metis 4 0)
    9.29  qed
    9.30  
    9.31 -ML {*AtpThread.problem_name := "set__singleton_example"*}
    9.32 +ML {*AtpWrapper.problem_name := "set__singleton_example"*}
    9.33  lemma (*singleton_example_2:*)
    9.34       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    9.35  by (metis Set.subsetI Union_upper insertCI set_eq_subset)
    9.36 @@ -260,7 +260,7 @@
    9.37    293-314.
    9.38  *}
    9.39  
    9.40 -ML {*AtpThread.problem_name := "set__Bledsoe_Fung"*}
    9.41 +ML {*AtpWrapper.problem_name := "set__Bledsoe_Fung"*}
    9.42  (*Notes: 1, the numbering doesn't completely agree with the paper. 
    9.43  2, we must rename set variables to avoid type clashes.*)
    9.44  lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
    10.1 --- a/src/HOL/Tools/atp_thread.ML	Tue Oct 14 15:45:46 2008 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,150 +0,0 @@
    10.4 -(*  Title:      HOL/Tools/atp_thread.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Fabian Immler, TU Muenchen
    10.7 -
    10.8 -Automatic provers as managed threads.
    10.9 -*)
   10.10 -
   10.11 -signature ATP_THREAD =
   10.12 -sig
   10.13 -  (* hooks for writing problemfiles *)
   10.14 -  val destdir: string ref
   10.15 -  val problem_name: string ref
   10.16 -  (* basic template *)
   10.17 -  val external_prover:
   10.18 -    ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
   10.19 -    Path.T * string ->
   10.20 -    (string * int -> bool) ->
   10.21 -    (string * string vector * Proof.context * thm * int -> string) ->
   10.22 -    int -> Proof.state -> Thread.thread
   10.23 -  (* provers as functions returning threads *)
   10.24 -  val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
   10.25 -  val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
   10.26 -  val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread
   10.27 -  val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
   10.28 -  val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread
   10.29 -  val remote_prover: string -> string -> int -> Proof.state -> Thread.thread
   10.30 -  val full_prover: Path.T * string  -> int -> Proof.state -> Thread.thread
   10.31 -  val spass_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
   10.32 -  val eprover_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
   10.33 -  val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
   10.34 -  val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread
   10.35 -  val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
   10.36 -  val spass: int -> Proof.state -> Thread.thread
   10.37 -  val eprover: int -> Proof.state -> Thread.thread
   10.38 -  val eprover_full: int -> Proof.state -> Thread.thread
   10.39 -  val vampire: int -> Proof.state -> Thread.thread
   10.40 -  val vampire_full: int -> Proof.state -> Thread.thread
   10.41 -end;
   10.42 -
   10.43 -structure AtpThread : ATP_THREAD =
   10.44 -struct
   10.45 -  
   10.46 -  (* preferences for path and filename to problemfiles *)
   10.47 -  val destdir = ref "";   (*Empty means write files to /tmp*)
   10.48 -  val problem_name = ref "prob";
   10.49 -      
   10.50 -  (*Setting up a Thread for an external prover*)
   10.51 -  fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
   10.52 -    let
   10.53 -    val destdir' = ! destdir
   10.54 -    val problem_name' = ! problem_name
   10.55 -    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
   10.56 -    (* path to unique problem file *)
   10.57 -    fun prob_pathname nr =
   10.58 -      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr)
   10.59 -      in if destdir' = "" then File.tmp_path probfile
   10.60 -        else if File.exists (Path.explode (destdir'))
   10.61 -        then Path.append  (Path.explode (destdir')) probfile
   10.62 -        else error ("No such directory: " ^ destdir')
   10.63 -      end
   10.64 -    (* write out problem file and call prover *)
   10.65 -    fun call_prover () =
   10.66 -      let
   10.67 -      val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
   10.68 -      val (filenames, thm_names_list) =
   10.69 -        write_problem_files prob_pathname (ctxt, chain_ths, goal)
   10.70 -      val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*)
   10.71 -
   10.72 -      val cmdline =
   10.73 -        if File.exists cmd then File.shell_path cmd ^ " " ^ args
   10.74 -        else error ("Bad executable: " ^ Path.implode cmd);
   10.75 -      val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1))
   10.76 -      val _ =
   10.77 -        if rc <> 0
   10.78 -        then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc)
   10.79 -        else ()
   10.80 -      (* remove *temporary* files *)
   10.81 -      val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else ()
   10.82 -      in
   10.83 -        if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)
   10.84 -        else NONE
   10.85 -      end
   10.86 -    in
   10.87 -      AtpManager.atp_thread call_prover produce_answer
   10.88 -    end;
   10.89 -
   10.90 -    
   10.91 -  (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)
   10.92 -
   10.93 -  fun tptp_prover_filter_opts_full max_new theory_const full command sg =
   10.94 -    external_prover
   10.95 -    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
   10.96 -    command
   10.97 -    ResReconstruct.check_success_e_vamp_spass
   10.98 -    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
   10.99 -    sg
  10.100 -    
  10.101 -  (* arbitrary atp with tptp input/output and problemfile as last argument*)
  10.102 -  fun tptp_prover_filter_opts max_new theory_const =
  10.103 -    tptp_prover_filter_opts_full max_new theory_const false;
  10.104 -  (* default settings*)  
  10.105 -  val tptp_prover = tptp_prover_filter_opts 60 true;
  10.106 -
  10.107 -  (* for structured proofs: prover must support TSTP *)
  10.108 -  fun full_prover_filter_opts max_new theory_const =
  10.109 -    tptp_prover_filter_opts_full max_new theory_const true;
  10.110 -  (* default settings*)
  10.111 -  val full_prover = full_prover_filter_opts 60 true;
  10.112 -
  10.113 -  fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts
  10.114 -    max_new theory_const
  10.115 -    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
  10.116 -  (* default settings*)
  10.117 -  val vampire = vampire_filter_opts 60 false;
  10.118 -    
  10.119 -  (* a vampire for full proof output *)
  10.120 -  fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts
  10.121 -    max_new theory_const
  10.122 -    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
  10.123 -  (* default settings*)
  10.124 -  val vampire_full = vampire_filter_opts 60 false;
  10.125 -
  10.126 -  fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts
  10.127 -    max_new theory_const
  10.128 -    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
  10.129 -  (* default settings *)
  10.130 -  val eprover = eprover_filter_opts 100 false;
  10.131 -    
  10.132 -  (* an E for full proof output*)
  10.133 -  fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts
  10.134 -    max_new theory_const
  10.135 -    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
  10.136 -  (* default settings *)
  10.137 -  val eprover_full = eprover_filter_opts_full 100 false;
  10.138 -
  10.139 -  fun spass_filter_opts max_new theory_const = external_prover
  10.140 -    (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
  10.141 -    (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
  10.142 -    ResReconstruct.check_success_e_vamp_spass
  10.143 -    ResReconstruct.lemma_list_dfg
  10.144 -  (* default settings*)
  10.145 -  val spass = spass_filter_opts 40 true;
  10.146 -    
  10.147 -  (* remote prover invocation via SystemOnTPTP *)
  10.148 -  fun remote_prover_filter_opts max_new theory_const name command =
  10.149 -    tptp_prover_filter_opts max_new theory_const
  10.150 -    (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command)
  10.151 -  val remote_prover = remote_prover_filter_opts 60 false
  10.152 -
  10.153 -end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Tue Oct 14 16:01:36 2008 +0200
    11.3 @@ -0,0 +1,150 @@
    11.4 +(*  Title:      HOL/Tools/atp_wrapper.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Fabian Immler, TU Muenchen
    11.7 +
    11.8 +Wrapper functions for external ATPs.
    11.9 +*)
   11.10 +
   11.11 +signature ATP_WRAPPER =
   11.12 +sig
   11.13 +  (* hooks for writing problemfiles *)
   11.14 +  val destdir: string ref
   11.15 +  val problem_name: string ref
   11.16 +  (* basic template *)
   11.17 +  val external_prover:
   11.18 +    ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
   11.19 +    Path.T * string ->
   11.20 +    (string * int -> bool) ->
   11.21 +    (string * string vector * Proof.context * thm * int -> string) ->
   11.22 +    int -> Proof.state -> Thread.thread
   11.23 +  (* provers as functions returning threads *)
   11.24 +  val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
   11.25 +  val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
   11.26 +  val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread
   11.27 +  val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
   11.28 +  val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread
   11.29 +  val remote_prover: string -> string -> int -> Proof.state -> Thread.thread
   11.30 +  val full_prover: Path.T * string  -> int -> Proof.state -> Thread.thread
   11.31 +  val spass_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
   11.32 +  val eprover_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
   11.33 +  val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
   11.34 +  val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread
   11.35 +  val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
   11.36 +  val spass: int -> Proof.state -> Thread.thread
   11.37 +  val eprover: int -> Proof.state -> Thread.thread
   11.38 +  val eprover_full: int -> Proof.state -> Thread.thread
   11.39 +  val vampire: int -> Proof.state -> Thread.thread
   11.40 +  val vampire_full: int -> Proof.state -> Thread.thread
   11.41 +end;
   11.42 +
   11.43 +structure AtpWrapper: ATP_WRAPPER =
   11.44 +struct
   11.45 +  
   11.46 +  (* preferences for path and filename to problemfiles *)
   11.47 +  val destdir = ref "";   (*Empty means write files to /tmp*)
   11.48 +  val problem_name = ref "prob";
   11.49 +      
   11.50 +  (*Setting up a Thread for an external prover*)
   11.51 +  fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
   11.52 +    let
   11.53 +    val destdir' = ! destdir
   11.54 +    val problem_name' = ! problem_name
   11.55 +    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
   11.56 +    (* path to unique problem file *)
   11.57 +    fun prob_pathname nr =
   11.58 +      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr)
   11.59 +      in if destdir' = "" then File.tmp_path probfile
   11.60 +        else if File.exists (Path.explode (destdir'))
   11.61 +        then Path.append  (Path.explode (destdir')) probfile
   11.62 +        else error ("No such directory: " ^ destdir')
   11.63 +      end
   11.64 +    (* write out problem file and call prover *)
   11.65 +    fun call_prover () =
   11.66 +      let
   11.67 +      val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
   11.68 +      val (filenames, thm_names_list) =
   11.69 +        write_problem_files prob_pathname (ctxt, chain_ths, goal)
   11.70 +      val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*)
   11.71 +
   11.72 +      val cmdline =
   11.73 +        if File.exists cmd then File.shell_path cmd ^ " " ^ args
   11.74 +        else error ("Bad executable: " ^ Path.implode cmd);
   11.75 +      val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1))
   11.76 +      val _ =
   11.77 +        if rc <> 0
   11.78 +        then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc)
   11.79 +        else ()
   11.80 +      (* remove *temporary* files *)
   11.81 +      val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else ()
   11.82 +      in
   11.83 +        if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)
   11.84 +        else NONE
   11.85 +      end
   11.86 +    in
   11.87 +      AtpManager.atp_thread call_prover produce_answer
   11.88 +    end;
   11.89 +
   11.90 +    
   11.91 +  (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)
   11.92 +
   11.93 +  fun tptp_prover_filter_opts_full max_new theory_const full command sg =
   11.94 +    external_prover
   11.95 +    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
   11.96 +    command
   11.97 +    ResReconstruct.check_success_e_vamp_spass
   11.98 +    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
   11.99 +    sg
  11.100 +    
  11.101 +  (* arbitrary atp with tptp input/output and problemfile as last argument*)
  11.102 +  fun tptp_prover_filter_opts max_new theory_const =
  11.103 +    tptp_prover_filter_opts_full max_new theory_const false;
  11.104 +  (* default settings*)  
  11.105 +  val tptp_prover = tptp_prover_filter_opts 60 true;
  11.106 +
  11.107 +  (* for structured proofs: prover must support TSTP *)
  11.108 +  fun full_prover_filter_opts max_new theory_const =
  11.109 +    tptp_prover_filter_opts_full max_new theory_const true;
  11.110 +  (* default settings*)
  11.111 +  val full_prover = full_prover_filter_opts 60 true;
  11.112 +
  11.113 +  fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts
  11.114 +    max_new theory_const
  11.115 +    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
  11.116 +  (* default settings*)
  11.117 +  val vampire = vampire_filter_opts 60 false;
  11.118 +    
  11.119 +  (* a vampire for full proof output *)
  11.120 +  fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts
  11.121 +    max_new theory_const
  11.122 +    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
  11.123 +  (* default settings*)
  11.124 +  val vampire_full = vampire_filter_opts 60 false;
  11.125 +
  11.126 +  fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts
  11.127 +    max_new theory_const
  11.128 +    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
  11.129 +  (* default settings *)
  11.130 +  val eprover = eprover_filter_opts 100 false;
  11.131 +    
  11.132 +  (* an E for full proof output*)
  11.133 +  fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts
  11.134 +    max_new theory_const
  11.135 +    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
  11.136 +  (* default settings *)
  11.137 +  val eprover_full = eprover_filter_opts_full 100 false;
  11.138 +
  11.139 +  fun spass_filter_opts max_new theory_const = external_prover
  11.140 +    (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
  11.141 +    (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
  11.142 +    ResReconstruct.check_success_e_vamp_spass
  11.143 +    ResReconstruct.lemma_list_dfg
  11.144 +  (* default settings*)
  11.145 +  val spass = spass_filter_opts 40 true;
  11.146 +    
  11.147 +  (* remote prover invocation via SystemOnTPTP *)
  11.148 +  fun remote_prover_filter_opts max_new theory_const name command =
  11.149 +    tptp_prover_filter_opts max_new theory_const
  11.150 +    (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command)
  11.151 +  val remote_prover = remote_prover_filter_opts 60 false
  11.152 +
  11.153 +end;