# HG changeset patch # User paulson # Date 1092997263 -7200 # Node ID 429666b097838ef968352b5a47dbc31b5a65e50d # Parent c7af682b9ee5f256996affa247ef25a204a2b242 proof reconstruction for external ATPs diff -r c7af682b9ee5 -r 429666b09783 src/HOL/Main.thy --- a/src/HOL/Main.thy Fri Aug 20 12:20:09 2004 +0200 +++ b/src/HOL/Main.thy Fri Aug 20 12:21:03 2004 +0200 @@ -6,7 +6,8 @@ header {* Main HOL *} theory Main -imports Map Infinite_Set Extraction Refute + imports Map Infinite_Set Extraction Refute Reconstruction + begin text {* diff -r c7af682b9ee5 -r 429666b09783 src/HOL/Reconstruction.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Reconstruction.thy Fri Aug 20 12:21:03 2004 +0200 @@ -0,0 +1,17 @@ +(* Title: HOL/Reconstruction.thy + ID: $Id$ + Author: Lawrence C Paulson + Copyright 2004 University of Cambridge +*) + +header{*Attributes for Reconstructing External Resolution Proofs*} + +theory Reconstruction + imports Hilbert_Choice + files "Tools/reconstruction.ML" + +begin + +setup Reconstruction.setup + +end \ No newline at end of file diff -r c7af682b9ee5 -r 429666b09783 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Aug 20 12:20:09 2004 +0200 +++ b/src/HOL/Tools/meson.ML Fri Aug 20 12:21:03 2004 +0200 @@ -408,7 +408,7 @@ in EVERY1 [METAHYPS (fn hyps => - (cut_rules_tac + (Method.insert_tac (map forall_intr_vars (make_meta_clauses (make_clauses hyps))) 1)), REPEAT_DETERM_N (length ts) o (etac thin_rl)] diff -r c7af682b9ee5 -r 429666b09783 src/HOL/Tools/reconstruction.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/reconstruction.ML Fri Aug 20 12:21:03 2004 +0200 @@ -0,0 +1,178 @@ +(* Title: HOL/Reconstruction.thy + ID: $Id$ + Author: Lawrence C Paulson and Claire Quigley + Copyright 2004 University of Cambridge +*) + +(*Attributes for reconstructing external resolution proofs*) + +structure Reconstruction = +let open Attrib +in +struct + +(**************************************************************) +(* extra functions necessary for factoring and paramodulation *) +(**************************************************************) + +fun mksubstlist [] sublist = sublist + | mksubstlist ((a,b)::rest) sublist = + let val vartype = type_of b + val avar = Var(a,vartype) + val newlist = ((avar,b)::sublist) + in mksubstlist rest newlist end; + + +fun get_unif_comb t eqterm = + if ((type_of t) = (type_of eqterm)) + then t + else + let val _ $ rand = t + in get_unif_comb rand eqterm end; + +fun get_unif_lit t eqterm = + if (can HOLogic.dest_eq t) + then + let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm) + in lhs end + else + get_unif_comb t eqterm; + + + +(**** attributes ****) + +(** Binary resolution **) + +fun binary_rule ((cl1, lit1), (cl2 , lit2)) = + select_literal (lit1 + 1) cl1 + RSN ((lit2 + 1), cl2); + +fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j))); + +fun gen_BINARY thm = syntax + ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax); +val BINARY_global = gen_BINARY global_thm; +val BINARY_local = gen_BINARY local_thm; + +(*I have not done the MRR rule because it seems to be identifical to +BINARY*) + + +fun inst_single sign t1 t2 cl = + let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2 + in hd (Seq.list_of(distinct_subgoals_tac + (cterm_instantiate [(ct1,ct2)] cl))) + end; + +fun inst_subst sign substs cl = + if (is_Var (fst(hd(substs)))) + then inst_single sign (fst (hd substs)) (snd (hd substs)) cl + else if (is_Var (snd(hd(substs)))) + then inst_single sign (snd (hd substs)) (fst (hd substs)) cl + else raise THM ("inst_subst", 0, [cl]); + +(*Grabs the environment from the result of Unify.unifiers*) +fun getnewenv thisseq = fst (hd (Seq.list_of thisseq)); + +(** Factoring **) + +fun factor_rule (cl, lit1, lit2) = + let + val prems = prems_of cl + val fac1 = List.nth (prems,lit1) + val fac2 = List.nth (prems,lit2) + val sign = sign_of_thm cl + val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)]) + val newenv = getnewenv unif_env + val envlist = Envir.alist_of newenv + in + inst_subst sign (mksubstlist envlist []) cl + end; + +fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j)); + +fun FACTOR x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x; + + +(** Paramodulation **) + +(*Get rid of a Not if it is present*) +fun maybe_dest_not (Const ("Not", _) $ t) = t + | maybe_dest_not t = t; + +fun paramod_rule ((cl1, lit1), (cl2 , lit2)) = + let val prems1 = prems_of cl1 + val prems2 = prems_of cl2 + val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2) + (* want to get first element of equality *) + + val fac1 = List.nth (prems1,lit1) + val (lhs, rhs) = HOLogic.dest_eq(maybe_dest_not + (HOLogic.dest_Trueprop fac1)) + (* get other literal involved in the paramodulation *) + val fac2 = List.nth (prems2,lit2) + + (* get bit of th2 to unify with lhs of cl1 *) + val unif_lit = get_unif_lit (HOLogic.dest_Trueprop fac2) lhs + val unif_env = Unify.unifiers (sign, Envir.empty 0, [(unif_lit, lhs)]) + val newenv = getnewenv unif_env + val envlist = Envir.alist_of newenv + (* instantiate cl2 with unifiers *) + + val newth1 = inst_subst sign (mksubstlist envlist []) cl1 + (*rewrite cl2 with the equality bit of cl2 i.e. lit2 *) + val facthm' = select_literal (lit1 + 1) newth1 + val equal_lit = concl_of facthm' + val cterm_eq = cterm_of sign equal_lit + val eq_thm = assume cterm_eq + val meta_eq_thm = mk_meta_eq eq_thm + val newth2= rewrite_rule [meta_eq_thm] cl2 + (*thin lit2 from cl2 *) + (* get cl1 with lit1 as concl, then resolve with thin_rl *) + val thm' = facthm' RS thin_rl + (* now resolve cl2 with last premise of thm' *) + val newthm = newth2 RSN ((length prems1), thm') + in newthm end + + +fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j))); + +fun gen_PARAMOD thm = syntax + ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax); +val PARAMOD_global = gen_PARAMOD global_thm; +val PARAMOD_local = gen_PARAMOD local_thm; + + +(** Demodulation, i.e. rewriting **) + +fun demod_rule (cl1,lit1,cl2) = + let val eq_lit_th = select_literal (lit1+1) cl1 + val equal_lit = concl_of eq_lit_th + val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2) + val cterm_eq = cterm_of sign equal_lit + val eq_thm = assume cterm_eq + val meta_eq_thm = mk_meta_eq eq_thm + val newth2= rewrite_rule [meta_eq_thm] cl2 + in newth2 end; + +fun demod_syntax (i, B) (x, A) = (x, demod_rule (A,i,B)); + +fun gen_DEMOD thm = syntax ((Scan.lift Args.nat -- thm) >> demod_syntax); +val DEMOD_global = gen_DEMOD global_thm; +val DEMOD_local = gen_DEMOD local_thm; + + +(** theory setup **) + +val setup = + [Attrib.add_attributes + [("BINARY", (BINARY_global, BINARY_local), "binary resolution"), + ("PARAMOD", (PARAMOD_global, PARAMOD_local), "paramodulation"), + ("DEMOD", (DEMOD_global, DEMOD_local), "demodulation"), + ("FACTOR", (FACTOR, FACTOR), "factoring")]]; + +end +end + + diff -r c7af682b9ee5 -r 429666b09783 src/HOL/ex/Classical.thy --- a/src/HOL/ex/Classical.thy Fri Aug 20 12:20:09 2004 +0200 +++ b/src/HOL/ex/Classical.thy Fri Aug 20 12:21:03 2004 +0200 @@ -743,6 +743,11 @@ lemma "(\x. P a x | (\y. P x y)) --> (\x. \y. P x y)" by meson +text{*Problem 54: NOT PROVED*} +lemma "(\y::'a. \z. \x. F x z = (x=y)) --> + ~ (\w. \x. F x w = (\u. F x u --> (\y. F y u & ~ (\z. F z u & F z y))))"oops + + text{*Problem 55*} text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). @@ -781,7 +786,6 @@ (~ p a | ~ p(f x) | p(f(f x))))" by meson - text{*A manual resolution proof of problem 19.*} lemma "\x. \y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" proof (rule ccontr, skolemize, make_clauses) @@ -790,10 +794,9 @@ and Q: "\U. Q U \ False" and PQ: "\U. \P (f U); \ Q (g U)\ \ False" have cl4: "\U. \ Q (g U) \ False" - by (blast intro: P PQ) - --{*Temporary: to be replaced by resolution attributes*} - show False - by (blast intro: Q cl4) + by (rule P [BINARY 0 PQ 0]) + show "False" + by (rule Q [BINARY 0 cl4 0]) qed end diff -r c7af682b9ee5 -r 429666b09783 src/HOL/hologic.ML --- a/src/HOL/hologic.ML Fri Aug 20 12:20:09 2004 +0200 +++ b/src/HOL/hologic.ML Fri Aug 20 12:21:03 2004 +0200 @@ -26,8 +26,9 @@ val mk_conj: term * term -> term val mk_disj: term * term -> term val mk_imp: term * term -> term + val dest_conj: term -> term list val dest_imp: term -> term * term - val dest_conj: term -> term list + val dest_not: term -> term val dest_concls: term -> term list val eq_const: typ -> term val all_const: typ -> term @@ -127,11 +128,14 @@ and mk_disj (t1, t2) = disj $ t1 $ t2 and mk_imp (t1, t2) = imp $ t1 $ t2; +fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t' + | dest_conj t = [t]; + fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) | dest_imp t = raise TERM ("dest_imp", [t]); -fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t' - | dest_conj t = [t]; +fun dest_not (Const ("Not", _) $ t) = t + | dest_not t = raise TERM ("dest_not", [t]); fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t; val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop;