--- a/Admin/Mercurial/isabelle-style.diff Thu Apr 29 15:24:22 2010 -0700
+++ b/Admin/Mercurial/isabelle-style.diff Fri Apr 30 08:47:07 2010 -0700
@@ -23,7 +23,16 @@
</div>
diff -u gitweb/map isabelle/map
--- gitweb/map 2010-02-01 16:34:34.000000000 +0100
-+++ isabelle/map 2010-03-03 15:13:25.000000000 +0100
++++ isabelle/map 2010-04-29 23:43:54.000000000 +0200
+@@ -78,7 +78,7 @@
+ <tr style="font-family:monospace" class="parity{parity}">
+ <td class="linenr" style="text-align: right;">
+ <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
+- title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
++ title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
+ </td>
+ <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
+ <td><pre>{line|escape}</pre></td>
@@ -206,9 +206,10 @@
<tr class="parity{parity}">
<td class="age"><i>{date|age}</i></td>
@@ -36,3 +45,12 @@
<span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
</a>
</td>
+@@ -225,6 +226,7 @@
+ <b>{desc|strip|firstline|escape|nonempty}</b>
+ </a>
+ </td>
++ <td><i>{author|person}</i></td>
+ <td class="link">
+ <a href="{url}file/{node|short}/{file|urlescape}{sessionvars%urlparameter}">file</a> | <a href="{url}diff/{node|short}/{file|urlescape}{sessionvars%urlparameter}">diff</a> | <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}">annotate</a> {rename%filelogrename}</td>
+ </tr>'
+Only in isabelle/: map~
--- a/src/FOL/simpdata.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/FOL/simpdata.ML Fri Apr 30 08:47:07 2010 -0700
@@ -26,7 +26,7 @@
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong rl =
+fun mk_meta_cong (_: simpset) rl =
Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
@@ -52,7 +52,7 @@
| _ => [th])
in atoms end;
-fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
+fun mksimps pairs (_: simpset) = map mk_eq o mk_atomize pairs o gen_all;
(** make simplification procedures for quantifier elimination **)
--- a/src/HOL/HOL.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/HOL.thy Fri Apr 30 08:47:07 2010 -0700
@@ -1491,7 +1491,7 @@
setup {*
Induct.setup #>
Context.theory_map (Induct.map_simpset (fn ss => ss
- setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #>
+ setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
map (Simplifier.rewrite_rule (map Thm.symmetric
@{thms induct_rulify_fallback induct_true_def induct_false_def})))
addsimprocs
--- a/src/HOL/Import/proof_kernel.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Import/proof_kernel.ML Fri Apr 30 08:47:07 2010 -0700
@@ -1249,7 +1249,7 @@
let
val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
val hol4ss = Simplifier.global_context thy empty_ss
- setmksimps single addsimps hol4rews1
+ setmksimps (K single) addsimps hol4rews1
in
Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
end
--- a/src/HOL/Import/shuffler.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Import/shuffler.ML Fri Apr 30 08:47:07 2010 -0700
@@ -489,7 +489,7 @@
let
val norms = ShuffleData.get thy
val ss = Simplifier.global_context thy empty_ss
- setmksimps single
+ setmksimps (K single)
addsimps (map (Thm.transfer thy) norms)
addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
fun chain f th =
--- a/src/HOL/Metis_Examples/Abstraction.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Metis_Examples/Abstraction.thy Fri Apr 30 08:47:07 2010 -0700
@@ -23,13 +23,11 @@
declare [[ atp_problem_prefix = "Abstraction__Collect_triv" ]]
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
-proof (neg_clausify)
-assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
-assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
-have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
- by (metis CollectD 0)
-show "False"
- by (metis 2 1)
+proof -
+ assume "a \<in> {x. P x}"
+ hence "a \<in> P" by (metis Collect_def)
+ hence "P a" by (metis mem_def)
+ thus "P a" by metis
qed
lemma Collect_triv: "a \<in> {x. P x} ==> P a"
@@ -38,76 +36,52 @@
declare [[ atp_problem_prefix = "Abstraction__Collect_mp" ]]
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
- by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq);
- --{*34 secs*}
+ by (metis Collect_imp_eq ComplD UnE)
declare [[ atp_problem_prefix = "Abstraction__Sigma_triv" ]]
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
-proof (neg_clausify)
-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)"
-assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> (b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) a"
-have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
- by (metis SigmaD1 0)
-have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
- by (metis SigmaD2 0)
-have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
- by (metis 1 2)
-show "False"
- by (metis 3 4)
+proof -
+ assume A1: "(a, b) \<in> Sigma A B"
+ hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
+ have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
+ have "b \<in> B a" by (metis F1)
+ thus "a \<in> A \<and> b \<in> B a" by (metis F2)
qed
lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
by (metis SigmaD1 SigmaD2)
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect" ]]
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-(*???metis says this is satisfiable!
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+(* Metis says this is satisfiable!
by (metis CollectD SigmaD1 SigmaD2)
*)
by (meson CollectD SigmaD1 SigmaD2)
-(*single-step*)
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 Un_empty_right vimage_Collect_eq vimage_def vimage_singleton_eq)
-
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-proof (neg_clausify)
-assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
-\<in> Sigma (A\<Colon>'a\<Colon>type set)
- (COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
-assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> a \<noteq> (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type)"
-have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
- by (metis 0 SigmaD1)
-have 3: "(b\<Colon>'b\<Colon>type)
-\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
- by (metis 0 SigmaD2)
-have 4: "(b\<Colon>'b\<Colon>type) \<in> Collect (COMBB (op = (a\<Colon>'a\<Colon>type)) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type))"
- by (metis 3)
-have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
- by (metis 1 2)
-have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
- by (metis 4 vimage_singleton_eq insert_def singleton_conv2 Un_empty_right vimage_Collect_eq vimage_def)
-show "False"
- by (metis 5 6)
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+proof -
+ assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
+ have F1: "\<forall>u. {u} = op = u" by (metis singleton_conv2 Collect_def)
+ have F2: "\<forall>y w v. v \<in> w -` op = y \<longrightarrow> w v = y"
+ by (metis F1 vimage_singleton_eq)
+ have F3: "\<forall>x w. (\<lambda>R. w (x R)) = x -` w"
+ by (metis vimage_Collect_eq Collect_def)
+ show "a \<in> A \<and> a = f b" by (metis A1 F2 F3 mem_Sigma_iff Collect_def)
qed
-(*Alternative structured proof, untyped*)
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-proof (neg_clausify)
-assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
-have 1: "b \<in> Collect (COMBB (op = a) f)"
- by (metis 0 SigmaD2)
-have 2: "f b = a"
- by (metis 1 vimage_Collect_eq singleton_conv2 insert_def Un_empty_right vimage_singleton_eq vimage_def)
-assume 3: "a \<notin> A \<or> a \<noteq> f b"
-have 4: "a \<in> A"
- by (metis 0 SigmaD1)
-have 5: "f b \<noteq> a"
- by (metis 4 3)
-show "False"
- by (metis 5 2)
+(* Alternative structured proof *)
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+proof -
+ assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
+ hence F1: "a \<in> A" by (metis mem_Sigma_iff)
+ have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
+ hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)
+ hence "a = f b" by (unfold mem_def)
+ thus "a \<in> A \<and> a = f b" by (metis F1)
qed
@@ -116,56 +90,40 @@
by (metis Collect_mem_eq SigmaD2)
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
-proof (neg_clausify)
-assume 0: "(cl, f) \<in> CLF"
-assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
-assume 2: "f \<notin> pset cl"
-have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
- by (metis SigmaD2 1)
-have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
- by (metis 3 Collect_mem_eq)
-have 5: "(cl, f) \<notin> CLF"
- by (metis 2 4)
-show "False"
- by (metis 5 0)
+proof -
+ assume A1: "(cl, f) \<in> CLF"
+ assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
+ have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+ have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
+ hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
+ hence "f \<in> pset cl" by (metis A1)
+ thus "f \<in> pset cl" by metis
qed
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]]
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
f \<in> pset cl \<rightarrow> pset cl"
-proof (neg_clausify)
-assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
-assume 1: "(cl, f)
-\<in> Sigma CL
- (COMBB Collect
- (COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
-show "False"
-(* by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
- by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
+proof -
+ assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
+ have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+ have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
+ hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
+ thus "f \<in> pset cl \<rightarrow> pset cl" by metis
qed
-
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Int" ]]
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
-proof (neg_clausify)
-assume 0: "(cl, f)
-\<in> Sigma CL
- (COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
-assume 1: "f \<notin> pset cl \<inter> cl"
-have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl"
- by (insert 0, simp add: COMBB_def)
-(* by (metis SigmaD2 0) ??doesn't terminate*)
-have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
- by (metis 2 Collect_mem_eq)
-have 4: "f \<notin> cl \<inter> pset cl"
- by (metis 1 Int_commute)
-have 5: "f \<in> cl \<inter> pset cl"
- by (metis 3 Int_commute)
-show "False"
- by (metis 5 4)
+proof -
+ assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
+ have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+ have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
+ hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def)
+ hence "f \<in> Id_on cl `` pset cl" by metis
+ hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
+ thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
qed
@@ -181,19 +139,13 @@
f \<in> pset cl \<inter> cl"
by auto
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
- --{*@{text Int_def} is redundant*}
-*)
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
lemma "(cl,f) \<in> CLF ==>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
by auto
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq Int_commute SigmaD2)
-*)
+
declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
lemma
@@ -201,9 +153,7 @@
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>
f \<in> pset cl \<rightarrow> pset cl"
by fast
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq SigmaD2 subsetD)
-*)
+
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
lemma
@@ -211,9 +161,7 @@
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
f \<in> pset cl \<rightarrow> pset cl"
by auto
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
-*)
+
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
lemma
@@ -225,37 +173,33 @@
declare [[ atp_problem_prefix = "Abstraction__map_eq_zipA" ]]
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
apply (induct xs)
-(*sledgehammer*)
-apply auto
-done
+ apply (metis map_is_Nil_conv zip.simps(1))
+by auto
declare [[ atp_problem_prefix = "Abstraction__map_eq_zipB" ]]
lemma "map (%w. (w -> w, w \<times> w)) xs =
zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
apply (induct xs)
-(*sledgehammer*)
-apply auto
-done
+ apply (metis Nil_is_map_conv zip_Nil)
+by auto
declare [[ atp_problem_prefix = "Abstraction__image_evenA" ]]
-lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
-(*sledgehammer*)
-by auto
+lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)"
+by (metis Collect_def image_subset_iff mem_def)
declare [[ atp_problem_prefix = "Abstraction__image_evenB" ]]
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A
==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
-(*sledgehammer*)
-by auto
+by (metis Collect_def imageI image_image image_subset_iff mem_def)
declare [[ atp_problem_prefix = "Abstraction__image_curry" ]]
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)"
-(*sledgehammer*)
+(*sledgehammer*)
by auto
declare [[ atp_problem_prefix = "Abstraction__image_TimesA" ]]
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
-(*sledgehammer*)
+(*sledgehammer*)
apply (rule equalityI)
(***Even the two inclusions are far too difficult
using [[ atp_problem_prefix = "Abstraction__image_TimesA_simpler"]]
@@ -283,15 +227,15 @@
declare [[ atp_problem_prefix = "Abstraction__image_TimesB" ]]
lemma image_TimesB:
- "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
-(*sledgehammer*)
+ "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
+(*sledgehammer*)
by force
declare [[ atp_problem_prefix = "Abstraction__image_TimesC" ]]
lemma image_TimesC:
"(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)"
-(*sledgehammer*)
+(*sledgehammer*)
by auto
end
--- a/src/HOL/Metis_Examples/BT.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Metis_Examples/BT.thy Fri Apr 30 08:47:07 2010 -0700
@@ -133,7 +133,7 @@
apply (rule ext)
apply (induct_tac y)
apply (metis bt_map.simps(1))
-by (metis COMBI_def bt_map.simps(2))
+by (metis bt_map.simps(2))
declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
--- a/src/HOL/Metis_Examples/BigO.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Metis_Examples/BigO.thy Fri Apr 30 08:47:07 2010 -0700
@@ -23,7 +23,7 @@
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
apply (rule_tac x = "abs c" in exI, auto)
- apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
+ apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult)
done
(*** Now various verions with an increasing shrink factor ***)
@@ -37,64 +37,25 @@
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
apply (rule_tac x = "abs c" in exI, auto)
-proof (neg_clausify)
-fix c x
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
- by (metis abs_mult mult_commute)
-have 1: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
- X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
- by (metis abs_mult_pos linorder_linear)
-have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
- \<not> (0\<Colon>'a\<Colon>linordered_idom) < X1 * X2 \<or>
- \<not> (0\<Colon>'a\<Colon>linordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom)"
- by (metis linorder_not_less mult_nonneg_nonpos2)
-assume 3: "\<And>x\<Colon>'b\<Colon>type.
- \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
- \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
- \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
- \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
- by (metis 4 abs_mult)
-have 6: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
- \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
- by (metis abs_ge_zero xt1(6))
-have 7: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
- X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
- by (metis not_leE 6)
-have 8: "(0\<Colon>'a\<Colon>linordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
- by (metis 5 7)
-have 9: "\<And>X1\<Colon>'a\<Colon>linordered_idom.
- \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
- (0\<Colon>'a\<Colon>linordered_idom) < X1"
- by (metis 8 order_less_le_trans)
-have 10: "(0\<Colon>'a\<Colon>linordered_idom)
-< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
- by (metis 3 9)
-have 11: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_idom)"
- by (metis abs_ge_zero 2 10)
-have 12: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
- by (metis mult_commute 1 11)
-have 13: "\<And>X1\<Colon>'b\<Colon>type.
- - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
- \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
- by (metis 3 abs_le_D2)
-have 14: "\<And>X1\<Colon>'b\<Colon>type.
- - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
- \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
- by (metis 0 12 13)
-have 15: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
- by (metis abs_mult abs_mult_pos abs_ge_zero)
-have 16: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. X1 \<le> \<bar>X2\<bar> \<or> \<not> X1 \<le> X2"
- by (metis xt1(6) abs_ge_self)
-have 17: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
- by (metis 16 abs_le_D1)
-have 18: "\<And>X1\<Colon>'b\<Colon>type.
- (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
- \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
- by (metis 17 3 15)
-show "False"
- by (metis abs_le_iff 5 18 14)
+proof -
+ fix c :: 'a and x :: 'b
+ assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
+ have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
+ have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+ by (metis abs_mult)
+ have F5: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1"
+ by (metis abs_mult_pos)
+ hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^isub>1" by (metis F2)
+ hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F2 abs_one)
+ hence "\<forall>x\<^isub>3. 0 \<le> \<bar>h x\<^isub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F3)
+ hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F1)
+ hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F5)
+ hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F4)
+ hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1)
+ hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1)
+ thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
qed
sledgehammer_params [shrink_factor = 2]
@@ -106,36 +67,17 @@
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
apply (rule_tac x = "abs c" in exI, auto);
-proof (neg_clausify)
-fix c x
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
- by (metis abs_mult mult_commute)
-assume 1: "\<And>x\<Colon>'b\<Colon>type.
- \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
- \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
- \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
- \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
- by (metis 2 abs_mult)
-have 4: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
- \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
- by (metis abs_ge_zero xt1(6))
-have 5: "(0\<Colon>'a\<Colon>linordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
- by (metis not_leE 4 3)
-have 6: "(0\<Colon>'a\<Colon>linordered_idom)
-< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
- by (metis 1 order_less_le_trans 5)
-have 7: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
- by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute)
-have 8: "\<And>X1\<Colon>'b\<Colon>type.
- - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
- \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
- by (metis 0 7 abs_le_D2 1)
-have 9: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
- by (metis abs_ge_self xt1(6) abs_le_D1)
-show "False"
- by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
+proof -
+ fix c :: 'a and x :: 'b
+ assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+ by (metis abs_mult)
+ have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
+ hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis A1 abs_ge_zero order_trans)
+ hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos)
+ hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero)
+ thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
qed
sledgehammer_params [shrink_factor = 3]
@@ -146,30 +88,17 @@
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto);
-proof (neg_clausify)
-fix c x
-assume 0: "\<And>x\<Colon>'b\<Colon>type.
- \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
- \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
- \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
- X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
- by (metis abs_ge_zero xt1(6) not_leE)
-have 3: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_idom)"
- by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0)
-have 4: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
- by (metis abs_ge_zero abs_mult_pos abs_mult)
-have 5: "\<And>X1\<Colon>'b\<Colon>type.
- (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
- \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
- by (metis 4 0 xt1(6) abs_ge_self abs_le_D1)
-show "False"
- by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
+ apply (rule_tac x = "abs c" in exI, auto)
+proof -
+ fix c :: 'a and x :: 'b
+ assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
+ hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
+ hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
+ thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
qed
-
sledgehammer_params [shrink_factor = 4]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
@@ -178,33 +107,18 @@
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto);
-proof (neg_clausify)
-fix c x (*sort/type constraint inserted by hand!*)
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
- by (metis abs_ge_zero abs_mult_pos abs_mult)
-assume 1: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
-have 2: "\<And>X1 X2. \<not> \<bar>X1\<bar> \<le> X2 \<or> (0\<Colon>'a) \<le> X2"
- by (metis abs_ge_zero order_trans)
-have 3: "\<And>X1. (0\<Colon>'a) \<le> c * \<bar>f X1\<bar>"
- by (metis 1 2)
-have 4: "\<And>X1. c * \<bar>f X1\<bar> = \<bar>c * f X1\<bar>"
- by (metis 0 abs_of_nonneg 3)
-have 5: "\<And>X1. - h X1 \<le> c * \<bar>f X1\<bar>"
- by (metis 1 abs_le_D2)
-have 6: "\<And>X1. - h X1 \<le> \<bar>c * f X1\<bar>"
- by (metis 4 5)
-have 7: "\<And>X1. h X1 \<le> c * \<bar>f X1\<bar>"
- by (metis 1 abs_le_D1)
-have 8: "\<And>X1. h X1 \<le> \<bar>c * f X1\<bar>"
- by (metis 4 7)
-assume 9: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
-have 10: "\<not> \<bar>h x\<bar> \<le> \<bar>c * f x\<bar>"
- by (metis abs_mult 9)
-show "False"
- by (metis 6 8 10 abs_leI)
+ apply (rule_tac x = "abs c" in exI, auto)
+proof -
+ fix c :: 'a and x :: 'b
+ assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+ have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
+ by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
+ hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
+ thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
qed
+sledgehammer_params [shrink_factor = 1]
lemma bigo_alt_def: "O(f) =
{h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
@@ -230,29 +144,13 @@
declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
lemma bigo_refl [intro]: "f : O(f)"
- apply(auto simp add: bigo_def)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
- by (metis mult_le_cancel_right1 order_eq_iff)
-have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
- by (metis order_eq_iff 1)
-show "False"
- by (metis 0 2)
-qed
+apply (auto simp add: bigo_def)
+by (metis class_semiring.mul_1 order_refl)
declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
lemma bigo_zero: "0 : O(g)"
- apply (auto simp add: bigo_def func_zero)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> (0\<Colon>'b) \<le> xa * \<bar>g (x xa)\<bar>"
-have 1: "\<not> (0\<Colon>'b) \<le> (0\<Colon>'b)"
- by (metis 0 mult_eq_0_iff)
-show "False"
- by (metis 1 linorder_neq_iff linorder_antisym_conv1)
-qed
+apply (auto simp add: bigo_def func_zero)
+by (metis class_semiring.mul_0 order_refl)
lemma bigo_zero2: "O(%x.0) = {%x.0}"
apply (auto simp add: bigo_def)
@@ -365,103 +263,36 @@
lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
f : O(g)"
apply (auto simp add: bigo_def)
-(*Version 1: one-shot proof*)
+(* Version 1: one-line proof *)
apply (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult)
done
lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
- f : O(g)"
- apply (auto simp add: bigo_def)
-(*Version 2: single-step proof*)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>x. f x \<le> c * g x"
-assume 1: "\<And>xa. \<not> f (x xa) \<le> xa * \<bar>g (x xa)\<bar>"
-have 2: "\<And>X3. c * g X3 = f X3 \<or> \<not> c * g X3 \<le> f X3"
- by (metis 0 order_antisym_conv)
-have 3: "\<And>X3. \<not> f (x \<bar>X3\<bar>) \<le> \<bar>X3 * g (x \<bar>X3\<bar>)\<bar>"
- by (metis 1 abs_mult)
-have 4: "\<And>X1 X3\<Colon>'b\<Colon>linordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
- by (metis linorder_linear abs_le_D1)
-have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
- by (metis abs_mult_self)
-have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>linordered_idom)"
- by (metis not_square_less_zero)
-have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
- by (metis abs_mult mult_commute)
-have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
- by (metis abs_mult 5)
-have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
- by (metis 3 4)
-have 10: "c * g (x \<bar>c\<bar>) = f (x \<bar>c\<bar>)"
- by (metis 2 9)
-have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
- by (metis abs_idempotent abs_mult 8)
-have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
- by (metis mult_commute 7 11)
-have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
- by (metis 8 7 12)
-have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
- by (metis abs_ge_self abs_le_D1 abs_if)
-have 15: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<bar>X3\<bar> < (0\<Colon>'b)"
- by (metis abs_ge_self abs_le_D1 abs_if)
-have 16: "\<And>X3. X3 * X3 < (0\<Colon>'b) \<or> X3 * \<bar>X3\<bar> \<le> X3 * X3"
- by (metis 15 13)
-have 17: "\<And>X3::'b. X3 * \<bar>X3\<bar> \<le> X3 * X3"
- by (metis 16 6)
-have 18: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<not> X3 < (0\<Colon>'b)"
- by (metis mult_le_cancel_left 17)
-have 19: "\<And>X3::'b. X3 \<le> \<bar>X3\<bar>"
- by (metis 18 14)
-have 20: "\<not> f (x \<bar>c\<bar>) \<le> \<bar>f (x \<bar>c\<bar>)\<bar>"
- by (metis 3 10)
-show "False"
- by (metis 20 19)
+ f : O(g)"
+apply (auto simp add: bigo_def)
+(* Version 2: structured proof *)
+proof -
+ assume "\<forall>x. f x \<le> c * g x"
+ thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
qed
+text{*So here is the easier (and more natural) problem using transitivity*}
+declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
+lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
+apply (auto simp add: bigo_def)
+(* Version 1: one-line proof *)
+by (metis abs_ge_self abs_mult order_trans)
text{*So here is the easier (and more natural) problem using transitivity*}
declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
apply (auto simp add: bigo_def)
- (*Version 1: one-shot proof*)
- apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less)
- done
-
-text{*So here is the easier (and more natural) problem using transitivity*}
-declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
-lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
- apply (auto simp add: bigo_def)
-(*Version 2: single-step proof*)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>A\<Colon>'a\<Colon>type.
- (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A
- \<le> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A"
-assume 1: "\<And>A\<Colon>'b\<Colon>linordered_idom.
- \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) A)
- \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x A)\<bar>"
-have 2: "\<And>X2\<Colon>'a\<Colon>type.
- \<not> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2
- < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2"
- by (metis 0 linorder_not_le)
-have 3: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
- \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
- \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)\<bar>"
- by (metis abs_mult 1)
-have 4: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
- \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)\<bar>
- < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
- by (metis 3 linorder_not_less)
-have 5: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
- X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
- < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
- by (metis abs_less_iff 4)
-show "False"
- by (metis 2 5)
+(* Version 2: structured proof *)
+proof -
+ assume "\<forall>x. f x \<le> c * g x"
+ thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
qed
-
lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==>
f : O(g)"
apply (erule bigo_bounded_alt [of f 1 g])
@@ -471,63 +302,37 @@
declare [[ atp_problem_prefix = "BigO__bigo_bounded2" ]]
lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
f : lb +o O(g)"
- apply (rule set_minus_imp_plus)
- apply (rule bigo_bounded)
- apply (auto simp add: diff_minus fun_Compl_def func_plus)
- prefer 2
- apply (drule_tac x = x in spec)+
- apply arith (*not clear that it's provable otherwise*)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>y. lb y \<le> f y"
-assume 1: "\<not> (0\<Colon>'b) \<le> f x + - lb x"
-have 2: "\<And>X3. (0\<Colon>'b) + X3 = X3"
- by (metis diff_eq_eq right_minus_eq)
-have 3: "\<not> (0\<Colon>'b) \<le> f x - lb x"
- by (metis 1 diff_minus)
-have 4: "\<not> (0\<Colon>'b) + lb x \<le> f x"
- by (metis 3 le_diff_eq)
-show "False"
- by (metis 4 2 0)
+apply (rule set_minus_imp_plus)
+apply (rule bigo_bounded)
+ apply (auto simp add: diff_minus fun_Compl_def func_plus)
+ prefer 2
+ apply (drule_tac x = x in spec)+
+ apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
+proof -
+ fix x :: 'a
+ assume "\<forall>x. lb x \<le> f x"
+ thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
qed
declare [[ atp_problem_prefix = "BigO__bigo_abs" ]]
lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
- apply (unfold bigo_def)
- apply auto
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
- by (metis mult_le_cancel_right1 order_eq_iff)
-have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
- by (metis order_eq_iff 1)
-show "False"
- by (metis 0 2)
-qed
+apply (unfold bigo_def)
+apply auto
+by (metis class_semiring.mul_1 order_refl)
declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
lemma bigo_abs2: "f =o O(%x. abs(f x))"
- apply (unfold bigo_def)
- apply auto
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
- by (metis mult_le_cancel_right1 order_eq_iff)
-have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
- by (metis order_eq_iff 1)
-show "False"
- by (metis 0 2)
-qed
+apply (unfold bigo_def)
+apply auto
+by (metis class_semiring.mul_1 order_refl)
lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
- apply (rule equalityI)
- apply (rule bigo_elt_subset)
- apply (rule bigo_abs2)
- apply (rule bigo_elt_subset)
- apply (rule bigo_abs)
-done
+proof -
+ have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
+ have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
+ have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2)
+ thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
+qed
lemma bigo_abs4: "f =o g +o O(h) ==>
(%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
@@ -597,63 +402,9 @@
abs_mult mult_pos_pos)
apply (erule ssubst)
apply (subst abs_mult)
-(*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
- just been done*)
-proof (neg_clausify)
-fix a c b ca x
-assume 0: "(0\<Colon>'b\<Colon>linordered_idom) < (c\<Colon>'b\<Colon>linordered_idom)"
-assume 1: "\<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-\<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-assume 2: "\<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-\<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-assume 3: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> *
- \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
- \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> *
- ((ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>)"
-have 4: "\<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> = c"
- by (metis abs_of_pos 0)
-have 5: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
- by (metis abs_mult 4)
-have 6: "(0\<Colon>'b\<Colon>linordered_idom) = (1\<Colon>'b\<Colon>linordered_idom) \<or>
-(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
- by (metis abs_not_less_zero abs_one linorder_neqE_linordered_idom)
-have 7: "(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
- by (metis 6 one_neq_zero)
-have 8: "\<bar>1\<Colon>'b\<Colon>linordered_idom\<bar> = (1\<Colon>'b\<Colon>linordered_idom)"
- by (metis abs_of_pos 7)
-have 9: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar>"
- by (metis abs_ge_zero 5)
-have 10: "\<And>X1\<Colon>'b\<Colon>linordered_idom. X1 * (1\<Colon>'b\<Colon>linordered_idom) = X1"
- by (metis mult_cancel_right2 mult_commute)
-have 11: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>linordered_idom\<bar>"
- by (metis abs_mult abs_idempotent 10)
-have 12: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
- by (metis 11 8 10)
-have 13: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>X1\<bar>"
- by (metis abs_ge_zero 12)
-have 14: "\<not> (0\<Colon>'b\<Colon>linordered_idom)
- \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
-\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
- by (metis 3 mult_mono)
-have 15: "\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
-\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
- \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
- by (metis 14 9)
-have 16: "\<not> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
- \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
- \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
- by (metis 15 13)
-have 17: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
- \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
- by (metis 16 2)
-show 18: "False"
- by (metis 17 1)
-qed
-
+(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
+ abs_mult has just been done *)
+by (metis abs_ge_zero mult_mono')
declare [[ atp_problem_prefix = "BigO__bigo_mult2" ]]
lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
@@ -672,7 +423,7 @@
declare [[ atp_problem_prefix = "BigO__bigo_mult3" ]]
lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
-by (metis bigo_mult set_times_intro subset_iff)
+by (metis bigo_mult set_rev_mp set_times_intro)
declare [[ atp_problem_prefix = "BigO__bigo_mult4" ]]
lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
@@ -809,40 +560,16 @@
by (metis bigo_const1 bigo_elt_subset);
lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)";
-(*??FAILS because the two occurrences of COMBK have different polymorphic types
-proof (neg_clausify)
-assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>linordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
-have 1: "COMBK (c\<Colon>'b\<Colon>linordered_idom) \<notin> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
-apply (rule notI)
-apply (rule 0 [THEN notE])
-apply (rule bigo_elt_subset)
-apply assumption;
-sorry
- by (metis 0 bigo_elt_subset) loops??
-show "False"
- by (metis 1 bigo_const1)
+(* "thus" had to be replaced by "show" with an explicit reference to "F1" *)
+proof -
+ have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
+ show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset)
qed
-*)
- apply (rule bigo_elt_subset)
- apply (rule bigo_const1)
-done
declare [[ atp_problem_prefix = "BigO__bigo_const3" ]]
lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
apply (simp add: bigo_def)
-proof (neg_clausify)
-assume 0: "(c\<Colon>'a\<Colon>linordered_field) \<noteq> (0\<Colon>'a\<Colon>linordered_field)"
-assume 1: "\<And>A\<Colon>'a\<Colon>linordered_field. \<not> (1\<Colon>'a\<Colon>linordered_field) \<le> A * \<bar>c\<Colon>'a\<Colon>linordered_field\<bar>"
-have 2: "(0\<Colon>'a\<Colon>linordered_field) = \<bar>c\<Colon>'a\<Colon>linordered_field\<bar> \<or>
-\<not> (1\<Colon>'a\<Colon>linordered_field) \<le> (1\<Colon>'a\<Colon>linordered_field)"
- by (metis 1 field_inverse)
-have 3: "\<bar>c\<Colon>'a\<Colon>linordered_field\<bar> = (0\<Colon>'a\<Colon>linordered_field)"
- by (metis linorder_neq_iff linorder_antisym_conv1 2)
-have 4: "(0\<Colon>'a\<Colon>linordered_field) = (c\<Colon>'a\<Colon>linordered_field)"
- by (metis 3 abs_eq_0)
-show "False"
- by (metis 0 4)
-qed
+by (metis abs_eq_0 left_inverse order_refl)
lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
by (rule bigo_elt_subset, rule bigo_const3, assumption)
@@ -854,15 +581,7 @@
declare [[ atp_problem_prefix = "BigO__bigo_const_mult1" ]]
lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
apply (simp add: bigo_def abs_mult)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa\<Colon>'b\<Colon>linordered_idom.
- \<not> \<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> *
- \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
- \<le> xa * \<bar>f (x xa)\<bar>"
-show "False"
- by (metis linorder_neq_iff linorder_antisym_conv1 0)
-qed
+by (metis le_less)
lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
by (rule bigo_elt_subset, rule bigo_const_mult1)
@@ -870,7 +589,7 @@
declare [[ atp_problem_prefix = "BigO__bigo_const_mult3" ]]
lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
apply (simp add: bigo_def)
-(*sledgehammer [no luck]*);
+(*sledgehammer [no luck]*)
apply (rule_tac x = "abs(inverse c)" in exI)
apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
apply (subst left_inverse)
@@ -1132,15 +851,17 @@
declare [[ atp_problem_prefix = "BigO__bigo_lesso1" ]]
lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
- apply (unfold lesso_def)
- apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
-(*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
-apply (metis bigo_zero)
+apply (unfold lesso_def)
+apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
+proof -
+ assume "(\<lambda>x. max (f x - g x) 0) = 0"
+ thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero)
+next
+ show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)"
apply (unfold func_zero)
apply (rule ext)
- apply (simp split: split_max)
-done
-
+ by (simp split: split_max)
+qed
declare [[ atp_problem_prefix = "BigO__bigo_lesso2" ]]
lemma bigo_lesso2: "f =o g +o O(h) ==>
@@ -1156,8 +877,9 @@
apply (erule thin_rl)
(*sledgehammer*);
apply (case_tac "0 <= k x - g x")
- prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*)
- apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.sup_absorb1 min_max.sup_commute)
+(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
+ le_max_iff_disj min_max.le_supE min_max.sup_absorb2
+ min_max.sup_commute) *)
proof (neg_clausify)
fix x
assume 0: "\<And>A. k A \<le> f A"
@@ -1177,6 +899,11 @@
by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)
show "False"
by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
+next
+ show "\<And>x\<Colon>'a.
+ \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
+ \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
+ by (metis abs_ge_zero le_cases min_max.sup_absorb2)
qed
declare [[ atp_problem_prefix = "BigO__bigo_lesso3" ]]
--- a/src/HOL/Metis_Examples/Message.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Metis_Examples/Message.thy Fri Apr 30 08:47:07 2010 -0700
@@ -4,11 +4,12 @@
Testing the metis method.
*)
-theory Message imports Main begin
+theory Message
+imports Main
+begin
-(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
-by blast
+by (metis Un_ac(2) Un_ac(3))
types
key = nat
@@ -20,7 +21,7 @@
specification (invKey)
invKey [simp]: "invKey (invKey K) = K"
invKey_symmetric: "all_symmetric --> invKey = id"
- by (rule exI [of _ id], auto)
+by (metis id_apply)
text{*The inverse of a symmetric key is itself; that of a public key
@@ -74,33 +75,28 @@
| Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
| Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
-
-declare [[ atp_problem_prefix = "Message__parts_mono" ]]
lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
apply auto
-apply (erule parts.induct)
-apply (metis Inj set_mp)
-apply (metis Fst)
-apply (metis Snd)
-apply (metis Body)
-done
-
+apply (erule parts.induct)
+ apply (metis parts.Inj set_rev_mp)
+ apply (metis parts.Fst)
+ apply (metis parts.Snd)
+by (metis parts.Body)
text{*Equations hold because constructors are injective.*}
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
-by auto
+by (metis agent.inject imageI image_iff)
-lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
-by auto
+lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x \<in> A)"
+by (metis image_iff msg.inject(4))
-lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
-by auto
+lemma Nonce_Key_image_eq [simp]: "Nonce x \<notin> Key`A"
+by (metis image_iff msg.distinct(23))
subsubsection{*Inverse of keys *}
-declare [[ atp_problem_prefix = "Message__invKey_eq" ]]
-lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
+lemma invKey_eq [simp]: "(invKey K = invKey K') = (K = K')"
by (metis invKey)
@@ -155,7 +151,7 @@
[| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
by (blast dest: parts.Fst parts.Snd)
- declare MPair_parts [elim!] parts.Body [dest!]
+declare MPair_parts [elim!] parts.Body [dest!]
text{*NB These two rules are UNSAFE in the formal sense, as they discard the
compound message. They work well on THIS FILE.
@{text MPair_parts} is left as SAFE because it speeds up proofs.
@@ -200,7 +196,6 @@
apply (simp only: parts_Un)
done
-declare [[ atp_problem_prefix = "Message__parts_insert_two" ]]
lemma parts_insert2:
"parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
@@ -237,7 +232,6 @@
lemma parts_idem [simp]: "parts (parts H) = parts H"
by blast
-declare [[ atp_problem_prefix = "Message__parts_subset_iff" ]]
lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
apply (rule iffI)
apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
@@ -247,13 +241,10 @@
lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
by (blast dest: parts_mono);
-
-declare [[ atp_problem_prefix = "Message__parts_cut" ]]
lemma parts_cut: "[|Y\<in> parts(insert X G); X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
-
subsubsection{*Rewrite rules for pulling out atomic messages *}
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
@@ -312,8 +303,6 @@
apply (erule parts.induct, auto)
done
-
-declare [[ atp_problem_prefix = "Message__msg_Nonce_supply" ]]
lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
apply (induct_tac "msg")
apply (simp_all add: parts_insert2)
@@ -364,8 +353,6 @@
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
-
-declare [[ atp_problem_prefix = "Message__parts_analz" ]]
lemma parts_analz [simp]: "parts (analz H) = parts H"
apply (rule equalityI)
apply (metis analz_subset_parts parts_subset_iff)
@@ -517,8 +504,8 @@
by (drule analz_mono, blast)
-declare [[ atp_problem_prefix = "Message__analz_cut" ]]
- declare analz_trans[intro]
+declare analz_trans[intro]
+
lemma analz_cut: "[| Y\<in> analz (insert X H); X\<in> analz H |] ==> Y\<in> analz H"
(*TOO SLOW
by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
@@ -535,7 +522,6 @@
text{*A congruence rule for "analz" *}
-declare [[ atp_problem_prefix = "Message__analz_subset_cong" ]]
lemma analz_subset_cong:
"[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
@@ -612,9 +598,6 @@
lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
by (intro Un_least synth_mono Un_upper1 Un_upper2)
-
-declare [[ atp_problem_prefix = "Message__synth_insert" ]]
-
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
@@ -635,7 +618,6 @@
lemma synth_trans: "[| X\<in> synth G; G \<subseteq> synth H |] ==> X\<in> synth H"
by (drule synth_mono, blast)
-declare [[ atp_problem_prefix = "Message__synth_cut" ]]
lemma synth_cut: "[| Y\<in> synth (insert X H); X\<in> synth H |] ==> Y\<in> synth H"
(*TOO SLOW
by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
@@ -667,7 +649,6 @@
subsubsection{*Combinations of parts, analz and synth *}
-declare [[ atp_problem_prefix = "Message__parts_synth" ]]
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
apply (rule equalityI)
apply (rule subsetI)
@@ -679,18 +660,14 @@
apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
done
-
-
-
-declare [[ atp_problem_prefix = "Message__analz_analz_Un" ]]
lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
apply (rule equalityI);
apply (metis analz_idem analz_subset_cong order_eq_refl)
apply (metis analz_increasing analz_subset_cong order_eq_refl)
done
-declare [[ atp_problem_prefix = "Message__analz_synth_Un" ]]
- declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
+declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
+
lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
apply (rule equalityI)
apply (rule subsetI)
@@ -702,102 +679,81 @@
apply blast
done
-declare [[ atp_problem_prefix = "Message__analz_synth" ]]
lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
-proof (neg_clausify)
-assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
-have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
- by (metis analz_synth_Un)
-have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
- by (metis 0)
-have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
- by (metis 1 Un_commute)
-have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
- by (metis 3 Un_empty_right)
-have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
- by (metis 4 Un_empty_right)
-have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
- by (metis 5 Un_commute)
-show "False"
- by (metis 2 6)
+proof -
+ have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)"
+ by (metis Un_commute analz_synth_Un)
+ hence "\<forall>x\<^isub>3 x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> UNION {} x\<^isub>3)"
+ by (metis UN_extend_simps(3))
+ hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)"
+ by (metis UN_extend_simps(3))
+ hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)"
+ by (metis Un_commute)
+ thus "analz (synth H) = analz H \<union> synth H" by metis
qed
subsubsection{*For reasoning about the Fake rule in traces *}
-declare [[ atp_problem_prefix = "Message__parts_insert_subset_Un" ]]
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
-proof (neg_clausify)
-assume 0: "X \<in> G"
-assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
-have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"
- by (metis 1 parts_Un)
-have 3: "\<not> insert X H \<subseteq> G \<union> H"
- by (metis 2 parts_mono)
-have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"
- by (metis 3 insert_subset)
-have 5: "X \<notin> G \<union> H"
- by (metis 4 Un_upper2)
-have 6: "X \<notin> G"
- by (metis 5 UnCI)
-show "False"
- by (metis 6 0)
+proof -
+ assume "X \<in> G"
+ hence "\<forall>u. X \<in> G \<union> u" by (metis Un_iff)
+ hence "X \<in> G \<union> H \<and> H \<subseteq> G \<union> H"
+ by (metis Un_upper2)
+ hence "insert X H \<subseteq> G \<union> H" by (metis insert_subset)
+ hence "parts (insert X H) \<subseteq> parts (G \<union> H)"
+ by (metis parts_mono)
+ thus "parts (insert X H) \<subseteq> parts G \<union> parts H"
+ by (metis parts_Un)
qed
-declare [[ atp_problem_prefix = "Message__Fake_parts_insert" ]]
lemma Fake_parts_insert:
"X \<in> synth (analz H) ==>
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-proof (neg_clausify)
-assume 0: "X \<in> synth (analz H)"
-assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"
- by (metis parts_synth parts_analz)
-have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"
- by (metis analz_synth analz_idem)
-have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"
- by (metis Un_upper1 analz_synth)
-have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
- by (metis 1 Un_commute)
-have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"
- by (metis 5 2)
-have 7: "\<not> insert X H \<subseteq> synth (analz H)"
- by (metis 6 parts_mono)
-have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"
- by (metis 7 insert_subset)
-have 9: "\<not> H \<subseteq> synth (analz H)"
- by (metis 8 0)
-have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"
- by (metis analz_subset_iff 4)
-have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"
- by (metis analz_subset_iff 10)
-have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>
- \<not> analz X3 \<subseteq> synth (analz X3)"
- by (metis Un_absorb1 3)
-have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"
- by (metis 12 synth_increasing)
-have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"
- by (metis 11 13)
-show "False"
- by (metis 9 14)
+sledgehammer
+proof -
+ assume A1: "X \<in> synth (analz H)"
+ have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"
+ by (metis analz_idem analz_synth)
+ have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))"
+ by (metis parts_analz parts_synth)
+ have F3: "synth (analz H) X" using A1 by (metis mem_def)
+ have "\<forall>x\<^isub>2 x\<^isub>1\<Colon>msg set. x\<^isub>1 \<le> sup x\<^isub>1 x\<^isub>2" by (metis inf_sup_ord(3))
+ hence F4: "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" by (metis analz_synth)
+ have F5: "X \<in> synth (analz H)" using F3 by (metis mem_def)
+ have "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)
+ \<longrightarrow> analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
+ using F1 by (metis subset_Un_eq)
+ hence F6: "\<forall>x\<^isub>1. analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
+ by (metis synth_increasing)
+ have "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" using F4 by (metis analz_subset_iff)
+ hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth (analz x\<^isub>1))" by (metis analz_subset_iff)
+ hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)" using F6 by metis
+ hence "H \<subseteq> synth (analz H)" by metis
+ hence "H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)" using F5 by metis
+ hence "insert X H \<subseteq> synth (analz H)" by (metis insert_subset)
+ hence "parts (insert X H) \<subseteq> parts (synth (analz H))" by (metis parts_mono)
+ hence "parts (insert X H) \<subseteq> parts H \<union> synth (analz H)" using F2 by metis
+ thus "parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" by (metis Un_commute)
qed
lemma Fake_parts_insert_in_Un:
"[|Z \<in> parts (insert X H); X: synth (analz H)|]
==> Z \<in> synth (analz H) \<union> parts H";
-by (blast dest: Fake_parts_insert [THEN subsetD, dest])
+by (blast dest: Fake_parts_insert [THEN subsetD, dest])
-declare [[ atp_problem_prefix = "Message__Fake_analz_insert" ]]
- declare analz_mono [intro] synth_mono [intro]
+declare analz_mono [intro] synth_mono [intro]
+
lemma Fake_analz_insert:
- "X\<in> synth (analz G) ==>
+ "X \<in> synth (analz G) ==>
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
-by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12))
+by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un
+ analz_mono analz_synth_Un insert_absorb)
-declare [[ atp_problem_prefix = "Message__Fake_analz_insert_simpler" ]]
-(*simpler problems? BUT METIS CAN'T PROVE
+(* Simpler problems? BUT METIS CAN'T PROVE THE LAST STEP
lemma Fake_analz_insert_simpler:
- "X\<in> synth (analz G) ==>
+ "X \<in> synth (analz G) ==>
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
apply (rule subsetI)
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
--- a/src/HOL/Metis_Examples/Tarski.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Metis_Examples/Tarski.thy Fri Apr 30 08:47:07 2010 -0700
@@ -514,67 +514,44 @@
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
apply (simp add: fix_def)
apply (rule conjI)
-proof (neg_clausify)
-assume 0: "H =
-Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
-assume 1: "lub (Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
- (COMBC op \<in> A)))
- cl
-\<notin> A"
-have 2: "lub H cl \<notin> A"
- by (metis 1 0)
-have 3: "(lub H cl, f (lub H cl)) \<in> r"
- by (metis lubH_le_flubH 0)
-have 4: "(f (lub H cl), lub H cl) \<in> r"
- by (metis flubH_le_lubH 0)
-have 5: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
- by (metis antisymE 4)
-have 6: "lub H cl = f (lub H cl)"
- by (metis 5 3)
-have 7: "(lub H cl, lub H cl) \<in> r"
- by (metis 6 4)
-have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl_on X1 r"
- by (metis 7 refl_onD2)
-have 9: "\<not> refl_on A r"
- by (metis 8 2)
-show "False"
- by (metis CO_refl_on 9);
-next --{*apparently the way to insert a second structured proof*}
- show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
- f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
- proof (neg_clausify)
- assume 0: "H =
- Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
- assume 1: "f (lub (Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
- (COMBC op \<in> A)))
- cl) \<noteq>
- lub (Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
- (COMBC op \<in> A)))
- cl"
- have 2: "f (lub H cl) \<noteq>
- lub (Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
- (COMBC op \<in> A)))
- cl"
- by (metis 1 0)
- have 3: "f (lub H cl) \<noteq> lub H cl"
- by (metis 2 0)
- have 4: "(lub H cl, f (lub H cl)) \<in> r"
- by (metis lubH_le_flubH 0)
- have 5: "(f (lub H cl), lub H cl) \<in> r"
- by (metis flubH_le_lubH 0)
- have 6: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
- by (metis antisymE 5)
- have 7: "lub H cl = f (lub H cl)"
- by (metis 6 4)
- show "False"
- by (metis 3 7)
- qed
+proof -
+ assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
+ have F1: "\<forall>x\<^isub>2. (\<lambda>R. R \<in> x\<^isub>2) = x\<^isub>2" by (metis Collect_def Collect_mem_eq)
+ have F2: "\<forall>x\<^isub>1 x\<^isub>2. (\<lambda>R. x\<^isub>2 (x\<^isub>1 R)) = x\<^isub>1 -` x\<^isub>2"
+ by (metis Collect_def vimage_Collect_eq)
+ have F3: "\<forall>x\<^isub>2 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<in> x\<^isub>2) = x\<^isub>1 -` x\<^isub>2"
+ by (metis Collect_def vimage_def)
+ have F4: "\<forall>x\<^isub>3 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<and> x\<^isub>3 R) = x\<^isub>1 \<inter> x\<^isub>3"
+ by (metis Collect_def Collect_conj_eq)
+ have F5: "(\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) = H" using A1 by (metis Collect_def)
+ have F6: "\<forall>x\<^isub>1\<subseteq>A. glb x\<^isub>1 (dual cl) \<in> A" by (metis lub_dual_glb lub_in_lattice)
+ have F7: "\<forall>x\<^isub>2 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<in> x\<^isub>2) = (\<lambda>R. x\<^isub>2 (x\<^isub>1 R))" by (metis F2 F3)
+ have "(\<lambda>R. (R, f R) \<in> r \<and> A R) = H" by (metis F1 F5)
+ hence "A \<inter> (\<lambda>R. r (R, f R)) = H" by (metis F4 F7 Int_commute)
+ hence "H \<subseteq> A" by (metis Int_lower1)
+ hence "H \<subseteq> A" by metis
+ hence "glb H (dual cl) \<in> A" using F6 by metis
+ hence "glb (\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) (dual cl) \<in> A" using F5 by metis
+ hence "lub (\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) cl \<in> A" by (metis lub_dual_glb)
+ thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" by (metis Collect_def)
+next
+ assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
+ have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+ have F2: "\<forall>w u. (\<lambda>R. u R \<and> w R) = u \<inter> w"
+ by (metis Collect_conj_eq Collect_def)
+ have F3: "\<forall>x v. (\<lambda>R. v R \<in> x) = v -` x" by (metis vimage_def Collect_def)
+ hence F4: "A \<inter> (\<lambda>R. (R, f R)) -` r = H" using A1 by auto
+ hence F5: "(f (lub H cl), lub H cl) \<in> r"
+ by (metis F1 F3 F2 Int_commute flubH_le_lubH Collect_def)
+ have F6: "(lub H cl, f (lub H cl)) \<in> r"
+ by (metis F1 F3 F2 F4 Int_commute lubH_le_flubH Collect_def)
+ have "(lub H cl, f (lub H cl)) \<in> r \<longrightarrow> f (lub H cl) = lub H cl"
+ using F5 by (metis antisymE)
+ hence "f (lub H cl) = lub H cl" using F6 by metis
+ thus "H = {x. (x, f x) \<in> r \<and> x \<in> A}
+ \<Longrightarrow> f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) =
+ lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
+ by (metis F4 F2 F3 F1 Collect_def Int_commute)
qed
lemma (in CLF) (*lubH_is_fixp:*)
@@ -744,18 +721,13 @@
"[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
==> (| pset = interval r a b, order = induced (interval r a b) r |)
\<in> PartialOrder"
-proof (neg_clausify)
-assume 0: "a \<in> A"
-assume 1: "b \<in> A"
-assume 2: "\<lparr>pset = interval r a b, order = induced (interval r a b) r\<rparr> \<notin> PartialOrder"
-have 3: "\<not> interval r a b \<subseteq> A"
- by (metis 2 po_subset_po)
-have 4: "b \<notin> A \<or> a \<notin> A"
- by (metis 3 interval_subset)
-have 5: "a \<notin> A"
- by (metis 4 1)
-show "False"
- by (metis 5 0)
+proof -
+ assume A1: "a \<in> A"
+ assume "b \<in> A"
+ hence "\<forall>u. u \<in> A \<longrightarrow> interval r u b \<subseteq> A" by (metis interval_subset)
+ hence "interval r a b \<subseteq> A" using A1 by metis
+ hence "interval r a b \<subseteq> A" by metis
+ thus ?thesis by (metis po_subset_po)
qed
lemma (in CLF) intv_CL_lub:
@@ -1096,9 +1068,9 @@
apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)
done
- declare (in CLF) fixf_po[rule del] P_def [simp del] A_def [simp del] r_def [simp del]
+
+declare (in CLF) fixf_po [rule del] P_def [simp del] A_def [simp del] r_def [simp del]
Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]
CompleteLatticeI_simp [rule del]
-
end
--- a/src/HOL/Metis_Examples/set.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Metis_Examples/set.thy Fri Apr 30 08:47:07 2010 -0700
@@ -12,20 +12,15 @@
(S(x,y) | ~S(y,z) | Q(Z,Z)) &
(Q(X,y) | ~Q(y,Z) | S(X,X))"
by metis
-(*??But metis can't prove the single-step version...*)
-
-
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis
sledgehammer_params [shrink_factor = 1]
-
(*multiple versions of this example*)
lemma (*equal_union: *)
- "(X = Y \<union> Z) =
- (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+ "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
proof (neg_clausify)
fix x
assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
@@ -269,15 +264,14 @@
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
"\<exists>A. a \<notin> A"
- "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
-apply (metis atMost_iff)
-apply (metis emptyE)
-apply (metis insert_iff singletonE)
+ "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
+apply (metis all_not_in_conv)+
+apply (metis mem_def)
apply (metis insertCI singletonE zless_le)
apply (metis Collect_def Collect_mem_eq)
apply (metis Collect_def Collect_mem_eq)
apply (metis DiffE)
-apply (metis pair_in_Id_conv)
+apply (metis pair_in_Id_conv)
done
end
--- a/src/HOL/Sledgehammer.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Sledgehammer.thy Fri Apr 30 08:47:07 2010 -0700
@@ -25,28 +25,28 @@
("Tools/Sledgehammer/metis_tactics.ML")
begin
-definition COMBI :: "'a \<Rightarrow> 'a"
- where "COMBI P \<equiv> P"
+definition COMBI :: "'a \<Rightarrow> 'a" where
+[no_atp]: "COMBI P \<equiv> P"
-definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
- where "COMBK P Q \<equiv> P"
+definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
+[no_atp]: "COMBK P Q \<equiv> P"
-definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
- where "COMBB P Q R \<equiv> P (Q R)"
+definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
+"COMBB P Q R \<equiv> P (Q R)"
-definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
- where "COMBC P Q R \<equiv> P R Q"
+definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
+[no_atp]: "COMBC P Q R \<equiv> P R Q"
-definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
- where "COMBS P Q R \<equiv> P R (Q R)"
+definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
+[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- where "fequal X Y \<equiv> (X = Y)"
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+"fequal X Y \<equiv> (X = Y)"
-lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
+lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
by (simp add: fequal_def)
-lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
+lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
by (simp add: fequal_def)
text{*These two represent the equivalence between Boolean equality and iff.
@@ -61,31 +61,31 @@
text{*Theorems for translation to combinators*}
-lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
+lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBS_def)
done
-lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
+lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBI_def)
done
-lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
+lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBK_def)
done
-lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
+lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBB_def)
done
-lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
+lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBC_def)
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Apr 30 08:47:07 2010 -0700
@@ -70,8 +70,10 @@
case pairself (find_first (fn s => String.isSubstring s output))
(ListPair.unzip delims) of
(SOME begin_delim, SOME end_delim) =>
- output |> first_field begin_delim |> the |> snd
- |> first_field end_delim |> the |> fst
+ (output |> first_field begin_delim |> the |> snd
+ |> first_field end_delim |> the |> fst
+ |> first_field "\n" |> the |> snd
+ handle Option.Option => "")
| _ => ""
fun extract_proof_and_outcome res_code proof_delims known_failures output =
@@ -139,8 +141,8 @@
fun prob_pathname nr =
let
val probfile =
- Path.basic (the_problem_prefix ^
- (if overlord then "_" ^ name else serial_string ())
+ Path.basic ((if overlord then "prob_" ^ name
+ else the_problem_prefix ^ serial_string ())
^ "_" ^ string_of_int nr)
in
if the_dest_dir = "" then File.tmp_path probfile
@@ -260,8 +262,10 @@
arguments = fn timeout =>
"--output_syntax tptp --mode casc -t " ^
string_of_int (to_generous_secs timeout),
- proof_delims = [("=========== Refutation ==========",
- "======= End of refutation =======")],
+ proof_delims =
+ [("=========== Refutation ==========",
+ "======= End of refutation ======="),
+ ("% SZS output start Refutation", "% SZS output end Refutation")],
known_failures =
[(Unprovable, "Satisfiability detected"),
(OutOfResources, "CANNOT PROVE"),
--- a/src/HOL/Tools/Function/fun.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Function/fun.ML Fri Apr 30 08:47:07 2010 -0700
@@ -151,7 +151,7 @@
lthy
|> add fixes statements config pat_completeness_auto |> snd
|> Local_Theory.restore
- |> prove_termination
+ |> prove_termination |> snd
end
val add_fun = gen_add_fun Function.add_function
--- a/src/HOL/Tools/Function/function.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Function/function.ML Fri Apr 30 08:47:07 2010 -0700
@@ -25,8 +25,10 @@
(Attrib.binding * string) list -> Function_Common.function_config ->
local_theory -> Proof.state
- val prove_termination: term option -> tactic -> local_theory -> local_theory
- val prove_termination_cmd: string option -> tactic -> local_theory -> local_theory
+ val prove_termination: term option -> tactic -> local_theory ->
+ info * local_theory
+ val prove_termination_cmd: string option -> tactic -> local_theory ->
+ info * local_theory
val termination : term option -> local_theory -> Proof.state
val termination_cmd : string option -> local_theory -> Proof.state
@@ -195,13 +197,15 @@
((qualify "induct",
[Attrib.internal (K (Rule_Cases.case_names case_names))]),
tinduct)
- |-> (fn (simps, (_, inducts)) =>
+ |-> (fn (simps, (_, inducts)) => fn lthy =>
let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
simps=SOME simps, inducts=SOME inducts, termination=termination }
in
- Local_Theory.declaration false (add_function_data o morph_function_data info')
- #> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)
+ (info',
+ lthy
+ |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+ |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
end)
end
in
@@ -233,7 +237,7 @@
|> ProofContext.note_thmss ""
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
- |> Proof.theorem NONE afterqed [[(goal, [])]]
+ |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
end
val termination = gen_termination Syntax.check_term
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Apr 30 08:47:07 2010 -0700
@@ -1260,15 +1260,15 @@
| t1 $ _ => term_under_def t1
| _ => t
-(* Here we crucially rely on "Refute.specialize_type" performing a preorder
- traversal of the term, without which the wrong occurrence of a constant could
- be matched in the face of overloading. *)
+(* Here we crucially rely on "specialize_type" performing a preorder traversal
+ of the term, without which the wrong occurrence of a constant could be
+ matched in the face of overloading. *)
fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
if is_built_in_const thy stds fast_descrs x then
[]
else
these (Symtab.lookup table s)
- |> map_filter (try (Refute.specialize_type thy x))
+ |> map_filter (try (specialize_type thy x))
|> filter (curry (op =) (Const x) o term_under_def)
fun normalized_rhs_of t =
@@ -1381,8 +1381,8 @@
SOME t' => is_constr_pattern_lhs thy t'
| NONE => false
-(* Similar to "Refute.specialize_type" but returns all matches rather than only
- the first (preorder) match. *)
+(* Similar to "specialize_type" but returns all matches rather than only the
+ first (preorder) match. *)
fun multi_specialize_type thy slack (s, T) t =
let
fun aux (Const (s', T')) ys =
@@ -1390,10 +1390,10 @@
ys |> (if AList.defined (op =) ys T' then
I
else
- cons (T', Refute.monomorphic_term
- (Sign.typ_match thy (T', T) Vartab.empty) t)
+ cons (T', monomorphic_term (Sign.typ_match thy (T', T)
+ Vartab.empty) t)
handle Type.TYPE_MATCH => I
- | Refute.REFUTE _ =>
+ | TERM _ =>
if slack then
I
else
@@ -1682,7 +1682,7 @@
let val abs_T = domain_type T in
typedef_info thy (fst (dest_Type abs_T)) |> the
|> pairf #Abs_inverse #Rep_inverse
- |> pairself (Refute.specialize_type thy x o prop_of o the)
+ |> pairself (specialize_type thy x o prop_of o the)
||> single |> op ::
end
fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
@@ -1697,7 +1697,7 @@
val set_t = Const (set_name, rep_T --> bool_T)
val set_t' =
prop_of_Rep |> HOLogic.dest_Trueprop
- |> Refute.specialize_type thy (dest_Const rep_t)
+ |> specialize_type thy (dest_Const rep_t)
|> HOLogic.dest_mem |> snd
in
[HOLogic.all_const abs_T
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Apr 30 08:47:07 2010 -0700
@@ -914,8 +914,8 @@
val class = Logic.class_of_const s
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
class)
- val ax1 = try (Refute.specialize_type thy x) of_class
- val ax2 = Option.map (Refute.specialize_type thy x o snd)
+ val ax1 = try (specialize_type thy x) of_class
+ val ax2 = Option.map (specialize_type thy x o snd)
(Refute.get_classdef thy class)
in
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
@@ -997,7 +997,7 @@
map (fn t => case Term.add_tvars t [] of
[] => t
| [(x, S)] =>
- Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
+ monomorphic_term (Vartab.make [(x, (S, T))]) t
| _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
\add_axioms_for_sort", [t]))
class_axioms
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Apr 30 08:47:07 2010 -0700
@@ -57,6 +57,8 @@
val bool_T : typ
val nat_T : typ
val int_T : typ
+ val monomorphic_term : Type.tyenv -> term -> term
+ val specialize_type : theory -> (string * typ) -> term -> term
val nat_subscript : int -> string
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -227,6 +229,9 @@
val nat_T = @{typ nat}
val int_T = @{typ int}
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
+
val subscript = implode o map (prefix "\<^isub>") o explode
fun nat_subscript n =
(* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Apr 30 08:47:07 2010 -0700
@@ -123,14 +123,16 @@
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
- | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
+fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
+ metis_lit pos s [Metis.Term.Var s']
+ | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
+ metis_lit pos s [Metis.Term.Fn (s',[])]
fun default_sort _ (TVar _) = false
| default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
fun metis_of_tfree tf =
- Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
+ Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
fun hol_thm_to_fol is_conjecture ctxt mode th =
let val thy = ProofContext.theory_of ctxt
@@ -138,11 +140,12 @@
(literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
in
if is_conjecture then
- (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
+ (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
+ add_type_literals types_sorts)
else
- let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
+ let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
val mtylits = if Config.get ctxt type_lits
- then map (metis_of_typeLit false) tylits else []
+ then map (metis_of_type_literals false) tylits else []
in
(Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
end
@@ -598,7 +601,9 @@
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
- in add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
+ in
+ add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
+ end;
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
@@ -669,7 +674,7 @@
val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
+ app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Apr 30 08:47:07 2010 -0700
@@ -392,13 +392,14 @@
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
-(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
+(* The single-name theorems go after the multiple-name ones, so that single
+ names are preferred when both are available. *)
fun name_thm_pairs respect_no_atp ctxt =
let
val (mults, singles) =
List.partition is_multi (all_valid_thms respect_no_atp ctxt)
- val ps = [] |> fold add_multi_names mults
- |> fold add_single_names singles
+ val ps = [] |> fold add_single_names singles
+ |> fold add_multi_names mults
in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
fun check_named ("", th) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 30 08:47:07 2010 -0700
@@ -44,9 +44,11 @@
TyConstr of name * fol_type list
val string_of_fol_type :
fol_type -> name_pool option -> string * name_pool option
- datatype type_literal = LTVar of string * string | LTFree of string * string
+ datatype type_literal =
+ TyLitVar of string * name |
+ TyLitFree of string * name
exception CLAUSE of string * term
- val add_typs : typ list -> type_literal list
+ val add_type_literals : typ list -> type_literal list
val get_tvar_strs: typ list -> string list
datatype arLit =
TConsLit of class * string * string list
@@ -68,7 +70,7 @@
arity_clause -> int Symtab.table -> int Symtab.table
val init_functab: int Symtab.table
val dfg_sign: bool -> string -> string
- val dfg_of_typeLit: bool -> type_literal -> string
+ val dfg_of_type_literal: bool -> type_literal -> string
val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
val string_of_preds: (string * Int.int) list -> string
val string_of_funcs: (string * int) list -> string
@@ -79,7 +81,8 @@
val dfg_classrel_clause: classrel_clause -> string
val dfg_arity_clause: arity_clause -> string
val tptp_sign: bool -> string -> string
- val tptp_of_typeLit : bool -> type_literal -> string
+ val tptp_of_type_literal :
+ bool -> type_literal -> name_pool option -> string * name_pool option
val gen_tptp_cls : int * string * kind * string list * string list -> string
val tptp_tfree_clause : string -> string
val tptp_arity_clause : arity_clause -> string
@@ -173,9 +176,7 @@
fun paren_pack [] = "" (*empty argument list*)
| paren_pack strings = "(" ^ commas strings ^ ")";
-(*TSTP format uses (...) rather than the old [...]*)
-fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")";
-
+fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")"
(*Remove the initial ' character from a type variable, if it is present*)
fun trim_type_var s =
@@ -230,9 +231,9 @@
fun empty_name_pool readable_names =
if readable_names then SOME (`I Symtab.empty) else NONE
+fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
fun pool_map f xs =
- fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
- o pair []
+ pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
fun add_nice_name full_name nice_prefix j the_pool =
let
@@ -306,8 +307,10 @@
val (ss, pool) = pool_map string_of_fol_type tys pool
in (s ^ paren_pack ss, pool) end
-(*First string is the type class; the second is a TVar or TFfree*)
-datatype type_literal = LTVar of string * string | LTFree of string * string;
+(* The first component is the type class; the second is a TVar or TFree. *)
+datatype type_literal =
+ TyLitVar of string * name |
+ TyLitFree of string * name
exception CLAUSE of string * term;
@@ -317,21 +320,21 @@
let val sorts = sorts_on_typs_aux ((x,i), ss)
in
if s = "HOL.type" then sorts
- else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
- else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
+ else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
+ else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
end;
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
| sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
-fun pred_of_sort (LTVar (s,ty)) = (s,1)
- | pred_of_sort (LTFree (s,ty)) = (s,1)
+fun pred_of_sort (TyLitVar (s, _)) = (s, 1)
+ | pred_of_sort (TyLitFree (s, _)) = (s, 1)
(*Given a list of sorted type variables, return a list of type literals.*)
-fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) []
+fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
- * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
+ * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
in a lemma has the same sort as 'a in the conjecture.
* Deleting such clauses will lead to problems with locales in other use of local results
where 'a is fixed. Probably we should delete clauses unless the sorts agree.
@@ -499,8 +502,10 @@
fun dfg_sign true s = s
| dfg_sign false s = "not(" ^ s ^ ")"
-fun dfg_of_typeLit pos (LTVar (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")")
- | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
+fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) =
+ dfg_sign pos (s ^ "(" ^ s' ^ ")")
+ | dfg_of_type_literal pos (TyLitFree (s, (s', _))) =
+ dfg_sign pos (s ^ "(" ^ s' ^ ")");
(*Enclose the clause body by quantifiers, if necessary*)
fun dfg_forall [] body = body
@@ -563,21 +568,23 @@
fun tptp_sign true s = s
| tptp_sign false s = "~ " ^ s
-fun tptp_of_typeLit pos (LTVar (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
- | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
+fun tptp_of_type_literal pos (TyLitVar (s, name)) =
+ nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
+ | tptp_of_type_literal pos (TyLitFree (s, name)) =
+ nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
fun tptp_cnf name kind formula =
"cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
- (tptp_pack (tylits @ lits))
+ (tptp_clause (tylits @ lits))
| gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
- (tptp_pack lits)
+ (tptp_clause lits)
fun tptp_tfree_clause tfree_lit =
- tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
+ tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit])
fun tptp_of_arLit (TConsLit (c,t,args)) =
tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
@@ -586,11 +593,11 @@
fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
tptp_cnf (string_of_ar axiom_name) "axiom"
- (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
+ (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
fun tptp_classrelLits sub sup =
let val tvar = "(T)"
- in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
+ in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 30 08:47:07 2010 -0700
@@ -302,9 +302,13 @@
(* Given a clause, returns its literals paired with a list of literals
concerning TFrees; the latter should only occur in conjecture clauses. *)
-fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
- pool_map (tptp_literal params) literals
- #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts))
+fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
+ pool =
+ let
+ val (lits, pool) = pool_map (tptp_literal params) literals pool
+ val (tylits, pool) = pool_map (tptp_of_type_literal pos)
+ (add_type_literals ctypes_sorts) pool
+ in ((lits, tylits), pool) end
fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
pool =
@@ -323,7 +327,7 @@
fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
pool_map (dfg_literal params) literals
- #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts))
+ #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
fun get_uvars (CombConst _) vars pool = (vars, pool)
| get_uvars (CombVar (name, _)) vars pool =
@@ -354,19 +358,19 @@
fun add_types tvars = fold add_fol_type_funcs tvars
fun add_decls (full_types, explicit_apply, cma, cnh)
- (CombConst ((c, _), _, tvars)) (funcs, preds) =
- if c = "equal" then
- (add_types tvars funcs, preds)
- else
- let val arity = min_arity_of cma c
- val ntys = if not full_types then length tvars else 0
- val addit = Symtab.update(c, arity+ntys)
- in
- if needs_hBOOL explicit_apply cnh c then
- (add_types tvars (addit funcs), preds)
- else
- (add_types tvars funcs, addit preds)
- end
+ (CombConst ((c, _), ctp, tvars)) (funcs, preds) =
+ (if c = "equal" then
+ (add_types tvars funcs, preds)
+ else
+ let val arity = min_arity_of cma c
+ val ntys = if not full_types then length tvars else 0
+ val addit = Symtab.update(c, arity + ntys)
+ in
+ if needs_hBOOL explicit_apply cnh c then
+ (add_types tvars (addit funcs), preds)
+ else
+ (add_types tvars funcs, addit preds)
+ end) |>> full_types ? add_fol_type_funcs ctp
| add_decls _ (CombVar (_, ctp)) (funcs, preds) =
(add_fol_type_funcs ctp funcs, preds)
| add_decls params (CombApp (P, Q)) decls =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Apr 30 08:47:07 2010 -0700
@@ -42,7 +42,16 @@
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
+(* Hack: Could return false positives (e.g., a user happens to declare a
+ constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+ Long_Name.base_name
+ #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
+val index_in_shape = find_index o exists o curry (op =)
fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
+fun is_conjecture_clause_number conjecture_shape num =
+ index_in_shape num conjecture_shape >= 0
fun ugly_name NONE s = s
| ugly_name (SOME the_pool) s =
@@ -51,15 +60,13 @@
| NONE => s
fun smart_lambda v t =
- Abs (case v of
- Const (s, _) =>
- List.last (space_explode skolem_infix (Long_Name.base_name s))
- | Var ((s, _), _) => s
- | Free (s, _) => s
- | _ => "", fastype_of v, abstract_over (v, t))
-
+ Abs (case v of
+ Const (s, _) =>
+ List.last (space_explode skolem_infix (Long_Name.base_name s))
+ | Var ((s, _), _) => s
+ | Free (s, _) => s
+ | _ => "", fastype_of v, abstract_over (v, t))
fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ smart_lambda v t
datatype ('a, 'b, 'c, 'd, 'e) raw_step =
Definition of 'a * 'b * 'c |
@@ -67,13 +74,30 @@
(**** PARSING OF TSTP FORMAT ****)
+fun strip_spaces_in_list [] = ""
+ | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
+ | strip_spaces_in_list [c1, c2] =
+ strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
+ | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+ if Char.isSpace c1 then
+ strip_spaces_in_list (c2 :: c3 :: cs)
+ else if Char.isSpace c2 then
+ if Char.isSpace c3 then
+ strip_spaces_in_list (c1 :: c3 :: cs)
+ else
+ str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
+ strip_spaces_in_list (c3 :: cs)
+ else
+ str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
+val strip_spaces = strip_spaces_in_list o String.explode
+
(* Syntax trees, either term list or formulae *)
datatype node = IntLeaf of int | StrNode of string * node list
-fun atom x = StrNode (x, [])
+fun str_leaf s = StrNode (s, [])
fun scons (x, y) = StrNode ("cons", [x, y])
-val slist_of = List.foldl scons (atom "nil")
+val slist_of = List.foldl scons (str_leaf "nil")
(*Strings enclosed in single quotes, e.g. filenames*)
val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
@@ -81,19 +105,22 @@
(*Integer constants, typically proof line numbers*)
val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+val parse_dollar_name =
+ Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
+
(* needed for SPASS's output format *)
-fun repair_bool_literal "true" = "c_True"
- | repair_bool_literal "false" = "c_False"
-fun repair_name pool "equal" = "c_equal"
+fun repair_name _ "$true" = "c_True"
+ | repair_name _ "$false" = "c_False"
+ | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
+ | repair_name _ "equal" = "c_equal" (* probably not needed *)
| repair_name pool s = ugly_name pool s
(* Generalized first-order terms, which include file names, numbers, etc. *)
(* The "x" argument is not strictly necessary, but without it Poly/ML loops
forever at compile time. *)
fun parse_term pool x =
- (parse_quoted >> atom
+ (parse_quoted >> str_leaf
|| parse_integer >> IntLeaf
- || $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal)
- || (Symbol.scan_id >> repair_name pool)
+ || (parse_dollar_name >> repair_name pool)
-- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
|| $$ "(" |-- parse_term pool --| $$ ")"
|| $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
@@ -112,16 +139,16 @@
parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
-- parse_term pool)
>> repair_predicate_term
-(* Literals can involve "~", "=", and "!=". *)
fun parse_literal pool x =
($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
-
fun parse_literals pool =
parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
-
-(* Clause: a list of literals separated by disjunction operators ("|"). *)
+fun parse_parenthesized_literals pool =
+ $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
fun parse_clause pool =
- $$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
+ parse_parenthesized_literals pool
+ ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
+ >> List.concat
fun ints_of_node (IntLeaf n) = cons n
| ints_of_node (StrNode (_, us)) = fold ints_of_node us
@@ -158,27 +185,34 @@
Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
--| Scan.option ($$ ","))) []
-(* It is not clear why some literals are followed by sequences of stars. We
- ignore them. *)
-fun parse_starred_predicate_term pool =
- parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
+(* It is not clear why some literals are followed by sequences of stars and/or
+ pluses. We ignore them. *)
+fun parse_decorated_predicate_term pool =
+ parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
fun parse_horn_clause pool =
- Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
- -- Scan.repeat (parse_starred_predicate_term pool)
- >> (fn ([], []) => [atom "c_False"]
- | (clauses1, clauses2) => map negate_node clauses1 @ clauses2)
+ Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
+ -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
+ -- Scan.repeat (parse_decorated_predicate_term pool)
+ >> (fn (([], []), []) => [str_leaf "c_False"]
+ | ((clauses1, clauses2), clauses3) =>
+ map negate_node (clauses1 @ clauses2) @ clauses3)
-(* Syntax: <num>[0:<inference><annotations>] ||
- <cnf_formulas> -> <cnf_formulas>. *)
+(* Syntax: <num>[0:<inference><annotations>]
+ <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
fun parse_spass_line pool =
parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
- -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
- -- parse_horn_clause pool --| $$ "."
+ -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
>> finish_spass_line
-fun parse_line pool = fst o (parse_tstp_line pool || parse_spass_line pool)
+fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
+fun parse_lines pool = Scan.repeat1 (parse_line pool)
+fun parse_proof pool =
+ fst o Scan.finite Symbol.stopper
+ (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
+ (parse_lines pool)))
+ o explode o strip_spaces
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
@@ -346,28 +380,48 @@
(*Update TVars/TFrees with detected sort constraints.*)
fun repair_sorts vt =
- let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
- | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
- | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
- fun tmsubst (Const (a, T)) = Const (a, tysubst T)
- | tmsubst (Free (a, T)) = Free (a, tysubst T)
- | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
- | tmsubst (t as Bound _) = t
- | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
- | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
- in not (Vartab.is_empty vt) ? tmsubst end;
+ let
+ fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
+ | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
+ | do_type (TFree (x, s)) =
+ TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
+ fun do_term (Const (a, T)) = Const (a, do_type T)
+ | do_term (Free (a, T)) = Free (a, do_type T)
+ | do_term (Var (xi, T)) = Var (xi, do_type T)
+ | do_term (t as Bound _) = t
+ | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
+ | do_term (t1 $ t2) = do_term t1 $ do_term t2
+ in not (Vartab.is_empty vt) ? do_term end
+
+fun unskolemize_term t =
+ fold forall_of (Term.add_consts t []
+ |> filter (is_skolem_const_name o fst) |> map Const) t
+
+val combinator_table =
+ [(@{const_name COMBI}, @{thm COMBI_def_raw}),
+ (@{const_name COMBK}, @{thm COMBK_def_raw}),
+ (@{const_name COMBB}, @{thm COMBB_def_raw}),
+ (@{const_name COMBC}, @{thm COMBC_def_raw}),
+ (@{const_name COMBS}, @{thm COMBS_def_raw})]
+
+fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
+ | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
+ | uncombine_term (t as Const (x as (s, _))) =
+ (case AList.lookup (op =) combinator_table s of
+ SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+ | NONE => t)
+ | uncombine_term t = t
(* Interpret a list of syntax trees as a clause, given by "real" literals and
sort constraints. "vt" holds the initial sort constraints, from the
conjecture clauses. *)
fun clause_of_nodes ctxt vt us =
- let val (vt, dt) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
- dt |> repair_sorts vt
+ let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
+ t |> repair_sorts vt
end
-fun check_clause ctxt =
+fun check_formula ctxt =
TypeInfer.constrain HOLogic.boolT
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
-fun checked_clause_of_nodes ctxt = check_clause ctxt oo clause_of_nodes ctxt
(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
clauses. **)
@@ -394,22 +448,26 @@
fun decode_line vt (Definition (num, u, us)) ctxt =
let
- val cl1 = clause_of_nodes ctxt vt [u]
- val vars = snd (strip_comb cl1)
+ val t1 = clause_of_nodes ctxt vt [u]
+ val vars = snd (strip_comb t1)
val frees = map unvarify_term vars
val unvarify_args = subst_atomic (vars ~~ frees)
- val cl2 = clause_of_nodes ctxt vt us
- val (cl1, cl2) =
- HOLogic.eq_const HOLogic.typeT $ cl1 $ cl2
- |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
+ val t2 = clause_of_nodes ctxt vt us
+ val (t1, t2) =
+ HOLogic.eq_const HOLogic.typeT $ t1 $ t2
+ |> unvarify_args |> uncombine_term |> check_formula ctxt
+ |> HOLogic.dest_eq
in
- (Definition (num, cl1, cl2),
- fold Variable.declare_term (maps OldTerm.term_frees [cl1, cl2]) ctxt)
+ (Definition (num, t1, t2),
+ fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
end
| decode_line vt (Inference (num, us, deps)) ctxt =
- let val cl = us |> clause_of_nodes ctxt vt |> check_clause ctxt in
- (Inference (num, cl, deps),
- fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+ let
+ val t = us |> clause_of_nodes ctxt vt
+ |> unskolemize_term |> uncombine_term |> check_formula ctxt
+ in
+ (Inference (num, t, deps),
+ fold Variable.declare_term (OldTerm.term_frees t) ctxt)
end
fun decode_lines ctxt lines =
let
@@ -431,9 +489,10 @@
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
only in type information.*)
-fun add_line _ (line as Definition _) lines = line :: lines
- | add_line thm_names (Inference (num, t, [])) lines =
- (* No dependencies: axiom or conjecture clause *)
+fun add_line _ _ (line as Definition _) lines = line :: lines
+ | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
+ (* No dependencies: axiom, conjecture clause, or internal axioms or
+ definitions (Vampire). *)
if is_axiom_clause_number thm_names num then
(* Axioms are not proof lines. *)
if is_only_type_information t then
@@ -443,9 +502,11 @@
(_, []) => lines (*no repetition of proof line*)
| (pre, Inference (num', _, _) :: post) =>
pre @ map (replace_deps_in_line (num', [num])) post
- else
+ else if is_conjecture_clause_number conjecture_shape num then
Inference (num, t, []) :: lines
- | add_line _ (Inference (num, t, deps)) lines =
+ else
+ map (replace_deps_in_line (num, [])) lines
+ | add_line _ _ (Inference (num, t, deps)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
Inference (num, t, deps) :: lines
@@ -466,21 +527,32 @@
and delete_dep num lines =
fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
-fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
- | is_bad_free _ = false
+(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
+ removing the offending lines often does the trick. *)
+fun is_bad_free frees (Free x) = not (member (op =) frees x)
+ | is_bad_free _ _ = false
-fun add_desired_line _ _ (line as Definition _) (j, lines) = (j, line :: lines)
- | add_desired_line ctxt _ (Inference (num, t, [])) (j, lines) =
- (j, Inference (num, t, []) :: lines) (* conjecture clauses must be kept *)
- | add_desired_line ctxt shrink_factor (Inference (num, t, deps)) (j, lines) =
+(* Vampire is keen on producing these. *)
+fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
+ $ t1 $ t2)) = (t1 aconv t2)
+ | is_trivial_formula t = false
+
+fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
+ (j, line :: lines)
+ | add_desired_line ctxt shrink_factor conjecture_shape thm_names frees
+ (Inference (num, t, deps)) (j, lines) =
(j + 1,
- if is_only_type_information t orelse
- not (null (Term.add_tvars t [])) orelse
- exists_subterm is_bad_free t orelse
- (length deps < 2 orelse j mod shrink_factor <> 0) then
- map (replace_deps_in_line (num, deps)) lines (* delete line *)
+ if is_axiom_clause_number thm_names num orelse
+ is_conjecture_clause_number conjecture_shape num orelse
+ (not (is_only_type_information t) andalso
+ null (Term.add_tvars t []) andalso
+ not (exists_subterm (is_bad_free frees) t) andalso
+ not (is_trivial_formula t) andalso
+ (null lines orelse (* last line must be kept *)
+ (length deps >= 2 andalso j mod shrink_factor = 0))) then
+ Inference (num, t, deps) :: lines (* keep line *)
else
- Inference (num, t, deps) :: lines)
+ map (replace_deps_in_line (num, deps)) lines) (* drop line *)
(** EXTRACTING LEMMAS **)
@@ -493,8 +565,6 @@
let
val tokens_of = String.tokens (not o is_ident_char)
fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
- | extract_num ("cnf" :: num :: "negated_conjecture" :: _) =
- Int.fromString num
| extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
| extract_num _ = NONE
in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
@@ -506,10 +576,9 @@
fun apply_command _ 1 = "by "
| apply_command 1 _ = "apply "
| apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
-fun metis_command i n [] =
- apply_command i n ^ "metis"
- | metis_command i n xs =
- apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")"
+fun metis_command i n [] = apply_command i n ^ "metis"
+ | metis_command i n ss =
+ apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
fun metis_line i n xs =
"Try this command: " ^
Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
@@ -532,9 +601,6 @@
val n = Logic.count_prems (prop_of goal)
in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
-val is_valid_line =
- String.isPrefix "fof(" orf String.isPrefix "cnf(" orf String.isSubstring "||"
-
(** Isar proof construction and manipulation **)
fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
@@ -551,13 +617,18 @@
Assume of label * term |
Have of qualifier list * label * term * byline
and byline =
- Facts of facts |
+ ByMetis of facts |
CaseSplit of step list list * facts
+fun smart_case_split [] facts = ByMetis facts
+ | smart_case_split proofs facts = CaseSplit (proofs, facts)
+
val raw_prefix = "X"
val assum_prefix = "A"
val fact_prefix = "F"
+fun string_for_label (s, num) = s ^ string_of_int num
+
fun add_fact_from_dep thm_names num =
if is_axiom_clause_number thm_names num then
apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
@@ -571,35 +642,19 @@
| step_for_line thm_names j (Inference (num, t, deps)) =
Have (if j = 1 then [Show] else [], (raw_prefix, num),
forall_vars t,
- Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
+ ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
-fun strip_spaces_in_list [] = ""
- | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
- | strip_spaces_in_list [c1, c2] =
- strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
- | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
- if Char.isSpace c1 then
- strip_spaces_in_list (c2 :: c3 :: cs)
- else if Char.isSpace c2 then
- if Char.isSpace c3 then
- strip_spaces_in_list (c1 :: c3 :: cs)
- else
- str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
- strip_spaces_in_list (c3 :: cs)
- else
- str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
-
-fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees =
+fun proof_from_atp_proof pool ctxt shrink_factor atp_proof conjecture_shape
+ thm_names frees =
let
val lines =
- atp_proof
- |> split_lines |> map strip_spaces |> filter is_valid_line
- |> map (parse_line pool o explode)
+ atp_proof ^ "$" (* the $ sign acts as a sentinel *)
+ |> parse_proof pool
|> decode_lines ctxt
- |> rpair [] |-> fold_rev (add_line thm_names)
+ |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
|> rpair [] |-> fold_rev add_nontrivial_line
- |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
+ |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor
+ conjecture_shape thm_names frees)
|> snd
in
(if null frees then [] else [Fix frees]) @
@@ -618,12 +673,13 @@
"drop_ls" are those that should be dropped in a case split. *)
type backpatches = (label * facts) list * (label list * label list)
-fun using_of_step (Have (_, _, _, by)) =
+fun used_labels_of_step (Have (_, _, _, by)) =
(case by of
- Facts (ls, _) => ls
- | CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls)
- | using_of_step _ = []
-and using_of proof = fold (union (op =) o using_of_step) proof []
+ ByMetis (ls, _) => ls
+ | CaseSplit (proofs, (ls, _)) =>
+ fold (union (op =) o used_labels_of) proofs ls)
+ | used_labels_of_step _ = []
+and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
fun new_labels_of_step (Fix _) = []
| new_labels_of_step (Let _) = []
@@ -644,7 +700,7 @@
if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
| _ => false) (tl proofs) andalso
not (exists (member (op =) (maps new_labels_of proofs))
- (using_of proof_tail)) then
+ (used_labels_of proof_tail)) then
SOME (l, t, map rev proofs, proof_tail)
else
NONE
@@ -657,23 +713,21 @@
| 1 => [Then]
| _ => [Ultimately]
-val index_in_shape = find_index o exists o curry (op =)
-
fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
let
val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
- fun find_hyp (_, j) = nth hyp_ts (index_in_shape j conjecture_shape)
+ fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
fun first_pass ([], contra) = ([], contra)
| first_pass ((step as Fix _) :: proof, contra) =
first_pass (proof, contra) |>> cons step
| first_pass ((step as Let _) :: proof, contra) =
first_pass (proof, contra) |>> cons step
- | first_pass ((step as Assume (l, t)) :: proof, contra) =
+ | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
if member (op =) concl_ls l then
first_pass (proof, contra ||> cons step)
else
- first_pass (proof, contra) |>> cons (Assume (l, find_hyp l))
- | first_pass ((step as Have (qs, l, t, Facts (ls, ss))) :: proof,
+ first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
+ | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof,
contra) =
if exists (member (op =) (fst contra)) ls then
first_pass (proof, contra |>> cons l ||> cons step)
@@ -691,10 +745,10 @@
clause_for_literals thy (map (negate_term thy o fst) assums)
else
concl_t,
- Facts (backpatch_labels patches (map snd assums)))], patches)
+ ByMetis (backpatch_labels patches (map snd assums)))], patches)
| second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
second_pass end_qs (proof, (t, l) :: assums, patches)
- | second_pass end_qs (Have (qs, l, t, Facts (ls, ss)) :: proof, assums,
+ | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
patches) =
if member (op =) (snd (snd patches)) l andalso
not (AList.defined (op =) (fst patches) l) then
@@ -710,7 +764,7 @@
Assume (l, negate_term thy t)
else
Have (qs, l, negate_term thy t,
- Facts (backpatch_label patches l)))
+ ByMetis (backpatch_label patches l)))
else
second_pass end_qs (proof, assums,
patches |>> cons (contra_l, (co_ls, ss)))
@@ -737,10 +791,10 @@
SOME (l, t, proofs, proof_tail) =>
Have (case_split_qualifiers proofs @
(if null proof_tail then end_qs else []), l, t,
- CaseSplit (proofs, facts)) :: proof_tail
+ smart_case_split proofs facts) :: proof_tail
| NONE =>
[Have (case_split_qualifiers proofs @ end_qs, no_label,
- concl_t, CaseSplit (proofs, facts))],
+ concl_t, smart_case_split proofs facts)],
patches)
end
| _ => raise Fail "malformed proof")
@@ -760,7 +814,7 @@
| do_step (Have (qs, l, t, by)) (proof, subst, assums) =
(Have (qs, l, t,
case by of
- Facts facts => Facts (relabel_facts subst facts)
+ ByMetis facts => ByMetis (relabel_facts subst facts)
| CaseSplit (proofs, facts) =>
CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
proof, subst, assums)
@@ -768,33 +822,18 @@
and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
in do_proof end
-
-(* Hack: Could return false positives (e.g., a user happens to declare a
- constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
- Long_Name.base_name
- #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
-fun unskolemize_term t =
- fold exists_of (Term.add_consts t []
- |> filter (is_skolem_const_name o fst) |> map Const) t
-
-fun unskolemize_step (Have (qs, l, t, by)) =
- Have (qs, l, unskolemize_term t, by)
- | unskolemize_step step = step
-
val then_chain_proof =
let
fun aux _ [] = []
| aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
| aux l' (Have (qs, l, t, by) :: proof) =
(case by of
- Facts (ls, ss) =>
+ ByMetis (ls, ss) =>
Have (if member (op =) ls l' then
(Then :: qs, l, t,
- Facts (filter_out (curry (op =) l') ls, ss))
+ ByMetis (filter_out (curry (op =) l') ls, ss))
else
- (qs, l, t, Facts (ls, ss)))
+ (qs, l, t, ByMetis (ls, ss)))
| CaseSplit (proofs, facts) =>
Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
aux l proof
@@ -803,17 +842,17 @@
fun kill_useless_labels_in_proof proof =
let
- val used_ls = using_of proof
+ val used_ls = used_labels_of proof
fun do_label l = if member (op =) used_ls l then l else no_label
- fun kill (Assume (l, t)) = Assume (do_label l, t)
- | kill (Have (qs, l, t, by)) =
+ fun do_step (Assume (l, t)) = Assume (do_label l, t)
+ | do_step (Have (qs, l, t, by)) =
Have (qs, do_label l, t,
case by of
CaseSplit (proofs, facts) =>
- CaseSplit (map (map kill) proofs, facts)
+ CaseSplit (map (map do_step) proofs, facts)
| _ => by)
- | kill step = step
- in map kill proof end
+ | do_step step = step
+ in map do_step proof end
fun prefix_for_depth n = replicate_string (n + 1)
@@ -837,10 +876,15 @@
let
val l' = (prefix_for_depth depth fact_prefix, next_fact)
in (l', (l, l') :: subst, next_fact + 1) end
- val relabel_facts = apfst (map_filter (AList.lookup (op =) subst))
+ val relabel_facts =
+ apfst (map (fn l =>
+ case AList.lookup (op =) subst l of
+ SOME l' => l'
+ | NONE => raise Fail ("unknown label " ^
+ quote (string_for_label l))))
val by =
case by of
- Facts facts => Facts (relabel_facts facts)
+ ByMetis facts => ByMetis (relabel_facts facts)
| CaseSplit (proofs, facts) =>
CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
relabel_facts facts)
@@ -861,8 +905,7 @@
fun do_free (s, T) =
maybe_quote s ^ " :: " ^
maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
- fun do_raw_label (s, j) = s ^ string_of_int j
- fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
+ fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
fun do_have qs =
(if member (op =) qs Moreover then "moreover " else "") ^
(if member (op =) qs Ultimately then "ultimately " else "") ^
@@ -871,18 +914,18 @@
else
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- fun do_using [] = ""
- | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
- fun do_by_facts [] = "by metis"
- | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")"
- fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss
+ fun do_facts (ls, ss) =
+ let
+ val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
+ val ss = ss |> sort_distinct string_ord
+ in metis_command 1 1 (map string_for_label ls @ ss) end
and do_step ind (Fix xs) =
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
| do_step ind (Let (t1, t2)) =
do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
| do_step ind (Assume (l, t)) =
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
- | do_step ind (Have (qs, l, t, Facts facts)) =
+ | do_step ind (Have (qs, l, t, ByMetis facts)) =
do_indent ind ^ do_have qs ^ " " ^
do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
| do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
@@ -898,8 +941,9 @@
suffix ^ "\n"
end
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
- (* One-step proofs are pointless; better use the Metis one-liner. *)
- and do_proof [_] = ""
+ (* One-step proofs are pointless; better use the Metis one-liner
+ directly. *)
+ and do_proof [Have (_, _, _, ByMetis _)] = ""
| do_proof proof =
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
do_indent 0 ^ "proof -\n" ^
@@ -916,11 +960,10 @@
val (one_line_proof, lemma_names) =
metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
fun isar_proof_for () =
- case proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names
- frees
+ case proof_from_atp_proof pool ctxt shrink_factor atp_proof
+ conjecture_shape thm_names frees
|> redirect_proof thy conjecture_shape hyp_ts concl_t
|> kill_duplicate_assumptions_in_proof
- |> map unskolemize_step
|> then_chain_proof
|> kill_useless_labels_in_proof
|> relabel_proof
@@ -935,7 +978,8 @@
|> the_default "Warning: The Isar proof construction failed.\n"
in (one_line_proof ^ isar_proof, lemma_names) end
-fun proof_text isar_proof isar_params =
- if isar_proof then isar_proof_text isar_params else metis_proof_text
+fun proof_text isar_proof isar_params other_params =
+ (if isar_proof then isar_proof_text isar_params else metis_proof_text)
+ other_params
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 30 08:47:07 2010 -0700
@@ -18,6 +18,8 @@
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
+ val monomorphic_term : Type.tyenv -> term -> term
+ val specialize_type : theory -> (string * typ) -> term -> term
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -103,4 +105,30 @@
OuterKeyword.is_keyword s) ? quote
end
+fun monomorphic_term subst t =
+ map_types (map_type_tvar (fn v =>
+ case Type.lookup subst v of
+ SOME typ => typ
+ | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
+ \variable", [t]))) t
+
+fun specialize_type thy (s, T) t =
+ let
+ fun subst_for (Const (s', T')) =
+ if s = s' then
+ SOME (Sign.typ_match thy (T', T) Vartab.empty)
+ handle Type.TYPE_MATCH => NONE
+ else
+ NONE
+ | subst_for (t1 $ t2) =
+ (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
+ | subst_for (Abs (_, _, t')) = subst_for t'
+ | subst_for _ = NONE
+ in
+ case subst_for t of
+ SOME subst => monomorphic_term subst t
+ | NONE => raise Type.TYPE_MATCH
+ end
+
+
end;
--- a/src/HOL/Tools/refute.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/refute.ML Fri Apr 30 08:47:07 2010 -0700
@@ -70,8 +70,6 @@
val is_IDT_constructor : theory -> string * typ -> bool
val is_IDT_recursor : theory -> string * typ -> bool
val is_const_of_class: theory -> string * typ -> bool
- val monomorphic_term : Type.tyenv -> term -> term
- val specialize_type : theory -> (string * typ) -> term -> term
val string_of_typ : typ -> string
val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
end; (* signature REFUTE *)
@@ -449,57 +447,8 @@
Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
end;
-(* ------------------------------------------------------------------------- *)
-(* monomorphic_term: applies a type substitution 'typeSubs' for all type *)
-(* variables in a term 't' *)
-(* ------------------------------------------------------------------------- *)
-
- (* Type.tyenv -> Term.term -> Term.term *)
-
- fun monomorphic_term typeSubs t =
- map_types (map_type_tvar
- (fn v =>
- case Type.lookup typeSubs v of
- NONE =>
- (* schematic type variable not instantiated *)
- raise REFUTE ("monomorphic_term",
- "no substitution for type variable " ^ fst (fst v) ^
- " in term " ^ Syntax.string_of_term_global Pure.thy t)
- | SOME typ =>
- typ)) t;
-
-(* ------------------------------------------------------------------------- *)
-(* specialize_type: given a constant 's' of type 'T', which is a subterm of *)
-(* 't', where 't' has a (possibly) more general type, the *)
-(* schematic type variables in 't' are instantiated to *)
-(* match the type 'T' (may raise Type.TYPE_MATCH) *)
-(* ------------------------------------------------------------------------- *)
-
- (* theory -> (string * Term.typ) -> Term.term -> Term.term *)
-
- fun specialize_type thy (s, T) t =
- let
- fun find_typeSubs (Const (s', T')) =
- if s=s' then
- SOME (Sign.typ_match thy (T', T) Vartab.empty)
- handle Type.TYPE_MATCH => NONE
- else
- NONE
- | find_typeSubs (Free _) = NONE
- | find_typeSubs (Var _) = NONE
- | find_typeSubs (Bound _) = NONE
- | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
- | find_typeSubs (t1 $ t2) =
- (case find_typeSubs t1 of SOME x => SOME x
- | NONE => find_typeSubs t2)
- in
- case find_typeSubs t of
- SOME typeSubs =>
- monomorphic_term typeSubs t
- | NONE =>
- (* no match found - perhaps due to sort constraints *)
- raise Type.TYPE_MATCH
- end;
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
(* ------------------------------------------------------------------------- *)
(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *)
--- a/src/HOL/Tools/simpdata.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOL/Tools/simpdata.ML Fri Apr 30 08:47:07 2010 -0700
@@ -48,7 +48,7 @@
| _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
| _ => th RS @{thm Eq_TrueI}
-fun mk_eq_True r =
+fun mk_eq_True (_: simpset) r =
SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
(* Produce theorems of the form
@@ -80,7 +80,7 @@
end;
(*Congruence rules for = (instead of ==)*)
-fun mk_meta_cong rl = zero_var_indexes
+fun mk_meta_cong (_: simpset) rl = zero_var_indexes
(let val rl' = Seq.hd (TRYALL (fn i => fn st =>
rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
in mk_meta_eq rl' handle THM _ =>
@@ -107,7 +107,7 @@
end;
in atoms end;
-fun mksimps pairs =
+fun mksimps pairs (_: simpset) =
map_filter (try mk_eq) o mk_atomize pairs o gen_all;
fun unsafe_solver_tac prems =
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Apr 30 08:47:07 2010 -0700
@@ -67,7 +67,7 @@
"Finite (mksch A B$tr$x$y) --> Finite tr"
-declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (K NONE))) *}
subsection "mksch rewrite rules"
@@ -967,7 +967,7 @@
done
-declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (SOME o symmetric_fun))) *}
end
--- a/src/Provers/hypsubst.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/Provers/hypsubst.ML Fri Apr 30 08:47:07 2010 -0700
@@ -156,7 +156,7 @@
let
val (k, _) = eq_var bnd true Bi
val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
- setmksimps (mk_eqs bnd)
+ setmksimps (K (mk_eqs bnd))
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
etac thin_rl i, rotate_tac (~k) i]
end handle THM _ => no_tac | EQ_VAR => no_tac) i st
--- a/src/Pure/Isar/proof_context.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/Pure/Isar/proof_context.ML Fri Apr 30 08:47:07 2010 -0700
@@ -505,7 +505,10 @@
fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
fun read_const ctxt strict ty text =
- let val (c, pos) = token_content text in
+ let
+ val (c, pos) = token_content text;
+ val _ = no_skolem false c;
+ in
(case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
(SOME x, false) =>
(Position.report (Markup.name x
--- a/src/Pure/meta_simplifier.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/Pure/meta_simplifier.ML Fri Apr 30 08:47:07 2010 -0700
@@ -51,10 +51,10 @@
val addsimprocs: simpset * simproc list -> simpset
val delsimprocs: simpset * simproc list -> simpset
val mksimps: simpset -> thm -> thm list
- val setmksimps: simpset * (thm -> thm list) -> simpset
- val setmkcong: simpset * (thm -> thm) -> simpset
- val setmksym: simpset * (thm -> thm option) -> simpset
- val setmkeqTrue: simpset * (thm -> thm option) -> simpset
+ val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
+ val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
+ val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
+ val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
val settermless: simpset * (term * term -> bool) -> simpset
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
val setloop': simpset * (simpset -> int -> tactic) -> simpset
@@ -92,10 +92,10 @@
{congs: (string * thm) list * string list,
procs: proc Net.net,
mk_rews:
- {mk: thm -> thm list,
- mk_cong: thm -> thm,
- mk_sym: thm -> thm option,
- mk_eq_True: thm -> thm option,
+ {mk: simpset -> thm -> thm list,
+ mk_cong: simpset -> thm -> thm,
+ mk_sym: simpset -> thm -> thm option,
+ mk_eq_True: simpset -> thm -> thm option,
reorient: theory -> term list -> term -> term -> bool},
termless: term * term -> bool,
subgoal_tac: simpset -> int -> tactic,
@@ -181,13 +181,6 @@
mk_eq_True: turn P into P == True;
termless: relation for ordered rewriting;*)
-type mk_rews =
- {mk: thm -> thm list,
- mk_cong: thm -> thm,
- mk_sym: thm -> thm option,
- mk_eq_True: thm -> thm option,
- reorient: theory -> term list -> term -> term -> bool};
-
datatype simpset =
Simpset of
{rules: rrule Net.net,
@@ -197,7 +190,12 @@
context: Proof.context option} *
{congs: (string * thm) list * string list,
procs: proc Net.net,
- mk_rews: mk_rews,
+ mk_rews:
+ {mk: simpset -> thm -> thm list,
+ mk_cong: simpset -> thm -> thm,
+ mk_sym: simpset -> thm -> thm option,
+ mk_eq_True: simpset -> thm -> thm option,
+ reorient: theory -> term list -> term -> term -> bool},
termless: term * term -> bool,
subgoal_tac: simpset -> int -> tactic,
loop_tacs: (string * (simpset -> int -> tactic)) list,
@@ -458,8 +456,8 @@
else (lhs, rhs)
end;
-fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
- (case mk_eq_True thm of
+fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
+ (case mk_eq_True ss thm of
NONE => []
| SOME eq_True =>
let
@@ -495,7 +493,7 @@
if reorient thy prems rhs lhs
then mk_eq_True ss (thm, name)
else
- (case mk_sym thm of
+ (case mk_sym ss thm of
NONE => []
| SOME thm' =>
let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
@@ -503,8 +501,8 @@
else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
end;
-fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
- maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk thm)) thms;
+fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
+ maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
fun extract_safe_rrules (ss, thm) =
maps (orient_rrule ss) (extract_rews (ss, [thm]));
@@ -588,7 +586,7 @@
if is_full_cong thm then NONE else SOME a);
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
-fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
+fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
in
@@ -674,7 +672,7 @@
in
-fun mksimps (Simpset (_, {mk_rews = {mk, ...}, ...})) = mk;
+fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
@@ -762,14 +760,14 @@
init_ss mk_rews termless subgoal_tac solvers
|> inherit_context ss;
-val basic_mk_rews: mk_rews =
- {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
- mk_cong = I,
- mk_sym = SOME o Drule.symmetric_fun,
- mk_eq_True = K NONE,
- reorient = default_reorient};
-
-val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []);
+val empty_ss =
+ init_ss
+ {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
+ mk_cong = K I,
+ mk_sym = K (SOME o Drule.symmetric_fun),
+ mk_eq_True = K (K NONE),
+ reorient = default_reorient}
+ Term_Ord.termless (K (K no_tac)) ([], []);
(* merge *) (*NOTE: ignores some fields of 2nd simpset*)
--- a/src/Pure/simplifier.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/Pure/simplifier.ML Fri Apr 30 08:47:07 2010 -0700
@@ -411,7 +411,7 @@
empty_ss setsubgoaler asm_simp_tac
setSSolver safe_solver
setSolver unsafe_solver
- setmksimps mksimps
+ setmksimps (K mksimps)
end));
end;
--- a/src/Sequents/simpdata.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/Sequents/simpdata.ML Fri Apr 30 08:47:07 2010 -0700
@@ -47,7 +47,7 @@
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong rl =
+fun mk_meta_cong (_: simpset) rl =
Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
@@ -71,7 +71,7 @@
setsubgoaler asm_simp_tac
setSSolver (mk_solver "safe" safe_solver)
setSolver (mk_solver "unsafe" unsafe_solver)
- setmksimps (map mk_meta_eq o atomize o gen_all)
+ setmksimps (K (map mk_meta_eq o atomize o gen_all))
setmkcong mk_meta_cong;
val LK_simps =
--- a/src/ZF/Main_ZF.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/ZF/Main_ZF.thy Fri Apr 30 08:47:07 2010 -0700
@@ -71,7 +71,7 @@
declaration {* fn _ =>
- Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
+ Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
*}
end
--- a/src/ZF/OrdQuant.thy Thu Apr 29 15:24:22 2010 -0700
+++ b/src/ZF/OrdQuant.thy Fri Apr 30 08:47:07 2010 -0700
@@ -363,7 +363,7 @@
ZF_mem_pairs);
*}
declaration {* fn _ =>
- Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
+ Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
*}
text {* Setting up the one-point-rule simproc *}
--- a/src/ZF/Tools/ind_cases.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/ZF/Tools/ind_cases.ML Fri Apr 30 08:47:07 2010 -0700
@@ -6,7 +6,7 @@
signature IND_CASES =
sig
- val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
+ val declare: string -> (Proof.context -> conv) -> theory -> theory
val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
val setup: theory -> theory
end;
@@ -19,7 +19,7 @@
structure IndCasesData = Theory_Data
(
- type T = (simpset -> cterm -> thm) Symtab.table;
+ type T = (Proof.context -> cterm -> thm) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data = Symtab.merge (K true) data;
@@ -28,16 +28,17 @@
fun declare name f = IndCasesData.map (Symtab.update (name, f));
-fun smart_cases thy ss read_prop s =
+fun smart_cases ctxt s =
let
+ val thy = ProofContext.theory_of ctxt;
fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
- val A = read_prop s handle ERROR msg => err msg;
+ val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
(Logic.strip_imp_concl A)))))) handle TERM _ => err "";
in
(case Symtab.lookup (IndCasesData.get thy) c of
NONE => error ("Unknown inductive cases rule for set " ^ quote c)
- | SOME f => f ss (Thm.cterm_of thy A))
+ | SOME f => f ctxt (Thm.cterm_of thy A))
end;
@@ -45,10 +46,10 @@
fun inductive_cases args thy =
let
- val mk_cases = smart_cases thy (global_simpset_of thy) (Syntax.read_prop_global thy);
+ val ctxt = ProofContext.init thy;
val facts = args |> map (fn ((name, srcs), props) =>
((name, map (Attrib.attribute thy) srcs),
- map (Thm.no_attributes o single o mk_cases) props));
+ map (Thm.no_attributes o single o smart_cases ctxt) props));
in thy |> PureThy.note_thmss "" facts |> snd end;
@@ -57,10 +58,7 @@
val setup =
Method.setup @{binding "ind_cases"}
(Scan.lift (Scan.repeat1 Args.name_source) >>
- (fn props => fn ctxt =>
- props
- |> map (smart_cases (ProofContext.theory_of ctxt) (simpset_of ctxt) (Syntax.read_prop ctxt))
- |> Method.erule 0))
+ (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props)))
"dynamic case analysis on sets";
--- a/src/ZF/Tools/inductive_package.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/ZF/Tools/inductive_package.ML Fri Apr 30 08:47:07 2010 -0700
@@ -268,9 +268,9 @@
the given defs. Cannot simply use the local con_defs because
con_defs=[] for inference systems.
Proposition A should have the form t:Si where Si is an inductive set*)
- fun make_cases ss A =
+ fun make_cases ctxt A =
rule_by_tactic
- (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
+ (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac)
(Thm.assume A RS elim)
|> Drule.export_without_context_open;
@@ -328,7 +328,7 @@
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
If the premises get simplified, then the proofs could fail.*)
val min_ss = Simplifier.global_context thy empty_ss
- setmksimps (map mk_eq o ZF_atomize o gen_all)
+ setmksimps (K (map mk_eq o ZF_atomize o gen_all))
setSolver (mk_solver "minimal"
(fn prems => resolve_tac (triv_rls@prems)
ORELSE' assume_tac
--- a/src/ZF/simpdata.ML Thu Apr 29 15:24:22 2010 -0700
+++ b/src/ZF/simpdata.ML Fri Apr 30 08:47:07 2010 -0700
@@ -44,7 +44,7 @@
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
change_simpset (fn ss =>
- ss setmksimps (map mk_eq o ZF_atomize o gen_all)
+ ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
addcongs [@{thm if_weak_cong}]);
local