src/HOL/Tools/reconstruction.ML
author paulson
Fri Aug 20 12:21:03 2004 +0200 (2004-08-20)
changeset 15151 429666b09783
child 15359 8bad1f42fec0
permissions -rw-r--r--
proof reconstruction for external ATPs
paulson@15151
     1
(*  Title:      HOL/Reconstruction.thy
paulson@15151
     2
    ID: $Id$
paulson@15151
     3
    Author:     Lawrence C Paulson and Claire Quigley
paulson@15151
     4
    Copyright   2004  University of Cambridge
paulson@15151
     5
*)
paulson@15151
     6
paulson@15151
     7
(*Attributes for reconstructing external resolution proofs*)
paulson@15151
     8
paulson@15151
     9
structure Reconstruction =
paulson@15151
    10
let open Attrib
paulson@15151
    11
in
paulson@15151
    12
struct
paulson@15151
    13
paulson@15151
    14
(**************************************************************)
paulson@15151
    15
(* extra functions necessary for factoring and paramodulation *)
paulson@15151
    16
(**************************************************************)
paulson@15151
    17
paulson@15151
    18
fun mksubstlist [] sublist = sublist
paulson@15151
    19
  | mksubstlist ((a,b)::rest) sublist = 
paulson@15151
    20
      let val vartype = type_of b
paulson@15151
    21
          val avar = Var(a,vartype)
paulson@15151
    22
          val newlist = ((avar,b)::sublist) 
paulson@15151
    23
      in mksubstlist rest newlist end;
paulson@15151
    24
paulson@15151
    25
paulson@15151
    26
fun get_unif_comb t eqterm =
paulson@15151
    27
    if ((type_of t) = (type_of eqterm))
paulson@15151
    28
    then t
paulson@15151
    29
    else
paulson@15151
    30
        let val _ $ rand = t
paulson@15151
    31
        in get_unif_comb rand eqterm end;
paulson@15151
    32
paulson@15151
    33
fun get_unif_lit t eqterm =
paulson@15151
    34
    if (can HOLogic.dest_eq t)
paulson@15151
    35
    then
paulson@15151
    36
	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
paulson@15151
    37
	in lhs end
paulson@15151
    38
    else
paulson@15151
    39
	get_unif_comb t eqterm;
paulson@15151
    40
paulson@15151
    41
paulson@15151
    42
paulson@15151
    43
(**** attributes ****)
paulson@15151
    44
paulson@15151
    45
(** Binary resolution **)
paulson@15151
    46
paulson@15151
    47
fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
paulson@15151
    48
     select_literal (lit1 + 1) cl1
paulson@15151
    49
     RSN ((lit2 + 1), cl2);
paulson@15151
    50
paulson@15151
    51
fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
paulson@15151
    52
paulson@15151
    53
fun gen_BINARY thm = syntax
paulson@15151
    54
      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
paulson@15151
    55
val BINARY_global = gen_BINARY global_thm;
paulson@15151
    56
val BINARY_local = gen_BINARY local_thm;
paulson@15151
    57
paulson@15151
    58
(*I have not done the MRR rule because it seems to be identifical to 
paulson@15151
    59
BINARY*)
paulson@15151
    60
paulson@15151
    61
paulson@15151
    62
fun inst_single sign t1 t2 cl =
paulson@15151
    63
    let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
paulson@15151
    64
    in  hd (Seq.list_of(distinct_subgoals_tac
paulson@15151
    65
			    (cterm_instantiate [(ct1,ct2)] cl)))  
paulson@15151
    66
    end;
paulson@15151
    67
paulson@15151
    68
fun inst_subst sign substs cl =
paulson@15151
    69
    if (is_Var (fst(hd(substs))))
paulson@15151
    70
    then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
paulson@15151
    71
    else if (is_Var (snd(hd(substs))))
paulson@15151
    72
    then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
paulson@15151
    73
    else raise THM ("inst_subst", 0, [cl]);
paulson@15151
    74
paulson@15151
    75
(*Grabs the environment from the result of Unify.unifiers*)
paulson@15151
    76
fun getnewenv thisseq = fst (hd (Seq.list_of thisseq));
paulson@15151
    77
paulson@15151
    78
(** Factoring **)
paulson@15151
    79
paulson@15151
    80
fun factor_rule (cl, lit1, lit2) =
paulson@15151
    81
    let
paulson@15151
    82
       val prems = prems_of cl
paulson@15151
    83
       val fac1 = List.nth (prems,lit1)
paulson@15151
    84
       val fac2 = List.nth (prems,lit2)
paulson@15151
    85
       val sign = sign_of_thm cl
paulson@15151
    86
       val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
paulson@15151
    87
       val newenv = getnewenv unif_env
paulson@15151
    88
       val envlist = Envir.alist_of newenv
paulson@15151
    89
     in
paulson@15151
    90
       inst_subst sign (mksubstlist envlist []) cl
paulson@15151
    91
    end;
paulson@15151
    92
paulson@15151
    93
fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
paulson@15151
    94
paulson@15151
    95
fun FACTOR x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
paulson@15151
    96
paulson@15151
    97
paulson@15151
    98
(** Paramodulation **)
paulson@15151
    99
