src/HOL/Induct/Sexp.thy
author paulson
Wed, 08 Aug 2001 14:51:10 +0200
changeset 11481 c77e5401f2ff
parent 10212 33fe2d701ddd
child 13079 e7738aa7267f
permissions -rw-r--r--
get it working again using Hilbert_Choice
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Sexp.thy
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     5
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     6
S-expressions, general binary trees for defining recursive data
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     7
structures by hand.
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     8
*)
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     9
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 8840
diff changeset
    10
Sexp = Datatype_Universe + Inductive +
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    11
consts
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    12
  sexp      :: 'a item set
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    13
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    14
  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    15
                'a item] => 'b"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    16
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    17
  sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    18
                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    19
  
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    20
  pred_sexp :: "('a item * 'a item)set"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    21
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    22
inductive sexp
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    23
  intrs
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    24
    LeafI  "Leaf(a): sexp"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    25
    NumbI  "Numb(i): sexp"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    26
    SconsI "[| M: sexp;  N: sexp |] ==> Scons M N : sexp"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    27
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    28
defs
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    29
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    30
  sexp_case_def 
11481
c77e5401f2ff get it working again using Hilbert_Choice
paulson
parents: 10212
diff changeset
    31
   "sexp_case c d e M == THE z. (EX x.   M=Leaf(x) & z=c(x))  
c77e5401f2ff get it working again using Hilbert_Choice
paulson
parents: 10212
diff changeset
    32
                            | (EX k.   M=Numb(k) & z=d(k))  
c77e5401f2ff get it working again using Hilbert_Choice
paulson
parents: 10212
diff changeset
    33
                            | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2)"
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    34
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    35
  pred_sexp_def
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    36
     "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    37
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    38
  sexp_rec_def
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    39
   "sexp_rec M c d e == wfrec pred_sexp
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    40
             (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    41
end