author | clasohm |
Wed, 02 Nov 1994 11:50:09 +0100 | |
changeset 156 | fd1be45b64bf |
parent 126 | 872f866e630f |
child 249 | 492493334e0f |
permissions | -rw-r--r-- |
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
1 |
(* Title: Substitutions/UTerm.thy |
0 | 2 |
Author: Martin Coen, Cambridge University Computer Laboratory |
3 |
Copyright 1993 University of Cambridge |
|
4 |
||
5 |
Simple term structure for unifiation. |
|
6 |
Binary trees with leaves that are constants or variables. |
|
7 |
*) |
|
8 |
||
9 |
UTerm = Sexp + |
|
10 |
||
11 |
types uterm 1 |
|
12 |
||
13 |
arities |
|
14 |
uterm :: (term)term |
|
15 |
||
16 |
consts |
|
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
17 |
uterm :: "'a item set => 'a item set" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
18 |
Rep_uterm :: "'a uterm => 'a item" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
19 |
Abs_uterm :: "'a item => 'a uterm" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
20 |
VAR :: "'a item => 'a item" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
21 |
CONST :: "'a item => 'a item" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
22 |
COMB :: "['a item, 'a item] => 'a item" |
0 | 23 |
Var :: "'a => 'a uterm" |
24 |
Const :: "'a => 'a uterm" |
|
25 |
Comb :: "['a uterm, 'a uterm] => 'a uterm" |
|
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
26 |
UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, \ |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
27 |
\ ['a item , 'a item, 'b, 'b]=>'b] => 'b" |
0 | 28 |
uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, \ |
29 |
\ ['a uterm, 'a uterm,'b,'b]=>'b] => 'b" |
|
30 |
||
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
31 |
defs |
0 | 32 |
(*defining the concrete constructors*) |
33 |
VAR_def "VAR(v) == In0(v)" |
|
34 |
CONST_def "CONST(v) == In1(In0(v))" |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
35 |
COMB_def "COMB(t,u) == In1(In1(t $ u))" |
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
36 |
|
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
37 |
inductive "uterm(A)" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
38 |
intrs |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
39 |
VAR_I "v:A ==> VAR(v) : uterm(A)" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
40 |
CONST_I "c:A ==> CONST(c) : uterm(A)" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
41 |
COMB_I "[| M:uterm(A); N:uterm(A) |] ==> COMB(M,N) : uterm(A)" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
42 |
|
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
43 |
rules |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
44 |
(*faking a type definition...*) |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
45 |
Rep_uterm "Rep_uterm(xs): uterm(range(Leaf))" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
46 |
Rep_uterm_inverse "Abs_uterm(Rep_uterm(xs)) = xs" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
47 |
Abs_uterm_inverse "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
48 |
|
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
49 |
defs |
0 | 50 |
(*defining the abstract constructors*) |
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
51 |
Var_def "Var(v) == Abs_uterm(VAR(Leaf(v)))" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
52 |
Const_def "Const(c) == Abs_uterm(CONST(Leaf(c)))" |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
53 |
Comb_def "Comb(t,u) == Abs_uterm(COMB(Rep_uterm(t),Rep_uterm(u)))" |
0 | 54 |
|
55 |
(*uterm recursion*) |
|
56 |
UTerm_rec_def |
|
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
57 |
"UTerm_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, \ |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
58 |
\ Case(%x g.b(x), Case(%y g. c(y), Split(%x y g. d(x,y,g(x),g(y))))))" |
0 | 59 |
|
60 |
uterm_rec_def |
|
61 |
"uterm_rec(t,b,c,d) == \ |
|
126
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
62 |
\ UTerm_rec(Rep_uterm(t), %x.b(Inv(Leaf,x)), %x.c(Inv(Leaf,x)), \ |
872f866e630f
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents:
48
diff
changeset
|
63 |
\ %x y q r.d(Abs_uterm(x),Abs_uterm(y),q,r))" |
0 | 64 |
|
65 |
end |