TFL/examples/Subst/Unify.thy

Subst as modified by Konrad Slind

Unify = Unifier + WF1 + "NNF" + 

datatype 'a subst = Fail | Subst ('a list)

consts

 "##"  :: "('a => 'b) => ('a => 'c) => 'a => ('b * 'c)"  (infixr 50)
   R0  :: "('a set * 'a set) set"
   R1  :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
   R   :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"


rules

  point_to_prod_def "(f ## g) x == (f x, g x)"

  (* finite proper subset -- should go in WF1.thy maybe *)
  R0_def "R0 == {p. fst p < snd p & finite(snd p)}"

  R1_def "R1 == rprod (measure uterm_size) (measure uterm_size)"

  (* The termination relation for the Unify function *)
  R_def  "R == inv_image  (R0 ** R1)
                          ((%(x,y). vars_of x Un vars_of y) ## (%x.x))"

end