proof reconstruction for external ATPs
authorpaulson
Fri Aug 20 12:21:03 2004 +0200 (2004-08-20)
changeset 15151429666b09783
parent 15150 c7af682b9ee5
child 15152 5c4d3f10ac5a
proof reconstruction for external ATPs
src/HOL/Main.thy
src/HOL/Reconstruction.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/reconstruction.ML
src/HOL/ex/Classical.thy
src/HOL/hologic.ML
     1.1 --- a/src/HOL/Main.thy	Fri Aug 20 12:20:09 2004 +0200
     1.2 +++ b/src/HOL/Main.thy	Fri Aug 20 12:21:03 2004 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Map Infinite_Set Extraction Refute
     1.8 +    imports Map Infinite_Set Extraction Refute Reconstruction
     1.9 +
    1.10  begin
    1.11  
    1.12  text {*
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Reconstruction.thy	Fri Aug 20 12:21:03 2004 +0200
     2.3 @@ -0,0 +1,17 @@
     2.4 +(*  Title:      HOL/Reconstruction.thy
     2.5 +    ID: $Id$
     2.6 +    Author:     Lawrence C Paulson
     2.7 +    Copyright   2004  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +header{*Attributes for Reconstructing External Resolution Proofs*}
    2.11 +
    2.12 +theory Reconstruction
    2.13 +    imports Hilbert_Choice
    2.14 +    files   "Tools/reconstruction.ML"
    2.15 +
    2.16 +begin
    2.17 +
    2.18 +setup Reconstruction.setup
    2.19 +
    2.20 +end
    2.21 \ No newline at end of file
     3.1 --- a/src/HOL/Tools/meson.ML	Fri Aug 20 12:20:09 2004 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Fri Aug 20 12:21:03 2004 +0200
     3.3 @@ -408,7 +408,7 @@
     3.4       in EVERY1 
     3.5  	 [METAHYPS
     3.6  	    (fn hyps => 
     3.7 -              (cut_rules_tac
     3.8 +              (Method.insert_tac
     3.9                  (map forall_intr_vars 
    3.10                    (make_meta_clauses (make_clauses hyps))) 1)),
    3.11  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/reconstruction.ML	Fri Aug 20 12:21:03 2004 +0200
     4.3 @@ -0,0 +1,178 @@
     4.4 +(*  Title:      HOL/Reconstruction.thy
     4.5 +    ID: $Id$
     4.6 +    Author:     Lawrence C Paulson and Claire Quigley
     4.7 +    Copyright   2004  University of Cambridge
     4.8 +*)
     4.9 +
    4.10 +(*Attributes for reconstructing external resolution proofs*)
    4.11 +
    4.12 +structure Reconstruction =
    4.13 +let open Attrib
    4.14 +in
    4.15 +struct
    4.16 +
    4.17 +(**************************************************************)
    4.18 +(* extra functions necessary for factoring and paramodulation *)
    4.19 +(**************************************************************)
    4.20 +
    4.21 +fun mksubstlist [] sublist = sublist
    4.22 +  | mksubstlist ((a,b)::rest) sublist = 
    4.23 +      let val vartype = type_of b
    4.24 +          val avar = Var(a,vartype)
    4.25 +          val newlist = ((avar,b)::sublist) 
    4.26 +      in mksubstlist rest newlist end;
    4.27 +
    4.28 +
    4.29 +fun get_unif_comb t eqterm =
    4.30 +    if ((type_of t) = (type_of eqterm))
    4.31 +    then t
    4.32 +    else
    4.33 +        let val _ $ rand = t
    4.34 +        in get_unif_comb rand eqterm end;
    4.35 +
    4.36 +fun get_unif_lit t eqterm =
    4.37 +    if (can HOLogic.dest_eq t)
    4.38 +    then
    4.39 +	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
    4.40 +	in lhs end
    4.41 +    else
    4.42 +	get_unif_comb t eqterm;
    4.43 +
    4.44 +
    4.45 +
    4.46 +(**** attributes ****)
    4.47 +
    4.48 +(** Binary resolution **)
    4.49 +
    4.50 +fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
    4.51 +     select_literal (lit1 + 1) cl1
    4.52 +     RSN ((lit2 + 1), cl2);
    4.53 +
    4.54 +fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
    4.55 +
    4.56 +fun gen_BINARY thm = syntax
    4.57 +      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
    4.58 +val BINARY_global = gen_BINARY global_thm;
    4.59 +val BINARY_local = gen_BINARY local_thm;
    4.60 +
    4.61 +(*I have not done the MRR rule because it seems to be identifical to 
    4.62 +BINARY*)
    4.63 +
    4.64 +
    4.65 +fun inst_single sign t1 t2 cl =
    4.66 +    let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
    4.67 +    in  hd (Seq.list_of(distinct_subgoals_tac
    4.68 +			    (cterm_instantiate [(ct1,ct2)] cl)))  
    4.69 +    end;
    4.70 +
    4.71 +fun inst_subst sign substs cl =
    4.72 +    if (is_Var (fst(hd(substs))))
    4.73 +    then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
    4.74 +    else if (is_Var (snd(hd(substs))))
    4.75 +    then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
    4.76 +    else raise THM ("inst_subst", 0, [cl]);
    4.77 +
    4.78 +(*Grabs the environment from the result of Unify.unifiers*)
    4.79 +fun getnewenv thisseq = fst (hd (Seq.list_of thisseq));
    4.80 +
    4.81 +(** Factoring **)
    4.82 +
    4.83 +fun factor_rule (cl, lit1, lit2) =
    4.84 +    let
    4.85 +       val prems = prems_of cl
    4.86 +       val fac1 = List.nth (prems,lit1)
    4.87 +       val fac2 = List.nth (prems,lit2)
    4.88 +       val sign = sign_of_thm cl
    4.89 +       val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
    4.90 +       val newenv = getnewenv unif_env
    4.91 +       val envlist = Envir.alist_of newenv
    4.92 +     in
    4.93 +       inst_subst sign (mksubstlist envlist []) cl
    4.94 +    end;
    4.95 +
    4.96 +fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
    4.97 +
    4.98 +fun FACTOR x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
    4.99 +
   4.100 +
   4.101 +(** Paramodulation **)
   4.102 +
   4.103 +(*Get rid of a Not if it is present*)
   4.104 +fun maybe_dest_not (Const ("Not", _) $ t) = t
   4.105 +  | maybe_dest_not t = t;
   4.106 +
   4.107 +fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
   4.108 +    let val prems1 = prems_of cl1
   4.109 +	val prems2 = prems_of cl2
   4.110 +        val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2)
   4.111 +	(* want to get first element of equality *)
   4.112 +
   4.113 +	val fac1 = List.nth (prems1,lit1) 
   4.114 +	val (lhs, rhs) = HOLogic.dest_eq(maybe_dest_not
   4.115 +					     (HOLogic.dest_Trueprop fac1))
   4.116 +	(* get other literal involved in the paramodulation *)
   4.117 +	val fac2 = List.nth (prems2,lit2) 
   4.118 +
   4.119 +       (* get bit of th2 to unify with lhs of cl1 *)
   4.120 +	val unif_lit = get_unif_lit (HOLogic.dest_Trueprop fac2) lhs
   4.121 +	val unif_env = Unify.unifiers (sign, Envir.empty 0, [(unif_lit, lhs)])
   4.122 +	val newenv = getnewenv unif_env
   4.123 +	val envlist = Envir.alist_of newenv
   4.124 +       (* instantiate cl2 with unifiers *)
   4.125 +
   4.126 +	val newth1 = inst_subst sign (mksubstlist envlist []) cl1
   4.127 +       (*rewrite cl2 with the equality bit of cl2 i.e. lit2 *)
   4.128 +	  val facthm' = select_literal (lit1 + 1) newth1
   4.129 +	  val equal_lit = concl_of facthm'
   4.130 +	  val cterm_eq = cterm_of sign equal_lit
   4.131 +	  val eq_thm = assume cterm_eq
   4.132 +	  val meta_eq_thm = mk_meta_eq eq_thm
   4.133 +	  val newth2= rewrite_rule [meta_eq_thm] cl2
   4.134 +       (*thin lit2 from cl2 *)
   4.135 +       (* get cl1 with lit1 as concl, then resolve with thin_rl *)
   4.136 +	  val thm' = facthm' RS thin_rl
   4.137 +       (* now resolve cl2 with last premise of thm' *)
   4.138 +	  val newthm = newth2  RSN ((length prems1), thm')
   4.139 +     in newthm end
   4.140 +
   4.141 +
   4.142 +fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
   4.143 +
   4.144 +fun gen_PARAMOD thm = syntax
   4.145 +      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
   4.146 +val PARAMOD_global = gen_PARAMOD global_thm;
   4.147 +val PARAMOD_local = gen_PARAMOD local_thm;
   4.148 +
   4.149 +
   4.150 +(** Demodulation, i.e. rewriting **)
   4.151 +
   4.152 +fun demod_rule (cl1,lit1,cl2) =
   4.153 +    let  val eq_lit_th = select_literal (lit1+1) cl1
   4.154 +	 val equal_lit = concl_of eq_lit_th
   4.155 +         val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2)
   4.156 +	 val cterm_eq = cterm_of sign equal_lit
   4.157 +	 val eq_thm = assume cterm_eq
   4.158 +	 val meta_eq_thm = mk_meta_eq eq_thm
   4.159 +	 val newth2= rewrite_rule [meta_eq_thm] cl2
   4.160 +    in newth2 end;
   4.161 +
   4.162 +fun demod_syntax (i, B) (x, A) = (x, demod_rule (A,i,B));
   4.163 +
   4.164 +fun gen_DEMOD thm = syntax ((Scan.lift Args.nat -- thm) >> demod_syntax);
   4.165 +val DEMOD_global = gen_DEMOD global_thm;
   4.166 +val DEMOD_local = gen_DEMOD local_thm;
   4.167 +
   4.168 +
   4.169 +(** theory setup **)
   4.170 +
   4.171 +val setup =
   4.172 +  [Attrib.add_attributes
   4.173 +     [("BINARY", (BINARY_global, BINARY_local), "binary resolution"),
   4.174 +      ("PARAMOD", (PARAMOD_global, PARAMOD_local), "paramodulation"),
   4.175 +      ("DEMOD", (DEMOD_global, DEMOD_local), "demodulation"),
   4.176 +      ("FACTOR", (FACTOR, FACTOR), "factoring")]];
   4.177 +
   4.178 +end
   4.179 +end
   4.180 +
   4.181 +
     5.1 --- a/src/HOL/ex/Classical.thy	Fri Aug 20 12:20:09 2004 +0200
     5.2 +++ b/src/HOL/ex/Classical.thy	Fri Aug 20 12:21:03 2004 +0200
     5.3 @@ -743,6 +743,11 @@
     5.4  lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
     5.5  by meson
     5.6  
     5.7 +text{*Problem 54: NOT PROVED*}
     5.8 +lemma "(\<forall>y::'a. \<exists>z. \<forall>x. F x z = (x=y)) -->
     5.9 +      ~ (\<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 
    5.10 +
    5.11 +
    5.12  text{*Problem 55*}
    5.13  
    5.14  text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
    5.15 @@ -781,7 +786,6 @@
    5.16              (~ p a | ~ p(f x) | p(f(f x))))"
    5.17  by meson
    5.18  
    5.19 -
    5.20  text{*A manual resolution proof of problem 19.*}
    5.21  lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
    5.22  proof (rule ccontr, skolemize, make_clauses)
    5.23 @@ -790,10 +794,9 @@
    5.24       and Q: "\<And>U. Q U \<Longrightarrow> False"
    5.25       and PQ: "\<And>U.  \<lbrakk>P (f U); \<not> Q (g U)\<rbrakk> \<Longrightarrow> False"
    5.26    have cl4: "\<And>U. \<not> Q (g U) \<Longrightarrow> False"
    5.27 -    by (blast intro: P PQ)
    5.28 -       --{*Temporary: to be replaced by resolution attributes*}
    5.29 -  show False
    5.30 -    by (blast intro: Q cl4)
    5.31 +    by (rule P [BINARY 0 PQ 0])
    5.32 +  show "False"
    5.33 +    by (rule Q [BINARY 0 cl4 0])
    5.34  qed
    5.35  
    5.36  end
     6.1 --- a/src/HOL/hologic.ML	Fri Aug 20 12:20:09 2004 +0200
     6.2 +++ b/src/HOL/hologic.ML	Fri Aug 20 12:21:03 2004 +0200
     6.3 @@ -26,8 +26,9 @@
     6.4    val mk_conj: term * term -> term
     6.5    val mk_disj: term * term -> term
     6.6    val mk_imp: term * term -> term
     6.7 +  val dest_conj: term -> term list
     6.8    val dest_imp: term -> term * term
     6.9 -  val dest_conj: term -> term list
    6.10 +  val dest_not: term -> term
    6.11    val dest_concls: term -> term list
    6.12    val eq_const: typ -> term
    6.13    val all_const: typ -> term
    6.14 @@ -127,11 +128,14 @@
    6.15  and mk_disj (t1, t2) = disj $ t1 $ t2
    6.16  and mk_imp (t1, t2) = imp $ t1 $ t2;
    6.17  
    6.18 +fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
    6.19 +  | dest_conj t = [t];
    6.20 +
    6.21  fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
    6.22    | dest_imp  t = raise TERM ("dest_imp", [t]);
    6.23  
    6.24 -fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
    6.25 -  | dest_conj t = [t];
    6.26 +fun dest_not (Const ("Not", _) $ t) = t
    6.27 +  | dest_not t = raise TERM ("dest_not", [t]);
    6.28  
    6.29  fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t;
    6.30  val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop;