# HG changeset patch # User paulson # Date 1191493978 -7200 # Node ID 646bdc51eb7deef44d83170f03fda1019161c841 # Parent 78e6a3cea367e889f749d7fc47ed6b353922cc8d combinator translation diff -r 78e6a3cea367 -r 646bdc51eb7d src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Wed Oct 03 22:33:17 2007 +0200 +++ b/src/HOL/ATP_Linkup.thy Thu Oct 04 12:32:58 2007 +0200 @@ -56,24 +56,6 @@ lemma equal_imp_fequal: "X=Y ==> fequal X Y" by (simp add: fequal_def) -lemma K_simp: "COMBK P == (%Q. P)" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBK_def) -done - -lemma I_simp: "COMBI == (%P. P)" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBI_def) -done - -lemma B_simp: "COMBB P Q == %R. P (Q R)" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBB_def) -done - text{*These two represent the equivalence between Boolean equality and iff. They can't be converted to clauses automatically, as the iff would be expanded...*} @@ -84,8 +66,41 @@ lemma iff_negative: "~P | ~Q | P=Q" by blast +text{*Theorems for translation to combinators*} + +lemma abs_S: "(%x. (f x) (g x)) == COMBS f g" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBS_def) +done + +lemma abs_I: "(%x. x) == COMBI" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBI_def) +done + +lemma abs_K: "(%x. y) == COMBK y" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBK_def) +done + +lemma abs_B: "(%x. a (g x)) == COMBB a g" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBB_def) +done + +lemma abs_C: "(%x. (f x) b) == COMBC f b" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBC_def) +done + + use "Tools/res_axioms.ML" --{*requires the combinators declared above*} -use "Tools/res_hol_clause.ML" --{*requires the combinators*} +use "Tools/res_hol_clause.ML" use "Tools/res_reconstruct.ML" use "Tools/watcher.ML" use "Tools/res_atp.ML" @@ -102,17 +117,14 @@ oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *} use "Tools/res_atp_methods.ML" -setup ResAtpMethods.setup - +setup ResAtpMethods.setup --{*Oracle ATP methods: still useful?*} +setup ResAxioms.setup --{*Sledgehammer*} subsection {* The Metis prover *} use "Tools/metis_tools.ML" setup MetisTools.setup -(*Sledgehammer*) -setup ResAxioms.setup - setup {* Theory.at_end ResAxioms.clause_cache_endtheory *} diff -r 78e6a3cea367 -r 646bdc51eb7d src/HOL/MetisExamples/Abstraction.thy --- a/src/HOL/MetisExamples/Abstraction.thy Wed Oct 03 22:33:17 2007 +0200 +++ b/src/HOL/MetisExamples/Abstraction.thy Thu Oct 04 12:32:58 2007 +0200 @@ -67,74 +67,107 @@ by (meson CollectD SigmaD1 SigmaD2) +(*single-step*) +lemma "(a,b) \ (SIGMA x: A. {y. x = f y}) ==> a \ A & a = f b" +by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def vimage_singleton_eq) -(*single-step*) + lemma "(a,b) \ (SIGMA x: A. {y. x = f y}) ==> a \ A & a = f b" proof (neg_clausify) -assume 0: "(a, b) \ Sigma A (llabs_subgoal_1 f)" -assume 1: "\f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)" -assume 2: "a \ A \ a \ f b" -have 3: "a \ A" - by (metis SigmaD1 0) -have 4: "f b \ a" - by (metis 3 2) -have 5: "f b = a" - by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 0) +assume 0: "(a\'a\type, b\'b\type) +\ Sigma (A\'a\type set) + (COMBB Collect (COMBC (COMBB COMBB op =) (f\'b\type \ 'a\type)))" +assume 1: "(a\'a\type) \ (A\'a\type set) \ a \ (f\'b\type \ 'a\type) (b\'b\type)" +have 2: "(a\'a\type) \ (A\'a\type set)" + by (metis 0 SigmaD1) +have 3: "(b\'b\type) +\ COMBB Collect (COMBC (COMBB COMBB op =) (f\'b\type \ 'a\type)) (a\'a\type)" + by (metis 0 SigmaD2) +have 4: "(b\'b\type) \ Collect (COMBB (op = (a\'a\type)) (f\'b\type \ 'a\type))" + by (metis 3) +have 5: "(f\'b\type \ 'a\type) (b\'b\type) \ (a\'a\type)" + by (metis 1 2) +have 6: "(f\'b\type \ 'a\type) (b\'b\type) = (a\'a\type)" + by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def) show "False" - by (metis 5 4) -qed finish_clausify + by (metis 5 6) +qed + +(*Alternative structured proof, untyped*) +lemma "(a,b) \ (SIGMA x: A. {y. x = f y}) ==> a \ A & a = f b" +proof (neg_clausify) +assume 0: "(a, b) \ Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))" +have 1: "b \ Collect (COMBB (op = a) f)" + by (metis 0 SigmaD2) +have 2: "f b = a" + by (metis 1 vimage_Collect_eq singleton_conv2 insert_def union_empty2 vimage_singleton_eq vimage_def) +assume 3: "a \ A \ a \ f b" +have 4: "a \ A" + by (metis 0 SigmaD1) +have 5: "f b \ a" + by (metis 4 3) +show "False" + by (metis 5 2) +qed ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*} lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL.{f. f \ pset cl}) ==> f \ pset cl" -apply (metis Collect_mem_eq SigmaD2); -done +by (metis Collect_mem_eq SigmaD2) lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL.{f. f \ pset cl}) ==> f \ pset cl" proof (neg_clausify) -assume 0: "\cl\'a\type set. - (llabs_subgoal_1\'a\type set \ 'a\type set) cl = - Collect (llabs_Set_XCollect_ex_eq_3 op \ (pset cl))" -assume 1: "(f\'a\type) \ pset (cl\'a\type set)" -assume 2: "(cl\'a\type set, f\'a\type) \ (CLF\('a\type set \ 'a\type) set)" -have 3: "llabs_Predicate_Xsup_Un_eq2_1 (CLF\('a\type set \ 'a\type) set) - (cl\'a\type set) (f\'a\type)" - by (metis acc_def 2) -assume 4: "(CLF\('a\type set \ 'a\type) set) = -Sigma (CL\'a\type set set) (llabs_subgoal_1\'a\type set \ 'a\type set)" +assume 0: "(cl, f) \ CLF" +assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \) pset))" +assume 2: "f \ pset cl" +have 3: "\X1 X2. X2 \ COMBB Collect (COMBB (COMBC op \) pset) X1 \ (X1, X2) \ CLF" + by (metis SigmaD2 1) +have 4: "\X1 X2. X2 \ pset X1 \ (X1, X2) \ CLF" + by (metis 3 Collect_mem_eq) +have 5: "(cl, f) \ CLF" + by (metis 2 4) show "False" - by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2) -qed finish_clausify (*ugly hack: combinators??*) + by (metis 5 0) +qed ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*} lemma "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> f \ pset cl \ pset cl" -apply (metis Collect_mem_eq SigmaD2); -done +proof (neg_clausify) +assume 0: "f \ Pi (pset cl) (COMBK (pset cl))" +assume 1: "(cl, f) +\ Sigma CL + (COMBB Collect + (COMBB (COMBC op \) (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) +qed -lemma - "(cl,f) \ (SIGMA cl::'a set : CL. {f. f \ pset cl \ pset cl}) ==> - f \ pset cl \ pset cl" -proof (neg_clausify) -assume 0: "\cl\'a\type set. - (llabs_subgoal_1\'a\type set \ ('a\type \ 'a\type) set) cl = - Collect - (llabs_Set_XCollect_ex_eq_3 op \ (Pi (pset cl) (COMBK (pset cl))))" -assume 1: "(f\'a\type \ 'a\type) \ Pi (pset (cl\'a\type set)) (COMBK (pset cl))" -assume 2: "(cl\'a\type set, f\'a\type \ 'a\type) -\ Sigma (CL\'a\type set set) - (llabs_subgoal_1\'a\type set \ ('a\type \ 'a\type) set)" -show "False" - by (metis 1 Collect_mem_eq 0 SigmaD2 2) -qed finish_clausify - (*Hack to prevent the "Additional hypotheses" error*) ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*} lemma "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" -by (metis Collect_mem_eq SigmaD2) +proof (neg_clausify) +assume 0: "(cl, f) +\ Sigma CL + (COMBB Collect (COMBB (COMBC op \) (COMBS (COMBB op \ pset) COMBI)))" +assume 1: "f \ pset cl \ cl" +have 2: "f \ COMBB Collect (COMBB (COMBC op \) (COMBS (COMBB op \ pset) COMBI)) cl" + by (insert 0, simp add: COMBB_def) +(* by (metis SigmaD2 0) ??doesn't terminate*) +have 3: "f \ COMBS (COMBB op \ pset) COMBI cl" + by (metis 2 Collect_mem_eq) +have 4: "f \ cl \ pset cl" + by (metis 1 Int_commute) +have 5: "f \ cl \ pset cl" + by (metis 3 Int_commute) +show "False" + by (metis 5 4) +qed + ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*} lemma @@ -146,28 +179,40 @@ lemma "(cl,f) \ CLF ==> CLF \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" +by auto +(*??no longer terminates, with combinators by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1) --{*@{text Int_def} is redundant} +*) ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*} lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> f \ pset cl \ cl" +by auto +(*??no longer terminates, with combinators by (metis Collect_mem_eq Int_commute SigmaD2) +*) ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*} lemma "(cl,f) \ CLF ==> CLF \ (SIGMA cl': CL. {f. f \ pset cl' \ pset cl'}) ==> f \ pset cl \ pset cl" +by auto +(*??no longer terminates, with combinators by (metis Collect_mem_eq SigmaD2 subsetD) +*) ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*} lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> f \ pset cl \ pset cl" +by auto +(*??no longer terminates, with combinators by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE) +*) ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*} lemma diff -r 78e6a3cea367 -r 646bdc51eb7d src/HOL/MetisExamples/Tarski.thy --- a/src/HOL/MetisExamples/Tarski.thy Wed Oct 03 22:33:17 2007 +0200 +++ b/src/HOL/MetisExamples/Tarski.thy Thu Oct 04 12:32:58 2007 +0200 @@ -515,8 +515,11 @@ apply (rule_tac t = "H" in ssubst, assumption) apply (rule CollectI) apply (rule conjI) -ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} -apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE monotone_f reflD1 reflD2) +ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} +(*??no longer terminates, with combinators +apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2) +*) +apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE [OF monotone_f] reflD1 reflD2) apply (metis CO_refl lubH_le_flubH reflD2) done declare CLF.f_in_funcset[rule del] funcset_mem[rule del] @@ -529,51 +532,73 @@ ML{*ResAtp.problem_name:="Tarski__CLF_lubH_is_fixp"*} (*Single-step version fails. The conjecture clauses refer to local abstraction functions (Frees), which prevents expand_defs_tac from removing those -"definitions" at the end of the proof. +"definitions" at the end of the proof. *) lemma (in CLF) lubH_is_fixp: "H = {x. (x, f x) \ r & x \ A} ==> lub H cl \ fix f A" apply (simp add: fix_def) apply (rule conjI) - proof (neg_clausify) -assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)" -assume 1: "lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl \ A" -have 2: "glb H (dual cl) \ A" - by (metis 0 1 lub_dual_glb) -have 3: "(glb H (dual cl), f (glb H (dual cl))) \ r" - by (metis 0 lubH_le_flubH lub_dual_glb) -have 4: "(f (glb H (dual cl)), glb H (dual cl)) \ r" - by (metis 0 flubH_le_lubH lub_dual_glb) -have 5: "glb H (dual cl) = f (glb H (dual cl)) \ -(glb H (dual cl), f (glb H (dual cl))) \ r" - by (metis 4 antisymE) -have 6: "glb H (dual cl) = f (glb H (dual cl))" - by (metis 3 5) -have 7: "(glb H (dual cl), glb H (dual cl)) \ r" - by (metis 4 6) -have 8: "\X1. glb H (dual cl) \ X1 \ \ refl X1 r" - by (metis reflD2 7) +proof (neg_clausify) +assume 0: "H = +Collect + (COMBS (COMBB op \ (COMBC (COMBB op \ (COMBS Pair f)) r)) (COMBC op \ A))" +assume 1: "lub (Collect + (COMBS (COMBB op \ (COMBC (COMBB op \ (COMBS Pair f)) r)) + (COMBC op \ A))) + cl +\ A" +have 2: "lub H cl \ A" + by (metis 1 0) +have 3: "(lub H cl, f (lub H cl)) \ r" + by (metis lubH_le_flubH 0) +have 4: "(f (lub H cl), lub H cl) \ r" + by (metis flubH_le_lubH 0) +have 5: "lub H cl = f (lub H cl) \ (lub H cl, f (lub H cl)) \ 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) \ r" + by (metis 6 4) +have 8: "\X1. lub H cl \ X1 \ \ refl X1 r" + by (metis 7 reflD2) have 9: "\ refl A r" - by (metis 2 8) + by (metis 8 2) show "False" - by (metis 9 CO_refl) -proof (neg_clausify) -assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)" -assume 1: "f (lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl) \ -lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl" -have 2: "(glb H (dual cl), f (glb H (dual cl))) \ r" - by (metis 0 lubH_le_flubH lub_dual_glb lub_dual_glb) -have 3: "f (glb H (dual cl)) \ glb H (dual cl)" - by (metis 0 1 lub_dual_glb) -have 4: "(f (glb H (dual cl)), glb H (dual cl)) \ r" - by (metis lub_dual_glb flubH_le_lubH 0) -have 5: "f (glb H (dual cl)) = glb H (dual cl) \ -(f (glb H (dual cl)), glb H (dual cl)) \ r" - by (metis antisymE 2) -have 6: "f (glb H (dual cl)) = glb H (dual cl)" - by (metis 5 4) -show "False" - by (metis 3 6) -*) + by (metis CO_refl 9); +next --{*apparently the way to insert a second structured proof*} + show "H = {x. (x, f x) \ r \ x \ A} \ + f (lub {x. (x, f x) \ r \ x \ A} cl) = lub {x. (x, f x) \ r \ x \ A} cl" + proof (neg_clausify) + assume 0: "H = + Collect + (COMBS (COMBB op \ (COMBC (COMBB op \ (COMBS Pair f)) r)) (COMBC op \ A))" + assume 1: "f (lub (Collect + (COMBS (COMBB op \ (COMBC (COMBB op \ (COMBS Pair f)) r)) + (COMBC op \ A))) + cl) \ + lub (Collect + (COMBS (COMBB op \ (COMBC (COMBB op \ (COMBS Pair f)) r)) + (COMBC op \ A))) + cl" + have 2: "f (lub H cl) \ + lub (Collect + (COMBS (COMBB op \ (COMBC (COMBB op \ (COMBS Pair f)) r)) + (COMBC op \ A))) + cl" + by (metis 1 0) + have 3: "f (lub H cl) \ lub H cl" + by (metis 2 0) + have 4: "(lub H cl, f (lub H cl)) \ r" + by (metis lubH_le_flubH 0) + have 5: "(f (lub H cl), lub H cl) \ r" + by (metis flubH_le_lubH 0) + have 6: "lub H cl = f (lub H cl) \ (lub H cl, f (lub H cl)) \ 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 +qed lemma (in CLF) lubH_is_fixp: "H = {x. (x, f x) \ r & x \ A} ==> lub H cl \ fix f A" @@ -616,9 +641,13 @@ apply (rule lubI) ML{*ResAtp.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*} apply (metis P_def equalityE fix_subset subset_trans) -apply (metis P_def fix_subset lubH_is_fixp set_mp subset_refl subset_trans) -apply (metis P_def fixf_le_lubH) -apply (metis P_def lubH_is_fixp) +apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) +(*??no longer terminates, with combinators +apply (metis P_def fix_def fixf_le_lubH) +apply (metis P_def fix_def lubH_least_fixf) +*) +apply (simp add: fixf_le_lubH) +apply (simp add: lubH_least_fixf) done declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del] @@ -662,21 +691,18 @@ ML{*ResAtp.problem_name:="Tarski__rel_imp_elem"*} declare (in CLF) CO_refl[simp] refl_def [simp] lemma (in CLF) rel_imp_elem: "(x, y) \ r ==> x \ A" -apply (metis CO_refl reflD1) -done +by (metis CO_refl reflD1) declare (in CLF) CO_refl[simp del] refl_def [simp del] ML{*ResAtp.problem_name:="Tarski__interval_subset"*} declare (in CLF) rel_imp_elem[intro] declare interval_def [simp] lemma (in CLF) interval_subset: "[| a \ A; b \ A |] ==> interval r a b \ A" -apply (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def) -done +by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def) declare (in CLF) rel_imp_elem[rule del] declare interval_def [simp del] - lemma (in CLF) intervalI: "[| (a, x) \ r; (x, b) \ r |] ==> x \ interval r a b" by (simp add: interval_def) @@ -966,8 +992,7 @@ ML{*ResAtp.problem_name:="Tarski__intY1_func"*} (*ALL THEOREMS*) lemma (in Tarski) intY1_func: "(%x: intY1. f x) \ intY1 -> intY1" -apply (metis intY1_f_closed restrict_in_funcset) -done +by (metis intY1_f_closed restrict_in_funcset) ML{*ResAtp.problem_name:="Tarski__intY1_mono"*} (*ALL THEOREMS*) lemma (in Tarski) intY1_mono [skolem]: diff -r 78e6a3cea367 -r 646bdc51eb7d src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Oct 03 22:33:17 2007 +0200 +++ b/src/HOL/Tools/meson.ML Thu Oct 04 12:32:58 2007 +0200 @@ -17,6 +17,7 @@ val first_order_resolve: thm -> thm -> thm val flexflex_first_order: thm -> thm val size_of_subgoals: thm -> int + val too_many_clauses: term -> bool val make_cnf: thm list -> thm -> thm list val finish_cnf: thm list -> thm list val generalize: thm -> thm diff -r 78e6a3cea367 -r 646bdc51eb7d src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Wed Oct 03 22:33:17 2007 +0200 +++ b/src/HOL/Tools/metis_tools.ML Thu Oct 04 12:32:58 2007 +0200 @@ -290,7 +290,10 @@ let val v = find_var x val t = fol_term_to_hol_RAW ctxt y in SOME (cterm_of thy v, t) end - handle Option => NONE (*List.find failed for the variable.*) + handle Option => + (Output.debug (fn() => "List.find failed for the variable " ^ x ^ + " in " ^ string_of_thm i_th); + NONE) fun remove_typeinst (a, t) = case Recon.strip_prefix ResClause.schematic_var_prefix a of SOME b => SOME (b, t) @@ -446,11 +449,11 @@ val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal"); val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal"); - val comb_I = ResHolClause.comb_I RS meta_eq_to_obj_eq; - val comb_K = ResHolClause.comb_K RS meta_eq_to_obj_eq; - val comb_B = ResHolClause.comb_B RS meta_eq_to_obj_eq; - - val ext_thm = cnf_th ResHolClause.ext; + val comb_I = cnf_th ResHolClause.comb_I; + val comb_K = cnf_th ResHolClause.comb_K; + val comb_B = cnf_th ResHolClause.comb_B; + val comb_C = cnf_th ResHolClause.comb_C; + val comb_S = cnf_th ResHolClause.comb_S; fun dest_Arity (ResClause.ArityClause{premLits,...}) = map ResClause.class_of_arityLit premLits; @@ -509,10 +512,14 @@ val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists (*Now check for the existence of certain combinators*) - val IK = if used "c_COMBI" orelse used "c_COMBK" then [comb_I,comb_K] else [] - val BC = if used "c_COMBB" then [comb_B] else [] - val EQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] - val lmap' = if isFO then lmap else foldl (add_thm ctxt) lmap ([ext_thm] @ EQ @ IK @ BC) + val thI = if used "c_COMBI" then [comb_I] else [] + val thK = if used "c_COMBK" then [comb_K] else [] + val thB = if used "c_COMBB" then [comb_B] else [] + val thC = if used "c_COMBC" then [comb_C] else [] + val thS = if used "c_COMBS" then [comb_S] else [] + val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] + val lmap' = if isFO then lmap + else foldl (add_thm ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI) in add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap' end; diff -r 78e6a3cea367 -r 646bdc51eb7d src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Oct 03 22:33:17 2007 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Oct 04 12:32:58 2007 +0200 @@ -769,7 +769,7 @@ (*Called by the oracle-based methods declared in res_atp_methods.ML*) fun write_subgoal_file dfg mode ctxt conjectures user_thms n = let val conj_cls = Meson.make_clauses conjectures - |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf + |> map ResAxioms.combinators |> Meson.finish_cnf val hyp_cls = cnf_hyps_thms ctxt val goal_cls = conj_cls@hyp_cls val goal_tms = map prop_of goal_cls diff -r 78e6a3cea367 -r 646bdc51eb7d src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Oct 03 22:33:17 2007 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Oct 04 12:32:58 2007 +0200 @@ -15,7 +15,7 @@ val cnf_rules_of_ths: thm list -> thm list val neg_clausify: thm list -> thm list val expand_defs_tac: thm -> tactic - val assume_abstract_list: string -> thm list -> thm list + val combinators: thm -> thm val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) @@ -31,26 +31,6 @@ (* FIXME legacy *) fun freeze_thm th = #1 (Drule.freeze_thaw th); -val lhs_of = #1 o Logic.dest_equals o Thm.prop_of; -val rhs_of = #2 o Logic.dest_equals o Thm.prop_of; - - -(*Store definitions of abstraction functions, ensuring that identical right-hand - sides are denoted by the same functions and thereby reducing the need for - extensionality in proofs. - FIXME! Store in theory data!!*) - -(*Populate the abstraction cache with common combinators.*) -fun seed th net = - let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th) - val t = Logic.legacy_varify (term_of ct) - in Net.insert_term Thm.eq_thm (t, th) net end; - -val abstraction_cache = ref - (seed (thm"ATP_Linkup.I_simp") - (seed (thm"ATP_Linkup.B_simp") - (seed (thm"ATP_Linkup.K_simp") Net.empty))); - (**** Transformation of Elimination Rules into First-Order Formulas****) @@ -149,7 +129,7 @@ in dec_sko (prop_of th) [] end; -(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****) +(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) (*Returns the vars of a theorem*) fun vars_of_thm th = @@ -175,201 +155,98 @@ strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x)) | _ => th; -(*Convert meta- to object-equality. Fails for theorems like split_comp_eq, - where some types have the empty sort.*) -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; -fun mk_object_eq th = th RS meta_eq_to_obj_eq - handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th); - -(*Apply a function definition to an argument, beta-reducing the result.*) -fun beta_comb cf x = - let val th1 = combination cf (reflexive x) - val th2 = beta_conversion false (Thm.rhs_of th1) - in transitive th1 th2 end; - -(*Apply a function definition to arguments, beta-reducing along the way.*) -fun list_combination cf [] = cf - | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs; - -fun list_cabs ([] , t) = t - | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t)); - fun assert_eta_free ct = let val t = term_of ct in if (t aconv Envir.eta_contract t) then () else error ("Eta redex in term: " ^ string_of_cterm ct) end; -fun eq_absdef (th1, th2) = - Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso - rhs_of th1 aconv rhs_of th2; - val lambda_free = not o Term.has_abs; val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); -fun dest_abs_list ct = - let val (cv,ct') = Thm.dest_abs NONE ct - val (cvs,cu) = dest_abs_list ct' - in (cv::cvs, cu) end - handle CTERM _ => ([],ct); +val abs_S = @{thm"abs_S"}; +val abs_K = @{thm"abs_K"}; +val abs_I = @{thm"abs_I"}; +val abs_B = @{thm"abs_B"}; +val abs_C = @{thm"abs_C"}; -fun abstract_rule_list [] [] th = th - | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th) - | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]); - - -val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0 +val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B)); +val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C)); +val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S)); -(*Does an existing abstraction definition have an RHS that matches the one we need now? - thy is the current theory, which must extend that of theorem th.*) -fun match_rhs thy t th = - let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ - " against\n" ^ string_of_thm th); - val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0) - val term_insts = map Meson.term_pair_of (Vartab.dest tenv) - val ct_pairs = if subthy (theory_of_thm th, thy) andalso - forall lambda_free (map #2 term_insts) - then map (pairself (cterm_of thy)) term_insts - else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*) - fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T) - val th' = cterm_instantiate ct_pairs th - in SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th') end - handle _ => NONE; +(*FIXME: requires more use of cterm constructors*) +fun abstract ct = + let val Abs(x,_,body) = term_of ct + val thy = theory_of_cterm ct + val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) + val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT + fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K + in + case body of + Const _ => makeK() + | Free _ => makeK() + | Var _ => makeK() (*though Var isn't expected*) + | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*) + | rator$rand => + if loose_bvar1 (rator,0) then (*C or S*) + if loose_bvar1 (rand,0) then (*S*) + let val crator = cterm_of thy (Abs(x,xT,rator)) + val crand = cterm_of thy (Abs(x,xT,rand)) + val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S + val (_,rhs) = Thm.dest_equals (cprop_of abs_S') + in + Thm.transitive abs_S' (Conv.binop_conv abstract rhs) + end + else (*C*) + let val crator = cterm_of thy (Abs(x,xT,rator)) + val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C + val (_,rhs) = Thm.dest_equals (cprop_of abs_C') + in + Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) + end + else if loose_bvar1 (rand,0) then (*B or eta*) + if rand = Bound 0 then eta_conversion ct + else (*B*) + let val crand = cterm_of thy (Abs(x,xT,rand)) + val abs_B' = cterm_instantiate [(f_B, cterm_of thy rator),(g_B,crand)] abs_B + val (_,rhs) = Thm.dest_equals (cprop_of abs_B') + in + Thm.transitive abs_B' (Conv.arg_conv abstract rhs) + end + else makeK() + | _ => error "abstract: Bad term" + end; (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested prefix for the constants. Resulting theory is returned in the first theorem. *) -fun declare_absfuns s th = - let val nref = ref 0 - fun abstract thy ct = - if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) - else - case term_of ct of - Abs _ => - let val cname = "llabs_" ^ s ^ "_" ^ Int.toString (inc nref) - val _ = assert_eta_free ct; - val (cvs,cta) = dest_abs_list ct - val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) - val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta); - val (u'_th,defs) = abstract thy cta - val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th); - val cu' = Thm.rhs_of u'_th - val u' = term_of cu' - val abs_v_u = fold_rev (lambda o term_of) cvs u' - (*get the formal parameters: ALL variables free in the term*) - val args = term_frees abs_v_u - val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments"); - val rhs = list_abs_free (map dest_Free args, abs_v_u) - (*Forms a lambda-abstraction over the formal parameters*) - val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu'); - val thy = theory_of_thm u'_th - val (ax,ax',thy) = - case List.mapPartial (match_rhs thy abs_v_u) - (Net.match_term (!abstraction_cache) u') of - (ax,ax')::_ => - (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax); - (ax,ax',thy)) - | [] => - let val _ = Output.debug (fn()=>"Lookup was empty"); - val Ts = map type_of args - val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu')) - val c = Const (Sign.full_name thy cname, cT) - val thy = - Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy - (*Theory is augmented with the constant, - then its definition*) - val cdef = cname ^ "_def" - val thy = Theory.add_defs_i true false - [(cdef, equals cT $ c $ rhs)] thy - handle ERROR _ => raise Clausify_failure thy - val ax = Thm.get_axiom_i thy (Sign.full_name thy cdef) - |> Drule.unvarify - |> mk_object_eq |> strip_lambdas (length args) - |> mk_meta_eq |> Meson.generalize - val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax) - val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^ - "Instance: " ^ string_of_thm ax'); - val _ = abstraction_cache := Net.insert_term eq_absdef - ((Logic.varify u'), ax) (!abstraction_cache) - handle Net.INSERT => - raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax]) - in (ax,ax',thy) end - in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax'); - (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end - | (t1$t2) => - let val (ct1,ct2) = Thm.dest_comb ct - val (th1,defs1) = abstract thy ct1 - val (th2,defs2) = abstract (theory_of_thm th1) ct2 - in (combination th1 th2, defs1@defs2) end - val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th); - val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th) - val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs - val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths)); - in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end; - -fun name_of def = try (#1 o dest_Free o lhs_of) def; - -(*A name is valid provided it isn't the name of a defined abstraction.*) -fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs)) - | valid_name defs _ = false; - -(*s is the theorem name (hint) or the word "subgoal"*) -fun assume_absfuns s th = - let val thy = theory_of_thm th - val cterm = cterm_of thy - val abs_count = ref 0 - fun abstract ct = - if lambda_free (term_of ct) then (reflexive ct, []) - else - case term_of ct of - Abs (_,T,u) => - let val _ = assert_eta_free ct; - val (cvs,cta) = dest_abs_list ct - val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) - val (u'_th,defs) = abstract cta - val cu' = Thm.rhs_of u'_th - val u' = term_of cu' - (*Could use Thm.cabs instead of lambda to work at level of cterms*) - val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu') - (*get the formal parameters: free variables not present in the defs - (to avoid taking abstraction function names as parameters) *) - val args = filter (valid_name defs) (term_frees abs_v_u) - val crhs = list_cabs (map cterm args, cterm abs_v_u) - (*Forms a lambda-abstraction over the formal parameters*) - val rhs = term_of crhs - val (ax,ax') = - case List.mapPartial (match_rhs thy abs_v_u) - (Net.match_term (!abstraction_cache) u') of - (ax,ax')::_ => - (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax); - (ax,ax')) - | [] => - let val Ts = map type_of args - val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu')) - val id = "llabs_" ^ s ^ "_" ^ Int.toString (inc abs_count) - val c = Free (id, const_ty) - val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs) - |> mk_object_eq |> strip_lambdas (length args) - |> mk_meta_eq |> Meson.generalize - val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax) - val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax) - (!abstraction_cache) - handle Net.INSERT => - raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax]) - in (ax,ax') end - in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax'); - (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end - | (t1$t2) => - let val (ct1,ct2) = Thm.dest_comb ct - val (t1',defs1) = abstract ct1 - val (t2',defs2) = abstract ct2 - in (combination t1' t2', defs1@defs2) end - val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th); - val (eqth,defs) = abstract (cprop_of th) - val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs - val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths)); - in map Drule.eta_contraction_rule ths end; - +fun combinators_aux ct = + if lambda_free (term_of ct) then reflexive ct + else + case term_of ct of + Abs _ => + let val _ = assert_eta_free ct; + val (cv,cta) = Thm.dest_abs NONE ct + val (v,Tv) = (dest_Free o term_of) cv + val _ = Output.debug (fn()=>" recursion: " ^ string_of_cterm cta); + val u_th = combinators_aux cta + val _ = Output.debug (fn()=>" returned " ^ string_of_thm u_th); + val cu = Thm.rhs_of u_th + val comb_eq = abstract (Thm.cabs cv cu) + in Output.debug (fn()=>" abstraction result: " ^ string_of_thm comb_eq); + (transitive (abstract_rule v cv u_th) comb_eq) end + | t1 $ t2 => + let val (ct1,ct2) = Thm.dest_comb ct + in combination (combinators_aux ct1) (combinators_aux ct2) end; + +fun combinators th = + if lambda_free (prop_of th) then th + else + let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th); + val th = Drule.eta_contraction_rule th + val eqth = combinators_aux (cprop_of th) + val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth); + in equal_elim eqth th end; (*cterms are used throughout for efficiency*) val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; @@ -430,27 +307,6 @@ [] => () | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths')); -fun assume_abstract s th = - if lambda_free (prop_of th) then [th] - else th |> Drule.eta_contraction_rule |> assume_absfuns s - |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") - -(*Replace lambdas by assumed function definitions in the theorems*) -fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths); - -(*Replace lambdas by declared function definitions in the theorems*) -fun declare_abstract s (thy, []) = (thy, []) - | declare_abstract s (thy, th::ths) = - let val (thy', th_defs) = - if lambda_free (prop_of th) then (thy, [th]) - else - th |> zero_var_indexes |> freeze_thm - |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s - handle Clausify_failure thy_e => (thy_e,[]) - val _ = assert_lambda_free th_defs "declare_abstract: lambdas" - val (thy'', ths') = declare_abstract (s^"'") (thy', ths) - in (thy'', th_defs @ ths') end; - (*Keep the full complexity of the original name*) fun flatten_name s = space_implode "_X" (NameSpace.explode s); @@ -465,7 +321,7 @@ (*Skolemize a named theorem, with Skolem functions as additional premises.*) fun skolem_thm th = let val nnfth = to_nnf th and s = fake_name th - in Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> assume_abstract_list s |> Meson.finish_cnf + in Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> map combinators |> Meson.finish_cnf end handle THM _ => []; @@ -480,8 +336,8 @@ val (thy',defs) = declare_skofuns s nnfth thy val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") - val (thy'',cnfs') = declare_abstract s (thy',cnfs) - in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end + val cnfs' = map combinators cnfs + in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end handle Clausify_failure thy_e => ([],thy_e) ) (try to_nnf th); @@ -575,8 +431,26 @@ val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)]; +val max_lambda_nesting = 3; + +fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) + | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1) + | excessive_lambdas _ = false; + +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT); + +(*Don't count nested lambdas at the level of formulas, as they are quantifiers*) +fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t + | excessive_lambdas_fm Ts t = + if is_formula_type (fastype_of1 (Ts, t)) + then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) + else excessive_lambdas (t, max_lambda_nesting); + +fun too_complex t = + Meson.too_many_clauses t orelse excessive_lambdas_fm [] t; + fun skolem_cache th thy = - if PureThy.is_internal th then thy + if PureThy.is_internal th orelse too_complex (prop_of th) then thy else #2 (skolem_cache_thm th thy); val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of; @@ -598,7 +472,7 @@ fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths); (*Expand all new*definitions of abstraction or Skolem functions in a proof state.*) -fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a +fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a | is_absko _ = false; fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*) @@ -607,7 +481,7 @@ (*This function tries to cope with open locales, which introduce hypotheses of the form Free == t, conjecture clauses, which introduce various hypotheses, and also definitions - of llabs_ and sko_ functions. *) + of sko_ functions. *) fun expand_defs_tac st0 st = let val hyps0 = #hyps (rep_thm st0) val hyps = #hyps (crep_thm st) @@ -652,7 +526,7 @@ val no_tvars = null o term_tvars o prop_of; val neg_clausify = - filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o Meson.make_clauses; + filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses; fun neg_conjecture_clauses st0 n = let val st = Seq.hd (neg_skolemize_tac n st0)