src/HOL/Tools/reconstruction.ML
changeset 19963 806eaa2a2a5e
parent 18729 216e31270509
child 20258 4fe3c0911907
equal deleted inserted replaced
19962:016ba2d907a7 19963:806eaa2a2a5e
     6 
     6 
     7 (*Attributes for reconstructing external resolution proofs*)
     7 (*Attributes for reconstructing external resolution proofs*)
     8 
     8 
     9 structure Reconstruction =
     9 structure Reconstruction =
    10 struct
    10 struct
    11 
       
    12 (**************************************************************)
       
    13 (* extra functions necessary for factoring and paramodulation *)
       
    14 (**************************************************************)
       
    15 
       
    16 fun mksubstlist [] sublist = sublist
       
    17   | mksubstlist ((a, (_, b)) :: rest) sublist =
       
    18       let val vartype = type_of b
       
    19           val avar = Var(a,vartype)
       
    20           val newlist = ((avar,b)::sublist)
       
    21       in mksubstlist rest newlist end;
       
    22 
       
    23 
    11 
    24 (**** attributes ****)
    12 (**** attributes ****)
    25 
    13 
    26 (** Binary resolution **)
    14 (** Binary resolution **)
    27 
    15 
    32 val binary = Attrib.syntax
    20 val binary = Attrib.syntax
    33   (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    21   (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    34     >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
    22     >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
    35 
    23 
    36 
    24 
    37 fun inst_single sign t1 t2 cl =
    25 (** Factoring **)
    38     let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
       
    39     in  hd (Seq.list_of(distinct_subgoals_tac
       
    40                             (cterm_instantiate [(ct1,ct2)] cl)))
       
    41     end;
       
    42 
    26 
    43 fun inst_subst sign substs cl =
    27 (*NB this code did not work at all before 29/6/2006. Even now its behaviour may
    44     if (is_Var (fst(hd(substs))))
    28   not be as expected. It unifies the designated literals
    45     then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
    29   and then deletes ALL duplicates of literals (not just those designated)*)
    46     else if (is_Var (snd(hd(substs))))
       
    47     then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
       
    48     else raise THM ("inst_subst", 0, [cl]);
       
    49 
    30 
       
    31 fun mksubstlist [] sublist = sublist
       
    32   | mksubstlist ((a, (T, b)) :: rest) sublist =
       
    33       mksubstlist rest ((Var(a,T), b)::sublist);
    50 
    34 
    51 (** Factoring **)
    35 fun reorient (x,y) = 
       
    36       if is_Var x then (x,y)
       
    37       else if is_Var y then (y,x)
       
    38       else error "Reconstruction.reorient: neither term is a Var";
       
    39 
       
    40 fun inst_subst sign subst cl =
       
    41   let val subst' = map (pairself (cterm_of sign) o reorient) subst
       
    42   in 
       
    43       Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl))
       
    44   end;
    52 
    45 
    53 fun factor_rule (cl, lit1, lit2) =
    46 fun factor_rule (cl, lit1, lit2) =
    54     let
    47     let
    55        val prems = prems_of cl
    48        val prems = prems_of cl
    56        val fac1 = List.nth (prems,lit1)
    49        val fac1 = List.nth (prems,lit1)