8840

1 
(* Title: HOL/Induct/Sexp.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Sexpressions, general binary trees for defining recursive data


7 
structures by hand.


8 
*)


9 


10 
Sexp = Univ + Inductive +


11 
consts


12 
sexp :: 'a item set


13 


14 
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,


15 
'a item] => 'b"


16 


17 
sexp_rec :: "['a item, 'a=>'b, nat=>'b,


18 
['a item, 'a item, 'b, 'b]=>'b] => 'b"


19 


20 
pred_sexp :: "('a item * 'a item)set"


21 


22 
inductive sexp


23 
intrs


24 
LeafI "Leaf(a): sexp"


25 
NumbI "Numb(i): sexp"


26 
SconsI "[ M: sexp; N: sexp ] ==> Scons M N : sexp"


27 


28 
defs


29 


30 
sexp_case_def


31 
"sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x))


32 
 (? k. M=Numb(k) & z=d(k))


33 
 (? N1 N2. M = Scons N1 N2 & z=e N1 N2)"


34 


35 
pred_sexp_def


36 
"pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"


37 


38 
sexp_rec_def


39 
"sexp_rec M c d e == wfrec pred_sexp


40 
(%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"


41 
end
