2113
|
1 |
Unify1 = Unifier + WF1 + "NNF" +
|
|
2 |
|
|
3 |
datatype 'a subst = Fail | Subst ('a list)
|
|
4 |
|
|
5 |
consts
|
|
6 |
|
|
7 |
"##" :: "('a => 'b) => ('a => 'c) => 'a => ('b * 'c)" (infixr 50)
|
|
8 |
R0 :: "('a set * 'a set) set"
|
|
9 |
R1 :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
|
|
10 |
R :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
|
|
11 |
|
|
12 |
|
|
13 |
rules
|
|
14 |
|
|
15 |
point_to_prod_def "(f ## g) x == (f x, g x)"
|
|
16 |
|
|
17 |
(* finite proper subset -- should go in WF1.thy maybe *)
|
|
18 |
R0_def "R0 == {p. fst p < snd p & finite(snd p)}"
|
|
19 |
|
|
20 |
R1_def "R1 == rprod (measure uterm_size) (measure uterm_size)"
|
|
21 |
|
|
22 |
(* The termination relation for the Unify function *)
|
|
23 |
R_def "R == inv_image (R0 ** R1)
|
|
24 |
((%(x,y). vars_of x Un vars_of y) ## (%x.x))"
|
|
25 |
|
|
26 |
end
|