--- 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 {*
--- /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
--- 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)]
--- /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
+
+
--- 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 "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
by meson
+text{*Problem 54: NOT PROVED*}
+lemma "(\<forall>y::'a. \<exists>z. \<forall>x. F x z = (x=y)) -->
+ ~ (\<exists>w. \<forall>x. F x w = (\<forall>u. F x u --> (\<exists>y. F y u & ~ (\<exists>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 "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
proof (rule ccontr, skolemize, make_clauses)
@@ -790,10 +794,9 @@
and Q: "\<And>U. Q U \<Longrightarrow> False"
and PQ: "\<And>U. \<lbrakk>P (f U); \<not> Q (g U)\<rbrakk> \<Longrightarrow> False"
have cl4: "\<And>U. \<not> Q (g U) \<Longrightarrow> 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
--- 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;