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