# HG changeset patch # User blanchet # Date 1286379861 -7200 # Node ID 626b1d360d426b9e4b201ddee175406912062b12 # Parent a62e01e9b22c50b31f3a099fc601bc68a76d651f# Parent d42ddd7407ca4efd0bff1b3e378ae34983fb9f75 merged diff -r a62e01e9b22c -r 626b1d360d42 NEWS --- a/NEWS Wed Oct 06 13:48:12 2010 +0200 +++ b/NEWS Wed Oct 06 17:44:21 2010 +0200 @@ -248,6 +248,46 @@ * Function package: .psimps rules are no longer implicitly declared [simp]. INCOMPATIBILITY. +* Weaker versions of the "meson" and "metis" proof methods are now available in + "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become + more powerful after "Hilbert_Choice" is loaded in "HOL-Main". + +* MESON: Renamed lemmas: + meson_not_conjD ~> Meson.not_conjD + meson_not_disjD ~> Meson.not_disjD + meson_not_notD ~> Meson.not_notD + meson_not_allD ~> Meson.not_allD + meson_not_exD ~> Meson.not_exD + meson_imp_to_disjD ~> Meson.imp_to_disjD + meson_not_impD ~> Meson.not_impD + meson_iff_to_disjD ~> Meson.iff_to_disjD + meson_not_iffD ~> Meson.not_iffD + meson_not_refl_disj_D ~> Meson.not_refl_disj_D + meson_conj_exD1 ~> Meson.conj_exD1 + meson_conj_exD2 ~> Meson.conj_exD2 + meson_disj_exD ~> Meson.disj_exD + meson_disj_exD1 ~> Meson.disj_exD1 + meson_disj_exD2 ~> Meson.disj_exD2 + meson_disj_assoc ~> Meson.disj_assoc + meson_disj_comm ~> Meson.disj_comm + meson_disj_FalseD1 ~> Meson.disj_FalseD1 + meson_disj_FalseD2 ~> Meson.disj_FalseD2 +INCOMPATIBILITY. + +* Sledgehammer: Renamed lemmas: + COMBI_def ~> Meson.COMBI_def + COMBK_def ~> Meson.COMBK_def + COMBB_def ~> Meson.COMBB_def + COMBC_def ~> Meson.COMBC_def + COMBS_def ~> Meson.COMBS_def + abs_I ~> Meson.abs_I + abs_K ~> Meson.abs_K + abs_B ~> Meson.abs_B + abs_C ~> Meson.abs_C + abs_S ~> Meson.abs_S +INCOMPATIBILITY. + + *** FOL *** * All constant names are now qualified. INCOMPATIBILITY. diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/ATP.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ATP.thy Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,17 @@ +(* Title: HOL/ATP.thy + Author: Fabian Immler, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen +*) + +header {* Automatic Theorem Provers (ATPs) *} + +theory ATP +imports Plain +uses "Tools/ATP/atp_problem.ML" + "Tools/ATP/atp_proof.ML" + "Tools/ATP/atp_systems.ML" +begin + +setup ATP_Systems.setup + +end diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Hilbert_Choice.thy Wed Oct 06 17:44:21 2010 +0200 @@ -7,8 +7,7 @@ theory Hilbert_Choice imports Nat Wellfounded Plain -uses ("Tools/meson.ML") - ("Tools/choice_specification.ML") +uses ("Tools/choice_specification.ML") begin subsection {* Hilbert's epsilon *} @@ -81,17 +80,7 @@ subsection{*Axiom of Choice, Proved Using the Description Operator*} -ML {* -structure Meson_Choices = Named_Thms -( - val name = "meson_choice" - val description = "choice axioms for MESON's (and Metis's) skolemizer" -) -*} - -setup Meson_Choices.setup - -lemma choice [meson_choice]: "\x. \y. Q x y ==> \f. \x. Q x (f x)" +lemma choice: "\x. \y. Q x y ==> \f. \x. Q x (f x)" by (fast elim: someI) lemma bchoice: "\x\S. \y. Q x y ==> \f. \x\S. Q x (f x)" @@ -451,128 +440,6 @@ done -subsection {* The Meson proof procedure *} - -subsubsection {* Negation Normal Form *} - -text {* de Morgan laws *} - -lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q" - and meson_not_disjD: "~(P|Q) ==> ~P & ~Q" - and meson_not_notD: "~~P ==> P" - and meson_not_allD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" - and meson_not_exD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" - by fast+ - -text {* Removal of @{text "-->"} and @{text "<->"} (positive and -negative occurrences) *} - -lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q" - and meson_not_impD: "~(P-->Q) ==> P & ~Q" - and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" - and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" - -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *} - and meson_not_refl_disj_D: "x ~= x | P ==> P" - by fast+ - - -subsubsection {* Pulling out the existential quantifiers *} - -text {* Conjunction *} - -lemma meson_conj_exD1: "!!P Q. (\x. P(x)) & Q ==> \x. P(x) & Q" - and meson_conj_exD2: "!!P Q. P & (\x. Q(x)) ==> \x. P & Q(x)" - by fast+ - - -text {* Disjunction *} - -lemma meson_disj_exD: "!!P Q. (\x. P(x)) | (\x. Q(x)) ==> \x. P(x) | Q(x)" - -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *} - -- {* With ex-Skolemization, makes fewer Skolem constants *} - and meson_disj_exD1: "!!P Q. (\x. P(x)) | Q ==> \x. P(x) | Q" - and meson_disj_exD2: "!!P Q. P | (\x. Q(x)) ==> \x. P | Q(x)" - by fast+ - - -subsubsection {* Generating clauses for the Meson Proof Procedure *} - -text {* Disjunctions *} - -lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)" - and meson_disj_comm: "P|Q ==> Q|P" - and meson_disj_FalseD1: "False|P ==> P" - and meson_disj_FalseD2: "P|False ==> P" - by fast+ - - -subsection{*Lemmas for Meson, the Model Elimination Procedure*} - -text{* Generation of contrapositives *} - -text{*Inserts negated disjunct after removing the negation; P is a literal. - Model elimination requires assuming the negation of every attempted subgoal, - hence the negated disjuncts.*} -lemma make_neg_rule: "~P|Q ==> ((~P==>P) ==> Q)" -by blast - -text{*Version for Plaisted's "Postive refinement" of the Meson procedure*} -lemma make_refined_neg_rule: "~P|Q ==> (P ==> Q)" -by blast - -text{*@{term P} should be a literal*} -lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)" -by blast - -text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't -insert new assumptions, for ordinary resolution.*} - -lemmas make_neg_rule' = make_refined_neg_rule - -lemma make_pos_rule': "[|P|Q; ~P|] ==> Q" -by blast - -text{* Generation of a goal clause -- put away the final literal *} - -lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)" -by blast - -lemma make_pos_goal: "P ==> ((P==>~P) ==> False)" -by blast - - -subsubsection{* Lemmas for Forward Proof*} - -text{*There is a similarity to congruence rules*} - -(*NOTE: could handle conjunctions (faster?) by - nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) -lemma conj_forward: "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q" -by blast - -lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q" -by blast - -(*Version of @{text disj_forward} for removal of duplicate literals*) -lemma disj_forward2: - "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q" -apply blast -done - -lemma all_forward: "[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)" -by blast - -lemma ex_forward: "[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)" -by blast - - -subsection {* Meson package *} - -use "Tools/meson.ML" - -setup Meson.setup - - subsection {* Specification package -- Hilbertized version *} lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c" @@ -580,5 +447,4 @@ use "Tools/choice_specification.ML" - end diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/IsaMakefile Wed Oct 06 17:44:21 2010 +0200 @@ -154,6 +154,8 @@ Groups.thy \ Inductive.thy \ Lattices.thy \ + Meson.thy \ + Metis.thy \ Nat.thy \ Option.thy \ Orderings.thy \ @@ -201,6 +203,12 @@ Tools/inductive_realizer.ML \ Tools/inductive_set.ML \ Tools/lin_arith.ML \ + Tools/Meson/meson.ML \ + Tools/Meson/meson_clausify.ML \ + Tools/Meson/meson_tactic.ML \ + Tools/Metis/metis_reconstruct.ML \ + Tools/Metis/metis_translate.ML \ + Tools/Metis/metis_tactics.ML \ Tools/nat_arith.ML \ Tools/primrec.ML \ Tools/prop_logic.ML \ @@ -219,12 +227,14 @@ $(SRC)/Provers/Arith/fast_lin_arith.ML \ $(SRC)/Provers/order.ML \ $(SRC)/Provers/trancl.ML \ + $(SRC)/Tools/Metis/metis.ML \ $(SRC)/Tools/rat.ML $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) @$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ + ATP.thy \ Big_Operators.thy \ Code_Evaluation.thy \ Code_Numeral.thy \ @@ -264,7 +274,6 @@ $(SRC)/Provers/Arith/cancel_numerals.ML \ $(SRC)/Provers/Arith/combine_numerals.ML \ $(SRC)/Provers/Arith/extract_common_term.ML \ - $(SRC)/Tools/Metis/metis.ML \ Tools/async_manager.ML \ Tools/ATP/atp_problem.ML \ Tools/ATP/atp_proof.ML \ @@ -275,7 +284,6 @@ Tools/int_arith.ML \ Tools/groebner.ML \ Tools/list_code.ML \ - Tools/meson.ML \ Tools/nat_numeral_simprocs.ML \ Tools/Nitpick/kodkod.ML \ Tools/Nitpick/kodkod_sat.ML \ @@ -315,10 +323,6 @@ Tools/recdef.ML \ Tools/record.ML \ Tools/semiring_normalizer.ML \ - Tools/Sledgehammer/meson_clausify.ML \ - Tools/Sledgehammer/metis_reconstruct.ML \ - Tools/Sledgehammer/metis_translate.ML \ - Tools/Sledgehammer/metis_tactics.ML \ Tools/Sledgehammer/sledgehammer.ML \ Tools/Sledgehammer/sledgehammer_filter.ML \ Tools/Sledgehammer/sledgehammer_minimize.ML \ diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/List.thy --- a/src/HOL/List.thy Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/List.thy Wed Oct 06 17:44:21 2010 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef +imports Plain Quotient Presburger Code_Numeral Recdef uses ("Tools/list_code.ML") begin diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Meson.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Meson.thy Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,207 @@ +(* Title: HOL/Meson.thy + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Tobias Nipkow, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2001 University of Cambridge +*) + +header {* MESON Proof Method *} + +theory Meson +imports Datatype +uses ("Tools/Meson/meson.ML") + ("Tools/Meson/meson_clausify.ML") + ("Tools/Meson/meson_tactic.ML") +begin + +section {* Negation Normal Form *} + +text {* de Morgan laws *} + +lemma not_conjD: "~(P&Q) ==> ~P | ~Q" + and not_disjD: "~(P|Q) ==> ~P & ~Q" + and not_notD: "~~P ==> P" + and not_allD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" + and not_exD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" + by fast+ + +text {* Removal of @{text "-->"} and @{text "<->"} (positive and +negative occurrences) *} + +lemma imp_to_disjD: "P-->Q ==> ~P | Q" + and not_impD: "~(P-->Q) ==> P & ~Q" + and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" + and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" + -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *} + and not_refl_disj_D: "x ~= x | P ==> P" + by fast+ + + +section {* Pulling out the existential quantifiers *} + +text {* Conjunction *} + +lemma conj_exD1: "!!P Q. (\x. P(x)) & Q ==> \x. P(x) & Q" + and conj_exD2: "!!P Q. P & (\x. Q(x)) ==> \x. P & Q(x)" + by fast+ + + +text {* Disjunction *} + +lemma disj_exD: "!!P Q. (\x. P(x)) | (\x. Q(x)) ==> \x. P(x) | Q(x)" + -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *} + -- {* With ex-Skolemization, makes fewer Skolem constants *} + and disj_exD1: "!!P Q. (\x. P(x)) | Q ==> \x. P(x) | Q" + and disj_exD2: "!!P Q. P | (\x. Q(x)) ==> \x. P | Q(x)" + by fast+ + +lemma disj_assoc: "(P|Q)|R ==> P|(Q|R)" + and disj_comm: "P|Q ==> Q|P" + and disj_FalseD1: "False|P ==> P" + and disj_FalseD2: "P|False ==> P" + by fast+ + + +text{* Generation of contrapositives *} + +text{*Inserts negated disjunct after removing the negation; P is a literal. + Model elimination requires assuming the negation of every attempted subgoal, + hence the negated disjuncts.*} +lemma make_neg_rule: "~P|Q ==> ((~P==>P) ==> Q)" +by blast + +text{*Version for Plaisted's "Postive refinement" of the Meson procedure*} +lemma make_refined_neg_rule: "~P|Q ==> (P ==> Q)" +by blast + +text{*@{term P} should be a literal*} +lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)" +by blast + +text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't +insert new assumptions, for ordinary resolution.*} + +lemmas make_neg_rule' = make_refined_neg_rule + +lemma make_pos_rule': "[|P|Q; ~P|] ==> Q" +by blast + +text{* Generation of a goal clause -- put away the final literal *} + +lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)" +by blast + +lemma make_pos_goal: "P ==> ((P==>~P) ==> False)" +by blast + + +section {* Lemmas for Forward Proof *} + +text{*There is a similarity to congruence rules*} + +(*NOTE: could handle conjunctions (faster?) by + nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) +lemma conj_forward: "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q" +by blast + +lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q" +by blast + +(*Version of @{text disj_forward} for removal of duplicate literals*) +lemma disj_forward2: + "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q" +apply blast +done + +lemma all_forward: "[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)" +by blast + +lemma ex_forward: "[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)" +by blast + + +section {* Clausification helper *} + +lemma TruepropI: "P \ Q \ Trueprop P \ Trueprop Q" +by simp + + +text{* Combinator translation helpers *} + +definition COMBI :: "'a \ 'a" where +[no_atp]: "COMBI P = P" + +definition COMBK :: "'a \ 'b \ 'a" where +[no_atp]: "COMBK P Q = P" + +definition COMBB :: "('b => 'c) \ ('a => 'b) \ 'a \ 'c" where [no_atp]: +"COMBB P Q R = P (Q R)" + +definition COMBC :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where +[no_atp]: "COMBC P Q R = P R Q" + +definition COMBS :: "('a \ 'b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where +[no_atp]: "COMBS P Q R = P R (Q R)" + +lemma abs_S [no_atp]: "\x. (f x) (g x) \ COMBS f g" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBS_def) +done + +lemma abs_I [no_atp]: "\x. x \ COMBI" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBI_def) +done + +lemma abs_K [no_atp]: "\x. y \ COMBK y" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBK_def) +done + +lemma abs_B [no_atp]: "\x. a (g x) \ COMBB a g" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBB_def) +done + +lemma abs_C [no_atp]: "\x. (f x) b \ COMBC f b" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBC_def) +done + + +section {* Skolemization helpers *} + +definition skolem :: "'a \ 'a" where +[no_atp]: "skolem = (\x. x)" + +lemma skolem_COMBK_iff: "P \ skolem (COMBK P (i\nat))" +unfolding skolem_def COMBK_def by (rule refl) + +lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] +lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] + + +section {* Meson package *} + +use "Tools/Meson/meson.ML" +use "Tools/Meson/meson_clausify.ML" +use "Tools/Meson/meson_tactic.ML" + +setup {* + Meson.setup + #> Meson_Tactic.setup +*} + +hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem +hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD + not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD + disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI + COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C + abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D + +end diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Metis.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis.thy Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,37 @@ +(* Title: HOL/Metis.thy + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen +*) + +header {* Metis Proof Method *} + +theory Metis +imports Meson +uses "~~/src/Tools/Metis/metis.ML" + ("Tools/Metis/metis_translate.ML") + ("Tools/Metis/metis_reconstruct.ML") + ("Tools/Metis/metis_tactics.ML") +begin + +definition fequal :: "'a \ 'a \ bool" where [no_atp]: +"fequal X Y \ (X = Y)" + +lemma fequal_imp_equal [no_atp]: "\ fequal X Y \ X = Y" +by (simp add: fequal_def) + +lemma equal_imp_fequal [no_atp]: "\ X = Y \ fequal X Y" +by (simp add: fequal_def) + +lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" +by auto + +use "Tools/Metis/metis_translate.ML" +use "Tools/Metis/metis_reconstruct.ML" +use "Tools/Metis/metis_tactics.ML" +setup Metis_Tactics.setup + +hide_const (open) fequal +hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal + +end diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Plain.thy --- a/src/HOL/Plain.thy Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Plain.thy Wed Oct 06 17:44:21 2010 +0200 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype FunDef Extraction +imports Datatype FunDef Extraction Metis begin text {* diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Oct 06 17:44:21 2010 +0200 @@ -242,7 +242,7 @@ lemma sigma_sets_Un: "a \ sigma_sets sp A \ b \ sigma_sets sp A \ a \ b \ sigma_sets sp A" apply (simp add: Un_range_binary range_binary_eq) -apply (rule Union, simp add: binary_def COMBK_def fun_upd_apply) +apply (rule Union, simp add: binary_def fun_upd_apply) done lemma sigma_sets_Inter: diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Quotient.thy Wed Oct 06 17:44:21 2010 +0200 @@ -5,7 +5,7 @@ header {* Definition of Quotient Types *} theory Quotient -imports Plain Sledgehammer +imports Plain Hilbert_Choice uses ("Tools/Quotient/quotient_info.ML") ("Tools/Quotient/quotient_typ.ML") @@ -319,12 +319,12 @@ lemma ball_reg_right: assumes a: "\x. R x \ P x \ Q x" shows "All P \ Ball R Q" - using a by (metis COMBC_def Collect_def Collect_mem_eq) + using a by (metis Collect_def Collect_mem_eq) lemma bex_reg_left: assumes a: "\x. R x \ Q x \ P x" shows "Bex R Q \ Ex P" - using a by (metis COMBC_def Collect_def Collect_mem_eq) + using a by (metis Collect_def Collect_mem_eq) lemma ball_reg_left: assumes a: "equivp R" @@ -381,13 +381,13 @@ assumes a: "!x :: 'a. (R x --> P x --> Q x)" and b: "Ball R P" shows "Ball R Q" - using a b by (metis COMBC_def Collect_def Collect_mem_eq) + using a b by (metis Collect_def Collect_mem_eq) lemma bex_reg: assumes a: "!x :: 'a. (R x --> P x --> Q x)" and b: "Bex R P" shows "Bex R Q" - using a b by (metis COMBC_def Collect_def Collect_mem_eq) + using a b by (metis Collect_def Collect_mem_eq) lemma ball_all_comm: diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Refute.thy --- a/src/HOL/Refute.thy Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Refute.thy Wed Oct 06 17:44:21 2010 +0200 @@ -8,7 +8,7 @@ header {* Refute *} theory Refute -imports Hilbert_Choice List +imports Hilbert_Choice List Sledgehammer uses "Tools/refute.ML" begin diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Oct 06 17:44:21 2010 +0200 @@ -1,125 +1,25 @@ (* Title: HOL/Sledgehammer.thy Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jia Meng, Cambridge University Computer Laboratory and NICTA - Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen *) header {* Sledgehammer: Isabelle--ATP Linkup *} theory Sledgehammer -imports Plain Hilbert_Choice -uses - ("Tools/ATP/atp_problem.ML") - ("Tools/ATP/atp_proof.ML") - ("Tools/ATP/atp_systems.ML") - ("~~/src/Tools/Metis/metis.ML") - ("Tools/Sledgehammer/meson_clausify.ML") - ("Tools/Sledgehammer/metis_translate.ML") - ("Tools/Sledgehammer/metis_reconstruct.ML") - ("Tools/Sledgehammer/metis_tactics.ML") - ("Tools/Sledgehammer/sledgehammer_util.ML") - ("Tools/Sledgehammer/sledgehammer_filter.ML") - ("Tools/Sledgehammer/sledgehammer_translate.ML") - ("Tools/Sledgehammer/sledgehammer_reconstruct.ML") - ("Tools/Sledgehammer/sledgehammer.ML") - ("Tools/Sledgehammer/sledgehammer_minimize.ML") - ("Tools/Sledgehammer/sledgehammer_isar.ML") +imports ATP +uses "Tools/Sledgehammer/sledgehammer_util.ML" + "Tools/Sledgehammer/sledgehammer_filter.ML" + "Tools/Sledgehammer/sledgehammer_translate.ML" + "Tools/Sledgehammer/sledgehammer_reconstruct.ML" + "Tools/Sledgehammer/sledgehammer.ML" + "Tools/Sledgehammer/sledgehammer_minimize.ML" + "Tools/Sledgehammer/sledgehammer_isar.ML" begin -lemma TruepropI: "P \ Q \ Trueprop P \ Trueprop Q" -by simp - -definition skolem :: "'a \ 'a" where -[no_atp]: "skolem = (\x. x)" - -definition COMBI :: "'a \ 'a" where -[no_atp]: "COMBI P = P" - -definition COMBK :: "'a \ 'b \ 'a" where -[no_atp]: "COMBK P Q = P" - -definition COMBB :: "('b => 'c) \ ('a => 'b) \ 'a \ 'c" where [no_atp]: -"COMBB P Q R = P (Q R)" - -definition COMBC :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where -[no_atp]: "COMBC P Q R = P R Q" - -definition COMBS :: "('a \ 'b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where -[no_atp]: "COMBS P Q R = P R (Q R)" - -definition fequal :: "'a \ 'a \ bool" where [no_atp]: -"fequal X Y \ (X = Y)" - -lemma fequal_imp_equal [no_atp]: "\ fequal X Y \ X = Y" -by (simp add: fequal_def) - -lemma equal_imp_fequal [no_atp]: "\ X = Y \ fequal X Y" -by (simp add: fequal_def) - -lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" -by auto - -lemma skolem_COMBK_iff: "P \ skolem (COMBK P (i\nat))" -unfolding skolem_def COMBK_def by (rule refl) - -lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] -lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] - -text{*Theorems for translation to combinators*} - -lemma abs_S [no_atp]: "\x. (f x) (g x) \ COMBS f g" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBS_def) -done - -lemma abs_I [no_atp]: "\x. x \ COMBI" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBI_def) -done - -lemma abs_K [no_atp]: "\x. y \ COMBK y" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBK_def) -done - -lemma abs_B [no_atp]: "\x. a (g x) \ COMBB a g" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBB_def) -done - -lemma abs_C [no_atp]: "\x. (f x) b \ COMBC f b" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBC_def) -done - -use "Tools/ATP/atp_problem.ML" -use "Tools/ATP/atp_proof.ML" -use "Tools/ATP/atp_systems.ML" -setup ATP_Systems.setup - -use "~~/src/Tools/Metis/metis.ML" -use "Tools/Sledgehammer/meson_clausify.ML" -setup Meson_Clausify.setup - -use "Tools/Sledgehammer/metis_translate.ML" -use "Tools/Sledgehammer/metis_reconstruct.ML" -use "Tools/Sledgehammer/metis_tactics.ML" -setup Metis_Tactics.setup - -use "Tools/Sledgehammer/sledgehammer_util.ML" -use "Tools/Sledgehammer/sledgehammer_filter.ML" -use "Tools/Sledgehammer/sledgehammer_translate.ML" -use "Tools/Sledgehammer/sledgehammer_reconstruct.ML" -use "Tools/Sledgehammer/sledgehammer.ML" -setup Sledgehammer.setup -use "Tools/Sledgehammer/sledgehammer_minimize.ML" -use "Tools/Sledgehammer/sledgehammer_isar.ML" -setup Sledgehammer_Isar.setup +setup {* + Sledgehammer.setup + #> Sledgehammer_Isar.setup +*} end diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Meson/meson.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Meson/meson.ML Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,720 @@ +(* Title: HOL/Tools/Meson/meson.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +The MESON resolution proof procedure for HOL. +When making clauses, avoids using the rewriter -- instead uses RS recursively. +*) + +signature MESON = +sig + val trace: bool Unsynchronized.ref + val term_pair_of: indexname * (typ * 'a) -> term * 'a + val size_of_subgoals: thm -> int + val has_too_many_clauses: Proof.context -> term -> bool + val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context + val finish_cnf: thm list -> thm list + val presimplify: thm -> thm + val make_nnf: Proof.context -> thm -> thm + val choice_theorems : theory -> thm list + val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm + val skolemize : Proof.context -> thm -> thm + val is_fol_term: theory -> term -> bool + val make_clauses_unsorted: thm list -> thm list + val make_clauses: thm list -> thm list + val make_horns: thm list -> thm list + val best_prolog_tac: (thm -> int) -> thm list -> tactic + val depth_prolog_tac: thm list -> tactic + val gocls: thm list -> thm list + val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic + val MESON: + tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context + -> int -> tactic + val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic + val safe_best_meson_tac: Proof.context -> int -> tactic + val depth_meson_tac: Proof.context -> int -> tactic + val prolog_step_tac': thm list -> int -> tactic + val iter_deepen_prolog_tac: thm list -> tactic + val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic + val make_meta_clause: thm -> thm + val make_meta_clauses: thm list -> thm list + val meson_tac: Proof.context -> thm list -> int -> tactic + val setup: theory -> theory +end + +structure Meson : MESON = +struct + +val trace = Unsynchronized.ref false; +fun trace_msg msg = if ! trace then tracing (msg ()) else (); + +val max_clauses_default = 60; +val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default); + +(*No known example (on 1-5-2007) needs even thirty*) +val iter_deepen_limit = 50; + +val disj_forward = @{thm disj_forward}; +val disj_forward2 = @{thm disj_forward2}; +val make_pos_rule = @{thm make_pos_rule}; +val make_pos_rule' = @{thm make_pos_rule'}; +val make_pos_goal = @{thm make_pos_goal}; +val make_neg_rule = @{thm make_neg_rule}; +val make_neg_rule' = @{thm make_neg_rule'}; +val make_neg_goal = @{thm make_neg_goal}; +val conj_forward = @{thm conj_forward}; +val all_forward = @{thm all_forward}; +val ex_forward = @{thm ex_forward}; + +val not_conjD = @{thm not_conjD}; +val not_disjD = @{thm not_disjD}; +val not_notD = @{thm not_notD}; +val not_allD = @{thm not_allD}; +val not_exD = @{thm not_exD}; +val imp_to_disjD = @{thm imp_to_disjD}; +val not_impD = @{thm not_impD}; +val iff_to_disjD = @{thm iff_to_disjD}; +val not_iffD = @{thm not_iffD}; +val conj_exD1 = @{thm conj_exD1}; +val conj_exD2 = @{thm conj_exD2}; +val disj_exD = @{thm disj_exD}; +val disj_exD1 = @{thm disj_exD1}; +val disj_exD2 = @{thm disj_exD2}; +val disj_assoc = @{thm disj_assoc}; +val disj_comm = @{thm disj_comm}; +val disj_FalseD1 = @{thm disj_FalseD1}; +val disj_FalseD2 = @{thm disj_FalseD2}; + + +(**** Operators for forward proof ****) + + +(** First-order Resolution **) + +fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); + +(*FIXME: currently does not "rename variables apart"*) +fun first_order_resolve thA thB = + (case + try (fn () => + let val thy = theory_of_thm thA + val tmA = concl_of thA + val Const("==>",_) $ tmB $ _ = prop_of thB + val tenv = + Pattern.first_order_match thy (tmB, tmA) + (Vartab.empty, Vartab.empty) |> snd + val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) + in thA RS (cterm_instantiate ct_pairs thB) end) () of + SOME th => th + | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) + +(* Applying "choice" swaps the bound variable names. We tweak + "Thm.rename_boundvars"'s input to get the desired names. *) +fun fix_bounds (_ $ (Const (@{const_name Ex}, _) + $ Abs (_, _, Const (@{const_name All}, _) $ _))) + (t0 $ (Const (@{const_name All}, T1) + $ Abs (a1, T1', Const (@{const_name Ex}, T2) + $ Abs (a2, T2', t')))) = + t0 $ (Const (@{const_name All}, T1) + $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t'))) + | fix_bounds _ t = t + +(* Hack to make it less likely that we lose our precious bound variable names in + "rename_bvs_RS" below, because of a clash. *) +val protect_prefix = "_" + +fun protect_bounds (t $ u) = protect_bounds t $ protect_bounds u + | protect_bounds (Abs (s, T, t')) = + Abs (protect_prefix ^ s, T, protect_bounds t') + | protect_bounds t = t + +(* Forward proof while preserving bound variables names*) +fun rename_bvs_RS th rl = + let + val t = concl_of th + val r = concl_of rl + val th' = th RS Thm.rename_boundvars r (protect_bounds r) rl + val t' = concl_of th' + in Thm.rename_boundvars t' (fix_bounds t' t) th' end + +(*raises exception if no rules apply*) +fun tryres (th, rls) = + let fun tryall [] = raise THM("tryres", 0, th::rls) + | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls) + in tryall rls end; + +(*Permits forward proof from rules that discharge assumptions. The supplied proof state st, + e.g. from conj_forward, should have the form + "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" + and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) +fun forward_res ctxt nf st = + let fun forward_tacf [prem] = rtac (nf prem) 1 + | forward_tacf prems = + error (cat_lines + ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: + Display.string_of_thm ctxt st :: + "Premises:" :: map (Display.string_of_thm ctxt) prems)) + in + case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st) + of SOME(th,_) => th + | NONE => raise THM("forward_res", 0, [st]) + end; + +(*Are any of the logical connectives in "bs" present in the term?*) +fun has_conns bs = + let fun has (Const _) = false + | has (Const(@{const_name Trueprop},_) $ p) = has p + | has (Const(@{const_name Not},_) $ p) = has p + | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q + | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q + | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p + | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p + | has _ = false + in has end; + + +(**** Clause handling ****) + +fun literals (Const(@{const_name Trueprop},_) $ P) = literals P + | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q + | literals (Const(@{const_name Not},_) $ P) = [(false,P)] + | literals P = [(true,P)]; + +(*number of literals in a term*) +val nliterals = length o literals; + + +(*** Tautology Checking ***) + +fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) = + signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) + | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits) + | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); + +fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); + +(*Literals like X=X are tautologous*) +fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u + | taut_poslit (Const(@{const_name True},_)) = true + | taut_poslit _ = false; + +fun is_taut th = + let val (poslits,neglits) = signed_lits th + in exists taut_poslit poslits + orelse + exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) + end + handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) + + +(*** To remove trivial negated equality literals from clauses ***) + +(*They are typically functional reflexivity axioms and are the converses of + injectivity equivalences*) + +val not_refl_disj_D = @{thm not_refl_disj_D}; + +(*Is either term a Var that does not properly occur in the other term?*) +fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) + | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u)) + | eliminable _ = false; + +fun refl_clause_aux 0 th = th + | refl_clause_aux n th = + case HOLogic.dest_Trueprop (concl_of th) of + (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) => + refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) + | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) => + if eliminable(t,u) + then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*) + else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) + | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) + | _ => (*not a disjunction*) th; + +fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) = + notequal_lits_count P + notequal_lits_count Q + | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1 + | notequal_lits_count _ = 0; + +(*Simplify a clause by applying reflexivity to its negated equality literals*) +fun refl_clause th = + let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) + in zero_var_indexes (refl_clause_aux neqs th) end + handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) + + +(*** Removal of duplicate literals ***) + +(*Forward proof, passing extra assumptions as theorems to the tactic*) +fun forward_res2 nf hyps st = + case Seq.pull + (REPEAT + (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) + st) + of SOME(th,_) => th + | NONE => raise THM("forward_res2", 0, [st]); + +(*Remove duplicates in P|Q by assuming ~P in Q + rls (initially []) accumulates assumptions of the form P==>False*) +fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc) + handle THM _ => tryres(th,rls) + handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2), + [disj_FalseD1, disj_FalseD2, asm_rl]) + handle THM _ => th; + +(*Remove duplicate literals, if there are any*) +fun nodups ctxt th = + if has_duplicates (op =) (literals (prop_of th)) + then nodups_aux ctxt [] th + else th; + + +(*** The basic CNF transformation ***) + +fun estimated_num_clauses bound t = + let + fun sum x y = if x < bound andalso y < bound then x+y else bound + fun prod x y = if x < bound andalso y < bound then x*y else bound + + (*Estimate the number of clauses in order to detect infeasible theorems*) + fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t + | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t + | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) = + if b then sum (signed_nclauses b t) (signed_nclauses b u) + else prod (signed_nclauses b t) (signed_nclauses b u) + | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) = + if b then prod (signed_nclauses b t) (signed_nclauses b u) + else sum (signed_nclauses b t) (signed_nclauses b u) + | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) = + if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) + else sum (signed_nclauses (not b) t) (signed_nclauses b u) + | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) = + if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*) + if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) + (prod (signed_nclauses (not b) u) (signed_nclauses b t)) + else sum (prod (signed_nclauses b t) (signed_nclauses b u)) + (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) + else 1 + | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t + | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t + | signed_nclauses _ _ = 1; (* literal *) + in signed_nclauses true t end + +fun has_too_many_clauses ctxt t = + let val max_cl = Config.get ctxt max_clauses in + estimated_num_clauses (max_cl + 1) t > max_cl + end + +(*Replaces universally quantified variables by FREE variables -- because + assumptions may not contain scheme variables. Later, generalize using Variable.export. *) +local + val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))); + val spec_varT = #T (Thm.rep_cterm spec_var); + fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu; +in + fun freeze_spec th ctxt = + let + val cert = Thm.cterm_of (ProofContext.theory_of ctxt); + val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; + val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; + in (th RS spec', ctxt') end +end; + +(*Used with METAHYPS below. There is one assumption, which gets bound to prem + and then normalized via function nf. The normal form is given to resolve_tac, + instantiate a Boolean variable created by resolution with disj_forward. Since + (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) +fun resop nf [prem] = resolve_tac (nf prem) 1; + +(* Any need to extend this list with "HOL.type_class", "HOL.eq_class", + and "Pure.term"? *) +val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); + +fun apply_skolem_theorem (th, rls) = + let + fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) + | tryall (rl :: rls) = + first_order_resolve th rl handle THM _ => tryall rls + in tryall rls end + +(* Conjunctive normal form, adding clauses from th in front of ths (for foldr). + Strips universal quantifiers and breaks up conjunctions. + Eliminates existential quantifiers using Skolemization theorems. *) +fun cnf old_skolem_ths ctxt (th, ths) = + let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *) + fun cnf_aux (th,ths) = + if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) + else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th)) + then nodups ctxt th :: ths (*no work to do, terminate*) + else case head_of (HOLogic.dest_Trueprop (concl_of th)) of + Const (@{const_name HOL.conj}, _) => (*conjunction*) + cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) + | Const (@{const_name All}, _) => (*universal quantifier*) + let val (th',ctxt') = freeze_spec th (!ctxtr) + in ctxtr := ctxt'; cnf_aux (th', ths) end + | Const (@{const_name Ex}, _) => + (*existential quantifier: Insert Skolem functions*) + cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) + | Const (@{const_name HOL.disj}, _) => + (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using + all combinations of converting P, Q to CNF.*) + let val tac = + Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN + (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1) + in Seq.list_of (tac (th RS disj_forward)) @ ths end + | _ => nodups ctxt th :: ths (*no work to do*) + and cnf_nil th = cnf_aux (th,[]) + val cls = + if has_too_many_clauses ctxt (concl_of th) + then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) + else cnf_aux (th,ths) + in (cls, !ctxtr) end; + +fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, []) + +(*Generalization, removal of redundant equalities, removal of tautologies.*) +fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths); + + +(**** Generation of contrapositives ****) + +fun is_left (Const (@{const_name Trueprop}, _) $ + (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true + | is_left _ = false; + +(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) +fun assoc_right th = + if is_left (prop_of th) then assoc_right (th RS disj_assoc) + else th; + +(*Must check for negative literal first!*) +val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; + +(*For ordinary resolution. *) +val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; + +(*Create a goal or support clause, conclusing False*) +fun make_goal th = (*Must check for negative literal first!*) + make_goal (tryres(th, clause_rules)) + handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); + +(*Sort clauses by number of literals*) +fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); + +fun sort_clauses ths = sort (make_ord fewerlits) ths; + +fun has_bool @{typ bool} = true + | has_bool (Type (_, Ts)) = exists has_bool Ts + | has_bool _ = false + +fun has_fun (Type (@{type_name fun}, _)) = true + | has_fun (Type (_, Ts)) = exists has_fun Ts + | has_fun _ = false + +(*Is the string the name of a connective? Really only | and Not can remain, + since this code expects to be called on a clause form.*) +val is_conn = member (op =) + [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, + @{const_name HOL.implies}, @{const_name Not}, + @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}]; + +(*True if the term contains a function--not a logical connective--where the type + of any argument contains bool.*) +val has_bool_arg_const = + exists_Const + (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T)); + +(*A higher-order instance of a first-order constant? Example is the definition of + one, 1, at a function type in theory Function_Algebras.*) +fun higher_inst_const thy (c,T) = + case binder_types T of + [] => false (*not a function type, OK*) + | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts; + +(*Returns false if any Vars in the theorem mention type bool. + Also rejects functions whose arguments are Booleans or other functions.*) +fun is_fol_term thy t = + Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso + not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T + | _ => false) t orelse + has_bool_arg_const t orelse + exists_Const (higher_inst_const thy) t orelse + has_meta_conn t); + +fun rigid t = not (is_Var (head_of t)); + +fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t + | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t + | ok4horn _ = false; + +(*Create a meta-level Horn clause*) +fun make_horn crules th = + if ok4horn (concl_of th) + then make_horn crules (tryres(th,crules)) handle THM _ => th + else th; + +(*Generate Horn clauses for all contrapositives of a clause. The input, th, + is a HOL disjunction.*) +fun add_contras crules th hcs = + let fun rots (0,_) = hcs + | rots (k,th) = zero_var_indexes (make_horn crules th) :: + rots(k-1, assoc_right (th RS disj_comm)) + in case nliterals(prop_of th) of + 1 => th::hcs + | n => rots(n, assoc_right th) + end; + +(*Use "theorem naming" to label the clauses*) +fun name_thms label = + let fun name1 th (k, ths) = + (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) + in fn ths => #2 (fold_rev name1 ths (length ths, [])) end; + +(*Is the given disjunction an all-negative support clause?*) +fun is_negative th = forall (not o #1) (literals (prop_of th)); + +val neg_clauses = filter is_negative; + + +(***** MESON PROOF PROCEDURE *****) + +fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi, + As) = rhyps(phi, A::As) + | rhyps (_, As) = As; + +(** Detecting repeated assumptions in a subgoal **) + +(*The stringtree detects repeated assumptions.*) +fun ins_term t net = Net.insert_term (op aconv) (t, t) net; + +(*detects repetitions in a list of terms*) +fun has_reps [] = false + | has_reps [_] = false + | has_reps [t,u] = (t aconv u) + | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true; + +(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) +fun TRYING_eq_assume_tac 0 st = Seq.single st + | TRYING_eq_assume_tac i st = + TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st) + handle THM _ => TRYING_eq_assume_tac (i-1) st; + +fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st; + +(*Loop checking: FAIL if trying to prove the same thing twice + -- if *ANY* subgoal has repeated literals*) +fun check_tac st = + if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) + then Seq.empty else Seq.single st; + + +(* net_resolve_tac actually made it slower... *) +fun prolog_step_tac horns i = + (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN + TRYALL_eq_assume_tac; + +(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) +fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz; + +fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0; + + +(*Negation Normal Form*) +val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, + not_impD, not_iffD, not_allD, not_exD, not_notD]; + +fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t + | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t + | ok4nnf _ = false; + +fun make_nnf1 ctxt th = + if ok4nnf (concl_of th) + then make_nnf1 ctxt (tryres(th, nnf_rls)) + handle THM ("tryres", _, _) => + forward_res ctxt (make_nnf1 ctxt) + (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) + handle THM ("tryres", _, _) => th + else th + +(*The simplification removes defined quantifiers and occurrences of True and False. + nnf_ss also includes the one-point simprocs, + which are needed to avoid the various one-point theorems from generating junk clauses.*) +val nnf_simps = + @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel + if_eq_cancel cases_simp} +val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms} + +val nnf_ss = + HOL_basic_ss addsimps nnf_extra_simps + addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; + +val presimplify = + rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss + +fun make_nnf ctxt th = case prems_of th of + [] => th |> presimplify |> make_nnf1 ctxt + | _ => raise THM ("make_nnf: premises in argument", 0, [th]); + +fun choice_theorems thy = + try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list + +(* Pull existential quantifiers to front. This accomplishes Skolemization for + clauses that arise from a subgoal. *) +fun skolemize_with_choice_theorems ctxt choice_ths = + let + fun aux th = + if not (has_conns [@{const_name Ex}] (prop_of th)) then + th + else + tryres (th, choice_ths @ + [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]) + |> aux + handle THM ("tryres", _, _) => + tryres (th, [conj_forward, disj_forward, all_forward]) + |> forward_res ctxt aux + |> aux + handle THM ("tryres", _, _) => + rename_bvs_RS th ex_forward + |> forward_res ctxt aux + in aux o make_nnf ctxt end + +fun skolemize ctxt = + let val thy = ProofContext.theory_of ctxt in + skolemize_with_choice_theorems ctxt (choice_theorems thy) + end + +(* "RS" can fail if "unify_search_bound" is too small. *) +fun try_skolemize ctxt th = + try (skolemize ctxt) th + |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^ + Display.string_of_thm ctxt th) + | _ => ()) + +fun add_clauses th cls = + let val ctxt0 = Variable.global_thm_context th + val (cnfs, ctxt) = make_cnf [] th ctxt0 + in Variable.export ctxt ctxt0 cnfs @ cls end; + +(*Make clauses from a list of theorems, previously Skolemized and put into nnf. + The resulting clauses are HOL disjunctions.*) +fun make_clauses_unsorted ths = fold_rev add_clauses ths []; +val make_clauses = sort_clauses o make_clauses_unsorted; + +(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) +fun make_horns ths = + name_thms "Horn#" + (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths [])); + +(*Could simply use nprems_of, which would count remaining subgoals -- no + discrimination as to their size! With BEST_FIRST, fails for problem 41.*) + +fun best_prolog_tac sizef horns = + BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); + +fun depth_prolog_tac horns = + DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); + +(*Return all negative clauses, as possible goal clauses*) +fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); + +fun skolemize_prems_tac ctxt prems = + cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE + +(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. + Function mkcl converts theorems to clauses.*) +fun MESON preskolem_tac mkcl cltac ctxt i st = + SELECT_GOAL + (EVERY [Object_Logic.atomize_prems_tac 1, + rtac ccontr 1, + preskolem_tac, + Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => + EVERY1 [skolemize_prems_tac ctxt negs, + Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st + handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) + + +(** Best-first search versions **) + +(*ths is a list of additional clauses (HOL disjunctions) to use.*) +fun best_meson_tac sizef = + MESON all_tac make_clauses + (fn cls => + THEN_BEST_FIRST (resolve_tac (gocls cls) 1) + (has_fewer_prems 1, sizef) + (prolog_step_tac (make_horns cls) 1)); + +(*First, breaks the goal into independent units*) +fun safe_best_meson_tac ctxt = + SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN + TRYALL (best_meson_tac size_of_subgoals ctxt)); + +(** Depth-first search version **) + +val depth_meson_tac = + MESON all_tac make_clauses + (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]); + + +(** Iterative deepening version **) + +(*This version does only one inference per call; + having only one eq_assume_tac speeds it up!*) +fun prolog_step_tac' horns = + let val (horn0s, _) = (*0 subgoals vs 1 or more*) + take_prefix Thm.no_prems horns + val nrtac = net_resolve_tac horns + in fn i => eq_assume_tac i ORELSE + match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) + ((assume_tac i APPEND nrtac i) THEN check_tac) + end; + +fun iter_deepen_prolog_tac horns = + ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns); + +fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses + (fn cls => + (case (gocls (cls @ ths)) of + [] => no_tac (*no goal clauses*) + | goes => + let + val horns = make_horns (cls @ ths) + val _ = trace_msg (fn () => + cat_lines ("meson method called:" :: + map (Display.string_of_thm ctxt) (cls @ ths) @ + ["clauses:"] @ map (Display.string_of_thm ctxt) horns)) + in + THEN_ITER_DEEPEN iter_deepen_limit + (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) + end)); + +fun meson_tac ctxt ths = + SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); + + +(**** Code to support ordinary resolution, rather than Model Elimination ****) + +(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), + with no contrapositives, for ordinary resolution.*) + +(*Rules to convert the head literal into a negated assumption. If the head + literal is already negated, then using notEfalse instead of notEfalse' + prevents a double negation.*) +val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE; +val notEfalse' = rotate_prems 1 notEfalse; + +fun negated_asm_of_head th = + th RS notEfalse handle THM _ => th RS notEfalse'; + +(*Converting one theorem from a disjunction to a meta-level clause*) +fun make_meta_clause th = + let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th + in + (zero_var_indexes o Thm.varifyT_global o thaw 0 o + negated_asm_of_head o make_horn resolution_clause_rules) fth + end; + +fun make_meta_clauses ths = + name_thms "MClause#" + (distinct Thm.eq_thm_prop (map make_meta_clause ths)); + +end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Meson/meson_clausify.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,367 @@ +(* Title: HOL/Tools/Meson/meson_clausify.ML + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen + +Transformation of HOL theorems into CNF forms. +*) + +signature MESON_CLAUSIFY = +sig + val new_skolem_var_prefix : string + val extensionalize_theorem : thm -> thm + val introduce_combinators_in_cterm : cterm -> thm + val introduce_combinators_in_theorem : thm -> thm + val to_definitional_cnf_with_quantifiers : theory -> thm -> thm + val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool + val cnf_axiom : + Proof.context -> bool -> int -> thm -> (thm * term) option * thm list +end; + +structure Meson_Clausify : MESON_CLAUSIFY = +struct + +open Meson + +(* the extra "?" helps prevent clashes *) +val new_skolem_var_prefix = "?SK" +val new_nonskolem_var_prefix = "?V" + +(**** Transformation of Elimination Rules into First-Order Formulas****) + +val cfalse = cterm_of @{theory HOL} HOLogic.false_const; +val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); + +(* Converts an elim-rule into an equivalent theorem that does not have the + predicate variable. Leaves other theorems unchanged. We simply instantiate + the conclusion variable to False. (Cf. "transform_elim_term" in + "Sledgehammer_Util".) *) +fun transform_elim_theorem th = + case concl_of th of (*conclusion variable*) + @{const Trueprop} $ (v as Var (_, @{typ bool})) => + Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th + | v as Var(_, @{typ prop}) => + Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th + | _ => th + + +(**** SKOLEMIZATION BY INFERENCE (lcp) ****) + +fun mk_old_skolem_term_wrapper t = + let val T = fastype_of t in + Const (@{const_name Meson.skolem}, T --> T) $ t + end + +fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t') + | beta_eta_in_abs_body t = Envir.beta_eta_contract t + +(*Traverse a theorem, accumulating Skolem function definitions.*) +fun old_skolem_defs th = + let + fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss = + (*Existential: declare a Skolem function, then insert into body and continue*) + let + val args = OldTerm.term_frees body + (* Forms a lambda-abstraction over the formal parameters *) + val rhs = + list_abs_free (map dest_Free args, + HOLogic.choice_const T $ beta_eta_in_abs_body body) + |> mk_old_skolem_term_wrapper + val comb = list_comb (rhs, args) + in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end + | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = + (*Universal quant: insert a free variable into body and continue*) + let val fname = Name.variant (OldTerm.add_term_names (p,[])) a + in dec_sko (subst_bound (Free(fname,T), p)) rhss end + | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q + | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q + | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss + | dec_sko _ rhss = rhss + in dec_sko (prop_of th) [] end; + + +(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) + +val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} + +(* Removes the lambdas from an equation of the form "t = (%x. u)". + (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) +fun extensionalize_theorem th = + case prop_of th of + _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _])) + $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all) + | _ => th + +fun is_quasi_lambda_free (Const (@{const_name Meson.skolem}, _) $ _) = true + | is_quasi_lambda_free (t1 $ t2) = + is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 + | is_quasi_lambda_free (Abs _) = false + | is_quasi_lambda_free _ = true + +val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); +val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); +val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); + +(* FIXME: Requires more use of cterm constructors. *) +fun abstract ct = + let + val thy = theory_of_cterm ct + val Abs(x,_,body) = term_of ct + val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) + val cxT = ctyp_of thy xT + val cbodyT = ctyp_of thy bodyT + fun makeK () = + instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] + @{thm abs_K} + in + case body of + Const _ => makeK() + | Free _ => makeK() + | Var _ => makeK() (*though Var isn't expected*) + | Bound 0 => instantiate' [SOME cxT] [] @{thm 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)] @{thm 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)] @{thm 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 Thm.eta_conversion ct + else (*B*) + let val crand = cterm_of thy (Abs(x,xT,rand)) + val crator = cterm_of thy rator + val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} + val (_,rhs) = Thm.dest_equals (cprop_of abs_B') + in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end + else makeK() + | _ => raise Fail "abstract: Bad term" + end; + +(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) +fun introduce_combinators_in_cterm ct = + if is_quasi_lambda_free (term_of ct) then + Thm.reflexive ct + else case term_of ct of + Abs _ => + let + val (cv, cta) = Thm.dest_abs NONE ct + val (v, _) = dest_Free (term_of cv) + val u_th = introduce_combinators_in_cterm cta + val cu = Thm.rhs_of u_th + val comb_eq = abstract (Thm.cabs cv cu) + in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end + | _ $ _ => + let val (ct1, ct2) = Thm.dest_comb ct in + Thm.combination (introduce_combinators_in_cterm ct1) + (introduce_combinators_in_cterm ct2) + end + +fun introduce_combinators_in_theorem th = + if is_quasi_lambda_free (prop_of th) then + th + else + let + val th = Drule.eta_contraction_rule th + val eqth = introduce_combinators_in_cterm (cprop_of th) + in Thm.equal_elim eqth th end + handle THM (msg, _, _) => + (warning ("Error in the combinator translation of " ^ + Display.string_of_thm_without_context th ^ + "\nException message: " ^ msg ^ "."); + (* A type variable of sort "{}" will make abstraction fail. *) + TrueI) + +(*cterms are used throughout for efficiency*) +val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop; + +(*Given an abstraction over n variables, replace the bound variables by free + ones. Return the body, along with the list of free variables.*) +fun c_variant_abs_multi (ct0, vars) = + let val (cv,ct) = Thm.dest_abs NONE ct0 + in c_variant_abs_multi (ct, cv::vars) end + handle CTERM _ => (ct0, rev vars); + +val skolem_def_raw = @{thms skolem_def_raw} + +(* Given the definition of a Skolem function, return a theorem to replace + an existential formula by a use of that function. + Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) +fun old_skolem_theorem_from_def thy rhs0 = + let + val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy + val rhs' = rhs |> Thm.dest_comb |> snd + val (ch, frees) = c_variant_abs_multi (rhs', []) + val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of + val T = + case hilbert of + Const (_, Type (@{type_name fun}, [_, T])) => T + | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"", + [hilbert]) + val cex = cterm_of thy (HOLogic.exists_const T) + val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) + val conc = + Drule.list_comb (rhs, frees) + |> Drule.beta_conv cabs |> Thm.capply cTrueprop + fun tacf [prem] = + rewrite_goals_tac skolem_def_raw + THEN rtac ((prem |> rewrite_rule skolem_def_raw) + RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1 + in + Goal.prove_internal [ex_tm] conc tacf + |> forall_intr_list frees + |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) + |> Thm.varifyT_global + end + +fun to_definitional_cnf_with_quantifiers thy th = + let + val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) + val eqth = eqth RS @{thm eq_reflection} + val eqth = eqth RS @{thm TruepropI} + in Thm.equal_elim eqth th end + +fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s = + (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^ + "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ + string_of_int index_no ^ "_" ^ s + +fun cluster_of_zapped_var_name s = + let val get_int = the o Int.fromString o nth (space_explode "_" s) in + ((get_int 1, (get_int 2, get_int 3)), + String.isPrefix new_skolem_var_prefix s) + end + +fun zap (cluster as (cluster_no, cluster_skolem)) index_no pos ct = + ct + |> (case term_of ct of + Const (s, _) $ Abs (s', _, _) => + if s = @{const_name all} orelse s = @{const_name All} orelse + s = @{const_name Ex} then + let + val skolem = (pos = (s = @{const_name Ex})) + val (cluster, index_no) = + if skolem = cluster_skolem then (cluster, index_no) + else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0) + in + Thm.dest_comb #> snd + #> Thm.dest_abs (SOME (zapped_var_name cluster index_no s')) + #> snd #> zap cluster (index_no + 1) pos + end + else + Conv.all_conv + | Const (s, _) $ _ $ _ => + if s = @{const_name "==>"} orelse s = @{const_name implies} then + Conv.combination_conv (Conv.arg_conv (zap cluster index_no (not pos))) + (zap cluster index_no pos) + else if s = @{const_name conj} orelse s = @{const_name disj} then + Conv.combination_conv (Conv.arg_conv (zap cluster index_no pos)) + (zap cluster index_no pos) + else + Conv.all_conv + | Const (s, _) $ _ => + if s = @{const_name Trueprop} then + Conv.arg_conv (zap cluster index_no pos) + else if s = @{const_name Not} then + Conv.arg_conv (zap cluster index_no (not pos)) + else + Conv.all_conv + | _ => Conv.all_conv) + +fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths + +val no_choice = + @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"} + |> Logic.varify_global + |> Skip_Proof.make_thm @{theory} + +(* Converts an Isabelle theorem into NNF. *) +fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt = + let + val thy = ProofContext.theory_of ctxt + val th = + th |> transform_elim_theorem + |> zero_var_indexes + |> new_skolemizer ? forall_intr_vars + val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single + val th = th |> Conv.fconv_rule Object_Logic.atomize + |> extensionalize_theorem + |> make_nnf ctxt + in + if new_skolemizer then + let + fun skolemize choice_ths = + skolemize_with_choice_theorems ctxt choice_ths + #> simplify (ss_only @{thms all_simps[symmetric]}) + val pull_out = + simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) + val (discharger_th, fully_skolemized_th) = + if null choice_ths then + th |> `I |>> pull_out ||> skolemize [no_choice] + else + th |> skolemize choice_ths |> `I + val t = + fully_skolemized_th |> cprop_of + |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context + |> cprop_of |> Thm.dest_equals |> snd |> term_of + in + if exists_subterm (fn Var ((s, _), _) => + String.isPrefix new_skolem_var_prefix s + | _ => false) t then + let + val (ct, ctxt) = + Variable.import_terms true [t] ctxt + |>> the_single |>> cterm_of thy + in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end + else + (NONE, th, ctxt) + end + else + (NONE, th, ctxt) + end + +(* Convert a theorem to CNF, with additional premises due to skolemization. *) +fun cnf_axiom ctxt0 new_skolemizer ax_no th = + let + val thy = ProofContext.theory_of ctxt0 + val choice_ths = choice_theorems thy + val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 + fun clausify th = + make_cnf (if new_skolemizer orelse null choice_ths then + [] + else + map (old_skolem_theorem_from_def thy) + (old_skolem_defs th)) th ctxt + val (cnf_ths, ctxt) = + clausify nnf_th + |> (fn ([], _) => + clausify (to_definitional_cnf_with_quantifiers thy nnf_th) + | p => p) + fun intr_imp ct th = + Thm.instantiate ([], map (pairself (cterm_of thy)) + [(Var (("i", 0), @{typ nat}), + HOLogic.mk_nat ax_no)]) + (zero_var_indexes @{thm skolem_COMBK_D}) + RS Thm.implies_intr ct th + in + (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0) + ##> (term_of #> HOLogic.dest_Trueprop + #> singleton (Variable.export_terms ctxt ctxt0))), + cnf_ths |> map (introduce_combinators_in_theorem + #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) + |> Variable.export ctxt ctxt0 + |> finish_cnf + |> map Thm.close_derivation) + end + handle THM _ => (NONE, []) + +end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Meson/meson_tactic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Meson/meson_tactic.ML Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,29 @@ +(* Title: HOL/Tools/Meson/meson_tactic.ML + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen + +The "meson" proof method for HOL. +*) + +signature MESON_TACTIC = +sig + val meson_general_tac : Proof.context -> thm list -> int -> tactic + val setup: theory -> theory +end; + +structure Meson_Tactic : MESON_TACTIC = +struct + +open Meson_Clausify + +fun meson_general_tac ctxt ths = + let val ctxt = Classical.put_claset HOL_cs ctxt in + Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths) + end + +val setup = + Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) + "MESON resolution proof procedure" + +end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Metis/metis_reconstruct.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,557 @@ +(* Title: HOL/Tools/Metis/metis_reconstruct.ML + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + Copyright Cambridge University 2007 + +Proof reconstruction for Metis. +*) + +signature METIS_RECONSTRUCT = +sig + type mode = Metis_Translate.mode + + val trace : bool Unsynchronized.ref + val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a + val untyped_aconv : term -> term -> bool + val replay_one_inference : + Proof.context -> mode -> (string * term) list + -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list + -> (Metis_Thm.thm * thm) list +end; + +structure Metis_Reconstruct : METIS_RECONSTRUCT = +struct + +open Metis_Translate + +val trace = Unsynchronized.ref false +fun trace_msg msg = if !trace then tracing (msg ()) else () + +datatype term_or_type = SomeTerm of term | SomeType of typ + +fun terms_of [] = [] + | terms_of (SomeTerm t :: tts) = t :: terms_of tts + | terms_of (SomeType _ :: tts) = terms_of tts; + +fun types_of [] = [] + | types_of (SomeTerm (Var ((a,idx), _)) :: tts) = + if String.isPrefix "_" a then + (*Variable generated by Metis, which might have been a type variable.*) + TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts + else types_of tts + | types_of (SomeTerm _ :: tts) = types_of tts + | types_of (SomeType T :: tts) = T :: types_of tts; + +fun apply_list rator nargs rands = + let val trands = terms_of rands + in if length trands = nargs then SomeTerm (list_comb(rator, trands)) + else raise Fail + ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ + " expected " ^ Int.toString nargs ^ + " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) + end; + +fun infer_types ctxt = + Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); + +(*We use 1 rather than 0 because variable references in clauses may otherwise conflict + with variable constraints in the goal...at least, type inference often fails otherwise. + SEE ALSO axiom_inf below.*) +fun mk_var (w, T) = Var ((w, 1), T) + +(*include the default sort, if available*) +fun mk_tfree ctxt w = + let val ww = "'" ^ w + in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; + +(*Remove the "apply" operator from an HO term*) +fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t + | strip_happ args x = (x, args); + +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) + +fun smart_invert_const "fequal" = @{const_name HOL.eq} + | smart_invert_const s = invert_const s + +fun hol_type_from_metis_term _ (Metis_Term.Var v) = + (case strip_prefix_and_unascii tvar_prefix v of + SOME w => make_tvar w + | NONE => make_tvar v) + | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = + (case strip_prefix_and_unascii type_const_prefix x of + SOME tc => Type (smart_invert_const tc, + map (hol_type_from_metis_term ctxt) tys) + | NONE => + case strip_prefix_and_unascii tfree_prefix x of + SOME tf => mk_tfree ctxt tf + | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); + +(*Maps metis terms to isabelle terms*) +fun hol_term_from_metis_PT ctxt fol_tm = + let val thy = ProofContext.theory_of ctxt + val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ + Metis_Term.toString fol_tm) + fun tm_to_tt (Metis_Term.Var v) = + (case strip_prefix_and_unascii tvar_prefix v of + SOME w => SomeType (make_tvar w) + | NONE => + case strip_prefix_and_unascii schematic_var_prefix v of + SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) + | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) ) + (*Var from Metis with a name like _nnn; possibly a type variable*) + | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) + | tm_to_tt (t as Metis_Term.Fn (".",_)) = + let val (rator,rands) = strip_happ [] t + in case rator of + Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) + | _ => case tm_to_tt rator of + SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) + | _ => raise Fail "tm_to_tt: HO application" + end + | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args) + and applic_to_tt ("=",ts) = + SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) + | applic_to_tt (a,ts) = + case strip_prefix_and_unascii const_prefix a of + SOME b => + let + val c = smart_invert_const b + val ntypes = num_type_args thy c + val nterms = length ts - ntypes + val tts = map tm_to_tt ts + val tys = types_of (List.take(tts,ntypes)) + val t = + if String.isPrefix new_skolem_const_prefix c then + Var (new_skolem_var_from_const c, + Type_Infer.paramify_vars (tl tys ---> hd tys)) + else + Const (c, dummyT) + in if length tys = ntypes then + apply_list t nterms (List.drop(tts,ntypes)) + else + raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ + " but gets " ^ Int.toString (length tys) ^ + " type arguments\n" ^ + cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ + " the terms are \n" ^ + cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) + end + | NONE => (*Not a constant. Is it a type constructor?*) + case strip_prefix_and_unascii type_const_prefix a of + SOME b => + SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts))) + | NONE => (*Maybe a TFree. Should then check that ts=[].*) + case strip_prefix_and_unascii tfree_prefix a of + SOME b => SomeType (mk_tfree ctxt b) + | NONE => (*a fixed variable? They are Skolem functions.*) + case strip_prefix_and_unascii fixed_var_prefix a of + SOME b => + let val opr = Free (b, HOLogic.typeT) + in apply_list opr (length ts) (map tm_to_tt ts) end + | NONE => raise Fail ("unexpected metis function: " ^ a) + in + case tm_to_tt fol_tm of + SomeTerm t => t + | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) + end + +(*Maps fully-typed metis terms to isabelle terms*) +fun hol_term_from_metis_FT ctxt fol_tm = + let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ + Metis_Term.toString fol_tm) + fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = + (case strip_prefix_and_unascii schematic_var_prefix v of + SOME w => mk_var(w, dummyT) + | NONE => mk_var(v, dummyT)) + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = + Const (@{const_name HOL.eq}, HOLogic.typeT) + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = + (case strip_prefix_and_unascii const_prefix x of + SOME c => Const (smart_invert_const c, dummyT) + | NONE => (*Not a constant. Is it a fixed variable??*) + case strip_prefix_and_unascii fixed_var_prefix x of + SOME v => Free (v, hol_type_from_metis_term ctxt ty) + | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = + cvt tm1 $ cvt tm2 + | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) + cvt tm1 $ cvt tm2 + | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) + | cvt (Metis_Term.Fn ("=", [tm1,tm2])) = + list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) + | cvt (t as Metis_Term.Fn (x, [])) = + (case strip_prefix_and_unascii const_prefix x of + SOME c => Const (smart_invert_const c, dummyT) + | NONE => (*Not a constant. Is it a fixed variable??*) + case strip_prefix_and_unascii fixed_var_prefix x of + SOME v => Free (v, dummyT) + | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); + hol_term_from_metis_PT ctxt t)) + | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); + hol_term_from_metis_PT ctxt t) + in fol_tm |> cvt end + +fun hol_term_from_metis FT = hol_term_from_metis_FT + | hol_term_from_metis _ = hol_term_from_metis_PT + +fun hol_terms_from_fol ctxt mode old_skolems fol_tms = + let val ts = map (hol_term_from_metis mode ctxt) fol_tms + val _ = trace_msg (fn () => " calling type inference:") + val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts + val ts' = ts |> map (reveal_old_skolem_terms old_skolems) + |> infer_types ctxt + val _ = app (fn t => trace_msg + (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ + " of type " ^ Syntax.string_of_typ ctxt (type_of t))) + ts' + in ts' end; + +(* ------------------------------------------------------------------------- *) +(* FOL step Inference Rules *) +(* ------------------------------------------------------------------------- *) + +(*for debugging only*) +(* +fun print_thpair (fth,th) = + (trace_msg (fn () => "============================================="); + trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); + trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); +*) + +fun lookth thpairs (fth : Metis_Thm.thm) = + the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) + handle Option.Option => + raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) + +fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); + +(* INFERENCE RULE: AXIOM *) + +fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); + (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) + +(* INFERENCE RULE: ASSUME *) + +val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} + +fun inst_excluded_middle thy i_atm = + let val th = EXCLUDED_MIDDLE + val [vx] = Term.add_vars (prop_of th) [] + val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] + in cterm_instantiate substs th end; + +fun assume_inf ctxt mode old_skolems atm = + inst_excluded_middle + (ProofContext.theory_of ctxt) + (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm)) + +(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying + to reconstruct them admits new possibilities of errors, e.g. concerning + sorts. Instead we try to arrange that new TVars are distinct and that types + can be inferred from terms. *) + +fun inst_inf ctxt mode old_skolems thpairs fsubst th = + let val thy = ProofContext.theory_of ctxt + val i_th = lookth thpairs th + val i_th_vars = Term.add_vars (prop_of i_th) [] + fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) + fun subst_translation (x,y) = + let val v = find_var x + (* We call "reveal_old_skolem_terms" and "infer_types" below. *) + val t = hol_term_from_metis mode ctxt y + in SOME (cterm_of thy (Var v), t) end + handle Option.Option => + (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); + NONE) + | TYPE _ => + (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); + NONE) + fun remove_typeinst (a, t) = + case strip_prefix_and_unascii schematic_var_prefix a of + SOME b => SOME (b, t) + | NONE => case strip_prefix_and_unascii tvar_prefix a of + SOME _ => NONE (*type instantiations are forbidden!*) + | NONE => SOME (a,t) (*internal Metis var?*) + val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) + val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) + val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) + val tms = rawtms |> map (reveal_old_skolem_terms old_skolems) + |> infer_types ctxt + val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) + val substs' = ListPair.zip (vars, map ctm_of tms) + val _ = trace_msg (fn () => + cat_lines ("subst_translations:" :: + (substs' |> map (fn (x, y) => + Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ + Syntax.string_of_term ctxt (term_of y))))); + in cterm_instantiate substs' i_th end + handle THM (msg, _, _) => + error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) + +(* INFERENCE RULE: RESOLVE *) + +(* Like RSN, but we rename apart only the type variables. Vars here typically + have an index of 1, and the use of RSN would increase this typically to 3. + Instantiations of those Vars could then fail. See comment on "mk_var". *) +fun resolve_inc_tyvars thy tha i thb = + let + val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha + fun aux tha thb = + case Thm.bicompose false (false, tha, nprems_of tha) i thb + |> Seq.list_of |> distinct Thm.eq_thm of + [th] => th + | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, + [tha, thb]) + in + aux tha thb + handle TERM z => + (* The unifier, which is invoked from "Thm.bicompose", will sometimes + refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a + "TERM" exception (with "add_ffpair" as first argument). We then + perform unification of the types of variables by hand and try + again. We could do this the first time around but this error + occurs seldom and we don't want to break existing proofs in subtle + ways or slow them down needlessly. *) + case [] |> fold (Term.add_vars o prop_of) [tha, thb] + |> AList.group (op =) + |> maps (fn ((s, _), T :: Ts) => + map (fn T' => (Free (s, T), Free (s, T'))) Ts) + |> rpair (Envir.empty ~1) + |-> fold (Pattern.unify thy) + |> Envir.type_env |> Vartab.dest + |> map (fn (x, (S, T)) => + pairself (ctyp_of thy) (TVar (x, S), T)) of + [] => raise TERM z + | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) + end + +fun mk_not (Const (@{const_name Not}, _) $ b) = b + | mk_not b = HOLogic.mk_not b + +(* Match untyped terms. *) +fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) + | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) + | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = + (a = b) (* The index is ignored, for some reason. *) + | untyped_aconv (Bound i) (Bound j) = (i = j) + | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u + | untyped_aconv (t1 $ t2) (u1 $ u2) = + untyped_aconv t1 u1 andalso untyped_aconv t2 u2 + | untyped_aconv _ _ = false + +(* Finding the relative location of an untyped term within a list of terms *) +fun literal_index lit = + let + val lit = Envir.eta_contract lit + fun get _ [] = raise Empty + | get n (x :: xs) = + if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then + n + else + get (n+1) xs + in get 1 end + +(* Permute a rule's premises to move the i-th premise to the last position. *) +fun make_last i th = + let val n = nprems_of th + in if 1 <= i andalso i <= n + then Thm.permute_prems (i-1) 1 th + else raise THM("select_literal", i, [th]) + end; + +(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing + double-negations. *) +val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection] + +(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) +val select_literal = negate_head oo make_last + +fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 = + let + val thy = ProofContext.theory_of ctxt + val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 + val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) + val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) + in + (* Trivial cases where one operand is type info *) + if Thm.eq_thm (TrueI, i_th1) then + i_th2 + else if Thm.eq_thm (TrueI, i_th2) then + i_th1 + else + let + val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems) + (Metis_Term.Fn atm) + val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) + val prems_th1 = prems_of i_th1 + val prems_th2 = prems_of i_th2 + val index_th1 = literal_index (mk_not i_atm) prems_th1 + handle Empty => raise Fail "Failed to find literal in th1" + val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) + val index_th2 = literal_index i_atm prems_th2 + handle Empty => raise Fail "Failed to find literal in th2" + val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) + in + resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 + end + end; + +(* INFERENCE RULE: REFL *) + +val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} + +val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); +val refl_idx = 1 + Thm.maxidx_of REFL_THM; + +fun refl_inf ctxt mode old_skolems t = + let val thy = ProofContext.theory_of ctxt + val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t + val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) + val c_t = cterm_incr_types thy refl_idx i_t + in cterm_instantiate [(refl_x, c_t)] REFL_THM end; + +(* INFERENCE RULE: EQUALITY *) + +val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} +val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} + +val metis_eq = Metis_Term.Fn ("=", []); + +fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) + | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) + | get_ty_arg_size _ _ = 0; + +fun equality_inf ctxt mode old_skolems (pos, atm) fp fr = + let val thy = ProofContext.theory_of ctxt + val m_tm = Metis_Term.Fn atm + val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr] + val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) + fun replace_item_list lx 0 (_::ls) = lx::ls + | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls + fun path_finder_FO tm [] = (tm, Bound 0) + | path_finder_FO tm (p::ps) = + let val (tm1,args) = strip_comb tm + val adjustment = get_ty_arg_size thy tm1 + val p' = if adjustment > p then p else p-adjustment + val tm_p = List.nth(args,p') + handle Subscript => + error ("Cannot replay Metis proof in Isabelle:\n" ^ + "equality_inf: " ^ Int.toString p ^ " adj " ^ + Int.toString adjustment ^ " term " ^ + Syntax.string_of_term ctxt tm) + val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ + " " ^ Syntax.string_of_term ctxt tm_p) + val (r,t) = path_finder_FO tm_p ps + in + (r, list_comb (tm1, replace_item_list t p' args)) + end + fun path_finder_HO tm [] = (tm, Bound 0) + | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) + | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) + | path_finder_HO tm ps = + raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ + "equality_inf, path_finder_HO: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm) + fun path_finder_FT tm [] _ = (tm, Bound 0) + | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = + path_finder_FT tm ps t1 + | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = + (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) + | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = + (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) + | path_finder_FT tm ps t = + raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ + "equality_inf, path_finder_FT: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm ^ + " fol-term: " ^ Metis_Term.toString t) + fun path_finder FO tm ps _ = path_finder_FO tm ps + | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = + (*equality: not curried, as other predicates are*) + if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) + else path_finder_HO tm (p::ps) (*1 selects second operand*) + | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = + path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) + | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) + (Metis_Term.Fn ("=", [t1,t2])) = + (*equality: not curried, as other predicates are*) + if p=0 then path_finder_FT tm (0::1::ps) + (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) + (*select first operand*) + else path_finder_FT tm (p::ps) + (Metis_Term.Fn (".", [metis_eq,t2])) + (*1 selects second operand*) + | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 + (*if not equality, ignore head to skip the hBOOL predicate*) + | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) + fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = + let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm + in (tm, nt $ tm_rslt) end + | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm + val (tm_subst, body) = path_finder_lit i_atm fp + val tm_abs = Abs ("x", type_of tm_subst, body) + val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) + val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) + val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) + val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) + val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) + val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') + val eq_terms = map (pairself (cterm_of thy)) + (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) + in cterm_instantiate eq_terms subst' end; + +val factor = Seq.hd o distinct_subgoals_tac; + +fun step ctxt mode old_skolems thpairs p = + case p of + (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) + | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm + | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => + factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1) + | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => + factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2) + | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm + | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => + equality_inf ctxt mode old_skolems f_lit f_p f_r + +fun flexflex_first_order th = + case Thm.tpairs_of th of + [] => th + | pairs => + let val thy = theory_of_thm th + val (_, tenv) = + fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) + val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) + val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th + in th' end + handle THM _ => th; + +fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) +fun is_isabelle_literal_genuine t = + case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true + +fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 + +fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs = + let + val _ = trace_msg (fn () => "=============================================") + val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) + val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) + val th = step ctxt mode old_skolems thpairs (fol_th, inf) + |> flexflex_first_order + val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) + val _ = trace_msg (fn () => "=============================================") + val num_metis_lits = + fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList + |> count is_metis_literal_genuine + val num_isabelle_lits = + th |> prems_of |> count is_isabelle_literal_genuine + val _ = if num_metis_lits = num_isabelle_lits then () + else error "Cannot replay Metis proof in Isabelle: Out of sync." + in (fol_th, th) :: thpairs end + +end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Metis/metis_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,433 @@ +(* Title: HOL/Tools/Metis/metis_tactics.ML + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + Copyright Cambridge University 2007 + +HOL setup for the Metis prover. +*) + +signature METIS_TACTICS = +sig + val trace : bool Unsynchronized.ref + val type_lits : bool Config.T + val new_skolemizer : bool Config.T + val metis_tac : Proof.context -> thm list -> int -> tactic + val metisF_tac : Proof.context -> thm list -> int -> tactic + val metisFT_tac : Proof.context -> thm list -> int -> tactic + val setup : theory -> theory +end + +structure Metis_Tactics : METIS_TACTICS = +struct + +open Metis_Translate +open Metis_Reconstruct + +structure Int_Pair_Graph = + Graph(type key = int * int val ord = prod_ord int_ord int_ord) + +fun trace_msg msg = if !trace then tracing (msg ()) else () + +val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true) +val (new_skolemizer, new_skolemizer_setup) = + Attrib.config_bool "metis_new_skolemizer" (K false) + +fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); + +fun have_common_thm ths1 ths2 = + exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) + +(*Determining which axiom clauses are actually used*) +fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) + | used_axioms _ _ = NONE; + +val clause_params = + {ordering = Metis_KnuthBendixOrder.default, + orderLiterals = Metis_Clause.UnsignedLiteralOrder, + orderTerms = true} +val active_params = + {clause = clause_params, + prefactor = #prefactor Metis_Active.default, + postfactor = #postfactor Metis_Active.default} +val waiting_params = + {symbolsWeight = 1.0, + variablesWeight = 0.0, + literalsWeight = 0.0, + models = []} +val resolution_params = {active = active_params, waiting = waiting_params} + +(* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *) + +fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy)) + +(* In principle, it should be sufficient to apply "assume_tac" to unify the + conclusion with one of the premises. However, in practice, this is unreliable + because of the mildly higher-order nature of the unification problems. + Typical constraints are of the form + "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x", + where the nonvariables are goal parameters. *) +(* FIXME: ### try Pattern.match instead *) +fun unify_first_prem_with_concl thy i th = + let + val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract + val prem = goal |> Logic.strip_assums_hyp |> hd + val concl = goal |> Logic.strip_assums_concl + fun pair_untyped_aconv (t1, t2) (u1, u2) = + untyped_aconv t1 u1 andalso untyped_aconv t2 u2 + fun add_terms tp inst = + if exists (pair_untyped_aconv tp) inst then inst + else tp :: map (apsnd (subst_atomic [tp])) inst + fun is_flex t = + case strip_comb t of + (Var _, args) => forall is_Bound args + | _ => false + fun unify_flex flex rigid = + case strip_comb flex of + (Var (z as (_, T)), args) => + add_terms (Var z, + fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid) + | _ => raise TERM ("unify_flex: expected flex", [flex]) + fun unify_potential_flex comb atom = + if is_flex comb then unify_flex comb atom + else if is_Var atom then add_terms (atom, comb) + else raise TERM ("unify_terms", [comb, atom]) + fun unify_terms (t, u) = + case (t, u) of + (t1 $ t2, u1 $ u2) => + if is_flex t then unify_flex t u + else if is_flex u then unify_flex u t + else fold unify_terms [(t1, u1), (t2, u2)] + | (_ $ _, _) => unify_potential_flex t u + | (_, _ $ _) => unify_potential_flex u t + | (Var _, _) => add_terms (t, u) + | (_, Var _) => add_terms (u, t) + | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u]) + in th |> term_instantiate thy (unify_terms (prem, concl) []) end + +fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no) +fun shuffle_ord p = + rev_order (prod_ord int_ord int_ord (pairself shuffle_key p)) + +val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} + +fun copy_prems_tac [] ns i = + if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i + | copy_prems_tac (1 :: ms) ns i = + rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i + | copy_prems_tac (m :: ms) ns i = + etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i + +fun instantiate_forall_tac thy params t i = + let + fun repair (t as (Var ((s, _), _))) = + (case find_index (fn ((s', _), _) => s' = s) params of + ~1 => t + | j => Bound j) + | repair (t $ u) = repair t $ repair u + | repair t = t + val t' = t |> repair |> fold (curry absdummy) (map snd params) + fun do_instantiate th = + let val var = Term.add_vars (prop_of th) [] |> the_single in + th |> term_instantiate thy [(Var var, t')] + end + in + etac @{thm allE} i + THEN rotate_tac ~1 i + THEN PRIMITIVE do_instantiate + end + +fun release_clusters_tac _ _ _ _ [] = K all_tac + | release_clusters_tac thy ax_counts substs params + ((ax_no, cluster_no) :: clusters) = + let + fun in_right_cluster s = + (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst) + = cluster_no + val cluster_substs = + substs + |> map_filter (fn (ax_no', (_, (_, tsubst))) => + if ax_no' = ax_no then + tsubst |> filter (in_right_cluster + o fst o fst o dest_Var o fst) + |> map snd |> SOME + else + NONE) + val n = length cluster_substs + fun do_cluster_subst cluster_subst = + map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1] + val params' = params (* FIXME ### existentials! *) + val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs + in + rotate_tac first_prem + THEN' (EVERY' (maps do_cluster_subst cluster_substs)) + THEN' rotate_tac (~ first_prem - length cluster_substs) + THEN' release_clusters_tac thy ax_counts substs params' clusters + end + +val cluster_ord = + prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord + +val tysubst_ord = + list_ord (prod_ord Term_Ord.fast_indexname_ord + (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) + +structure Int_Tysubst_Table = + Table(type key = int * (indexname * (sort * typ)) list + val ord = prod_ord int_ord tysubst_ord) + +(* Attempts to derive the theorem "False" from a theorem of the form + "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the + specified axioms. The axioms have leading "All" and "Ex" quantifiers, which + must be eliminated first. *) +fun discharge_skolem_premises ctxt axioms prems_imp_false = + if prop_of prems_imp_false aconv @{prop False} then + prems_imp_false + else + let + val thy = ProofContext.theory_of ctxt + (* distinguish variables with same name but different types *) + val prems_imp_false' = + prems_imp_false |> try (forall_intr_vars #> gen_all) + |> the_default prems_imp_false + val prems_imp_false = + if prop_of prems_imp_false aconv prop_of prems_imp_false' then + prems_imp_false + else + prems_imp_false' + fun match_term p = + let + val (tyenv, tenv) = + Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) + val tsubst = + tenv |> Vartab.dest + |> sort (cluster_ord + o pairself (Meson_Clausify.cluster_of_zapped_var_name + o fst o fst)) + |> map (Meson.term_pair_of + #> pairself (Envir.subst_term_types tyenv)) + val tysubst = tyenv |> Vartab.dest + in (tysubst, tsubst) end + fun subst_info_for_prem subgoal_no prem = + case prem of + _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => + let val ax_no = HOLogic.dest_nat num in + (ax_no, (subgoal_no, + match_term (nth axioms ax_no |> the |> snd, t))) + end + | _ => raise TERM ("discharge_skolem_premises: Malformed premise", + [prem]) + fun cluster_of_var_name skolem s = + let + val ((ax_no, (cluster_no, _)), skolem') = + Meson_Clausify.cluster_of_zapped_var_name s + in + if skolem' = skolem andalso cluster_no > 0 then + SOME (ax_no, cluster_no) + else + NONE + end + fun clusters_in_term skolem t = + Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) + fun deps_for_term_subst (var, t) = + case clusters_in_term false var of + [] => NONE + | [(ax_no, cluster_no)] => + SOME ((ax_no, cluster_no), + clusters_in_term true t + |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) + | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) + val prems = Logic.strip_imp_prems (prop_of prems_imp_false) + val substs = prems |> map2 subst_info_for_prem (1 upto length prems) + |> sort (int_ord o pairself fst) + val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs + val clusters = maps (op ::) depss + val ordered_clusters = + Int_Pair_Graph.empty + |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) + |> fold Int_Pair_Graph.add_deps_acyclic depss + |> Int_Pair_Graph.topological_order + handle Int_Pair_Graph.CYCLES _ => + error "Cannot replay Metis proof in Isabelle without axiom of \ + \choice." + val params0 = + [] |> fold (Term.add_vars o snd) (map_filter I axioms) + |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst)) + |> filter (fn (((_, (cluster_no, _)), skolem), _) => + cluster_no = 0 andalso skolem) + |> sort shuffle_ord |> map snd + val ax_counts = + Int_Tysubst_Table.empty + |> fold (fn (ax_no, (_, (tysubst, _))) => + Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) + (Integer.add 1)) substs + |> Int_Tysubst_Table.dest +(* for debugging: + fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = + "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ + "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ + commas (map ((fn (s, t) => s ^ " |-> " ^ t) + o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" + val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ + cat_lines (map string_for_subst_info substs)) + val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0) + val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) + val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) +*) + fun rotation_for_subgoal i = + find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs + in + Goal.prove ctxt [] [] @{prop False} + (K (cut_rules_tac + (map (fst o the o nth axioms o fst o fst) ax_counts) 1 + THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) + THEN copy_prems_tac (map snd ax_counts) [] 1 + THEN release_clusters_tac thy ax_counts substs params0 + ordered_clusters 1 + THEN match_tac [prems_imp_false] 1 + THEN ALLGOALS (fn i => + rtac @{thm Meson.skolem_COMBK_I} i + THEN rotate_tac (rotation_for_subgoal i) i + THEN PRIMITIVE (unify_first_prem_with_concl thy i) + THEN assume_tac i))) + end + +(* Main function to start Metis proof and reconstruction *) +fun FOL_SOLVE mode ctxt cls ths0 = + let val thy = ProofContext.theory_of ctxt + val type_lits = Config.get ctxt type_lits + val new_skolemizer = + Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) + val th_cls_pairs = + map2 (fn j => fn th => + (Thm.get_name_hint th, + Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) + (0 upto length ths0 - 1) ths0 + val thss = map (snd o snd) th_cls_pairs + val dischargers = map (fst o snd) th_cls_pairs + val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls + val _ = trace_msg (fn () => "THEOREM CLAUSES") + val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss + val (mode, {axioms, tfrees, old_skolems}) = + build_logic_map mode ctxt type_lits cls thss + val _ = if null tfrees then () + else (trace_msg (fn () => "TFREE CLAUSES"); + app (fn TyLitFree ((s, _), (s', _)) => + trace_msg (fn () => s ^ "(" ^ s' ^ ")")) 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 + val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) + val _ = trace_msg (fn () => "START METIS PROVE PROCESS") + in + case filter (is_false o prop_of) cls of + false_th::_ => [false_th RS @{thm FalseE}] + | [] => + case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} + |> Metis_Resolution.loop of + Metis_Resolution.Contradiction mth => + let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ + Metis_Thm.toString mth) + val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt + (*add constraints arising from converting goal to clause form*) + val proof = Metis_Proof.proof mth + val result = + fold (replay_one_inference ctxt' mode old_skolems) proof axioms + and used = map_filter (used_axioms axioms) proof + val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") + val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used + val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => + if have_common_thm used cls then NONE else SOME name) + in + if not (null cls) andalso not (have_common_thm used cls) then + warning "Metis: The assumptions are inconsistent." + else + (); + if not (null unused) then + warning ("Metis: Unused theorems: " ^ commas_quote unused + ^ ".") + else + (); + case result of + (_,ith)::_ => + (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + [discharge_skolem_premises ctxt dischargers ith]) + | _ => (trace_msg (fn () => "Metis: No result"); []) + end + | Metis_Resolution.Satisfiable _ => + (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); + []) + end; + +(* Extensionalize "th", because that makes sense and that's what Sledgehammer + does, but also keep an unextensionalized version of "th" for backward + compatibility. *) +fun also_extensionalize_theorem th = + let val th' = Meson_Clausify.extensionalize_theorem th in + if Thm.eq_thm (th, th') then [th] + else th :: Meson.make_clauses_unsorted [th'] + end + +val neg_clausify = + single + #> Meson.make_clauses_unsorted + #> maps also_extensionalize_theorem + #> map Meson_Clausify.introduce_combinators_in_theorem + #> Meson.finish_cnf + +fun preskolem_tac ctxt st0 = + (if exists (Meson.has_too_many_clauses ctxt) + (Logic.prems_of_goal (prop_of st0) 1) then + cnf.cnfx_rewrite_tac ctxt 1 + else + all_tac) st0 + +val type_has_top_sort = + exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) + +fun generic_metis_tac mode ctxt ths i st0 = + let + val _ = trace_msg (fn () => + "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) + in + if exists_type type_has_top_sort (prop_of st0) then + (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) + else + Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) + (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) + ctxt i st0 + end + +val metis_tac = generic_metis_tac HO +val metisF_tac = generic_metis_tac FO +val metisFT_tac = generic_metis_tac FT + +(* Whenever "X" has schematic type variables, we treat "using X by metis" as + "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. + We don't do it for nonschematic facts "X" because this breaks a few proofs + (in the rare and subtle case where a proof relied on extensionality not being + applied) and brings few benefits. *) +val has_tvar = + exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of +fun method name mode = + Method.setup name (Attrib.thms >> (fn ths => fn ctxt => + METHOD (fn facts => + let + val (schem_facts, nonschem_facts) = + List.partition has_tvar facts + in + HEADGOAL (Method.insert_tac nonschem_facts THEN' + CHANGED_PROP + o generic_metis_tac mode ctxt (schem_facts @ ths)) + end))) + +val setup = + type_lits_setup + #> new_skolemizer_setup + #> method @{binding metis} HO "Metis for FOL/HOL problems" + #> method @{binding metisF} FO "Metis for FOL problems" + #> method @{binding metisFT} FT + "Metis for FOL/HOL problems with fully-typed translation" + +end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Metis/metis_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Oct 06 17:44:21 2010 +0200 @@ -0,0 +1,771 @@ +(* Title: HOL/Tools/Metis/metis_translate.ML + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +Translation of HOL to FOL for Metis. +*) + +signature METIS_TRANSLATE = +sig + type name = string * string + datatype type_literal = + TyLitVar of name * name | + TyLitFree of name * name + datatype arLit = + TConsLit of name * name * name list | + TVarLit of name * name + datatype arity_clause = + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} + datatype class_rel_clause = + ClassRelClause of {name: string, subclass: name, superclass: name} + datatype combtyp = + CombTVar of name | + CombTFree of name | + CombType of name * combtyp list + datatype combterm = + CombConst of name * combtyp * combtyp list (* Const and Free *) | + CombVar of name * combtyp | + CombApp of combterm * combterm + datatype fol_literal = FOLLiteral of bool * combterm + + datatype mode = FO | HO | FT + type logic_map = + {axioms: (Metis_Thm.thm * thm) list, + tfrees: type_literal list, + old_skolems: (string * term) list} + + val type_wrapper_name : string + val bound_var_prefix : string + val schematic_var_prefix: string + val fixed_var_prefix: string + val tvar_prefix: string + val tfree_prefix: string + val const_prefix: string + val type_const_prefix: string + val class_prefix: string + val new_skolem_const_prefix : string + val invert_const: string -> string + val ascii_of: string -> string + val unascii_of: string -> string + val strip_prefix_and_unascii: string -> string -> string option + val make_bound_var : string -> string + val make_schematic_var : string * int -> string + val make_fixed_var : string -> string + val make_schematic_type_var : string * int -> string + val make_fixed_type_var : string -> string + val make_fixed_const : string -> string + val make_fixed_type_const : string -> string + val make_type_class : string -> string + val num_type_args: theory -> string -> int + val new_skolem_var_from_const: string -> indexname + val type_literals_for_types : typ list -> type_literal list + val make_class_rel_clauses : + theory -> class list -> class list -> class_rel_clause list + val make_arity_clauses : + theory -> string list -> class list -> class list * arity_clause list + val combtyp_of : combterm -> combtyp + val strip_combterm_comb : combterm -> combterm * combterm list + val combterm_from_term : + theory -> int -> (string * typ) list -> term -> combterm * typ list + val reveal_old_skolem_terms : (string * term) list -> term -> term + val tfree_classes_of_terms : term list -> string list + val tvar_classes_of_terms : term list -> string list + val type_consts_of_terms : theory -> term list -> string list + val string_of_mode : mode -> string + val build_logic_map : + mode -> Proof.context -> bool -> thm list -> thm list list + -> mode * logic_map +end + +structure Metis_Translate : METIS_TRANSLATE = +struct + +val type_wrapper_name = "ti" + +val bound_var_prefix = "B_" +val schematic_var_prefix = "V_" +val fixed_var_prefix = "v_" + +val tvar_prefix = "T_"; +val tfree_prefix = "t_"; + +val const_prefix = "c_"; +val type_const_prefix = "tc_"; +val class_prefix = "class_"; + +val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" +val old_skolem_const_prefix = skolem_const_prefix ^ "o" +val new_skolem_const_prefix = skolem_const_prefix ^ "n" + +fun union_all xss = fold (union (op =)) xss [] + +(* Readable names for the more common symbolic functions. Do not mess with the + last nine entries of the table unless you know what you are doing. *) +val const_trans_table = + Symtab.make [(@{type_name Product_Type.prod}, "prod"), + (@{type_name Sum_Type.sum}, "sum"), + (@{const_name HOL.eq}, "equal"), + (@{const_name HOL.conj}, "and"), + (@{const_name HOL.disj}, "or"), + (@{const_name HOL.implies}, "implies"), + (@{const_name Set.member}, "member"), + (@{const_name Metis.fequal}, "fequal"), + (@{const_name Meson.COMBI}, "COMBI"), + (@{const_name Meson.COMBK}, "COMBK"), + (@{const_name Meson.COMBB}, "COMBB"), + (@{const_name Meson.COMBC}, "COMBC"), + (@{const_name Meson.COMBS}, "COMBS"), + (@{const_name True}, "True"), + (@{const_name False}, "False"), + (@{const_name If}, "If")] + +(* Invert the table of translations between Isabelle and ATPs. *) +val const_trans_table_inv = + Symtab.update ("fequal", @{const_name HOL.eq}) + (Symtab.make (map swap (Symtab.dest const_trans_table))) + +val invert_const = perhaps (Symtab.lookup const_trans_table_inv) + +(*Escaping of special characters. + Alphanumeric characters are left unchanged. + The character _ goes to __ + Characters in the range ASCII space to / go to _A to _P, respectively. + Other characters go to _nnn where nnn is the decimal ASCII code.*) +val A_minus_space = Char.ord #"A" - Char.ord #" "; + +fun stringN_of_int 0 _ = "" + | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); + +fun ascii_of_c c = + if Char.isAlphaNum c then String.str c + else if c = #"_" then "__" + else if #" " <= c andalso c <= #"/" + then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) + else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) + +val ascii_of = String.translate ascii_of_c; + +(** Remove ASCII armouring from names in proof files **) + +(*We don't raise error exceptions because this code can run inside the watcher. + Also, the errors are "impossible" (hah!)*) +fun unascii_aux rcs [] = String.implode(rev rcs) + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) + (*Three types of _ escapes: __, _A to _P, _nnn*) + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs + | unascii_aux rcs (#"_" :: c :: cs) = + if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs + else + let val digits = List.take (c::cs, 3) handle Subscript => [] + in + case Int.fromString (String.implode digits) of + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) + end + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs +val unascii_of = unascii_aux [] o String.explode + +(* If string s has the prefix s1, return the result of deleting it, + un-ASCII'd. *) +fun strip_prefix_and_unascii s1 s = + if String.isPrefix s1 s then + SOME (unascii_of (String.extract (s, size s1, NONE))) + else + NONE + +(*Remove the initial ' character from a type variable, if it is present*) +fun trim_type_var s = + if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) + else error ("trim_type: Malformed type variable encountered: " ^ s); + +fun ascii_of_indexname (v,0) = ascii_of v + | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; + +fun make_bound_var x = bound_var_prefix ^ ascii_of x +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x + +fun make_schematic_type_var (x,i) = + tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); + +fun lookup_const c = + case Symtab.lookup const_trans_table c of + SOME c' => c' + | NONE => ascii_of c + +(* HOL.eq MUST BE "equal" because it's built into ATPs. *) +fun make_fixed_const @{const_name HOL.eq} = "equal" + | make_fixed_const c = const_prefix ^ lookup_const c + +fun make_fixed_type_const c = type_const_prefix ^ lookup_const c + +fun make_type_class clas = class_prefix ^ ascii_of clas; + +(* The number of type arguments of a constant, zero if it's monomorphic. For + (instances of) Skolem pseudoconstants, this information is encoded in the + constant name. *) +fun num_type_args thy s = + if String.isPrefix skolem_const_prefix s then + s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the + else + (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length + +fun new_skolem_var_from_const s = + let + val ss = s |> space_explode Long_Name.separator + val n = length ss + in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end + + +(**** Definitions and functions for FOL clauses for TPTP format output ****) + +type name = string * string + +(**** Isabelle FOL clauses ****) + +(* The first component is the type class; the second is a TVar or TFree. *) +datatype type_literal = + TyLitVar of name * name | + TyLitFree of name * name + +(*Make literals for sorted type variables*) +fun sorts_on_typs_aux (_, []) = [] + | sorts_on_typs_aux ((x,i), s::ss) = + let val sorts = sorts_on_typs_aux ((x,i), ss) + in + if s = "HOL.type" then 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); + +(*Given a list of sorted type variables, return a list of type literals.*) +fun type_literals_for_types Ts = + fold (union (op =)) (map sorts_on_typs Ts) [] + +(** make axiom and conjecture clauses. **) + +(**** Isabelle arities ****) + +datatype arLit = + TConsLit of name * name * name list | + TVarLit of name * name + +datatype arity_clause = + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} + + +fun gen_TVars 0 = [] + | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); + +fun pack_sort(_,[]) = [] + | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) + | pack_sort(tvar, cls::srt) = + (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) + +(*Arity of type constructor tcon :: (arg1,...,argN)res*) +fun make_axiom_arity_clause (tcons, name, (cls,args)) = + let + val tvars = gen_TVars (length args) + val tvars_srts = ListPair.zip (tvars, args) + in + ArityClause {name = name, + conclLit = TConsLit (`make_type_class cls, + `make_fixed_type_const tcons, + tvars ~~ tvars), + premLits = map TVarLit (union_all (map pack_sort tvars_srts))} + end + + +(**** Isabelle class relations ****) + +datatype class_rel_clause = + ClassRelClause of {name: string, subclass: name, superclass: name} + +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) +fun class_pairs _ [] _ = [] + | class_pairs thy subs supers = + let + val class_less = Sorts.class_less (Sign.classes_of thy) + fun add_super sub super = class_less (sub, super) ? cons (sub, super) + fun add_supers sub = fold (add_super sub) supers + in fold add_supers subs [] end + +fun make_class_rel_clause (sub,super) = + ClassRelClause {name = sub ^ "_" ^ super, + subclass = `make_type_class sub, + superclass = `make_type_class super} + +fun make_class_rel_clauses thy subs supers = + map make_class_rel_clause (class_pairs thy subs supers); + + +(** Isabelle arities **) + +fun arity_clause _ _ (_, []) = [] + | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) + arity_clause seen n (tcons,ars) + | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = + if member (op =) seen class then (*multiple arities for the same tycon, class pair*) + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: + arity_clause seen (n+1) (tcons,ars) + else + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: + arity_clause (class::seen) n (tcons,ars) + +fun multi_arity_clause [] = [] + | multi_arity_clause ((tcons, ars) :: tc_arlists) = + arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists + +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy + provided its arguments have the corresponding sorts.*) +fun type_class_pairs thy tycons classes = + let val alg = Sign.classes_of thy + fun domain_sorts tycon = Sorts.mg_domain alg tycon o single + fun add_class tycon class = + cons (class, domain_sorts tycon class) + handle Sorts.CLASS_ERROR _ => I + fun try_classes tycon = (tycon, fold (add_class tycon) classes []) + in map try_classes tycons end; + +(*Proving one (tycon, class) membership may require proving others, so iterate.*) +fun iter_type_class_pairs _ _ [] = ([], []) + | iter_type_class_pairs thy tycons classes = + let val cpairs = type_class_pairs thy tycons classes + val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) + |> subtract (op =) classes |> subtract (op =) HOLogic.typeS + val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses + in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; + +fun make_arity_clauses thy tycons classes = + let val (classes', cpairs) = iter_type_class_pairs thy tycons classes + in (classes', multi_arity_clause cpairs) end; + +datatype combtyp = + CombTVar of name | + CombTFree of name | + CombType of name * combtyp list + +datatype combterm = + CombConst of name * combtyp * combtyp list (* Const and Free *) | + CombVar of name * combtyp | + CombApp of combterm * combterm + +datatype fol_literal = FOLLiteral of bool * combterm + +(*********************************************************************) +(* convert a clause with type Term.term to a clause with type clause *) +(*********************************************************************) + +(*Result of a function type; no need to check that the argument type matches.*) +fun result_type (CombType (_, [_, tp2])) = tp2 + | result_type _ = raise Fail "non-function type" + +fun combtyp_of (CombConst (_, tp, _)) = tp + | combtyp_of (CombVar (_, tp)) = tp + | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) + +(*gets the head of a combinator application, along with the list of arguments*) +fun strip_combterm_comb u = + let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) + | stripc x = x + in stripc(u,[]) end + +fun combtype_of (Type (a, Ts)) = + let val (folTypes, ts) = combtypes_of Ts in + (CombType (`make_fixed_type_const a, folTypes), ts) + end + | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) + | combtype_of (tp as TVar (x, _)) = + (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp]) +and combtypes_of Ts = + let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in + (folTyps, union_all ts) + end + +(* same as above, but no gathering of sort information *) +fun simple_combtype_of (Type (a, Ts)) = + CombType (`make_fixed_type_const a, map simple_combtype_of Ts) + | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) + | simple_combtype_of (TVar (x, _)) = + CombTVar (make_schematic_type_var x, string_of_indexname x) + +fun new_skolem_const_name th_no s num_T_args = + [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args] + |> space_implode Long_Name.separator + +(* Converts a term (with combinators) into a combterm. Also accummulates sort + infomation. *) +fun combterm_from_term thy th_no bs (P $ Q) = + let val (P', tsP) = combterm_from_term thy th_no bs P + val (Q', tsQ) = combterm_from_term thy th_no bs Q + in (CombApp (P', Q'), union (op =) tsP tsQ) end + | combterm_from_term thy _ _ (Const (c, T)) = + let + val (tp, ts) = combtype_of T + val tvar_list = + (if String.isPrefix old_skolem_const_prefix c then + [] |> Term.add_tvarsT T |> map TVar + else + (c, T) |> Sign.const_typargs thy) + |> map simple_combtype_of + val c' = CombConst (`make_fixed_const c, tp, tvar_list) + in (c',ts) end + | combterm_from_term _ _ _ (Free (v, T)) = + let val (tp, ts) = combtype_of T + val v' = CombConst (`make_fixed_var v, tp, []) + in (v',ts) end + | combterm_from_term _ th_no _ (Var (v as (s, _), T)) = + let + val (tp, ts) = combtype_of T + val v' = + if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then + let + val tys = T |> strip_type |> swap |> op :: + val s' = new_skolem_const_name th_no s (length tys) + in + CombConst (`make_fixed_const s', tp, map simple_combtype_of tys) + end + else + CombVar ((make_schematic_var v, string_of_indexname v), tp) + in (v', ts) end + | combterm_from_term _ _ bs (Bound j) = + let + val (s, T) = nth bs j + val (tp, ts) = combtype_of T + val v' = CombConst (`make_bound_var s, tp, []) + in (v', ts) end + | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs" + +fun predicate_of thy th_no ((@{const Not} $ P), pos) = + predicate_of thy th_no (P, not pos) + | predicate_of thy th_no (t, pos) = + (combterm_from_term thy th_no [] (Envir.eta_contract t), pos) + +fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) = + literals_of_term1 args thy th_no P + | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) = + literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q + | literals_of_term1 (lits, ts) thy th_no P = + let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in + (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') + end +val literals_of_term = literals_of_term1 ([], []) + +fun old_skolem_const_name i j num_T_args = + old_skolem_const_prefix ^ Long_Name.separator ^ + (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) + +fun conceal_old_skolem_terms i old_skolems t = + if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then + let + fun aux old_skolems + (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) = + let + val (old_skolems, s) = + if i = ~1 then + (old_skolems, @{const_name undefined}) + else case AList.find (op aconv) old_skolems t of + s :: _ => (old_skolems, s) + | [] => + let + val s = old_skolem_const_name i (length old_skolems) + (length (Term.add_tvarsT T [])) + in ((s, t) :: old_skolems, s) end + in (old_skolems, Const (s, T)) end + | aux old_skolems (t1 $ t2) = + let + val (old_skolems, t1) = aux old_skolems t1 + val (old_skolems, t2) = aux old_skolems t2 + in (old_skolems, t1 $ t2) end + | aux old_skolems (Abs (s, T, t')) = + let val (old_skolems, t') = aux old_skolems t' in + (old_skolems, Abs (s, T, t')) + end + | aux old_skolems t = (old_skolems, t) + in aux old_skolems t end + else + (old_skolems, t) + +fun reveal_old_skolem_terms old_skolems = + map_aterms (fn t as Const (s, _) => + if String.isPrefix old_skolem_const_prefix s then + AList.lookup (op =) old_skolems s |> the + |> map_types Type_Infer.paramify_vars + else + t + | t => t) + + +(***************************************************************) +(* Type Classes Present in the Axiom or Conjecture Clauses *) +(***************************************************************) + +fun set_insert (x, s) = Symtab.update (x, ()) s + +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) + +(*Remove this trivial type class*) +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; + +fun tfree_classes_of_terms ts = + let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; + +fun tvar_classes_of_terms ts = + let val sorts_list = map (map #2 o OldTerm.term_tvars) ts + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; + +(*fold type constructors*) +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) + | fold_type_consts _ _ x = x; + +(*Type constructors used to instantiate overloaded constants are the only ones needed.*) +fun add_type_consts_in_term thy = + let + fun aux (Const x) = + fold (fold_type_consts set_insert) (Sign.const_typargs thy x) + | aux (Abs (_, _, u)) = aux u + | aux (Const (@{const_name Meson.skolem}, _) $ _) = I + | aux (t $ u) = aux t #> aux u + | aux _ = I + in aux end + +fun type_consts_of_terms thy ts = + Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); + +(* ------------------------------------------------------------------------- *) +(* HOL to FOL (Isabelle to Metis) *) +(* ------------------------------------------------------------------------- *) + +datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *) + +fun string_of_mode FO = "FO" + | string_of_mode HO = "HO" + | string_of_mode FT = "FT" + +fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *) + | fn_isa_to_met_sublevel x = x +fun fn_isa_to_met_toplevel "equal" = "=" + | fn_isa_to_met_toplevel x = x + +fun metis_lit b c args = (b, (c, args)); + +fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s + | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, []) + | metis_term_from_combtyp (CombType ((s, _), tps)) = + Metis_Term.Fn (s, map metis_term_from_combtyp tps); + +(*These two functions insert type literals before the real literals. That is the + opposite order from TPTP linkup, but maybe OK.*) + +fun hol_term_to_fol_FO tm = + case strip_combterm_comb tm of + (CombConst ((c, _), _, tys), tms) => + let val tyargs = map metis_term_from_combtyp tys + val args = map hol_term_to_fol_FO tms + in Metis_Term.Fn (c, tyargs @ args) end + | (CombVar ((v, _), _), []) => Metis_Term.Var v + | _ => raise Fail "non-first-order combterm" + +fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = + Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) + | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s + | hol_term_to_fol_HO (CombApp (tm1, tm2)) = + Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); + +(*The fully-typed translation, to avoid type errors*) +fun wrap_type (tm, ty) = + Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty]) + +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty) + | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = + wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty) + | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = + wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), + combtyp_of tm) + +fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = + let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm + val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys + val lits = map hol_term_to_fol_FO tms + in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end + | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = + (case strip_combterm_comb tm of + (CombConst(("equal", _), _, _), tms) => + metis_lit pos "=" (map hol_term_to_fol_HO tms) + | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) + | hol_literal_to_fol FT (FOLLiteral (pos, tm)) = + (case strip_combterm_comb tm of + (CombConst(("equal", _), _, _), tms) => + metis_lit pos "=" (map hol_term_to_fol_FT tms) + | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); + +fun literals_of_hol_term thy th_no mode t = + let val (lits, types_sorts) = literals_of_term thy th_no t + 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_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_type_literals true tf)); + +fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th = + let + val thy = ProofContext.theory_of ctxt + val (old_skolems, (mlits, types_sorts)) = + th |> prop_of |> Logic.strip_imp_concl + |> conceal_old_skolem_terms j old_skolems + ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode) + in + if is_conjecture then + (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), + type_literals_for_types types_sorts, old_skolems) + else + let + val tylits = filter_out (default_sort ctxt) types_sorts + |> type_literals_for_types + val mtylits = + if type_lits then map (metis_of_type_literals false) tylits else [] + in + (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], + old_skolems) + end + end; + +val helpers = + [("c_COMBI", (false, map (`I) @{thms Meson.COMBI_def})), + ("c_COMBK", (false, map (`I) @{thms Meson.COMBK_def})), + ("c_COMBB", (false, map (`I) @{thms Meson.COMBB_def})), + ("c_COMBC", (false, map (`I) @{thms Meson.COMBC_def})), + ("c_COMBS", (false, map (`I) @{thms Meson.COMBS_def})), + ("c_fequal", (false, map (rpair @{thm equal_imp_equal}) + @{thms fequal_imp_equal equal_imp_fequal})), + ("c_True", (true, map (`I) @{thms True_or_False})), + ("c_False", (true, map (`I) @{thms True_or_False})), + ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))] + +(* ------------------------------------------------------------------------- *) +(* Logic maps manage the interface between HOL and first-order logic. *) +(* ------------------------------------------------------------------------- *) + +type logic_map = + {axioms: (Metis_Thm.thm * thm) list, + tfrees: type_literal list, + old_skolems: (string * term) list} + +fun is_quasi_fol_clause thy = + Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of + +(*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 + Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] + |> type_literals_for_types + end; + +(*Insert non-logical axioms corresponding to all accumulated TFrees*) +fun add_tfrees {axioms, tfrees, old_skolems} : logic_map = + {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ + axioms, + tfrees = tfrees, old_skolems = old_skolems} + +(*transform isabelle type / arity clause to metis clause *) +fun add_type_thm [] lmap = lmap + | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} = + add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, + old_skolems = old_skolems} + +fun const_in_metis c (pred, tm_list) = + let + fun in_mterm (Metis_Term.Var _) = false + | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list + | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list + in c = pred orelse exists in_mterm tm_list end; + +(* ARITY CLAUSE *) +fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = + metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] + | m_arity_cls (TVarLit ((c, _), (s, _))) = + metis_lit false c [Metis_Term.Var s] +(*TrueI is returned as the Isabelle counterpart because there isn't any.*) +fun arity_cls (ArityClause {conclLit, premLits, ...}) = + (TrueI, + Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); + +(* CLASSREL CLAUSE *) +fun m_class_rel_cls (subclass, _) (superclass, _) = + [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]]; +fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = + (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass))); + +fun type_ext thy tms = + let val subs = tfree_classes_of_terms tms + val supers = tvar_classes_of_terms tms + and tycons = type_consts_of_terms thy tms + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses + end; + +(* Function to generate metis clauses, including comb and type clauses *) +fun build_logic_map mode0 ctxt type_lits cls thss = + let val thy = ProofContext.theory_of ctxt + (*The modes FO and FT are sticky. HO can be downgraded to FO.*) + fun set_mode FO = FO + | set_mode HO = + if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO + else HO + | set_mode FT = FT + val mode = set_mode mode0 + (*transform isabelle clause to metis clause *) + fun add_thm th_no is_conjecture (metis_ith, isa_ith) + {axioms, tfrees, old_skolems} : logic_map = + let + val (mth, tfree_lits, old_skolems) = + hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms) + old_skolems metis_ith + in + {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, + tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} + end; + val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} + |> fold (add_thm 0 true o `I) cls + |> add_tfrees + |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths) + (1 upto length thss ~~ thss) + val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) + fun is_used c = + exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists + val lmap = + if mode = FO then + lmap + else + let + val helper_ths = + helpers |> filter (is_used o fst) + |> maps (fn (c, (needs_full_types, thms)) => + if not (is_used c) orelse + needs_full_types andalso mode <> FT then + [] + else + thms) + in lmap |> fold (add_thm ~1 false) helper_ths end + in + (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) + end + +end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Sledgehammer/meson_clausify.ML --- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML Wed Oct 06 13:48:12 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,394 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/meson_clausify.ML - Author: Jia Meng, Cambridge University Computer Laboratory and NICTA - Author: Jasmin Blanchette, TU Muenchen - -Transformation of axiom rules (elim/intro/etc) into CNF forms. -*) - -signature MESON_CLAUSIFY = -sig - val new_skolem_var_prefix : string - val extensionalize_theorem : thm -> thm - val introduce_combinators_in_cterm : cterm -> thm - val introduce_combinators_in_theorem : thm -> thm - val to_definitional_cnf_with_quantifiers : theory -> thm -> thm - val cluster_of_zapped_var_name : string -> (int * int) * bool - val cnf_axiom : - Proof.context -> bool -> int -> thm -> (thm * term) option * thm list - val meson_general_tac : Proof.context -> thm list -> int -> tactic - val setup: theory -> theory -end; - -structure Meson_Clausify : MESON_CLAUSIFY = -struct - -(* the extra "?" helps prevent clashes *) -val new_skolem_var_prefix = "?SK" -val new_nonskolem_var_prefix = "?V" - -(**** Transformation of Elimination Rules into First-Order Formulas****) - -val cfalse = cterm_of @{theory HOL} HOLogic.false_const; -val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); - -(* Converts an elim-rule into an equivalent theorem that does not have the - predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_term" in - "Sledgehammer_Util".) *) -fun transform_elim_theorem th = - case concl_of th of (*conclusion variable*) - @{const Trueprop} $ (v as Var (_, @{typ bool})) => - Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th - | v as Var(_, @{typ prop}) => - Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th - | _ => th - - -(**** SKOLEMIZATION BY INFERENCE (lcp) ****) - -fun mk_old_skolem_term_wrapper t = - let val T = fastype_of t in - Const (@{const_name skolem}, T --> T) $ t - end - -fun beta_eta_under_lambdas (Abs (s, T, t')) = - Abs (s, T, beta_eta_under_lambdas t') - | beta_eta_under_lambdas t = Envir.beta_eta_contract t - -(*Traverse a theorem, accumulating Skolem function definitions.*) -fun old_skolem_defs th = - let - fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss = - (*Existential: declare a Skolem function, then insert into body and continue*) - let - val args = OldTerm.term_frees body - (* Forms a lambda-abstraction over the formal parameters *) - val rhs = - list_abs_free (map dest_Free args, - HOLogic.choice_const T $ beta_eta_under_lambdas body) - |> mk_old_skolem_term_wrapper - val comb = list_comb (rhs, args) - in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end - | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = - (*Universal quant: insert a free variable into body and continue*) - let val fname = Name.variant (OldTerm.add_term_names (p,[])) a - in dec_sko (subst_bound (Free(fname,T), p)) rhss end - | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q - | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q - | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss - | dec_sko _ rhss = rhss - in dec_sko (prop_of th) [] end; - - -(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) - -val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} - -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) -fun extensionalize_theorem th = - case prop_of th of - _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _])) - $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all) - | _ => th - -fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true - | is_quasi_lambda_free (t1 $ t2) = - is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 - | is_quasi_lambda_free (Abs _) = false - | is_quasi_lambda_free _ = true - -val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); -val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); -val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); - -(* FIXME: Requires more use of cterm constructors. *) -fun abstract ct = - let - val thy = theory_of_cterm ct - val Abs(x,_,body) = term_of ct - val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) - val cxT = ctyp_of thy xT - val cbodyT = ctyp_of thy bodyT - fun makeK () = - instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] - @{thm abs_K} - in - case body of - Const _ => makeK() - | Free _ => makeK() - | Var _ => makeK() (*though Var isn't expected*) - | Bound 0 => instantiate' [SOME cxT] [] @{thm 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)] @{thm 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)] @{thm 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 Thm.eta_conversion ct - else (*B*) - let val crand = cterm_of thy (Abs(x,xT,rand)) - val crator = cterm_of thy rator - val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} - val (_,rhs) = Thm.dest_equals (cprop_of abs_B') - in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end - else makeK() - | _ => raise Fail "abstract: Bad term" - end; - -(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) -fun introduce_combinators_in_cterm ct = - if is_quasi_lambda_free (term_of ct) then - Thm.reflexive ct - else case term_of ct of - Abs _ => - let - val (cv, cta) = Thm.dest_abs NONE ct - val (v, _) = dest_Free (term_of cv) - val u_th = introduce_combinators_in_cterm cta - val cu = Thm.rhs_of u_th - val comb_eq = abstract (Thm.cabs cv cu) - in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end - | _ $ _ => - let val (ct1, ct2) = Thm.dest_comb ct in - Thm.combination (introduce_combinators_in_cterm ct1) - (introduce_combinators_in_cterm ct2) - end - -fun introduce_combinators_in_theorem th = - if is_quasi_lambda_free (prop_of th) then - th - else - let - val th = Drule.eta_contraction_rule th - val eqth = introduce_combinators_in_cterm (cprop_of th) - in Thm.equal_elim eqth th end - handle THM (msg, _, _) => - (warning ("Error in the combinator translation of " ^ - Display.string_of_thm_without_context th ^ - "\nException message: " ^ msg ^ "."); - (* A type variable of sort "{}" will make abstraction fail. *) - TrueI) - -(*cterms are used throughout for efficiency*) -val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop; - -(*Given an abstraction over n variables, replace the bound variables by free - ones. Return the body, along with the list of free variables.*) -fun c_variant_abs_multi (ct0, vars) = - let val (cv,ct) = Thm.dest_abs NONE ct0 - in c_variant_abs_multi (ct, cv::vars) end - handle CTERM _ => (ct0, rev vars); - -val skolem_def_raw = @{thms skolem_def_raw} - -(* Given the definition of a Skolem function, return a theorem to replace - an existential formula by a use of that function. - Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) -fun old_skolem_theorem_from_def thy rhs0 = - let - val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy - val rhs' = rhs |> Thm.dest_comb |> snd - val (ch, frees) = c_variant_abs_multi (rhs', []) - val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of - val T = - case hilbert of - Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T - | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"", - [hilbert]) - val cex = cterm_of thy (HOLogic.exists_const T) - val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) - val conc = - Drule.list_comb (rhs, frees) - |> Drule.beta_conv cabs |> Thm.capply cTrueprop - fun tacf [prem] = - rewrite_goals_tac skolem_def_raw - THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1 - in - Goal.prove_internal [ex_tm] conc tacf - |> forall_intr_list frees - |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) - |> Thm.varifyT_global - end - -fun to_definitional_cnf_with_quantifiers thy th = - let - val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) - val eqth = eqth RS @{thm eq_reflection} - val eqth = eqth RS @{thm TruepropI} - in Thm.equal_elim eqth th end - -fun zapped_var_name ax_no (cluster_no, skolem) s = - (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^ - "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s - -fun cluster_of_zapped_var_name s = - ((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)), - String.isPrefix new_skolem_var_prefix s) - -fun rename_vars_to_be_zapped ax_no = - let - fun aux (cluster as (cluster_no, cluster_skolem)) pos t = - case t of - (t1 as Const (s, _)) $ Abs (s', T, t') => - if s = @{const_name all} orelse s = @{const_name All} orelse - s = @{const_name Ex} then - let - val skolem = (pos = (s = @{const_name Ex})) - val cluster = - if skolem = cluster_skolem then cluster - else (cluster_no |> cluster_skolem ? Integer.add 1, skolem) - val s' = zapped_var_name ax_no cluster s' - in t1 $ Abs (s', T, aux cluster pos t') end - else - t - | (t1 as Const (s, _)) $ t2 $ t3 => - if s = @{const_name "==>"} orelse s = @{const_name implies} then - t1 $ aux cluster (not pos) t2 $ aux cluster pos t3 - else if s = @{const_name conj} orelse s = @{const_name disj} then - t1 $ aux cluster pos t2 $ aux cluster pos t3 - else - t - | (t1 as Const (s, _)) $ t2 => - if s = @{const_name Trueprop} then t1 $ aux cluster pos t2 - else if s = @{const_name Not} then t1 $ aux cluster (not pos) t2 - else t - | _ => t - in aux (0, true) true end - -fun zap pos ct = - ct - |> (case term_of ct of - Const (s, _) $ Abs (s', _, _) => - if s = @{const_name all} orelse s = @{const_name All} orelse - s = @{const_name Ex} then - Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos - else - Conv.all_conv - | Const (s, _) $ _ $ _ => - if s = @{const_name "==>"} orelse s = @{const_name implies} then - Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) - else if s = @{const_name conj} orelse s = @{const_name disj} then - Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) - else - Conv.all_conv - | Const (s, _) $ _ => - if s = @{const_name Trueprop} then Conv.arg_conv (zap pos) - else if s = @{const_name Not} then Conv.arg_conv (zap (not pos)) - else Conv.all_conv - | _ => Conv.all_conv) - -fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths - -val no_choice = - @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"} - |> Logic.varify_global - |> Skip_Proof.make_thm @{theory} - -(* Converts an Isabelle theorem into NNF. *) -fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt = - let - val thy = ProofContext.theory_of ctxt - val th = - th |> transform_elim_theorem - |> zero_var_indexes - |> new_skolemizer ? forall_intr_vars - val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single - val th = th |> Conv.fconv_rule Object_Logic.atomize - |> extensionalize_theorem - |> Meson.make_nnf ctxt - in - if new_skolemizer then - let - fun rename_bound_vars th = - let val t = concl_of th in - th |> Thm.rename_boundvars t (rename_vars_to_be_zapped ax_no t) - end - fun skolemize choice_ths = - Meson.skolemize_with_choice_thms ctxt choice_ths - #> simplify (ss_only @{thms all_simps[symmetric]}) - val pull_out = - simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) - val (discharger_th, fully_skolemized_th) = - if null choice_ths then - th |> rename_bound_vars |> `I |>> pull_out ||> skolemize [no_choice] - else - th |> skolemize choice_ths |> rename_bound_vars |> `I - val t = - fully_skolemized_th |> cprop_of - |> zap true |> Drule.export_without_context - |> cprop_of |> Thm.dest_equals |> snd |> term_of - in - if exists_subterm (fn Var ((s, _), _) => - String.isPrefix new_skolem_var_prefix s - | _ => false) t then - let - val (ct, ctxt) = - Variable.import_terms true [t] ctxt - |>> the_single |>> cterm_of thy - in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end - else - (NONE, th, ctxt) - end - else - (NONE, th, ctxt) - end - -(* Convert a theorem to CNF, with additional premises due to skolemization. *) -fun cnf_axiom ctxt0 new_skolemizer ax_no th = - let - val thy = ProofContext.theory_of ctxt0 - val choice_ths = Meson_Choices.get ctxt0 - val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 - fun clausify th = - Meson.make_cnf (if new_skolemizer then - [] - else - map (old_skolem_theorem_from_def thy) - (old_skolem_defs th)) th ctxt - val (cnf_ths, ctxt) = - clausify nnf_th - |> (fn ([], _) => - clausify (to_definitional_cnf_with_quantifiers thy nnf_th) - | p => p) - fun intr_imp ct th = - Thm.instantiate ([], map (pairself (cterm_of @{theory})) - [(Var (("i", 1), @{typ nat}), - HOLogic.mk_nat ax_no)]) - @{thm skolem_COMBK_D} - RS Thm.implies_intr ct th - in - (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0) - ##> (term_of #> HOLogic.dest_Trueprop - #> singleton (Variable.export_terms ctxt ctxt0))), - cnf_ths |> map (introduce_combinators_in_theorem - #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) - |> Variable.export ctxt ctxt0 - |> Meson.finish_cnf - |> map Thm.close_derivation) - end - handle THM _ => (NONE, []) - -fun meson_general_tac ctxt ths = - let val ctxt = Classical.put_claset HOL_cs ctxt in - Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths) - end - -val setup = - Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) - "MESON resolution proof procedure" - -end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Wed Oct 06 13:48:12 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,555 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML - Author: Kong W. Susanto, Cambridge University Computer Laboratory - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - Copyright Cambridge University 2007 - -Proof reconstruction for Metis. -*) - -signature METIS_RECONSTRUCT = -sig - type mode = Metis_Translate.mode - - val trace : bool Unsynchronized.ref - val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a - val untyped_aconv : term -> term -> bool - val replay_one_inference : - Proof.context -> mode -> (string * term) list - -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list - -> (Metis_Thm.thm * thm) list -end; - -structure Metis_Reconstruct : METIS_RECONSTRUCT = -struct - -open Metis_Translate - -val trace = Unsynchronized.ref false -fun trace_msg msg = if !trace then tracing (msg ()) else () - -datatype term_or_type = SomeTerm of term | SomeType of typ - -fun terms_of [] = [] - | terms_of (SomeTerm t :: tts) = t :: terms_of tts - | terms_of (SomeType _ :: tts) = terms_of tts; - -fun types_of [] = [] - | types_of (SomeTerm (Var ((a,idx), _)) :: tts) = - if String.isPrefix "_" a then - (*Variable generated by Metis, which might have been a type variable.*) - TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts - else types_of tts - | types_of (SomeTerm _ :: tts) = types_of tts - | types_of (SomeType T :: tts) = T :: types_of tts; - -fun apply_list rator nargs rands = - let val trands = terms_of rands - in if length trands = nargs then SomeTerm (list_comb(rator, trands)) - else raise Fail - ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ - " expected " ^ Int.toString nargs ^ - " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) - end; - -fun infer_types ctxt = - Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); - -(*We use 1 rather than 0 because variable references in clauses may otherwise conflict - with variable constraints in the goal...at least, type inference often fails otherwise. - SEE ALSO axiom_inf below.*) -fun mk_var (w, T) = Var ((w, 1), T) - -(*include the default sort, if available*) -fun mk_tfree ctxt w = - let val ww = "'" ^ w - in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; - -(*Remove the "apply" operator from an HO term*) -fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t - | strip_happ args x = (x, args); - -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) - -fun smart_invert_const "fequal" = @{const_name HOL.eq} - | smart_invert_const s = invert_const s - -fun hol_type_from_metis_term _ (Metis_Term.Var v) = - (case strip_prefix_and_unascii tvar_prefix v of - SOME w => make_tvar w - | NONE => make_tvar v) - | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = - (case strip_prefix_and_unascii type_const_prefix x of - SOME tc => Type (smart_invert_const tc, - map (hol_type_from_metis_term ctxt) tys) - | NONE => - case strip_prefix_and_unascii tfree_prefix x of - SOME tf => mk_tfree ctxt tf - | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); - -(*Maps metis terms to isabelle terms*) -fun hol_term_from_metis_PT ctxt fol_tm = - let val thy = ProofContext.theory_of ctxt - val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ - Metis_Term.toString fol_tm) - fun tm_to_tt (Metis_Term.Var v) = - (case strip_prefix_and_unascii tvar_prefix v of - SOME w => SomeType (make_tvar w) - | NONE => - case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) - | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) ) - (*Var from Metis with a name like _nnn; possibly a type variable*) - | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) - | tm_to_tt (t as Metis_Term.Fn (".",_)) = - let val (rator,rands) = strip_happ [] t - in case rator of - Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) - | _ => case tm_to_tt rator of - SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) - | _ => raise Fail "tm_to_tt: HO application" - end - | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args) - and applic_to_tt ("=",ts) = - SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) - | applic_to_tt (a,ts) = - case strip_prefix_and_unascii const_prefix a of - SOME b => - let - val c = smart_invert_const b - val ntypes = num_type_args thy c - val nterms = length ts - ntypes - val tts = map tm_to_tt ts - val tys = types_of (List.take(tts,ntypes)) - val t = if String.isPrefix new_skolem_const_prefix c then - Var (new_skolem_var_from_const c, tl tys ---> hd tys) - else - Const (c, dummyT) - in if length tys = ntypes then - apply_list t nterms (List.drop(tts,ntypes)) - else - raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ - " but gets " ^ Int.toString (length tys) ^ - " type arguments\n" ^ - cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ - " the terms are \n" ^ - cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) - end - | NONE => (*Not a constant. Is it a type constructor?*) - case strip_prefix_and_unascii type_const_prefix a of - SOME b => - SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts))) - | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case strip_prefix_and_unascii tfree_prefix a of - SOME b => SomeType (mk_tfree ctxt b) - | NONE => (*a fixed variable? They are Skolem functions.*) - case strip_prefix_and_unascii fixed_var_prefix a of - SOME b => - let val opr = Free (b, HOLogic.typeT) - in apply_list opr (length ts) (map tm_to_tt ts) end - | NONE => raise Fail ("unexpected metis function: " ^ a) - in - case tm_to_tt fol_tm of - SomeTerm t => t - | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) - end - -(*Maps fully-typed metis terms to isabelle terms*) -fun hol_term_from_metis_FT ctxt fol_tm = - let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ - Metis_Term.toString fol_tm) - fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = - (case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => mk_var(w, dummyT) - | NONE => mk_var(v, dummyT)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = - Const (@{const_name HOL.eq}, HOLogic.typeT) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, hol_type_from_metis_term ctxt ty) - | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) - | cvt (Metis_Term.Fn ("=", [tm1,tm2])) = - list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) - | cvt (t as Metis_Term.Fn (x, [])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); - hol_term_from_metis_PT ctxt t)) - | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); - hol_term_from_metis_PT ctxt t) - in fol_tm |> cvt end - -fun hol_term_from_metis FT = hol_term_from_metis_FT - | hol_term_from_metis _ = hol_term_from_metis_PT - -fun hol_terms_from_fol ctxt mode old_skolems fol_tms = - let val ts = map (hol_term_from_metis mode ctxt) fol_tms - val _ = trace_msg (fn () => " calling type inference:") - val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts - val ts' = ts |> map (reveal_old_skolem_terms old_skolems) - |> infer_types ctxt - val _ = app (fn t => trace_msg - (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ - " of type " ^ Syntax.string_of_typ ctxt (type_of t))) - ts' - in ts' end; - -(* ------------------------------------------------------------------------- *) -(* FOL step Inference Rules *) -(* ------------------------------------------------------------------------- *) - -(*for debugging only*) -(* -fun print_thpair (fth,th) = - (trace_msg (fn () => "============================================="); - trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); - trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); -*) - -fun lookth thpairs (fth : Metis_Thm.thm) = - the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) - handle Option.Option => - raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) - -fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); - -(* INFERENCE RULE: AXIOM *) - -fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); - (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) - -(* INFERENCE RULE: ASSUME *) - -val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} - -fun inst_excluded_middle thy i_atm = - let val th = EXCLUDED_MIDDLE - val [vx] = Term.add_vars (prop_of th) [] - val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] - in cterm_instantiate substs th end; - -fun assume_inf ctxt mode old_skolems atm = - inst_excluded_middle - (ProofContext.theory_of ctxt) - (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm)) - -(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying - to reconstruct them admits new possibilities of errors, e.g. concerning - sorts. Instead we try to arrange that new TVars are distinct and that types - can be inferred from terms. *) - -fun inst_inf ctxt mode old_skolems thpairs fsubst th = - let val thy = ProofContext.theory_of ctxt - val i_th = lookth thpairs th - val i_th_vars = Term.add_vars (prop_of i_th) [] - fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) - fun subst_translation (x,y) = - let val v = find_var x - (* We call "reveal_old_skolem_terms" and "infer_types" below. *) - val t = hol_term_from_metis mode ctxt y - in SOME (cterm_of thy (Var v), t) end - handle Option.Option => - (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - | TYPE _ => - (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - fun remove_typeinst (a, t) = - case strip_prefix_and_unascii schematic_var_prefix a of - SOME b => SOME (b, t) - | NONE => case strip_prefix_and_unascii tvar_prefix a of - SOME _ => NONE (*type instantiations are forbidden!*) - | NONE => SOME (a,t) (*internal Metis var?*) - val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) - val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) - val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) - val tms = rawtms |> map (reveal_old_skolem_terms old_skolems) - |> infer_types ctxt - val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) - val substs' = ListPair.zip (vars, map ctm_of tms) - val _ = trace_msg (fn () => - cat_lines ("subst_translations:" :: - (substs' |> map (fn (x, y) => - Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ - Syntax.string_of_term ctxt (term_of y))))); - in cterm_instantiate substs' i_th end - handle THM (msg, _, _) => - error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) - -(* INFERENCE RULE: RESOLVE *) - -(* Like RSN, but we rename apart only the type variables. Vars here typically - have an index of 1, and the use of RSN would increase this typically to 3. - Instantiations of those Vars could then fail. See comment on "mk_var". *) -fun resolve_inc_tyvars thy tha i thb = - let - val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha - fun aux tha thb = - case Thm.bicompose false (false, tha, nprems_of tha) i thb - |> Seq.list_of |> distinct Thm.eq_thm of - [th] => th - | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, - [tha, thb]) - in - aux tha thb - handle TERM z => - (* The unifier, which is invoked from "Thm.bicompose", will sometimes - refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a - "TERM" exception (with "add_ffpair" as first argument). We then - perform unification of the types of variables by hand and try - again. We could do this the first time around but this error - occurs seldom and we don't want to break existing proofs in subtle - ways or slow them down needlessly. *) - case [] |> fold (Term.add_vars o prop_of) [tha, thb] - |> AList.group (op =) - |> maps (fn ((s, _), T :: Ts) => - map (fn T' => (Free (s, T), Free (s, T'))) Ts) - |> rpair (Envir.empty ~1) - |-> fold (Pattern.unify thy) - |> Envir.type_env |> Vartab.dest - |> map (fn (x, (S, T)) => - pairself (ctyp_of thy) (TVar (x, S), T)) of - [] => raise TERM z - | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) - end - -fun mk_not (Const (@{const_name Not}, _) $ b) = b - | mk_not b = HOLogic.mk_not b - -(* Match untyped terms. *) -fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) - | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) - | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = - (a = b) (* The index is ignored, for some reason. *) - | untyped_aconv (Bound i) (Bound j) = (i = j) - | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u - | untyped_aconv (t1 $ t2) (u1 $ u2) = - untyped_aconv t1 u1 andalso untyped_aconv t2 u2 - | untyped_aconv _ _ = false - -(* Finding the relative location of an untyped term within a list of terms *) -fun literal_index lit = - let - val lit = Envir.eta_contract lit - fun get _ [] = raise Empty - | get n (x :: xs) = - if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then - n - else - get (n+1) xs - in get 1 end - -(* Permute a rule's premises to move the i-th premise to the last position. *) -fun make_last i th = - let val n = nprems_of th - in if 1 <= i andalso i <= n - then Thm.permute_prems (i-1) 1 th - else raise THM("select_literal", i, [th]) - end; - -(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing - double-negations. *) -val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection] - -(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) -val select_literal = negate_head oo make_last - -fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 = - let - val thy = ProofContext.theory_of ctxt - val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 - val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) - val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) - in - (* Trivial cases where one operand is type info *) - if Thm.eq_thm (TrueI, i_th1) then - i_th2 - else if Thm.eq_thm (TrueI, i_th2) then - i_th1 - else - let - val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems) - (Metis_Term.Fn atm) - val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) - val prems_th1 = prems_of i_th1 - val prems_th2 = prems_of i_th2 - val index_th1 = literal_index (mk_not i_atm) prems_th1 - handle Empty => raise Fail "Failed to find literal in th1" - val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) - val index_th2 = literal_index i_atm prems_th2 - handle Empty => raise Fail "Failed to find literal in th2" - val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) - in - resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 - end - end; - -(* INFERENCE RULE: REFL *) - -val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} - -val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); -val refl_idx = 1 + Thm.maxidx_of REFL_THM; - -fun refl_inf ctxt mode old_skolems t = - let val thy = ProofContext.theory_of ctxt - val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t - val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) - val c_t = cterm_incr_types thy refl_idx i_t - in cterm_instantiate [(refl_x, c_t)] REFL_THM end; - -(* INFERENCE RULE: EQUALITY *) - -val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} -val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} - -val metis_eq = Metis_Term.Fn ("=", []); - -fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) - | get_ty_arg_size _ _ = 0; - -fun equality_inf ctxt mode old_skolems (pos, atm) fp fr = - let val thy = ProofContext.theory_of ctxt - val m_tm = Metis_Term.Fn atm - val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr] - val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) - fun replace_item_list lx 0 (_::ls) = lx::ls - | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls - fun path_finder_FO tm [] = (tm, Bound 0) - | path_finder_FO tm (p::ps) = - let val (tm1,args) = strip_comb tm - val adjustment = get_ty_arg_size thy tm1 - val p' = if adjustment > p then p else p-adjustment - val tm_p = List.nth(args,p') - handle Subscript => - error ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf: " ^ Int.toString p ^ " adj " ^ - Int.toString adjustment ^ " term " ^ - Syntax.string_of_term ctxt tm) - val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ - " " ^ Syntax.string_of_term ctxt tm_p) - val (r,t) = path_finder_FO tm_p ps - in - (r, list_comb (tm1, replace_item_list t p' args)) - end - fun path_finder_HO tm [] = (tm, Bound 0) - | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) - | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) - | path_finder_HO tm ps = - raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_HO: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm) - fun path_finder_FT tm [] _ = (tm, Bound 0) - | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = - path_finder_FT tm ps t1 - | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = - (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) - | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = - (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) - | path_finder_FT tm ps t = - raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_FT: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - " fol-term: " ^ Metis_Term.toString t) - fun path_finder FO tm ps _ = path_finder_FO tm ps - | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = - (*equality: not curried, as other predicates are*) - if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) - else path_finder_HO tm (p::ps) (*1 selects second operand*) - | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = - path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) - | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) - (Metis_Term.Fn ("=", [t1,t2])) = - (*equality: not curried, as other predicates are*) - if p=0 then path_finder_FT tm (0::1::ps) - (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) - (*select first operand*) - else path_finder_FT tm (p::ps) - (Metis_Term.Fn (".", [metis_eq,t2])) - (*1 selects second operand*) - | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 - (*if not equality, ignore head to skip the hBOOL predicate*) - | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) - fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = - let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm - in (tm, nt $ tm_rslt) end - | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm - val (tm_subst, body) = path_finder_lit i_atm fp - val tm_abs = Abs ("x", type_of tm_subst, body) - val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) - val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) - val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) - val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) - val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') - val eq_terms = map (pairself (cterm_of thy)) - (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) - in cterm_instantiate eq_terms subst' end; - -val factor = Seq.hd o distinct_subgoals_tac; - -fun step ctxt mode old_skolems thpairs p = - case p of - (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) - | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm - | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1) - | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => - factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2) - | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm - | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inf ctxt mode old_skolems f_lit f_p f_r - -fun flexflex_first_order th = - case Thm.tpairs_of th of - [] => th - | pairs => - let val thy = theory_of_thm th - val (_, tenv) = - fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) - val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) - val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th - in th' end - handle THM _ => th; - -fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) -fun is_isabelle_literal_genuine t = - case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true - -fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 - -fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs = - let - val _ = trace_msg (fn () => "=============================================") - val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) - val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) - val th = step ctxt mode old_skolems thpairs (fol_th, inf) - |> flexflex_first_order - val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) - val _ = trace_msg (fn () => "=============================================") - val num_metis_lits = - fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList - |> count is_metis_literal_genuine - val num_isabelle_lits = - th |> prems_of |> count is_isabelle_literal_genuine - val _ = if num_metis_lits = num_isabelle_lits then () - else error "Cannot replay Metis proof in Isabelle: Out of sync." - in (fol_th, th) :: thpairs end - -end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Oct 06 13:48:12 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,341 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML - Author: Kong W. Susanto, Cambridge University Computer Laboratory - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - Copyright Cambridge University 2007 - -HOL setup for the Metis prover. -*) - -signature METIS_TACTICS = -sig - val trace : bool Unsynchronized.ref - val type_lits : bool Config.T - val new_skolemizer : bool Config.T - val metis_tac : Proof.context -> thm list -> int -> tactic - val metisF_tac : Proof.context -> thm list -> int -> tactic - val metisFT_tac : Proof.context -> thm list -> int -> tactic - val setup : theory -> theory -end - -structure Metis_Tactics : METIS_TACTICS = -struct - -open Metis_Translate -open Metis_Reconstruct - -structure Int_Pair_Graph = - Graph(type key = int * int val ord = prod_ord int_ord int_ord) - -fun trace_msg msg = if !trace then tracing (msg ()) else () - -val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true) -val (new_skolemizer, new_skolemizer_setup) = - Attrib.config_bool "metis_new_skolemizer" (K false) - -fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); - -fun have_common_thm ths1 ths2 = - exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) - -(*Determining which axiom clauses are actually used*) -fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) - | used_axioms _ _ = NONE; - -val clause_params = - {ordering = Metis_KnuthBendixOrder.default, - orderLiterals = Metis_Clause.UnsignedLiteralOrder, - orderTerms = true} -val active_params = - {clause = clause_params, - prefactor = #prefactor Metis_Active.default, - postfactor = #postfactor Metis_Active.default} -val waiting_params = - {symbolsWeight = 1.0, - variablesWeight = 0.0, - literalsWeight = 0.0, - models = []} -val resolution_params = {active = active_params, waiting = waiting_params} - -(* In principle, it should be sufficient to apply "assume_tac" to unify the - conclusion with one of the premises. However, in practice, this fails - horribly because of the mildly higher-order nature of the unification - problems. Typical constraints are of the form "?x a b =?= b", where "a" and - "b" are goal parameters. *) -fun unify_prem_with_concl thy i th = - let - val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract - val prem = goal |> Logic.strip_assums_hyp |> the_single - val concl = goal |> Logic.strip_assums_concl - fun add_types Tp instT = - if exists (curry (op =) Tp) instT then instT - else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT - fun unify_types (T, U) = - if T = U then - I - else case (T, U) of - (TVar _, _) => add_types (T, U) - | (_, TVar _) => add_types (U, T) - | (Type (s, Ts), Type (t, Us)) => - if s = t andalso length Ts = length Us then fold unify_types (Ts ~~ Us) - else raise TYPE ("unify_types", [T, U], []) - | _ => raise TYPE ("unify_types", [T, U], []) - fun pair_untyped_aconv (t1, t2) (u1, u2) = - untyped_aconv t1 u1 andalso untyped_aconv t2 u2 - fun add_terms tp inst = - if exists (pair_untyped_aconv tp) inst then inst - else tp :: map (apsnd (subst_atomic [tp])) inst - fun is_flex t = - case strip_comb t of - (Var _, args) => forall (is_Bound orf is_Var (*FIXME: orf is_Free*)) args - | _ => false - fun unify_flex flex rigid = - case strip_comb flex of - (Var (z as (_, T)), args) => - add_terms (Var z, - (* FIXME: reindex bound variables *) - fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid) - | _ => raise TERM ("unify_flex: expected flex", [flex]) - fun unify_potential_flex comb atom = - if is_flex comb then unify_flex comb atom - else if is_Var atom then add_terms (atom, comb) - else raise TERM ("unify_terms", [comb, atom]) - fun unify_terms (t, u) = - case (t, u) of - (t1 $ t2, u1 $ u2) => - if is_flex t then unify_flex t u - else if is_flex u then unify_flex u t - else fold unify_terms [(t1, u1), (t2, u2)] - | (_ $ _, _) => unify_potential_flex t u - | (_, _ $ _) => unify_potential_flex u t - | (Var _, _) => add_terms (t, u) - | (_, Var _) => add_terms (u, t) - | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u]) - - val inst = [] |> unify_terms (prem, concl) - val _ = trace_msg (fn () => cat_lines (map (fn (t, u) => - Syntax.string_of_term @{context} t ^ " |-> " ^ - Syntax.string_of_term @{context} u) inst)) - val instT = fold (fn Tp => unify_types (pairself fastype_of Tp) - handle TERM _ => I) inst [] - val inst = inst |> map (pairself (subst_atomic_types instT)) - val cinstT = instT |> map (pairself (ctyp_of thy)) - val cinst = inst |> map (pairself (cterm_of thy)) - in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end - handle Empty => th (* ### FIXME *) - -val cluster_ord = prod_ord (prod_ord int_ord int_ord) bool_ord - -(* Attempts to derive the theorem "False" from a theorem of the form - "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the - specified axioms. The axioms have leading "All" and "Ex" quantifiers, which - must be eliminated first. *) -fun discharge_skolem_premises ctxt axioms prems_imp_false = - case prop_of prems_imp_false of - @{prop False} => prems_imp_false - | prems_imp_false_prop => - let - val thy = ProofContext.theory_of ctxt - fun match_term p = - let - val (tyenv, tenv) = - Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) - val tsubst = - tenv |> Vartab.dest - |> sort (cluster_ord - o pairself (Meson_Clausify.cluster_of_zapped_var_name - o fst o fst)) - |> map (Meson.term_pair_of - #> pairself (Envir.subst_term_types tyenv)) - in (tyenv, tsubst) end - fun subst_info_for_prem assm_no prem = - case prem of - _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) => - let val ax_no = HOLogic.dest_nat num in - (ax_no, (assm_no, match_term (nth axioms ax_no |> snd, t))) - end - | _ => raise TERM ("discharge_skolem_premises: Malformed premise", - [prem]) - fun cluster_of_var_name skolem s = - let val (jj, skolem') = Meson_Clausify.cluster_of_zapped_var_name s in - if skolem' = skolem then SOME jj else NONE - end - fun clusters_in_term skolem t = - Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) - fun deps_for_term_subst (var, t) = - case clusters_in_term false var of - [] => NONE - | [(ax_no, cluster_no)] => - SOME ((ax_no, cluster_no), - clusters_in_term true t - |> cluster_no > 0 ? cons (ax_no, cluster_no - 1)) - | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) - val prems = Logic.strip_imp_prems prems_imp_false_prop - val substs = map2 subst_info_for_prem (0 upto length prems - 1) prems - val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs - val clusters = maps (op ::) depss - val ordered_clusters = - Int_Pair_Graph.empty - |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) - |> fold Int_Pair_Graph.add_deps_acyclic depss - |> Int_Pair_Graph.topological_order - handle Int_Pair_Graph.CYCLES _ => - error "Cannot replay Metis proof in Isabelle without axiom of \ - \choice." -(* for debugging: - val _ = tracing ("SUBSTS: " ^ PolyML.makestring substs) - val _ = tracing ("ORDERED: " ^ PolyML.makestring ordered_clusters) -*) - in - Goal.prove ctxt [] [] @{prop False} - (K (cut_rules_tac (map fst axioms) 1 - THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) - (* two copies are better than one (FIXME) *) - THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1 - THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1) - THEN match_tac [prems_imp_false] 1 - THEN DETERM_UNTIL_SOLVED - (rtac @{thm skolem_COMBK_I} 1 - THEN PRIMITIVE (unify_prem_with_concl thy 1) - THEN assume_tac 1))) - end - -(* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE mode ctxt cls ths0 = - let val thy = ProofContext.theory_of ctxt - val type_lits = Config.get ctxt type_lits - val new_skolemizer = - Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt) - val th_cls_pairs = - map2 (fn j => fn th => - (Thm.get_name_hint th, - Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) - (0 upto length ths0 - 1) ths0 - val thss = map (snd o snd) th_cls_pairs - val dischargers = map_filter (fst o snd) th_cls_pairs - val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls - val _ = trace_msg (fn () => "THEOREM CLAUSES") - val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss - val (mode, {axioms, tfrees, old_skolems}) = - build_logic_map mode ctxt type_lits cls thss - val _ = if null tfrees then () - else (trace_msg (fn () => "TFREE CLAUSES"); - app (fn TyLitFree ((s, _), (s', _)) => - trace_msg (fn () => s ^ "(" ^ s' ^ ")")) 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 - val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) - val _ = trace_msg (fn () => "START METIS PROVE PROCESS") - in - case filter (is_false o prop_of) cls of - false_th::_ => [false_th RS @{thm FalseE}] - | [] => - case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} - |> Metis_Resolution.loop of - Metis_Resolution.Contradiction mth => - let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ - Metis_Thm.toString mth) - val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt - (*add constraints arising from converting goal to clause form*) - val proof = Metis_Proof.proof mth - val result = - fold (replay_one_inference ctxt' mode old_skolems) proof axioms - and used = map_filter (used_axioms axioms) proof - val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") - val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used - val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => - if have_common_thm used cls then NONE else SOME name) - in - if not (null cls) andalso not (have_common_thm used cls) then - warning "Metis: The assumptions are inconsistent." - else - (); - if not (null unused) then - warning ("Metis: Unused theorems: " ^ commas_quote unused - ^ ".") - else - (); - case result of - (_,ith)::_ => - (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); - [discharge_skolem_premises ctxt dischargers ith]) - | _ => (trace_msg (fn () => "Metis: No result"); []) - end - | Metis_Resolution.Satisfiable _ => - (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); - []) - end; - -(* Extensionalize "th", because that makes sense and that's what Sledgehammer - does, but also keep an unextensionalized version of "th" for backward - compatibility. *) -fun also_extensionalize_theorem th = - let val th' = Meson_Clausify.extensionalize_theorem th in - if Thm.eq_thm (th, th') then [th] - else th :: Meson.make_clauses_unsorted [th'] - end - -val neg_clausify = - single - #> Meson.make_clauses_unsorted - #> maps also_extensionalize_theorem - #> map Meson_Clausify.introduce_combinators_in_theorem - #> Meson.finish_cnf - -fun preskolem_tac ctxt st0 = - (if exists (Meson.has_too_many_clauses ctxt) - (Logic.prems_of_goal (prop_of st0) 1) then - cnf.cnfx_rewrite_tac ctxt 1 - else - all_tac) st0 - -val type_has_top_sort = - exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) - -fun generic_metis_tac mode ctxt ths i st0 = - let - val _ = trace_msg (fn () => - "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) - in - if exists_type type_has_top_sort (prop_of st0) then - (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) - else - Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) - (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) - ctxt i st0 - end - -val metis_tac = generic_metis_tac HO -val metisF_tac = generic_metis_tac FO -val metisFT_tac = generic_metis_tac FT - -(* Whenever "X" has schematic type variables, we treat "using X by metis" as - "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. - We don't do it for nonschematic facts "X" because this breaks a few proofs - (in the rare and subtle case where a proof relied on extensionality not being - applied) and brings few benefits. *) -val has_tvar = - exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of -fun method name mode = - Method.setup name (Attrib.thms >> (fn ths => fn ctxt => - METHOD (fn facts => - let - val (schem_facts, nonschem_facts) = - List.partition has_tvar facts - in - HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP - o generic_metis_tac mode ctxt (schem_facts @ ths)) - end))) - -val setup = - type_lits_setup - #> new_skolemizer_setup - #> method @{binding metis} HO "Metis for FOL/HOL problems" - #> method @{binding metisF} FO "Metis for FOL problems" - #> method @{binding metisFT} FT - "Metis for FOL/HOL problems with fully-typed translation" - -end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Sledgehammer/metis_translate.ML --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Oct 06 13:48:12 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,771 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/metis_translate.ML - Author: Jia Meng, Cambridge University Computer Laboratory and NICTA - Author: Kong W. Susanto, Cambridge University Computer Laboratory - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Translation of HOL to FOL for Metis. -*) - -signature METIS_TRANSLATE = -sig - type name = string * string - datatype type_literal = - TyLitVar of name * name | - TyLitFree of name * name - datatype arLit = - TConsLit of name * name * name list | - TVarLit of name * name - datatype arity_clause = - ArityClause of {name: string, conclLit: arLit, premLits: arLit list} - datatype class_rel_clause = - ClassRelClause of {name: string, subclass: name, superclass: name} - datatype combtyp = - CombTVar of name | - CombTFree of name | - CombType of name * combtyp list - datatype combterm = - CombConst of name * combtyp * combtyp list (* Const and Free *) | - CombVar of name * combtyp | - CombApp of combterm * combterm - datatype fol_literal = FOLLiteral of bool * combterm - - datatype mode = FO | HO | FT - type logic_map = - {axioms: (Metis_Thm.thm * thm) list, - tfrees: type_literal list, - old_skolems: (string * term) list} - - val type_wrapper_name : string - val bound_var_prefix : string - val schematic_var_prefix: string - val fixed_var_prefix: string - val tvar_prefix: string - val tfree_prefix: string - val const_prefix: string - val type_const_prefix: string - val class_prefix: string - val new_skolem_const_prefix : string - val invert_const: string -> string - val ascii_of: string -> string - val unascii_of: string -> string - val strip_prefix_and_unascii: string -> string -> string option - val make_bound_var : string -> string - val make_schematic_var : string * int -> string - val make_fixed_var : string -> string - val make_schematic_type_var : string * int -> string - val make_fixed_type_var : string -> string - val make_fixed_const : string -> string - val make_fixed_type_const : string -> string - val make_type_class : string -> string - val num_type_args: theory -> string -> int - val new_skolem_var_from_const: string -> indexname - val type_literals_for_types : typ list -> type_literal list - val make_class_rel_clauses : - theory -> class list -> class list -> class_rel_clause list - val make_arity_clauses : - theory -> string list -> class list -> class list * arity_clause list - val combtyp_of : combterm -> combtyp - val strip_combterm_comb : combterm -> combterm * combterm list - val combterm_from_term : - theory -> int -> (string * typ) list -> term -> combterm * typ list - val reveal_old_skolem_terms : (string * term) list -> term -> term - val tfree_classes_of_terms : term list -> string list - val tvar_classes_of_terms : term list -> string list - val type_consts_of_terms : theory -> term list -> string list - val string_of_mode : mode -> string - val build_logic_map : - mode -> Proof.context -> bool -> thm list -> thm list list - -> mode * logic_map -end - -structure Metis_Translate : METIS_TRANSLATE = -struct - -val type_wrapper_name = "ti" - -val bound_var_prefix = "B_" -val schematic_var_prefix = "V_" -val fixed_var_prefix = "v_" - -val tvar_prefix = "T_"; -val tfree_prefix = "t_"; - -val const_prefix = "c_"; -val type_const_prefix = "tc_"; -val class_prefix = "class_"; - -val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" -val old_skolem_const_prefix = skolem_const_prefix ^ "o" -val new_skolem_const_prefix = skolem_const_prefix ^ "n" - -fun union_all xss = fold (union (op =)) xss [] - -(* Readable names for the more common symbolic functions. Do not mess with the - last nine entries of the table unless you know what you are doing. *) -val const_trans_table = - Symtab.make [(@{type_name Product_Type.prod}, "prod"), - (@{type_name Sum_Type.sum}, "sum"), - (@{const_name HOL.eq}, "equal"), - (@{const_name HOL.conj}, "and"), - (@{const_name HOL.disj}, "or"), - (@{const_name HOL.implies}, "implies"), - (@{const_name Set.member}, "member"), - (@{const_name fequal}, "fequal"), - (@{const_name COMBI}, "COMBI"), - (@{const_name COMBK}, "COMBK"), - (@{const_name COMBB}, "COMBB"), - (@{const_name COMBC}, "COMBC"), - (@{const_name COMBS}, "COMBS"), - (@{const_name True}, "True"), - (@{const_name False}, "False"), - (@{const_name If}, "If")] - -(* Invert the table of translations between Isabelle and ATPs. *) -val const_trans_table_inv = - Symtab.update ("fequal", @{const_name HOL.eq}) - (Symtab.make (map swap (Symtab.dest const_trans_table))) - -val invert_const = perhaps (Symtab.lookup const_trans_table_inv) - -(*Escaping of special characters. - Alphanumeric characters are left unchanged. - The character _ goes to __ - Characters in the range ASCII space to / go to _A to _P, respectively. - Other characters go to _nnn where nnn is the decimal ASCII code.*) -val A_minus_space = Char.ord #"A" - Char.ord #" "; - -fun stringN_of_int 0 _ = "" - | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); - -fun ascii_of_c c = - if Char.isAlphaNum c then String.str c - else if c = #"_" then "__" - else if #" " <= c andalso c <= #"/" - then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) - else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) - -val ascii_of = String.translate ascii_of_c; - -(** Remove ASCII armouring from names in proof files **) - -(*We don't raise error exceptions because this code can run inside the watcher. - Also, the errors are "impossible" (hah!)*) -fun unascii_aux rcs [] = String.implode(rev rcs) - | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) - (*Three types of _ escapes: __, _A to _P, _nnn*) - | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs - | unascii_aux rcs (#"_" :: c :: cs) = - if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) - then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs - else - let val digits = List.take (c::cs, 3) handle Subscript => [] - in - case Int.fromString (String.implode digits) of - NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) - | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) - end - | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs -val unascii_of = unascii_aux [] o String.explode - -(* If string s has the prefix s1, return the result of deleting it, - un-ASCII'd. *) -fun strip_prefix_and_unascii s1 s = - if String.isPrefix s1 s then - SOME (unascii_of (String.extract (s, size s1, NONE))) - else - NONE - -(*Remove the initial ' character from a type variable, if it is present*) -fun trim_type_var s = - if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) - else error ("trim_type: Malformed type variable encountered: " ^ s); - -fun ascii_of_indexname (v,0) = ascii_of v - | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; - -fun make_bound_var x = bound_var_prefix ^ ascii_of x -fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v -fun make_fixed_var x = fixed_var_prefix ^ ascii_of x - -fun make_schematic_type_var (x,i) = - tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); - -fun lookup_const c = - case Symtab.lookup const_trans_table c of - SOME c' => c' - | NONE => ascii_of c - -(* HOL.eq MUST BE "equal" because it's built into ATPs. *) -fun make_fixed_const @{const_name HOL.eq} = "equal" - | make_fixed_const c = const_prefix ^ lookup_const c - -fun make_fixed_type_const c = type_const_prefix ^ lookup_const c - -fun make_type_class clas = class_prefix ^ ascii_of clas; - -(* The number of type arguments of a constant, zero if it's monomorphic. For - (instances of) Skolem pseudoconstants, this information is encoded in the - constant name. *) -fun num_type_args thy s = - if String.isPrefix skolem_const_prefix s then - s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the - else - (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length - -fun new_skolem_var_from_const s = - let - val ss = s |> space_explode Long_Name.separator - val n = length ss - in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end - - -(**** Definitions and functions for FOL clauses for TPTP format output ****) - -type name = string * string - -(**** Isabelle FOL clauses ****) - -(* The first component is the type class; the second is a TVar or TFree. *) -datatype type_literal = - TyLitVar of name * name | - TyLitFree of name * name - -(*Make literals for sorted type variables*) -fun sorts_on_typs_aux (_, []) = [] - | sorts_on_typs_aux ((x,i), s::ss) = - let val sorts = sorts_on_typs_aux ((x,i), ss) - in - if s = "HOL.type" then 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); - -(*Given a list of sorted type variables, return a list of type literals.*) -fun type_literals_for_types Ts = - fold (union (op =)) (map sorts_on_typs Ts) [] - -(** make axiom and conjecture clauses. **) - -(**** Isabelle arities ****) - -datatype arLit = - TConsLit of name * name * name list | - TVarLit of name * name - -datatype arity_clause = - ArityClause of {name: string, conclLit: arLit, premLits: arLit list} - - -fun gen_TVars 0 = [] - | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); - -fun pack_sort(_,[]) = [] - | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) - | pack_sort(tvar, cls::srt) = - (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) - -(*Arity of type constructor tcon :: (arg1,...,argN)res*) -fun make_axiom_arity_clause (tcons, name, (cls,args)) = - let - val tvars = gen_TVars (length args) - val tvars_srts = ListPair.zip (tvars, args) - in - ArityClause {name = name, - conclLit = TConsLit (`make_type_class cls, - `make_fixed_type_const tcons, - tvars ~~ tvars), - premLits = map TVarLit (union_all (map pack_sort tvars_srts))} - end - - -(**** Isabelle class relations ****) - -datatype class_rel_clause = - ClassRelClause of {name: string, subclass: name, superclass: name} - -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) -fun class_pairs _ [] _ = [] - | class_pairs thy subs supers = - let - val class_less = Sorts.class_less (Sign.classes_of thy) - fun add_super sub super = class_less (sub, super) ? cons (sub, super) - fun add_supers sub = fold (add_super sub) supers - in fold add_supers subs [] end - -fun make_class_rel_clause (sub,super) = - ClassRelClause {name = sub ^ "_" ^ super, - subclass = `make_type_class sub, - superclass = `make_type_class super} - -fun make_class_rel_clauses thy subs supers = - map make_class_rel_clause (class_pairs thy subs supers); - - -(** Isabelle arities **) - -fun arity_clause _ _ (_, []) = [] - | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) - arity_clause seen n (tcons,ars) - | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = - if member (op =) seen class then (*multiple arities for the same tycon, class pair*) - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: - arity_clause seen (n+1) (tcons,ars) - else - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: - arity_clause (class::seen) n (tcons,ars) - -fun multi_arity_clause [] = [] - | multi_arity_clause ((tcons, ars) :: tc_arlists) = - arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists - -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy - provided its arguments have the corresponding sorts.*) -fun type_class_pairs thy tycons classes = - let val alg = Sign.classes_of thy - fun domain_sorts tycon = Sorts.mg_domain alg tycon o single - fun add_class tycon class = - cons (class, domain_sorts tycon class) - handle Sorts.CLASS_ERROR _ => I - fun try_classes tycon = (tycon, fold (add_class tycon) classes []) - in map try_classes tycons end; - -(*Proving one (tycon, class) membership may require proving others, so iterate.*) -fun iter_type_class_pairs _ _ [] = ([], []) - | iter_type_class_pairs thy tycons classes = - let val cpairs = type_class_pairs thy tycons classes - val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) - |> subtract (op =) classes |> subtract (op =) HOLogic.typeS - val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses - in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; - -fun make_arity_clauses thy tycons classes = - let val (classes', cpairs) = iter_type_class_pairs thy tycons classes - in (classes', multi_arity_clause cpairs) end; - -datatype combtyp = - CombTVar of name | - CombTFree of name | - CombType of name * combtyp list - -datatype combterm = - CombConst of name * combtyp * combtyp list (* Const and Free *) | - CombVar of name * combtyp | - CombApp of combterm * combterm - -datatype fol_literal = FOLLiteral of bool * combterm - -(*********************************************************************) -(* convert a clause with type Term.term to a clause with type clause *) -(*********************************************************************) - -(*Result of a function type; no need to check that the argument type matches.*) -fun result_type (CombType (_, [_, tp2])) = tp2 - | result_type _ = raise Fail "non-function type" - -fun combtyp_of (CombConst (_, tp, _)) = tp - | combtyp_of (CombVar (_, tp)) = tp - | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) - -(*gets the head of a combinator application, along with the list of arguments*) -fun strip_combterm_comb u = - let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) - | stripc x = x - in stripc(u,[]) end - -fun combtype_of (Type (a, Ts)) = - let val (folTypes, ts) = combtypes_of Ts in - (CombType (`make_fixed_type_const a, folTypes), ts) - end - | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) - | combtype_of (tp as TVar (x, _)) = - (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp]) -and combtypes_of Ts = - let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in - (folTyps, union_all ts) - end - -(* same as above, but no gathering of sort information *) -fun simple_combtype_of (Type (a, Ts)) = - CombType (`make_fixed_type_const a, map simple_combtype_of Ts) - | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) - | simple_combtype_of (TVar (x, _)) = - CombTVar (make_schematic_type_var x, string_of_indexname x) - -fun new_skolem_const_name th_no s num_T_args = - [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args] - |> space_implode Long_Name.separator - -(* Converts a term (with combinators) into a combterm. Also accummulates sort - infomation. *) -fun combterm_from_term thy th_no bs (P $ Q) = - let val (P', tsP) = combterm_from_term thy th_no bs P - val (Q', tsQ) = combterm_from_term thy th_no bs Q - in (CombApp (P', Q'), union (op =) tsP tsQ) end - | combterm_from_term thy _ _ (Const (c, T)) = - let - val (tp, ts) = combtype_of T - val tvar_list = - (if String.isPrefix old_skolem_const_prefix c then - [] |> Term.add_tvarsT T |> map TVar - else - (c, T) |> Sign.const_typargs thy) - |> map simple_combtype_of - val c' = CombConst (`make_fixed_const c, tp, tvar_list) - in (c',ts) end - | combterm_from_term _ _ _ (Free (v, T)) = - let val (tp, ts) = combtype_of T - val v' = CombConst (`make_fixed_var v, tp, []) - in (v',ts) end - | combterm_from_term _ th_no _ (Var (v as (s, _), T)) = - let - val (tp, ts) = combtype_of T - val v' = - if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then - let - val tys = T |> strip_type |> swap |> op :: - val s' = new_skolem_const_name th_no s (length tys) - in - CombConst (`make_fixed_const s', tp, map simple_combtype_of tys) - end - else - CombVar ((make_schematic_var v, string_of_indexname v), tp) - in (v', ts) end - | combterm_from_term _ _ bs (Bound j) = - let - val (s, T) = nth bs j - val (tp, ts) = combtype_of T - val v' = CombConst (`make_bound_var s, tp, []) - in (v', ts) end - | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs" - -fun predicate_of thy th_no ((@{const Not} $ P), pos) = - predicate_of thy th_no (P, not pos) - | predicate_of thy th_no (t, pos) = - (combterm_from_term thy th_no [] (Envir.eta_contract t), pos) - -fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) = - literals_of_term1 args thy th_no P - | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) = - literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q - | literals_of_term1 (lits, ts) thy th_no P = - let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in - (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') - end -val literals_of_term = literals_of_term1 ([], []) - -fun old_skolem_const_name i j num_T_args = - old_skolem_const_prefix ^ Long_Name.separator ^ - (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) - -fun conceal_old_skolem_terms i old_skolems t = - if exists_Const (curry (op =) @{const_name skolem} o fst) t then - let - fun aux old_skolems - (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) = - let - val (old_skolems, s) = - if i = ~1 then - (old_skolems, @{const_name undefined}) - else case AList.find (op aconv) old_skolems t of - s :: _ => (old_skolems, s) - | [] => - let - val s = old_skolem_const_name i (length old_skolems) - (length (Term.add_tvarsT T [])) - in ((s, t) :: old_skolems, s) end - in (old_skolems, Const (s, T)) end - | aux old_skolems (t1 $ t2) = - let - val (old_skolems, t1) = aux old_skolems t1 - val (old_skolems, t2) = aux old_skolems t2 - in (old_skolems, t1 $ t2) end - | aux old_skolems (Abs (s, T, t')) = - let val (old_skolems, t') = aux old_skolems t' in - (old_skolems, Abs (s, T, t')) - end - | aux old_skolems t = (old_skolems, t) - in aux old_skolems t end - else - (old_skolems, t) - -fun reveal_old_skolem_terms old_skolems = - map_aterms (fn t as Const (s, _) => - if String.isPrefix old_skolem_const_prefix s then - AList.lookup (op =) old_skolems s |> the - |> map_types Type_Infer.paramify_vars - else - t - | t => t) - - -(***************************************************************) -(* Type Classes Present in the Axiom or Conjecture Clauses *) -(***************************************************************) - -fun set_insert (x, s) = Symtab.update (x, ()) s - -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) - -(*Remove this trivial type class*) -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; - -fun tfree_classes_of_terms ts = - let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; - -fun tvar_classes_of_terms ts = - let val sorts_list = map (map #2 o OldTerm.term_tvars) ts - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; - -(*fold type constructors*) -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) - | fold_type_consts _ _ x = x; - -(*Type constructors used to instantiate overloaded constants are the only ones needed.*) -fun add_type_consts_in_term thy = - let - fun aux (Const x) = - fold (fold_type_consts set_insert) (Sign.const_typargs thy x) - | aux (Abs (_, _, u)) = aux u - | aux (Const (@{const_name skolem}, _) $ _) = I - | aux (t $ u) = aux t #> aux u - | aux _ = I - in aux end - -fun type_consts_of_terms thy ts = - Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); - -(* ------------------------------------------------------------------------- *) -(* HOL to FOL (Isabelle to Metis) *) -(* ------------------------------------------------------------------------- *) - -datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *) - -fun string_of_mode FO = "FO" - | string_of_mode HO = "HO" - | string_of_mode FT = "FT" - -fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *) - | fn_isa_to_met_sublevel x = x -fun fn_isa_to_met_toplevel "equal" = "=" - | fn_isa_to_met_toplevel x = x - -fun metis_lit b c args = (b, (c, args)); - -fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s - | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, []) - | metis_term_from_combtyp (CombType ((s, _), tps)) = - Metis_Term.Fn (s, map metis_term_from_combtyp tps); - -(*These two functions insert type literals before the real literals. That is the - opposite order from TPTP linkup, but maybe OK.*) - -fun hol_term_to_fol_FO tm = - case strip_combterm_comb tm of - (CombConst ((c, _), _, tys), tms) => - let val tyargs = map metis_term_from_combtyp tys - val args = map hol_term_to_fol_FO tms - in Metis_Term.Fn (c, tyargs @ args) end - | (CombVar ((v, _), _), []) => Metis_Term.Var v - | _ => raise Fail "non-first-order combterm" - -fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = - Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) - | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s - | hol_term_to_fol_HO (CombApp (tm1, tm2)) = - Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); - -(*The fully-typed translation, to avoid type errors*) -fun wrap_type (tm, ty) = - Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty]) - -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty) - | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = - wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty) - | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = - wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), - combtyp_of tm) - -fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = - let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm - val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys - val lits = map hol_term_to_fol_FO tms - in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end - | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = - (case strip_combterm_comb tm of - (CombConst(("equal", _), _, _), tms) => - metis_lit pos "=" (map hol_term_to_fol_HO tms) - | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) - | hol_literal_to_fol FT (FOLLiteral (pos, tm)) = - (case strip_combterm_comb tm of - (CombConst(("equal", _), _, _), tms) => - metis_lit pos "=" (map hol_term_to_fol_FT tms) - | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); - -fun literals_of_hol_term thy th_no mode t = - let val (lits, types_sorts) = literals_of_term thy th_no t - 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_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_type_literals true tf)); - -fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th = - let - val thy = ProofContext.theory_of ctxt - val (old_skolems, (mlits, types_sorts)) = - th |> prop_of |> Logic.strip_imp_concl - |> conceal_old_skolem_terms j old_skolems - ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode) - in - if is_conjecture then - (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), - type_literals_for_types types_sorts, old_skolems) - else - let - val tylits = filter_out (default_sort ctxt) types_sorts - |> type_literals_for_types - val mtylits = - if type_lits then map (metis_of_type_literals false) tylits else [] - in - (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], - old_skolems) - end - end; - -val helpers = - [("c_COMBI", (false, map (`I) @{thms COMBI_def})), - ("c_COMBK", (false, map (`I) @{thms COMBK_def})), - ("c_COMBB", (false, map (`I) @{thms COMBB_def})), - ("c_COMBC", (false, map (`I) @{thms COMBC_def})), - ("c_COMBS", (false, map (`I) @{thms COMBS_def})), - ("c_fequal", (false, map (rpair @{thm equal_imp_equal}) - @{thms fequal_imp_equal equal_imp_fequal})), - ("c_True", (true, map (`I) @{thms True_or_False})), - ("c_False", (true, map (`I) @{thms True_or_False})), - ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))] - -(* ------------------------------------------------------------------------- *) -(* Logic maps manage the interface between HOL and first-order logic. *) -(* ------------------------------------------------------------------------- *) - -type logic_map = - {axioms: (Metis_Thm.thm * thm) list, - tfrees: type_literal list, - old_skolems: (string * term) list} - -fun is_quasi_fol_clause thy = - Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of - -(*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 - Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] - |> type_literals_for_types - end; - -(*Insert non-logical axioms corresponding to all accumulated TFrees*) -fun add_tfrees {axioms, tfrees, old_skolems} : logic_map = - {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ - axioms, - tfrees = tfrees, old_skolems = old_skolems} - -(*transform isabelle type / arity clause to metis clause *) -fun add_type_thm [] lmap = lmap - | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} = - add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, - old_skolems = old_skolems} - -fun const_in_metis c (pred, tm_list) = - let - fun in_mterm (Metis_Term.Var _) = false - | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list - | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list - in c = pred orelse exists in_mterm tm_list end; - -(* ARITY CLAUSE *) -fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = - metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] - | m_arity_cls (TVarLit ((c, _), (s, _))) = - metis_lit false c [Metis_Term.Var s] -(*TrueI is returned as the Isabelle counterpart because there isn't any.*) -fun arity_cls (ArityClause {conclLit, premLits, ...}) = - (TrueI, - Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); - -(* CLASSREL CLAUSE *) -fun m_class_rel_cls (subclass, _) (superclass, _) = - [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]]; -fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = - (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass))); - -fun type_ext thy tms = - let val subs = tfree_classes_of_terms tms - val supers = tvar_classes_of_terms tms - and tycons = type_consts_of_terms thy tms - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses - end; - -(* Function to generate metis clauses, including comb and type clauses *) -fun build_logic_map mode0 ctxt type_lits cls thss = - let val thy = ProofContext.theory_of ctxt - (*The modes FO and FT are sticky. HO can be downgraded to FO.*) - fun set_mode FO = FO - | set_mode HO = - if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO - else HO - | set_mode FT = FT - val mode = set_mode mode0 - (*transform isabelle clause to metis clause *) - fun add_thm th_no is_conjecture (metis_ith, isa_ith) - {axioms, tfrees, old_skolems} : logic_map = - let - val (mth, tfree_lits, old_skolems) = - hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms) - old_skolems metis_ith - in - {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, - tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} - end; - val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} - |> fold (add_thm 0 true o `I) cls - |> add_tfrees - |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths) - (1 upto length thss ~~ thss) - val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) - fun is_used c = - exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists - val lmap = - if mode = FO then - lmap - else - let - val helper_ths = - helpers |> filter (is_used o fst) - |> maps (fn (c, (needs_full_types, thms)) => - if not (is_used c) orelse - needs_full_types andalso mode <> FT then - [] - else - thms) - in lmap |> fold (add_thm ~1 false) helper_ths end - in - (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) - end - -end; diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Oct 06 17:44:21 2010 +0200 @@ -1,6 +1,8 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen + +Sledgehammer's relevance filter. *) signature SLEDGEHAMMER_FILTER = @@ -585,6 +587,7 @@ fun is_formula_too_complex t = apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t +(* FIXME: Extend to "Meson" and "Metis" *) val exists_sledgehammer_const = exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Oct 06 17:44:21 2010 +0200 @@ -370,11 +370,11 @@ pair (raw_term_from_pred thy full_types tfrees u) 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})] + [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), + (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), + (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), + (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), + (@{const_name Meson.COMBS}, @{thm Meson.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') diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Oct 06 13:48:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Oct 06 17:44:21 2010 +0200 @@ -222,15 +222,15 @@ count_combformula combformula val optional_helpers = - [(["c_COMBI"], @{thms COMBI_def}), - (["c_COMBK"], @{thms COMBK_def}), - (["c_COMBB"], @{thms COMBB_def}), - (["c_COMBC"], @{thms COMBC_def}), - (["c_COMBS"], @{thms COMBS_def})] + [(["c_COMBI"], @{thms Meson.COMBI_def}), + (["c_COMBK"], @{thms Meson.COMBK_def}), + (["c_COMBB"], @{thms Meson.COMBB_def}), + (["c_COMBC"], @{thms Meson.COMBC_def}), + (["c_COMBS"], @{thms Meson.COMBS_def})] val optional_typed_helpers = [(["c_True", "c_False", "c_If"], @{thms True_or_False}), (["c_If"], @{thms if_True if_False})] -val mandatory_helpers = @{thms fequal_def} +val mandatory_helpers = @{thms Metis.fequal_def} val init_counters = [optional_helpers, optional_typed_helpers] |> maps (maps fst) @@ -300,7 +300,7 @@ let val ty_args = if full_types then [] else ty_args in if s = "equal" then if top_level andalso length args = 2 then (name, []) - else (("c_fequal", @{const_name fequal}), ty_args) + else (("c_fequal", @{const_name Metis.fequal}), ty_args) else if top_level then case s of "c_False" => (("$false", s'), []) diff -r a62e01e9b22c -r 626b1d360d42 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Oct 06 13:48:12 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,702 +0,0 @@ -(* Title: HOL/Tools/meson.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - -The MESON resolution proof procedure for HOL. -When making clauses, avoids using the rewriter -- instead uses RS recursively. -*) - -signature MESON = -sig - val trace: bool Unsynchronized.ref - val term_pair_of: indexname * (typ * 'a) -> term * 'a - val size_of_subgoals: thm -> int - val has_too_many_clauses: Proof.context -> term -> bool - val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context - val finish_cnf: thm list -> thm list - val presimplify: thm -> thm - val make_nnf: Proof.context -> thm -> thm - val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm - val skolemize : Proof.context -> thm -> thm - val is_fol_term: theory -> term -> bool - val make_clauses_unsorted: thm list -> thm list - val make_clauses: thm list -> thm list - val make_horns: thm list -> thm list - val best_prolog_tac: (thm -> int) -> thm list -> tactic - val depth_prolog_tac: thm list -> tactic - val gocls: thm list -> thm list - val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic - val MESON: - tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context - -> int -> tactic - val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic - val safe_best_meson_tac: Proof.context -> int -> tactic - val depth_meson_tac: Proof.context -> int -> tactic - val prolog_step_tac': thm list -> int -> tactic - val iter_deepen_prolog_tac: thm list -> tactic - val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic - val make_meta_clause: thm -> thm - val make_meta_clauses: thm list -> thm list - val meson_tac: Proof.context -> thm list -> int -> tactic - val setup: theory -> theory -end - -structure Meson : MESON = -struct - -val trace = Unsynchronized.ref false; -fun trace_msg msg = if ! trace then tracing (msg ()) else (); - -val max_clauses_default = 60; -val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default); - -(*No known example (on 1-5-2007) needs even thirty*) -val iter_deepen_limit = 50; - -val disj_forward = @{thm disj_forward}; -val disj_forward2 = @{thm disj_forward2}; -val make_pos_rule = @{thm make_pos_rule}; -val make_pos_rule' = @{thm make_pos_rule'}; -val make_pos_goal = @{thm make_pos_goal}; -val make_neg_rule = @{thm make_neg_rule}; -val make_neg_rule' = @{thm make_neg_rule'}; -val make_neg_goal = @{thm make_neg_goal}; -val conj_forward = @{thm conj_forward}; -val all_forward = @{thm all_forward}; -val ex_forward = @{thm ex_forward}; - -val not_conjD = @{thm meson_not_conjD}; -val not_disjD = @{thm meson_not_disjD}; -val not_notD = @{thm meson_not_notD}; -val not_allD = @{thm meson_not_allD}; -val not_exD = @{thm meson_not_exD}; -val imp_to_disjD = @{thm meson_imp_to_disjD}; -val not_impD = @{thm meson_not_impD}; -val iff_to_disjD = @{thm meson_iff_to_disjD}; -val not_iffD = @{thm meson_not_iffD}; -val conj_exD1 = @{thm meson_conj_exD1}; -val conj_exD2 = @{thm meson_conj_exD2}; -val disj_exD = @{thm meson_disj_exD}; -val disj_exD1 = @{thm meson_disj_exD1}; -val disj_exD2 = @{thm meson_disj_exD2}; -val disj_assoc = @{thm meson_disj_assoc}; -val disj_comm = @{thm meson_disj_comm}; -val disj_FalseD1 = @{thm meson_disj_FalseD1}; -val disj_FalseD2 = @{thm meson_disj_FalseD2}; - - -(**** Operators for forward proof ****) - - -(** First-order Resolution **) - -fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); - -(*FIXME: currently does not "rename variables apart"*) -fun first_order_resolve thA thB = - (case - try (fn () => - let val thy = theory_of_thm thA - val tmA = concl_of thA - val Const("==>",_) $ tmB $ _ = prop_of thB - val tenv = - Pattern.first_order_match thy (tmB, tmA) - (Vartab.empty, Vartab.empty) |> snd - val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) - in thA RS (cterm_instantiate ct_pairs thB) end) () of - SOME th => th - | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) - -(* Applying "choice" swaps the bound variable names. We tweak - "Thm.rename_boundvars"'s input to get the desired names. *) -fun tweak_bounds (_ $ (Const (@{const_name Ex}, _) - $ Abs (_, _, Const (@{const_name All}, _) $ _))) - (t0 $ (Const (@{const_name All}, T1) - $ Abs (a1, T1', Const (@{const_name Ex}, T2) - $ Abs (a2, T2', t')))) = - t0 $ (Const (@{const_name All}, T1) - $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t'))) - | tweak_bounds _ t = t - -(* Forward proof while preserving bound variables names*) -fun rename_bvs_RS th rl = - let - val th' = th RS rl - val t = concl_of th - val t' = concl_of th' - in Thm.rename_boundvars t' (tweak_bounds t' t) th' end - -(*raises exception if no rules apply*) -fun tryres (th, rls) = - let fun tryall [] = raise THM("tryres", 0, th::rls) - | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls) - in tryall rls end; - -(*Permits forward proof from rules that discharge assumptions. The supplied proof state st, - e.g. from conj_forward, should have the form - "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" - and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) -fun forward_res ctxt nf st = - let fun forward_tacf [prem] = rtac (nf prem) 1 - | forward_tacf prems = - error (cat_lines - ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: - Display.string_of_thm ctxt st :: - "Premises:" :: map (Display.string_of_thm ctxt) prems)) - in - case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st) - of SOME(th,_) => th - | NONE => raise THM("forward_res", 0, [st]) - end; - -(*Are any of the logical connectives in "bs" present in the term?*) -fun has_conns bs = - let fun has (Const _) = false - | has (Const(@{const_name Trueprop},_) $ p) = has p - | has (Const(@{const_name Not},_) $ p) = has p - | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q - | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q - | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p - | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p - | has _ = false - in has end; - - -(**** Clause handling ****) - -fun literals (Const(@{const_name Trueprop},_) $ P) = literals P - | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q - | literals (Const(@{const_name Not},_) $ P) = [(false,P)] - | literals P = [(true,P)]; - -(*number of literals in a term*) -val nliterals = length o literals; - - -(*** Tautology Checking ***) - -fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) = - signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) - | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits) - | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); - -fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); - -(*Literals like X=X are tautologous*) -fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u - | taut_poslit (Const(@{const_name True},_)) = true - | taut_poslit _ = false; - -fun is_taut th = - let val (poslits,neglits) = signed_lits th - in exists taut_poslit poslits - orelse - exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) - end - handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) - - -(*** To remove trivial negated equality literals from clauses ***) - -(*They are typically functional reflexivity axioms and are the converses of - injectivity equivalences*) - -val not_refl_disj_D = @{thm meson_not_refl_disj_D}; - -(*Is either term a Var that does not properly occur in the other term?*) -fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) - | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u)) - | eliminable _ = false; - -fun refl_clause_aux 0 th = th - | refl_clause_aux n th = - case HOLogic.dest_Trueprop (concl_of th) of - (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) => - refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) - | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) => - if eliminable(t,u) - then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*) - else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) - | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) - | _ => (*not a disjunction*) th; - -fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) = - notequal_lits_count P + notequal_lits_count Q - | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1 - | notequal_lits_count _ = 0; - -(*Simplify a clause by applying reflexivity to its negated equality literals*) -fun refl_clause th = - let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) - in zero_var_indexes (refl_clause_aux neqs th) end - handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) - - -(*** Removal of duplicate literals ***) - -(*Forward proof, passing extra assumptions as theorems to the tactic*) -fun forward_res2 nf hyps st = - case Seq.pull - (REPEAT - (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) - st) - of SOME(th,_) => th - | NONE => raise THM("forward_res2", 0, [st]); - -(*Remove duplicates in P|Q by assuming ~P in Q - rls (initially []) accumulates assumptions of the form P==>False*) -fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc) - handle THM _ => tryres(th,rls) - handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2), - [disj_FalseD1, disj_FalseD2, asm_rl]) - handle THM _ => th; - -(*Remove duplicate literals, if there are any*) -fun nodups ctxt th = - if has_duplicates (op =) (literals (prop_of th)) - then nodups_aux ctxt [] th - else th; - - -(*** The basic CNF transformation ***) - -fun estimated_num_clauses bound t = - let - fun sum x y = if x < bound andalso y < bound then x+y else bound - fun prod x y = if x < bound andalso y < bound then x*y else bound - - (*Estimate the number of clauses in order to detect infeasible theorems*) - fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t - | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t - | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) = - if b then sum (signed_nclauses b t) (signed_nclauses b u) - else prod (signed_nclauses b t) (signed_nclauses b u) - | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) = - if b then prod (signed_nclauses b t) (signed_nclauses b u) - else sum (signed_nclauses b t) (signed_nclauses b u) - | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) = - if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) - else sum (signed_nclauses (not b) t) (signed_nclauses b u) - | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) = - if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*) - if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) - (prod (signed_nclauses (not b) u) (signed_nclauses b t)) - else sum (prod (signed_nclauses b t) (signed_nclauses b u)) - (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) - else 1 - | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t - | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t - | signed_nclauses _ _ = 1; (* literal *) - in signed_nclauses true t end - -fun has_too_many_clauses ctxt t = - let val max_cl = Config.get ctxt max_clauses in - estimated_num_clauses (max_cl + 1) t > max_cl - end - -(*Replaces universally quantified variables by FREE variables -- because - assumptions may not contain scheme variables. Later, generalize using Variable.export. *) -local - val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))); - val spec_varT = #T (Thm.rep_cterm spec_var); - fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu; -in - fun freeze_spec th ctxt = - let - val cert = Thm.cterm_of (ProofContext.theory_of ctxt); - val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; - val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; - in (th RS spec', ctxt') end -end; - -(*Used with METAHYPS below. There is one assumption, which gets bound to prem - and then normalized via function nf. The normal form is given to resolve_tac, - instantiate a Boolean variable created by resolution with disj_forward. Since - (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) -fun resop nf [prem] = resolve_tac (nf prem) 1; - -(* Any need to extend this list with "HOL.type_class", "HOL.eq_class", - and "Pure.term"? *) -val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); - -fun apply_skolem_theorem (th, rls) = - let - fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) - | tryall (rl :: rls) = - first_order_resolve th rl handle THM _ => tryall rls - in tryall rls end - -(* Conjunctive normal form, adding clauses from th in front of ths (for foldr). - Strips universal quantifiers and breaks up conjunctions. - Eliminates existential quantifiers using Skolemization theorems. *) -fun cnf old_skolem_ths ctxt (th, ths) = - let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *) - fun cnf_aux (th,ths) = - if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) - else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th)) - then nodups ctxt th :: ths (*no work to do, terminate*) - else case head_of (HOLogic.dest_Trueprop (concl_of th)) of - Const (@{const_name HOL.conj}, _) => (*conjunction*) - cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) - | Const (@{const_name All}, _) => (*universal quantifier*) - let val (th',ctxt') = freeze_spec th (!ctxtr) - in ctxtr := ctxt'; cnf_aux (th', ths) end - | Const (@{const_name Ex}, _) => - (*existential quantifier: Insert Skolem functions*) - cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) - | Const (@{const_name HOL.disj}, _) => - (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using - all combinations of converting P, Q to CNF.*) - let val tac = - Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN - (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1) - in Seq.list_of (tac (th RS disj_forward)) @ ths end - | _ => nodups ctxt th :: ths (*no work to do*) - and cnf_nil th = cnf_aux (th,[]) - val cls = - if has_too_many_clauses ctxt (concl_of th) - then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) - else cnf_aux (th,ths) - in (cls, !ctxtr) end; - -fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, []) - -(*Generalization, removal of redundant equalities, removal of tautologies.*) -fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths); - - -(**** Generation of contrapositives ****) - -fun is_left (Const (@{const_name Trueprop}, _) $ - (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true - | is_left _ = false; - -(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) -fun assoc_right th = - if is_left (prop_of th) then assoc_right (th RS disj_assoc) - else th; - -(*Must check for negative literal first!*) -val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; - -(*For ordinary resolution. *) -val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; - -(*Create a goal or support clause, conclusing False*) -fun make_goal th = (*Must check for negative literal first!*) - make_goal (tryres(th, clause_rules)) - handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); - -(*Sort clauses by number of literals*) -fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); - -fun sort_clauses ths = sort (make_ord fewerlits) ths; - -fun has_bool @{typ bool} = true - | has_bool (Type (_, Ts)) = exists has_bool Ts - | has_bool _ = false - -fun has_fun (Type (@{type_name fun}, _)) = true - | has_fun (Type (_, Ts)) = exists has_fun Ts - | has_fun _ = false - -(*Is the string the name of a connective? Really only | and Not can remain, - since this code expects to be called on a clause form.*) -val is_conn = member (op =) - [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, - @{const_name HOL.implies}, @{const_name Not}, - @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}]; - -(*True if the term contains a function--not a logical connective--where the type - of any argument contains bool.*) -val has_bool_arg_const = - exists_Const - (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T)); - -(*A higher-order instance of a first-order constant? Example is the definition of - one, 1, at a function type in theory Function_Algebras.*) -fun higher_inst_const thy (c,T) = - case binder_types T of - [] => false (*not a function type, OK*) - | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts; - -(*Returns false if any Vars in the theorem mention type bool. - Also rejects functions whose arguments are Booleans or other functions.*) -fun is_fol_term thy t = - Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso - not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T - | _ => false) t orelse - has_bool_arg_const t orelse - exists_Const (higher_inst_const thy) t orelse - has_meta_conn t); - -fun rigid t = not (is_Var (head_of t)); - -fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t - | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t - | ok4horn _ = false; - -(*Create a meta-level Horn clause*) -fun make_horn crules th = - if ok4horn (concl_of th) - then make_horn crules (tryres(th,crules)) handle THM _ => th - else th; - -(*Generate Horn clauses for all contrapositives of a clause. The input, th, - is a HOL disjunction.*) -fun add_contras crules th hcs = - let fun rots (0,_) = hcs - | rots (k,th) = zero_var_indexes (make_horn crules th) :: - rots(k-1, assoc_right (th RS disj_comm)) - in case nliterals(prop_of th) of - 1 => th::hcs - | n => rots(n, assoc_right th) - end; - -(*Use "theorem naming" to label the clauses*) -fun name_thms label = - let fun name1 th (k, ths) = - (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) - in fn ths => #2 (fold_rev name1 ths (length ths, [])) end; - -(*Is the given disjunction an all-negative support clause?*) -fun is_negative th = forall (not o #1) (literals (prop_of th)); - -val neg_clauses = filter is_negative; - - -(***** MESON PROOF PROCEDURE *****) - -fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi, - As) = rhyps(phi, A::As) - | rhyps (_, As) = As; - -(** Detecting repeated assumptions in a subgoal **) - -(*The stringtree detects repeated assumptions.*) -fun ins_term t net = Net.insert_term (op aconv) (t, t) net; - -(*detects repetitions in a list of terms*) -fun has_reps [] = false - | has_reps [_] = false - | has_reps [t,u] = (t aconv u) - | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true; - -(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) -fun TRYING_eq_assume_tac 0 st = Seq.single st - | TRYING_eq_assume_tac i st = - TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st) - handle THM _ => TRYING_eq_assume_tac (i-1) st; - -fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st; - -(*Loop checking: FAIL if trying to prove the same thing twice - -- if *ANY* subgoal has repeated literals*) -fun check_tac st = - if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) - then Seq.empty else Seq.single st; - - -(* net_resolve_tac actually made it slower... *) -fun prolog_step_tac horns i = - (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN - TRYALL_eq_assume_tac; - -(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) -fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz; - -fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0; - - -(*Negation Normal Form*) -val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, - not_impD, not_iffD, not_allD, not_exD, not_notD]; - -fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t - | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t - | ok4nnf _ = false; - -fun make_nnf1 ctxt th = - if ok4nnf (concl_of th) - then make_nnf1 ctxt (tryres(th, nnf_rls)) - handle THM ("tryres", _, _) => - forward_res ctxt (make_nnf1 ctxt) - (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) - handle THM ("tryres", _, _) => th - else th - -(*The simplification removes defined quantifiers and occurrences of True and False. - nnf_ss also includes the one-point simprocs, - which are needed to avoid the various one-point theorems from generating junk clauses.*) -val nnf_simps = - @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel - if_eq_cancel cases_simp} -val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms} - -val nnf_ss = - HOL_basic_ss addsimps nnf_extra_simps - addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; - -val presimplify = - rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss - -fun make_nnf ctxt th = case prems_of th of - [] => th |> presimplify |> make_nnf1 ctxt - | _ => raise THM ("make_nnf: premises in argument", 0, [th]); - -(* Pull existential quantifiers to front. This accomplishes Skolemization for - clauses that arise from a subgoal. *) -fun skolemize_with_choice_thms ctxt choice_ths = - let - fun aux th = - if not (has_conns [@{const_name Ex}] (prop_of th)) then - th - else - tryres (th, choice_ths @ - [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]) - |> aux - handle THM ("tryres", _, _) => - tryres (th, [conj_forward, disj_forward, all_forward]) - |> forward_res ctxt aux - |> aux - handle THM ("tryres", _, _) => - rename_bvs_RS th ex_forward - |> forward_res ctxt aux - in aux o make_nnf ctxt end - -fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt) - -(* "RS" can fail if "unify_search_bound" is too small. *) -fun try_skolemize ctxt th = - try (skolemize ctxt) th - |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^ - Display.string_of_thm ctxt th) - | _ => ()) - -fun add_clauses th cls = - let val ctxt0 = Variable.global_thm_context th - val (cnfs, ctxt) = make_cnf [] th ctxt0 - in Variable.export ctxt ctxt0 cnfs @ cls end; - -(*Make clauses from a list of theorems, previously Skolemized and put into nnf. - The resulting clauses are HOL disjunctions.*) -fun make_clauses_unsorted ths = fold_rev add_clauses ths []; -val make_clauses = sort_clauses o make_clauses_unsorted; - -(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) -fun make_horns ths = - name_thms "Horn#" - (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths [])); - -(*Could simply use nprems_of, which would count remaining subgoals -- no - discrimination as to their size! With BEST_FIRST, fails for problem 41.*) - -fun best_prolog_tac sizef horns = - BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); - -fun depth_prolog_tac horns = - DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); - -(*Return all negative clauses, as possible goal clauses*) -fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); - -fun skolemize_prems_tac ctxt prems = - cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE - -(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. - Function mkcl converts theorems to clauses.*) -fun MESON preskolem_tac mkcl cltac ctxt i st = - SELECT_GOAL - (EVERY [Object_Logic.atomize_prems_tac 1, - rtac ccontr 1, - preskolem_tac, - Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => - EVERY1 [skolemize_prems_tac ctxt negs, - Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st - handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) - - -(** Best-first search versions **) - -(*ths is a list of additional clauses (HOL disjunctions) to use.*) -fun best_meson_tac sizef = - MESON all_tac make_clauses - (fn cls => - THEN_BEST_FIRST (resolve_tac (gocls cls) 1) - (has_fewer_prems 1, sizef) - (prolog_step_tac (make_horns cls) 1)); - -(*First, breaks the goal into independent units*) -fun safe_best_meson_tac ctxt = - SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN - TRYALL (best_meson_tac size_of_subgoals ctxt)); - -(** Depth-first search version **) - -val depth_meson_tac = - MESON all_tac make_clauses - (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]); - - -(** Iterative deepening version **) - -(*This version does only one inference per call; - having only one eq_assume_tac speeds it up!*) -fun prolog_step_tac' horns = - let val (horn0s, _) = (*0 subgoals vs 1 or more*) - take_prefix Thm.no_prems horns - val nrtac = net_resolve_tac horns - in fn i => eq_assume_tac i ORELSE - match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) - ((assume_tac i APPEND nrtac i) THEN check_tac) - end; - -fun iter_deepen_prolog_tac horns = - ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns); - -fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses - (fn cls => - (case (gocls (cls @ ths)) of - [] => no_tac (*no goal clauses*) - | goes => - let - val horns = make_horns (cls @ ths) - val _ = trace_msg (fn () => - cat_lines ("meson method called:" :: - map (Display.string_of_thm ctxt) (cls @ ths) @ - ["clauses:"] @ map (Display.string_of_thm ctxt) horns)) - in - THEN_ITER_DEEPEN iter_deepen_limit - (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) - end)); - -fun meson_tac ctxt ths = - SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); - - -(**** Code to support ordinary resolution, rather than Model Elimination ****) - -(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), - with no contrapositives, for ordinary resolution.*) - -(*Rules to convert the head literal into a negated assumption. If the head - literal is already negated, then using notEfalse instead of notEfalse' - prevents a double negation.*) -val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE; -val notEfalse' = rotate_prems 1 notEfalse; - -fun negated_asm_of_head th = - th RS notEfalse handle THM _ => th RS notEfalse'; - -(*Converting one theorem from a disjunction to a meta-level clause*) -fun make_meta_clause th = - let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th - in - (zero_var_indexes o Thm.varifyT_global o thaw 0 o - negated_asm_of_head o make_horn resolution_clause_rules) fth - end; - -fun make_meta_clauses ths = - name_thms "MClause#" - (distinct Thm.eq_thm_prop (map make_meta_clause ths)); - -end;