removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
authorpaulson
Thu Sep 27 17:55:28 2007 +0200 (2007-09-27)
changeset 2474273b8b42a36b6
parent 24741 a53f5db5acbb
child 24743 cfcdb9817c49
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions
src/HOL/ATP_Linkup.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Complex/ex/NSPrimes.thy
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/IOA/IOA.thy
src/HOL/Main.thy
src/HOL/MetisExamples/Abstraction.thy
src/HOL/MetisExamples/set.thy
src/HOL/PreList.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_axioms.ML
src/HOL/W0/W0.thy
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/ATP_Linkup.thy	Thu Sep 27 17:28:05 2007 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Thu Sep 27 17:55:28 2007 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  header{* The Isabelle-ATP Linkup *}
     1.5  
     1.6  theory ATP_Linkup
     1.7 -imports Divides Record Hilbert_Choice
     1.8 +imports Divides Record Hilbert_Choice Presburger Relation_Power SAT Recdef Extraction 
     1.9 +   (*It must be a parent or a child of every other theory, to prevent theory-merge errors.*)
    1.10  uses
    1.11    "Tools/polyhash.ML"
    1.12    "Tools/res_clause.ML"
    1.13 @@ -110,4 +111,11 @@
    1.14  use "Tools/metis_tools.ML"
    1.15  setup MetisTools.setup
    1.16  
    1.17 +(*Sledgehammer*)
    1.18 +setup ResAxioms.setup
    1.19 +
    1.20 +setup {*
    1.21 +  Theory.at_end ResAxioms.clause_cache_endtheory
    1.22 +*}
    1.23 +
    1.24  end
     2.1 --- a/src/HOL/Algebra/Exponent.thy	Thu Sep 27 17:28:05 2007 +0200
     2.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu Sep 27 17:55:28 2007 +0200
     2.3 @@ -205,15 +205,10 @@
     2.4  apply (rule notnotD)
     2.5  apply (rule notI)
     2.6  apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
     2.7 -apply (drule_tac m = a in less_imp_le)
     2.8 +apply (drule less_imp_le [of a])
     2.9  apply (drule le_imp_power_dvd)
    2.10  apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
    2.11 -apply (frule_tac m = k in less_imp_le)
    2.12 -apply (drule_tac c = m in le_extend_mult, assumption)
    2.13 -apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
    2.14 -prefer 2 apply assumption
    2.15 -apply (rule dvd_refl [THEN dvd_mult2])
    2.16 -apply (drule_tac n = k in dvd_imp_le, auto)
    2.17 +apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less)
    2.18  done
    2.19  
    2.20  lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]  
     3.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Thu Sep 27 17:28:05 2007 +0200
     3.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Thu Sep 27 17:55:28 2007 +0200
     3.3 @@ -44,7 +44,7 @@
     3.4       [| deg p <= deg r; deg q <= deg r;  
     3.5          coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==>  
     3.6       deg (p + q) < deg r"
     3.7 -  apply (rule_tac j = "deg r - 1" in le_less_trans)
     3.8 +  apply (rule le_less_trans [of _ "deg r - 1"])
     3.9     prefer 2
    3.10     apply arith
    3.11    apply (rule deg_aboveI)
    3.12 @@ -248,13 +248,8 @@
    3.13       f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);  
    3.14       f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"
    3.15    apply (subgoal_tac "q1 = q2")
    3.16 -   apply clarify
    3.17 -   apply (rule_tac a = "q2 * g + r1 - q2 * g" and b = "q2 * g + r2 - q2 * g" in box_equals)
    3.18 -     apply simp
    3.19 -    apply (simp (no_asm))
    3.20 -   apply (simp (no_asm))
    3.21 -  apply (rule long_div_quo_unique)
    3.22 -  apply assumption+
    3.23 +   apply (metis a_comm a_lcancel m_comm)
    3.24 +  apply (metis a_comm l_zero long_div_quo_unique m_comm conc)
    3.25    done
    3.26  
    3.27  end
     4.1 --- a/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 27 17:28:05 2007 +0200
     4.2 +++ b/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 27 17:55:28 2007 +0200
     4.3 @@ -215,8 +215,7 @@
     4.4  apply (rule inj_onI)
     4.5  apply (rule ccontr, auto)
     4.6  apply (drule injf_max_order_preserving2)
     4.7 -apply (cut_tac m = x and n = y in less_linear, auto)
     4.8 -apply (auto dest!: spec)
     4.9 +apply (metis linorder_antisym_conv3 order_less_le)
    4.10  done
    4.11  
    4.12  lemma infinite_set_has_order_preserving_inj:
     5.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Thu Sep 27 17:28:05 2007 +0200
     5.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Thu Sep 27 17:55:28 2007 +0200
     5.3 @@ -185,7 +185,7 @@
     5.4    apply (erule_tac x=i in allE , erule (1) notE impE)
     5.5    apply simp
     5.6    apply clarify
     5.7 -  apply (drule le_imp_less_or_eq)
     5.8 +  apply (drule Nat.le_imp_less_or_eq)
     5.9    apply (erule disjE)
    5.10     apply (subgoal_tac "Suc (ind x)\<le>r")
    5.11      apply fast
    5.12 @@ -276,7 +276,7 @@
    5.13     apply (erule_tac x=i in allE , erule (1) notE impE)
    5.14     apply simp
    5.15     apply clarify
    5.16 -   apply (drule le_imp_less_or_eq)
    5.17 +   apply (drule Nat.le_imp_less_or_eq)
    5.18     apply (erule disjE)
    5.19      apply (subgoal_tac "Suc (ind x)\<le>r")
    5.20       apply fast
    5.21 @@ -309,7 +309,7 @@
    5.22   apply (erule_tac x=i in allE , erule (1) notE impE)
    5.23   apply simp
    5.24   apply clarify
    5.25 - apply (drule le_imp_less_or_eq)
    5.26 + apply (drule Nat.le_imp_less_or_eq)
    5.27   apply (erule disjE)
    5.28    apply (subgoal_tac "Suc (ind x)\<le>r")
    5.29     apply fast
     6.1 --- a/src/HOL/HoareParallel/Graph.thy	Thu Sep 27 17:28:05 2007 +0200
     6.2 +++ b/src/HOL/HoareParallel/Graph.thy	Thu Sep 27 17:55:28 2007 +0200
     6.3 @@ -1,4 +1,3 @@
     6.4 -
     6.5  header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms}
     6.6  
     6.7  \section {Formalization of the Memory} *}
     6.8 @@ -337,7 +336,7 @@
     6.9   apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
    6.10   apply simp
    6.11   apply(case_tac "j\<le>R")
    6.12 -  apply(drule le_imp_less_or_eq)
    6.13 +  apply(drule Nat.le_imp_less_or_eq)
    6.14    apply(erule disjE)
    6.15     apply(erule allE , erule (1) notE impE)
    6.16     apply force
     7.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu Sep 27 17:28:05 2007 +0200
     7.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu Sep 27 17:55:28 2007 +0200
     7.3 @@ -383,8 +383,7 @@
     7.4  apply force
     7.5  --{* 1 subgoal left *}
     7.6  apply clarify
     7.7 -apply(drule le_imp_less_or_eq)
     7.8 -apply(disjE_tac)
     7.9 +apply(drule Nat.le_imp_less_or_eq)
    7.10  apply (simp_all add:Blacks_def)
    7.11  done
    7.12  
     8.1 --- a/src/HOL/Hyperreal/Integration.thy	Thu Sep 27 17:28:05 2007 +0200
     8.2 +++ b/src/HOL/Hyperreal/Integration.thy	Thu Sep 27 17:55:28 2007 +0200
     8.3 @@ -553,18 +553,15 @@
     8.4  done
     8.5  
     8.6  lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n"
     8.7 -apply (cut_tac m = n and n = "psize D" in less_linear, auto)
     8.8 -apply (cut_tac m = m and n = n in less_linear)
     8.9 -apply (cut_tac m = m and n = "psize D" in less_linear)
    8.10 +apply (cut_tac less_linear [of n "psize D"], auto)
    8.11 +apply (cut_tac less_linear [of m n])
    8.12 +apply (cut_tac less_linear [of m "psize D"])
    8.13  apply (auto dest: partition_gt)
    8.14  apply (drule_tac n = m in partition_lt_gen, auto)
    8.15  apply (frule partition_eq_bound)
    8.16  apply (drule_tac [2] partition_gt, auto)
    8.17 -apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
    8.18 -apply (auto dest: partition_eq_bound)
    8.19 -apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
    8.20 -apply (frule partition_eq_bound, assumption)
    8.21 -apply (drule_tac m = m in partition_eq_bound, auto)
    8.22 +apply (metis dense_linear_order_class.dlo_simps(8) le_def partition_rhs partition_rhs2)
    8.23 +apply (metis Nat.le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
    8.24  done
    8.25  
    8.26  lemma lemma_additivity4_psize_eq:
    8.27 @@ -577,7 +574,7 @@
    8.28  apply (auto intro: partition_lt_Suc)
    8.29  apply (drule_tac n = n in partition_lt_gen, assumption)
    8.30  apply (arith, arith)
    8.31 -apply (cut_tac m = na and n = "psize D" in less_linear)
    8.32 +apply (cut_tac m = na and n = "psize D" in Nat.less_linear)
    8.33  apply (auto dest: partition_lt_cancel)
    8.34  apply (rule_tac x=N and y=n in linorder_cases)
    8.35  apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
    8.36 @@ -609,12 +606,8 @@
    8.37       "[| partition(a,b) D; D na < D n; D n < D (Suc na);
    8.38           n < psize D |]
    8.39        ==> False"
    8.40 -apply (cut_tac m = n and n = "Suc na" in less_linear, auto)
    8.41 -apply (drule_tac [2] n = n in partition_lt_gen, auto)
    8.42 -apply (cut_tac m = "psize D" and n = na in less_linear)
    8.43 -apply (auto simp add: partition_rhs2 less_Suc_eq)
    8.44 -apply (drule_tac n = na in partition_lt_gen, auto)
    8.45 -done
    8.46 +by (metis not_less_eq partition_lt_cancel real_of_nat_less_iff)
    8.47 +
    8.48  
    8.49  lemma psize_const [simp]: "psize (%x. k) = 0"
    8.50  by (auto simp add: psize_def)
     9.1 --- a/src/HOL/Hyperreal/Poly.thy	Thu Sep 27 17:28:05 2007 +0200
     9.2 +++ b/src/HOL/Hyperreal/Poly.thy	Thu Sep 27 17:55:28 2007 +0200
     9.3 @@ -739,10 +739,7 @@
     9.4        ==> EX! n. ([-a, 1] %^ n) divides p &
     9.5                   ~(([-a, 1] %^ (Suc n)) divides p)"
     9.6  apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
     9.7 -apply (cut_tac m = y and n = n in less_linear)
     9.8 -apply (drule_tac m = n in poly_exp_divides)
     9.9 -apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
    9.10 -            simp del: pmult_Cons pexp_Suc)
    9.11 +apply (metis Suc_leI Nat.less_linear poly_exp_divides)
    9.12  done
    9.13  
    9.14  text{*Order*}
    10.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 27 17:28:05 2007 +0200
    10.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 27 17:55:28 2007 +0200
    10.3 @@ -348,8 +348,8 @@
    10.4  
    10.5  instance star :: (semiring_0_cancel) semiring_0_cancel ..
    10.6  
    10.7 -instance star :: (comm_semiring) comm_semiring
    10.8 -by (intro_classes, transfer, rule distrib)
    10.9 +instance star :: (comm_semiring) comm_semiring 
   10.10 +by (intro_classes, transfer, rule left_distrib)
   10.11  
   10.12  instance star :: (comm_semiring_0) comm_semiring_0 ..
   10.13  instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
    11.1 --- a/src/HOL/IOA/IOA.thy	Thu Sep 27 17:28:05 2007 +0200
    11.2 +++ b/src/HOL/IOA/IOA.thy	Thu Sep 27 17:55:28 2007 +0200
    11.3 @@ -251,9 +251,7 @@
    11.4     apply (rule_tac x = "Suc n" in exI)
    11.5     apply (simp (no_asm))
    11.6    apply simp
    11.7 -  apply (rule allI)
    11.8 -  apply (cut_tac m = "na" and n = "n" in less_linear)
    11.9 -  apply auto
   11.10 +  apply (metis ioa_triple_proj less_antisym)
   11.11    done
   11.12  
   11.13  
    12.1 --- a/src/HOL/Main.thy	Thu Sep 27 17:28:05 2007 +0200
    12.2 +++ b/src/HOL/Main.thy	Thu Sep 27 17:55:28 2007 +0200
    12.3 @@ -11,14 +11,8 @@
    12.4  text {*
    12.5    Theory @{text Main} includes everything.  Note that theory @{text
    12.6    PreList} already includes most HOL theories.
    12.7 -
    12.8 -  \medskip Late clause setup: installs \emph{all} known theorems
    12.9 -  into the clause cache; cf.\ theory @{text ATP_Linkup}. 
   12.10 -  FIXME: delete once @{text end_theory} actions are installed!
   12.11  *}
   12.12  
   12.13 -setup ResAxioms.clause_cache_setup
   12.14 -
   12.15  ML {* val HOL_proofs = !proofs *}
   12.16  
   12.17  end
    13.1 --- a/src/HOL/MetisExamples/Abstraction.thy	Thu Sep 27 17:28:05 2007 +0200
    13.2 +++ b/src/HOL/MetisExamples/Abstraction.thy	Thu Sep 27 17:55:28 2007 +0200
    13.3 @@ -90,13 +90,20 @@
    13.4  apply (metis Collect_mem_eq SigmaD2);
    13.5  done
    13.6  
    13.7 -lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"proof (neg_clausify)
    13.8 -assume 0: "(cl, f) \<in> CLF"
    13.9 -assume 1: "CLF = Sigma CL llabs_subgoal_1"
   13.10 -assume 2: "\<And>cl. llabs_subgoal_1 cl = Collect (llabs_Predicate_Xsup_Un_eq_1_ (pset cl))"
   13.11 -assume 3: "f \<notin> pset cl"
   13.12 +lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
   13.13 +proof (neg_clausify)
   13.14 +assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
   13.15 +   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
   13.16 +   Collect (llabs_Set_XCollect_ex_eq_3_ op \<in> (pset cl))"
   13.17 +assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
   13.18 +assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type) \<in> (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)"
   13.19 +have 3: "llabs_Predicate_Xsup_Un_eq2_1_ (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
   13.20 + (cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
   13.21 +  by (metis acc_def 2)
   13.22 +assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
   13.23 +Sigma (CL\<Colon>'a\<Colon>type set set) (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set)"
   13.24  show "False"
   13.25 -  by (metis 0 1 SigmaD2 3 2 Collect_mem_eq)
   13.26 +  by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2)
   13.27  qed finish_clausify (*ugly hack: combinators??*)
   13.28  
   13.29  ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
   13.30 @@ -110,15 +117,16 @@
   13.31      "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   13.32      f \<in> pset cl \<rightarrow> pset cl"
   13.33  proof (neg_clausify)
   13.34 -assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1"
   13.35 -assume 1: "\<And>cl. llabs_subgoal_1 cl =
   13.36 -     Collect
   13.37 -      (llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))))"
   13.38 -assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
   13.39 -have 3: "\<not> llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))) f"
   13.40 -  by (metis Collect_mem_eq 2)
   13.41 +assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
   13.42 +   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
   13.43 +   Collect
   13.44 +    (llabs_Set_XCollect_ex_eq_3_ op \<in> (Pi (pset cl) (COMBK (pset cl))))"
   13.45 +assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
   13.46 +assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
   13.47 +\<in> Sigma (CL\<Colon>'a\<Colon>type set set)
   13.48 +   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set)"
   13.49  show "False"
   13.50 -  by (metis acc_def 0 Collect_mem_eq SigmaD2 3 1 Collect_mem_eq)
   13.51 +  by (metis 1 Collect_mem_eq 0 SigmaD2 2)
   13.52  qed finish_clausify
   13.53      (*Hack to prevent the "Additional hypotheses" error*)
   13.54  
    14.1 --- a/src/HOL/MetisExamples/set.thy	Thu Sep 27 17:28:05 2007 +0200
    14.2 +++ b/src/HOL/MetisExamples/set.thy	Thu Sep 27 17:55:28 2007 +0200
    14.3 @@ -11,7 +11,7 @@
    14.4  
    14.5  lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
    14.6                 (S(x,y) | ~S(y,z) | Q(Z,Z))  &
    14.7 -               (Q(X,y) | ~Q(y,Z) | S(X,X))"
    14.8 +               (Q(X,y) | ~Q(y,Z) | S(X,X))" 
    14.9  by metis
   14.10  (*??But metis can't prove the single-step version...*)
   14.11  
    15.1 --- a/src/HOL/PreList.thy	Thu Sep 27 17:28:05 2007 +0200
    15.2 +++ b/src/HOL/PreList.thy	Thu Sep 27 17:55:28 2007 +0200
    15.3 @@ -7,7 +7,7 @@
    15.4  header {* A Basis for Building the Theory of Lists *}
    15.5  
    15.6  theory PreList
    15.7 -imports Presburger Relation_Power SAT Recdef Extraction Record ATP_Linkup
    15.8 +imports ATP_Linkup
    15.9  uses "Tools/function_package/lexicographic_order.ML"
   15.10       "Tools/function_package/fundef_datatype.ML"
   15.11  begin
   15.12 @@ -21,7 +21,4 @@
   15.13  setup LexicographicOrder.setup
   15.14  setup FundefDatatype.setup
   15.15  
   15.16 -(*Sledgehammer*)
   15.17 -setup ResAxioms.setup
   15.18 -
   15.19  end
    16.1 --- a/src/HOL/Tools/meson.ML	Thu Sep 27 17:28:05 2007 +0200
    16.2 +++ b/src/HOL/Tools/meson.ML	Thu Sep 27 17:55:28 2007 +0200
    16.3 @@ -209,10 +209,10 @@
    16.4  
    16.5  (*** The basic CNF transformation ***)
    16.6  
    16.7 -val max_clauses = ref 40;
    16.8 +val max_clauses = 40;
    16.9  
   16.10 -fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
   16.11 -fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
   16.12 +fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses;
   16.13 +fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses;
   16.14  
   16.15  (*Estimate the number of clauses in order to detect infeasible theorems*)
   16.16  fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
   16.17 @@ -239,7 +239,7 @@
   16.18  
   16.19  val nclauses = signed_nclauses true;
   16.20  
   16.21 -fun too_many_clauses t = nclauses t >= !max_clauses;
   16.22 +fun too_many_clauses t = nclauses t >= max_clauses;
   16.23  
   16.24  (*Replaces universally quantified variables by FREE variables -- because
   16.25    assumptions may not contain scheme variables.  Later, we call "generalize". *)
   16.26 @@ -396,7 +396,7 @@
   16.27        [] => false (*not a function type, OK*)
   16.28      | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
   16.29  
   16.30 -(*Raises an exception if any Vars in the theorem mention type bool.
   16.31 +(*Returns false if any Vars in the theorem mention type bool.
   16.32    Also rejects functions whose arguments are Booleans or other functions.*)
   16.33  fun is_fol_term thy t =
   16.34      Term.is_first_order ["all","All","Ex"] t andalso
    17.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Sep 27 17:28:05 2007 +0200
    17.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Sep 27 17:55:28 2007 +0200
    17.3 @@ -21,19 +21,13 @@
    17.4    val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
    17.5    val atpset_rules_of: Proof.context -> (string * thm) list
    17.6    val meson_method_setup: theory -> theory
    17.7 -  val clause_cache_setup: theory -> theory
    17.8 +  val clause_cache_endtheory: theory -> theory option
    17.9    val setup: theory -> theory
   17.10  end;
   17.11  
   17.12  structure ResAxioms: RES_AXIOMS =
   17.13  struct
   17.14  
   17.15 -(*For running the comparison between combinators and abstractions.
   17.16 -  CANNOT be a ref, as the setting is used while Isabelle is built.
   17.17 -  Currently TRUE: the combinator code cannot be used with proof reconstruction
   17.18 -  because it is not performed by inference!!*)
   17.19 -val abstract_lambdas = true;
   17.20 -
   17.21  (* FIXME legacy *)
   17.22  fun freeze_thm th = #1 (Drule.freeze_thaw th);
   17.23  
   17.24 @@ -74,22 +68,19 @@
   17.25             Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
   17.26      | _ => th;
   17.27  
   17.28 -(**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
   17.29 -
   17.30 -(*Transfer a theorem into theory ATP_Linkup.thy if it is not already
   17.31 -  inside that theory -- because it's needed for Skolemization *)
   17.32 -
   17.33 -(*This will refer to the final version of theory ATP_Linkup.*)
   17.34 -val recon_thy_ref = Theory.check_thy @{theory}
   17.35 -
   17.36 -(*If called while ATP_Linkup is being created, it will transfer to the
   17.37 -  current version. If called afterward, it will transfer to the final version.*)
   17.38 -fun transfer_to_ATP_Linkup th =
   17.39 -    transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
   17.40 -
   17.41 +(*To enforce single-threading*)
   17.42 +exception Clausify_failure of theory;
   17.43  
   17.44  (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
   17.45  
   17.46 +fun rhs_extra_types lhsT rhs =
   17.47 +  let val lhs_vars = Term.add_tfreesT lhsT []
   17.48 +      fun add_new_TFrees (TFree v) =
   17.49 +	    if member (op =) lhs_vars v then I else insert (op =) (TFree v)
   17.50 +	| add_new_TFrees _ = I
   17.51 +      val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
   17.52 +  in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
   17.53 +
   17.54  (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
   17.55    prefix for the Skolem constant. Result is a new theory*)
   17.56  fun declare_skofuns s th thy =
   17.57 @@ -97,18 +88,26 @@
   17.58        fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
   17.59              (*Existential: declare a Skolem function, then insert into body and continue*)
   17.60              let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref))
   17.61 -                val args = term_frees xtp  (*get the formal parameter list*)
   17.62 -                val Ts = map type_of args
   17.63 -                val cT = Ts ---> T
   17.64 +                val args0 = term_frees xtp  (*get the formal parameter list*)
   17.65 +                val Ts = map type_of args0
   17.66 +                val extraTs = rhs_extra_types (Ts ---> T) xtp
   17.67 +                val _ = if null extraTs then () else
   17.68 +                   warning ("Skolemization: extra type vars: " ^ 
   17.69 +                            commas_quote (map (Sign.string_of_typ thy) extraTs)); 
   17.70 +                val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
   17.71 +                val args = argsx @ args0
   17.72 +                val cT = extraTs ---> Ts ---> T
   17.73                  val c = Const (Sign.full_name thy cname, cT)
   17.74                  val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
   17.75                          (*Forms a lambda-abstraction over the formal parameters*)
   17.76 +                val _ = Output.debug (fn () => "declaring the constant " ^ cname)
   17.77                  val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
   17.78                             (*Theory is augmented with the constant, then its def*)
   17.79                  val cdef = cname ^ "_def"
   17.80                  val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
   17.81 +                            handle ERROR _ => raise Clausify_failure thy'
   17.82              in dec_sko (subst_bound (list_comb(c,args), p))
   17.83 -                       (thy'', get_axiom thy'' cdef :: axs)
   17.84 +			       (thy'', get_axiom thy'' cdef :: axs)
   17.85              end
   17.86          | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
   17.87              (*Universal quant: insert a free variable into body and continue*)
   17.88 @@ -280,6 +279,7 @@
   17.89                            val cdef = cname ^ "_def"
   17.90                            val thy = Theory.add_defs_i false false
   17.91                                         [(cdef, equals cT $ c $ rhs)] thy
   17.92 +                                    handle ERROR _ => raise Clausify_failure thy
   17.93                            val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef));
   17.94                            val ax = get_axiom thy cdef |> freeze_thm
   17.95                                       |> mk_object_eq |> strip_lambdas (length args)
   17.96 @@ -402,6 +402,17 @@
   17.97         |> Thm.varifyT
   17.98    end;
   17.99  
  17.100 +
  17.101 +(*This will refer to the final version of theory ATP_Linkup.*)
  17.102 +val atp_linkup_thy_ref = Theory.check_thy @{theory}
  17.103 +
  17.104 +(*Transfer a theorem into theory ATP_Linkup.thy if it is not already
  17.105 +  inside that theory -- because it's needed for Skolemization.
  17.106 +  If called while ATP_Linkup is being created, it will transfer to the
  17.107 +  current version. If called afterward, it will transfer to the final version.*)
  17.108 +fun transfer_to_ATP_Linkup th =
  17.109 +    transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
  17.110 +
  17.111  (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
  17.112  fun to_nnf th =
  17.113      th |> transfer_to_ATP_Linkup
  17.114 @@ -423,26 +434,21 @@
  17.115            |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
  17.116  
  17.117  (*Replace lambdas by assumed function definitions in the theorems*)
  17.118 -fun assume_abstract_list s ths =
  17.119 -  if abstract_lambdas then List.concat (map (assume_abstract s) ths)
  17.120 -  else map Drule.eta_contraction_rule ths;
  17.121 +fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths);
  17.122  
  17.123  (*Replace lambdas by declared function definitions in the theorems*)
  17.124 -fun declare_abstract' s (thy, []) = (thy, [])
  17.125 -  | declare_abstract' s (thy, th::ths) =
  17.126 +fun declare_abstract s (thy, []) = (thy, [])
  17.127 +  | declare_abstract s (thy, th::ths) =
  17.128        let val (thy', th_defs) =
  17.129              if lambda_free (prop_of th) then (thy, [th])
  17.130              else
  17.131                  th |> zero_var_indexes |> freeze_thm
  17.132                     |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s
  17.133 +                handle Clausify_failure thy_e => (thy_e,[])
  17.134            val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
  17.135 -          val (thy'', ths') = declare_abstract' s (thy', ths)
  17.136 +          val (thy'', ths') = declare_abstract (s^"'") (thy', ths)
  17.137        in  (thy'', th_defs @ ths')  end;
  17.138  
  17.139 -fun declare_abstract s (thy, ths) =
  17.140 -  if abstract_lambdas then declare_abstract' s (thy, ths)
  17.141 -  else (thy, map Drule.eta_contraction_rule ths);
  17.142 -
  17.143  (*Keep the full complexity of the original name*)
  17.144  fun flatten_name s = space_implode "_X" (NameSpace.explode s);
  17.145  
  17.146 @@ -450,6 +456,10 @@
  17.147    if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
  17.148    else gensym "unknown_thm_";
  17.149  
  17.150 +fun name_or_string th =
  17.151 +  if PureThy.has_name_hint th then PureThy.get_name_hint th
  17.152 +  else string_of_thm th;
  17.153 +
  17.154  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
  17.155  fun skolem_thm th =
  17.156    let val nnfth = to_nnf th and s = fake_name th
  17.157 @@ -461,62 +471,51 @@
  17.158    It returns a modified theory, unless skolemization fails.*)
  17.159  fun skolem thy th =
  17.160       Option.map
  17.161 -        (fn (nnfth, s) =>
  17.162 -          let val _ = Output.debug (fn () => "skolemizing " ^ s ^ ": ")
  17.163 +        (fn nnfth =>
  17.164 +          let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
  17.165 +              val _ = Output.debug (fn () => string_of_thm nnfth)
  17.166 +              val s = fake_name th
  17.167                val (thy',defs) = declare_skofuns s nnfth thy
  17.168                val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
  17.169 +              val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
  17.170                val (thy'',cnfs') = declare_abstract s (thy',cnfs)
  17.171 -          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'')
  17.172 -          end)
  17.173 -      (SOME (to_nnf th, fake_name th)  handle THM _ => NONE);
  17.174 +          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end
  17.175 +          handle Clausify_failure thy_e => ([],thy_e)
  17.176 +        )
  17.177 +      (try to_nnf th);
  17.178  
  17.179 +(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
  17.180 +  Skolem functions.*)
  17.181  structure ThmCache = TheoryDataFun
  17.182  (
  17.183 -  type T = (thm list) Thmtab.table ref;
  17.184 -  val empty : T = ref Thmtab.empty;
  17.185 -  fun copy (ref tab) : T = ref tab;
  17.186 +  type T = (thm list) Thmtab.table;
  17.187 +  val empty = Thmtab.empty;
  17.188 +  fun copy tab : T = tab;
  17.189    val extend = copy;
  17.190 -  fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
  17.191 +  fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2);
  17.192  );
  17.193  
  17.194 -(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
  17.195 -  Skolem functions. The global one holds theorems proved prior to this point. Theory data
  17.196 -  holds the remaining ones.*)
  17.197 -val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table);
  17.198 -
  17.199  (*Populate the clause cache using the supplied theorem. Return the clausal form
  17.200    and modified theory.*)
  17.201 -fun skolem_cache_thm clause_cache th thy =
  17.202 -  case Thmtab.lookup (!clause_cache) th of
  17.203 +fun skolem_cache_thm th thy =
  17.204 +  case Thmtab.lookup (ThmCache.get thy) th of
  17.205        NONE =>
  17.206          (case skolem thy (Thm.transfer thy th) of
  17.207               NONE => ([th],thy)
  17.208             | SOME (cls,thy') =>
  17.209 -                 (if null cls
  17.210 -                  then warning ("skolem_cache: empty clause set for " ^ string_of_thm th)
  17.211 -                  else ();
  17.212 -                  change clause_cache (Thmtab.update (th, cls));
  17.213 -                  (cls,thy')))
  17.214 +                 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ 
  17.215 +                                         " clauses inserted into cache: " ^ name_or_string th);
  17.216 +                  (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy')))
  17.217      | SOME cls => (cls,thy);
  17.218  
  17.219  (*Exported function to convert Isabelle theorems into axiom clauses*)
  17.220  fun cnf_axiom th =
  17.221 -  let val cache = ThmCache.get (Thm.theory_of_thm th)
  17.222 -                  handle ERROR _ => global_clause_cache
  17.223 -      val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th
  17.224 +  let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th)
  17.225    in
  17.226 -     case in_cache of
  17.227 -       NONE =>
  17.228 -         (case Thmtab.lookup (!global_clause_cache) th of
  17.229 -           NONE =>
  17.230 -             let val cls = map Goal.close_result (skolem_thm th)
  17.231 -             in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^
  17.232 -                                 (if PureThy.has_name_hint th then PureThy.get_name_hint th
  17.233 -                                  else string_of_thm th));
  17.234 -                change cache (Thmtab.update (th, cls)); cls
  17.235 -             end
  17.236 -         | SOME cls => cls)
  17.237 -     | SOME cls => cls
  17.238 +      case Thmtab.lookup (ThmCache.get thy) th of
  17.239 +	  NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
  17.240 +		   map Goal.close_result (skolem_thm th))
  17.241 +	| SOME cls => cls
  17.242    end;
  17.243  
  17.244  fun pairname th = (PureThy.get_name_hint th, th);
  17.245 @@ -572,14 +571,23 @@
  17.246  
  17.247  (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
  17.248  
  17.249 -fun skolem_cache clause_cache th thy = #2 (skolem_cache_thm clause_cache th thy);
  17.250 +val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
  17.251 +
  17.252 +fun skolem_cache th thy = #2 (skolem_cache_thm th thy);
  17.253 +
  17.254 +fun skolem_cache_all thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
  17.255 +
  17.256 +fun skolem_cache_new thy = fold skolem_cache (map #2 (PureThy.thms_of thy)) thy;
  17.257  
  17.258  (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
  17.259    lambda_free, but then the individual theory caches become much bigger.*)
  17.260  
  17.261 -fun clause_cache_setup thy =
  17.262 -  fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy;
  17.263 -
  17.264 +(*The new constant is a hack to prevent multiple execution*)
  17.265 +fun clause_cache_endtheory thy =
  17.266 +  let val _ = Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy)
  17.267 +  in
  17.268 +    Option.map skolem_cache_new (try mark_skolemized thy)
  17.269 +  end;
  17.270  
  17.271  (*** meson proof methods ***)
  17.272  
  17.273 @@ -672,7 +680,7 @@
  17.274    | conj_rule ths = foldr1 conj2_rule ths;
  17.275  
  17.276  fun skolem_attr (Context.Theory thy, th) =
  17.277 -      let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy
  17.278 +      let val (cls, thy') = skolem_cache_thm th thy
  17.279        in (Context.Theory thy', conj_rule cls) end
  17.280    | skolem_attr (context, th) = (context, th)
  17.281  
  17.282 @@ -684,6 +692,6 @@
  17.283    [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
  17.284      "conversion of goal to conjecture clauses")];
  17.285  
  17.286 -val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods;
  17.287 +val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods;
  17.288  
  17.289  end;
    18.1 --- a/src/HOL/W0/W0.thy	Thu Sep 27 17:28:05 2007 +0200
    18.2 +++ b/src/HOL/W0/W0.thy	Thu Sep 27 17:55:28 2007 +0200
    18.3 @@ -208,11 +208,8 @@
    18.4       addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
    18.5    -- {* @{text \<Longleftarrow>} *}
    18.6    apply (unfold free_tv_subst cod_def dom_def)
    18.7 -  apply (tactic "safe_tac set_cs")
    18.8 -   apply (cut_tac m = m and n = n in less_linear)
    18.9 -   apply (tactic "fast_tac (HOL_cs addSIs [@{thm less_or_eq_imp_le}]) 1")
   18.10 -  apply (cut_tac m = ma and n = n in less_linear)
   18.11 -  apply (fast intro!: less_or_eq_imp_le)
   18.12 +  apply safe
   18.13 +  apply (metis linorder_not_less)+
   18.14    done
   18.15  
   18.16  lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"
    19.1 --- a/src/HOL/ex/Primrec.thy	Thu Sep 27 17:28:05 2007 +0200
    19.2 +++ b/src/HOL/ex/Primrec.thy	Thu Sep 27 17:55:28 2007 +0200
    19.3 @@ -219,7 +219,7 @@
    19.4  text {* PROPERTY A 11 *}
    19.5  
    19.6  lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (4 + (i1 + i2), j)"
    19.7 -  apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans)
    19.8 +  apply (rule less_trans [of _ "ack (Suc (Suc 0), ack (i1 + i2, j))" _])
    19.9     prefer 2
   19.10     apply (rule ack_nest_bound [THEN less_le_trans])
   19.11     apply (simp add: Suc3_eq_add_3)
   19.12 @@ -235,11 +235,10 @@
   19.13    "\<exists>k'. \<forall>i j. ..."} *}
   19.14  
   19.15  lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (4 + k, j)"
   19.16 -  apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
   19.17 -   prefer 2
   19.18 +  apply (rule less_trans [of _ "ack (k, j) + ack (0, j)" _])
   19.19 +   apply (blast intro: add_less_mono less_ack2) 
   19.20     apply (rule ack_add_bound [THEN less_le_trans])
   19.21     apply simp
   19.22 -  apply (rule add_less_mono less_ack2 | assumption)+
   19.23    done
   19.24  
   19.25  
   19.26 @@ -333,7 +332,7 @@
   19.27  lemma ack_not_PRIMREC: "\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack (x, x))"
   19.28    apply (rule notI)
   19.29    apply (erule ack_bounds_PRIMREC [THEN exE])
   19.30 -  apply (rule less_irrefl)
   19.31 +  apply (rule Nat.less_irrefl)
   19.32    apply (drule_tac x = "[x]" in spec)
   19.33    apply simp
   19.34    done