Subst/UTerm.thy
author clasohm
Wed, 02 Nov 1994 11:50:09 +0100
changeset 156 fd1be45b64bf
parent 126 872f866e630f
child 249 492493334e0f
permissions -rw-r--r--
added IOA to isabelle/HOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
126
872f866e630f Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents: 48
diff changeset
     1
(*  Title: 	Substitutions/UTerm.thy
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
    Author: 	Martin Coen, Cambridge University Computer Laboratory
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
Simple term structure for unifiation.
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
Binary trees with leaves that are constants or variables.
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
UTerm = Sexp +
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    11
types uterm 1
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    12
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    13
arities 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    14
  uterm     :: (term)term
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    15
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    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
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    23
  Var       :: "'a => 'a uterm"
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    24
  Const     :: "'a => 'a uterm"
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    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
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    28
  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    29
\                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    30
126
872f866e630f Subst/UTerm: updated for inductive defs; streamlined proofs
lcp
parents: 48
diff changeset
    31
defs
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    32
     (*defining the concrete constructors*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    33
  VAR_def  	"VAR(v) == In0(v)"
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    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
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    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
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    54
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    55
     (*uterm recursion*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    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
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    59
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    60
  uterm_rec_def
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    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
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    64
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    65
end