Sexp.thy
author clasohm
Tue, 24 Oct 1995 14:59:17 +0100
changeset 251 f04b33ce250f
parent 249 492493334e0f
permissions -rw-r--r--
added calls of init_html and make_chart
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
     1
(*  Title: 	HOL/Sexp
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
S-expressions, general binary trees for defining recursive data structures
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
Sexp = Univ +
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
consts
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    11
  sexp      :: "'a item set"
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    12
249
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    13
  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    14
                'a item] => 'b"
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    15
249
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    16
  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    17
                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    18
  
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    19
  pred_sexp :: "('a item * 'a item)set"
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    20
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    21
inductive "sexp"
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    22
  intrs
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    23
    LeafI  "Leaf(a): sexp"
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    24
    NumbI  "Numb(a): sexp"
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    25
    SconsI "[| M: sexp;  N: sexp |] ==> M$N : sexp"
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    26
178
12dd5d2e266b rules -> defs
nipkow
parents: 128
diff changeset
    27
defs
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    28
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    29
  sexp_case_def	
249
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    30
   "sexp_case(c,d,e,M) == @ z. (? x.   M=Leaf(x) & z=c(x))  
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    31
                            | (? k.   M=Numb(k) & z=d(k))  
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    32
                            | (? N1 N2. M = N1 $ N2  & z=e(N1,N2))"
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    33
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    34
  pred_sexp_def
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    35
     "pred_sexp == UN M: sexp. UN N: sexp. {<M, M$N>, <N, M$N>}"
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    36
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents: 110
diff changeset
    37
  sexp_rec_def
249
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    38
   "sexp_rec(M,c,d,e) == wfrec(pred_sexp, M,  
492493334e0f removed \...\ inside strings
clasohm
parents: 178
diff changeset
    39
             %M g. sexp_case(c, d, %N1 N2. e(N1, N2, g(N1), g(N2)), M))"
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    40
end