fixed the "factor" method
authorpaulson
Thu Jun 29 18:10:59 2006 +0200 (2006-06-29)
changeset 19963806eaa2a2a5e
parent 19962 016ba2d907a7
child 19964 73704ba4bed1
fixed the "factor" method
src/HOL/Tools/reconstruction.ML
     1.1 --- a/src/HOL/Tools/reconstruction.ML	Thu Jun 29 13:53:05 2006 +0200
     1.2 +++ b/src/HOL/Tools/reconstruction.ML	Thu Jun 29 18:10:59 2006 +0200
     1.3 @@ -9,18 +9,6 @@
     1.4  structure Reconstruction =
     1.5  struct
     1.6  
     1.7 -(**************************************************************)
     1.8 -(* extra functions necessary for factoring and paramodulation *)
     1.9 -(**************************************************************)
    1.10 -
    1.11 -fun mksubstlist [] sublist = sublist
    1.12 -  | mksubstlist ((a, (_, b)) :: rest) sublist =
    1.13 -      let val vartype = type_of b
    1.14 -          val avar = Var(a,vartype)
    1.15 -          val newlist = ((avar,b)::sublist)
    1.16 -      in mksubstlist rest newlist end;
    1.17 -
    1.18 -
    1.19  (**** attributes ****)
    1.20  
    1.21  (** Binary resolution **)
    1.22 @@ -34,21 +22,26 @@
    1.23      >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
    1.24  
    1.25  
    1.26 -fun inst_single sign t1 t2 cl =
    1.27 -    let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
    1.28 -    in  hd (Seq.list_of(distinct_subgoals_tac
    1.29 -                            (cterm_instantiate [(ct1,ct2)] cl)))
    1.30 -    end;
    1.31 +(** Factoring **)
    1.32 +
    1.33 +(*NB this code did not work at all before 29/6/2006. Even now its behaviour may
    1.34 +  not be as expected. It unifies the designated literals
    1.35 +  and then deletes ALL duplicates of literals (not just those designated)*)
    1.36 +
    1.37 +fun mksubstlist [] sublist = sublist
    1.38 +  | mksubstlist ((a, (T, b)) :: rest) sublist =
    1.39 +      mksubstlist rest ((Var(a,T), b)::sublist);
    1.40  
    1.41 -fun inst_subst sign substs cl =
    1.42 -    if (is_Var (fst(hd(substs))))
    1.43 -    then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
    1.44 -    else if (is_Var (snd(hd(substs))))
    1.45 -    then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
    1.46 -    else raise THM ("inst_subst", 0, [cl]);
    1.47 +fun reorient (x,y) = 
    1.48 +      if is_Var x then (x,y)
    1.49 +      else if is_Var y then (y,x)
    1.50 +      else error "Reconstruction.reorient: neither term is a Var";
    1.51  
    1.52 -
    1.53 -(** Factoring **)
    1.54 +fun inst_subst sign subst cl =
    1.55 +  let val subst' = map (pairself (cterm_of sign) o reorient) subst
    1.56 +  in 
    1.57 +      Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl))
    1.58 +  end;
    1.59  
    1.60  fun factor_rule (cl, lit1, lit2) =
    1.61      let