# HG changeset patch
# User wenzelm
# Date 957812370 -7200
# Node ID 18b76c137c41a9e29ecd4b6d1b7aff845feb26ea
# Parent  31da5b9790c00b39112489bd1fe5166269a98897
moved theory Sexp to Induct examples;

diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Induct/Sexp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Sexp.ML	Mon May 08 20:59:30 2000 +0200
@@ -0,0 +1,130 @@
+(*  Title:      HOL/Sexp
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+S-expressions, general binary trees for defining recursive data structures
+*)
+
+open Sexp;
+
+(** sexp_case **)
+
+Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
+by (Blast_tac 1);
+qed "sexp_case_Leaf";
+
+Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
+by (Blast_tac 1);
+qed "sexp_case_Numb";
+
+Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
+by (Blast_tac 1);
+qed "sexp_case_Scons";
+
+Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
+
+
+(** Introduction rules for sexp constructors **)
+
+val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
+by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
+qed "sexp_In0I";
+
+val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
+by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
+qed "sexp_In1I";
+
+AddIs sexp.intrs;
+
+Goal "range(Leaf) <= sexp";
+by (Blast_tac 1);
+qed "range_Leaf_subset_sexp";
+
+val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
+by (rtac (major RS setup_induction) 1);
+by (etac sexp.induct 1);
+by (ALLGOALS Blast_tac);
+qed "Scons_D";
+
+(** Introduction rules for 'pred_sexp' **)
+
+Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
+by (Blast_tac 1);
+qed "pred_sexp_subset_Sigma";
+
+(* (a,b) : pred_sexp^+ ==> a : sexp *)
+val trancl_pred_sexpD1 = 
+    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
+and trancl_pred_sexpD2 = 
+    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
+
+Goalw [pred_sexp_def]
+    "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
+by (Blast_tac 1);
+qed "pred_sexpI1";
+
+Goalw [pred_sexp_def]
+    "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
+by (Blast_tac 1);
+qed "pred_sexpI2";
+
+(*Combinations involving transitivity and the rules above*)
+val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
+and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
+
+val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
+and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
+
+(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
+Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
+                        pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
+
+val major::prems = goalw Sexp.thy [pred_sexp_def]
+    "[| p : pred_sexp;                                       \
+\       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
+\       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
+\    |] ==> R";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
+qed "pred_sexpE";
+
+Goal "wf(pred_sexp)";
+by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
+by (etac sexp.induct 1);
+by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
+qed "wf_pred_sexp";
+
+
+(*** sexp_rec -- by wf recursion on pred_sexp ***)
+
+Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
+                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
+by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
+
+(* sexp_rec a c d e =
+   sexp_case c d
+    (%N1 N2.
+        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
+         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
+*)
+bind_thm("sexp_rec_unfold", 
+	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
+
+(** conversion rules **)
+
+Goal "sexp_rec (Leaf a) c d h = c(a)";
+by (stac sexp_rec_unfold 1);
+by (rtac sexp_case_Leaf 1);
+qed "sexp_rec_Leaf";
+
+Goal "sexp_rec (Numb k) c d h = d(k)";
+by (stac sexp_rec_unfold 1);
+by (rtac sexp_case_Numb 1);
+qed "sexp_rec_Numb";
+
+Goal "[| M: sexp;  N: sexp |] ==> \
+\    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
+by (rtac (sexp_rec_unfold RS trans) 1);
+by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
+qed "sexp_rec_Scons";
diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Induct/Sexp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Sexp.thy	Mon May 08 20:59:30 2000 +0200
@@ -0,0 +1,41 @@
+(*  Title:      HOL/Induct/Sexp.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+S-expressions, general binary trees for defining recursive data
+structures by hand.
+*)
+
+Sexp = Univ + Inductive +
+consts
+  sexp      :: 'a item set
+
+  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
+                'a item] => 'b"
+
+  sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
+                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
+  
+  pred_sexp :: "('a item * 'a item)set"
+
+inductive sexp
+  intrs
+    LeafI  "Leaf(a): sexp"
+    NumbI  "Numb(i): sexp"
+    SconsI "[| M: sexp;  N: sexp |] ==> Scons M N : sexp"
+
+defs
+
+  sexp_case_def 
+   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
+                            | (? k.   M=Numb(k) & z=d(k))  
+                            | (? N1 N2. M = Scons N1 N2  & z=e N1 N2)"
+
+  pred_sexp_def
+     "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
+
+  sexp_rec_def
+   "sexp_rec M c d e == wfrec pred_sexp
+             (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
+end
diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon May 08 20:58:49 2000 +0200
+++ b/src/HOL/IsaMakefile	Mon May 08 20:59:30 2000 +0200
@@ -31,40 +31,40 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
-  $(SRC)/Provers/Arith/cancel_sums.ML					\
-  $(SRC)/Provers/Arith/assoc_fold.ML					\
-  $(SRC)/Provers/Arith/combine_numerals.ML				\
-  $(SRC)/Provers/Arith/cancel_numerals.ML				\
-  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML	\
-  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
-  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML		\
-  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML		\
-  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml	\
-  $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml		\
-  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig		\
-  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml	\
-  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy		\
-  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML		\
-  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy		\
-  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy		\
-  Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy	\
-  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy		\
-  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy	\
-  Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML	\
-  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML	\
-  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML	\
-  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy		\
-  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy	\
-  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML	\
-  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML		\
-  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML			\
-  Tools/induct_method.ML Tools/inductive_package.ML			\
-  Tools/numeral_syntax.ML Tools/primrec_package.ML			\
-  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML	\
-  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy	\
-  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML	\
-  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy	\
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+  $(SRC)/Provers/Arith/cancel_sums.ML		\
+  $(SRC)/Provers/Arith/assoc_fold.ML		\
+  $(SRC)/Provers/Arith/combine_numerals.ML	\
+  $(SRC)/Provers/Arith/cancel_numerals.ML	\
+  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
+  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
+  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
+  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
+  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
+  $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
+  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
+  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
+  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
+  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
+  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
+  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
+  Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
+  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
+  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
+  Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
+  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
+  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
+  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
+  Relation.ML Relation.thy Set.ML Set.thy String.thy SVC_Oracle.ML \
+  SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
+  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
+  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
+  Tools/induct_method.ML Tools/inductive_package.ML \
+  Tools/numeral_syntax.ML Tools/primrec_package.ML \
+  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
+  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
+  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
+  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
   simpdata.ML subset.ML subset.thy thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
@@ -133,11 +133,11 @@
   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
-  Induct/Multiset0.ML Induct/Multiset0.thy \
-  Induct/Multiset.ML Induct/Multiset.thy \
-  Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \
-  Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/ABexp.ML \
-  Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
+  Induct/Multiset0.ML Induct/Multiset0.thy Induct/Multiset.ML \
+  Induct/Multiset.thy Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
+  Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
+  Induct/SList.ML Induct/SList.thy Induct/ABexp.ML Induct/ABexp.thy \
+  Induct/Term.ML Induct/Term.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Induct
 
 
diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Mon May 08 20:58:49 2000 +0200
+++ b/src/HOL/PreList.thy	Mon May 08 20:59:30 2000 +0200
@@ -8,8 +8,7 @@
 *)
 
 theory PreList =
-  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
-  + SVC_Oracle
+  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
 files "Integ/NatSimprocs.ML":
 
 end
diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Mon May 08 20:58:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(*  Title:      HOL/Sexp
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-S-expressions, general binary trees for defining recursive data structures
-*)
-
-open Sexp;
-
-(** sexp_case **)
-
-Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
-by (Blast_tac 1);
-qed "sexp_case_Leaf";
-
-Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
-by (Blast_tac 1);
-qed "sexp_case_Numb";
-
-Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
-by (Blast_tac 1);
-qed "sexp_case_Scons";
-
-Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
-
-
-(** Introduction rules for sexp constructors **)
-
-val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
-by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
-qed "sexp_In0I";
-
-val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
-by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
-qed "sexp_In1I";
-
-AddIs sexp.intrs;
-
-Goal "range(Leaf) <= sexp";
-by (Blast_tac 1);
-qed "range_Leaf_subset_sexp";
-
-val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
-by (rtac (major RS setup_induction) 1);
-by (etac sexp.induct 1);
-by (ALLGOALS Blast_tac);
-qed "Scons_D";
-
-(** Introduction rules for 'pred_sexp' **)
-
-Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
-by (Blast_tac 1);
-qed "pred_sexp_subset_Sigma";
-
-(* (a,b) : pred_sexp^+ ==> a : sexp *)
-val trancl_pred_sexpD1 = 
-    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
-and trancl_pred_sexpD2 = 
-    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
-
-Goalw [pred_sexp_def]
-    "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
-by (Blast_tac 1);
-qed "pred_sexpI1";
-
-Goalw [pred_sexp_def]
-    "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
-by (Blast_tac 1);
-qed "pred_sexpI2";
-
-(*Combinations involving transitivity and the rules above*)
-val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
-and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
-
-val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
-and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
-
-(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
-Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
-                        pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
-
-val major::prems = goalw Sexp.thy [pred_sexp_def]
-    "[| p : pred_sexp;                                       \
-\       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
-\       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
-\    |] ==> R";
-by (cut_facts_tac [major] 1);
-by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
-qed "pred_sexpE";
-
-Goal "wf(pred_sexp)";
-by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
-by (etac sexp.induct 1);
-by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
-qed "wf_pred_sexp";
-
-
-(*** sexp_rec -- by wf recursion on pred_sexp ***)
-
-Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
-                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
-by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
-
-(* sexp_rec a c d e =
-   sexp_case c d
-    (%N1 N2.
-        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
-         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
-*)
-bind_thm("sexp_rec_unfold", 
-	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
-
-(** conversion rules **)
-
-Goal "sexp_rec (Leaf a) c d h = c(a)";
-by (stac sexp_rec_unfold 1);
-by (rtac sexp_case_Leaf 1);
-qed "sexp_rec_Leaf";
-
-Goal "sexp_rec (Numb k) c d h = d(k)";
-by (stac sexp_rec_unfold 1);
-by (rtac sexp_case_Numb 1);
-qed "sexp_rec_Numb";
-
-Goal "[| M: sexp;  N: sexp |] ==> \
-\    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
-by (rtac (sexp_rec_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
-qed "sexp_rec_Scons";
diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Sexp.thy
--- a/src/HOL/Sexp.thy	Mon May 08 20:58:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(*  Title:      HOL/Sexp
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-S-expressions, general binary trees for defining recursive data structures
-*)
-
-Sexp = Univ + Inductive +
-consts
-  sexp      :: 'a item set
-
-  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
-                'a item] => 'b"
-
-  sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
-                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
-  
-  pred_sexp :: "('a item * 'a item)set"
-
-inductive sexp
-  intrs
-    LeafI  "Leaf(a): sexp"
-    NumbI  "Numb(i): sexp"
-    SconsI "[| M: sexp;  N: sexp |] ==> Scons M N : sexp"
-
-defs
-
-  sexp_case_def 
-   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
-                            | (? k.   M=Numb(k) & z=d(k))  
-                            | (? N1 N2. M = Scons N1 N2  & z=e N1 N2)"
-
-  pred_sexp_def
-     "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
-
-  sexp_rec_def
-   "sexp_rec M c d e == wfrec pred_sexp
-             (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
-end