paulson@15151
   100
(*Get rid of a Not if it is present*)
paulson@15151
   101
fun maybe_dest_not (Const ("Not", _) $ t) = t
paulson@15151
   102
  | maybe_dest_not t = t;
paulson@15151
   103
paulson@15151
   104
fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
paulson@15151
   105
    let val prems1 = prems_of cl1
paulson@15151
   106
	val prems2 = prems_of cl2
paulson@15151
   107
        val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2)
paulson@15151
   108
	(* want to get first element of equality *)
paulson@15151
   109
paulson@15151
   110
	val fac1 = List.nth (prems1,lit1) 
paulson@15151
   111
	val (lhs, rhs) = HOLogic.dest_eq(maybe_dest_not
paulson@15151
   112
					     (HOLogic.dest_Trueprop fac1))
paulson@15151
   113
	(* get other literal involved in the paramodulation *)
paulson@15151
   114
	val fac2 = List.nth (prems2,lit2) 
paulson@15151
   115
paulson@15151
   116
       (* get bit of th2 to unify with lhs of cl1 *)
paulson@15151
   117
	val unif_lit = get_unif_lit (HOLogic.dest_Trueprop fac2) lhs
paulson@15151
   118
	val unif_env = Unify.unifiers (sign, Envir.empty 0, [(unif_lit, lhs)])
paulson@15151
   119
	val newenv = getnewenv unif_env
paulson@15151
   120
	val envlist = Envir.alist_of newenv
paulson@15151
   121
       (* instantiate cl2 with unifiers *)
paulson@15151
   122
paulson@15151
   123
	val newth1 = inst_subst sign (mksubstlist envlist []) cl1
paulson@15151
   124
       (*rewrite cl2 with the equality bit of cl2 i.e. lit2 *)
paulson@15151
   125
	  val facthm' = select_literal (lit1 + 1) newth1
paulson@15151
   126
	  val equal_lit = concl_of facthm'
paulson@15151
   127
	  val cterm_eq = cterm_of sign equal_lit
paulson@15151
   128
	  val eq_thm = assume cterm_eq
paulson@15151
   129
	  val meta_eq_thm = mk_meta_eq eq_thm
paulson@15151
   130
	  val newth2= rewrite_rule [meta_eq_thm] cl2
paulson@15151
   131
       (*thin lit2 from cl2 *)
paulson@15151
   132
       (* get cl1 with lit1 as concl, then resolve with thin_rl *)
paulson@15151
   133
	  val thm' = facthm' RS thin_rl
paulson@15151
   134
       (* now resolve cl2 with last premise of thm' *)
paulson@15151
   135
	  val newthm = newth2  RSN ((length prems1), thm')
paulson@15151
   136
     in newthm end
paulson@15151
   137
paulson@15151
   138
paulson@15151
   139
fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
paulson@15151
   140
paulson@15151
   141
fun gen_PARAMOD thm = syntax
paulson@15151
   142
      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
paulson@15151
   143
val PARAMOD_global = gen_PARAMOD global_thm;
paulson@15151
   144
val PARAMOD_local = gen_PARAMOD local_thm;
paulson@15151
   145
paulson@15151
   146
paulson@15151
   147
(** Demodulation, i.e. rewriting **)
paulson@15151
   148
paulson@15151
   149
fun demod_rule (cl1,lit1,cl2) =
paulson@15151
   150
    let  val eq_lit_th = select_literal (lit1+1) cl1
paulson@15151
   151
	 val equal_lit = concl_of eq_lit_th
paulson@15151
   152
         val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2)
paulson@15151
   153
	 val cterm_eq = cterm_of sign equal_lit
paulson@15151
   154
	 val eq_thm = assume cterm_eq
paulson@15151
   155
	 val meta_eq_thm = mk_meta_eq eq_thm
paulson@15151
   156
	 val newth2= rewrite_rule [meta_eq_thm] cl2
paulson@15151
   157
    in newth2 end;
paulson@15151
   158
paulson@15151
   159
fun demod_syntax (i, B) (x, A) = (x, demod_rule (A,i,B));
paulson@15151
   160
paulson@15151
   161
fun gen_DEMOD thm = syntax ((Scan.lift Args.nat -- thm) >> demod_syntax);
paulson@15151
   162
val DEMOD_global = gen_DEMOD global_thm;
paulson@15151
   163
val DEMOD_local = gen_DEMOD local_thm;
paulson@15151
   164
paulson@15151
   165
paulson@15151
   166
(** theory setup **)
paulson@15151
   167
paulson@15151
   168
val setup =
paulson@15151
   169
  [Attrib.add_attributes
paulson@15151
   170
     [("BINARY", (BINARY_global, BINARY_local), "binary resolution"),
paulson@15151
   171
      ("PARAMOD", (PARAMOD_global, PARAMOD_local), "paramodulation"),
paulson@15151
   172
      ("DEMOD", (DEMOD_global, DEMOD_local), "demodulation"),
paulson@15151
   173
      ("FACTOR", (FACTOR, FACTOR), "factoring")]];
paulson@15151
   174
paulson@15151
   175
end
paulson@15151
   176
end
paulson@15151
   177
paulson@15151
   178