moved theory Sexp to Induct examples;
authorwenzelm
Mon May 08 20:59:30 2000 +0200 (2000-05-08)
changeset 884018b76c137c41
parent 8839 31da5b9790c0
child 8841 95f2b61f2389
moved theory Sexp to Induct examples;
src/HOL/Induct/Sexp.ML
src/HOL/Induct/Sexp.thy
src/HOL/IsaMakefile
src/HOL/PreList.thy
src/HOL/Sexp.ML
src/HOL/Sexp.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/Sexp.ML	Mon May 08 20:59:30 2000 +0200
     1.3 @@ -0,0 +1,130 @@
     1.4 +(*  Title:      HOL/Sexp
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +S-expressions, general binary trees for defining recursive data structures
    1.10 +*)
    1.11 +
    1.12 +open Sexp;
    1.13 +
    1.14 +(** sexp_case **)
    1.15 +
    1.16 +Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    1.17 +by (Blast_tac 1);
    1.18 +qed "sexp_case_Leaf";
    1.19 +
    1.20 +Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    1.21 +by (Blast_tac 1);
    1.22 +qed "sexp_case_Numb";
    1.23 +
    1.24 +Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
    1.25 +by (Blast_tac 1);
    1.26 +qed "sexp_case_Scons";
    1.27 +
    1.28 +Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
    1.29 +
    1.30 +
    1.31 +(** Introduction rules for sexp constructors **)
    1.32 +
    1.33 +val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
    1.34 +by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
    1.35 +qed "sexp_In0I";
    1.36 +
    1.37 +val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
    1.38 +by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
    1.39 +qed "sexp_In1I";
    1.40 +
    1.41 +AddIs sexp.intrs;
    1.42 +
    1.43 +Goal "range(Leaf) <= sexp";
    1.44 +by (Blast_tac 1);
    1.45 +qed "range_Leaf_subset_sexp";
    1.46 +
    1.47 +val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
    1.48 +by (rtac (major RS setup_induction) 1);
    1.49 +by (etac sexp.induct 1);
    1.50 +by (ALLGOALS Blast_tac);
    1.51 +qed "Scons_D";
    1.52 +
    1.53 +(** Introduction rules for 'pred_sexp' **)
    1.54 +
    1.55 +Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
    1.56 +by (Blast_tac 1);
    1.57 +qed "pred_sexp_subset_Sigma";
    1.58 +
    1.59 +(* (a,b) : pred_sexp^+ ==> a : sexp *)
    1.60 +val trancl_pred_sexpD1 = 
    1.61 +    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
    1.62 +and trancl_pred_sexpD2 = 
    1.63 +    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
    1.64 +
    1.65 +Goalw [pred_sexp_def]
    1.66 +    "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
    1.67 +by (Blast_tac 1);
    1.68 +qed "pred_sexpI1";
    1.69 +
    1.70 +Goalw [pred_sexp_def]
    1.71 +    "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
    1.72 +by (Blast_tac 1);
    1.73 +qed "pred_sexpI2";
    1.74 +
    1.75 +(*Combinations involving transitivity and the rules above*)
    1.76 +val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
    1.77 +and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
    1.78 +
    1.79 +val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
    1.80 +and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
    1.81 +
    1.82 +(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
    1.83 +Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
    1.84 +                        pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
    1.85 +
    1.86 +val major::prems = goalw Sexp.thy [pred_sexp_def]
    1.87 +    "[| p : pred_sexp;                                       \
    1.88 +\       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
    1.89 +\       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
    1.90 +\    |] ==> R";
    1.91 +by (cut_facts_tac [major] 1);
    1.92 +by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
    1.93 +qed "pred_sexpE";
    1.94 +
    1.95 +Goal "wf(pred_sexp)";
    1.96 +by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
    1.97 +by (etac sexp.induct 1);
    1.98 +by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
    1.99 +qed "wf_pred_sexp";
   1.100 +
   1.101 +
   1.102 +(*** sexp_rec -- by wf recursion on pred_sexp ***)
   1.103 +
   1.104 +Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
   1.105 +                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
   1.106 +by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
   1.107 +
   1.108 +(* sexp_rec a c d e =
   1.109 +   sexp_case c d
   1.110 +    (%N1 N2.
   1.111 +        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
   1.112 +         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
   1.113 +*)
   1.114 +bind_thm("sexp_rec_unfold", 
   1.115 +	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
   1.116 +
   1.117 +(** conversion rules **)
   1.118 +
   1.119 +Goal "sexp_rec (Leaf a) c d h = c(a)";
   1.120 +by (stac sexp_rec_unfold 1);
   1.121 +by (rtac sexp_case_Leaf 1);
   1.122 +qed "sexp_rec_Leaf";
   1.123 +
   1.124 +Goal "sexp_rec (Numb k) c d h = d(k)";
   1.125 +by (stac sexp_rec_unfold 1);
   1.126 +by (rtac sexp_case_Numb 1);
   1.127 +qed "sexp_rec_Numb";
   1.128 +
   1.129 +Goal "[| M: sexp;  N: sexp |] ==> \
   1.130 +\    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
   1.131 +by (rtac (sexp_rec_unfold RS trans) 1);
   1.132 +by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
   1.133 +qed "sexp_rec_Scons";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Induct/Sexp.thy	Mon May 08 20:59:30 2000 +0200
     2.3 @@ -0,0 +1,41 @@
     2.4 +(*  Title:      HOL/Induct/Sexp.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1992  University of Cambridge
     2.8 +
     2.9 +S-expressions, general binary trees for defining recursive data
    2.10 +structures by hand.
    2.11 +*)
    2.12 +
    2.13 +Sexp = Univ + Inductive +
    2.14 +consts
    2.15 +  sexp      :: 'a item set
    2.16 +
    2.17 +  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
    2.18 +                'a item] => 'b"
    2.19 +
    2.20 +  sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
    2.21 +                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
    2.22 +  
    2.23 +  pred_sexp :: "('a item * 'a item)set"
    2.24 +
    2.25 +inductive sexp
    2.26 +  intrs
    2.27 +    LeafI  "Leaf(a): sexp"
    2.28 +    NumbI  "Numb(i): sexp"
    2.29 +    SconsI "[| M: sexp;  N: sexp |] ==> Scons M N : sexp"
    2.30 +
    2.31 +defs
    2.32 +
    2.33 +  sexp_case_def 
    2.34 +   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
    2.35 +                            | (? k.   M=Numb(k) & z=d(k))  
    2.36 +                            | (? N1 N2. M = Scons N1 N2  & z=e N1 N2)"
    2.37 +
    2.38 +  pred_sexp_def
    2.39 +     "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
    2.40 +
    2.41 +  sexp_rec_def
    2.42 +   "sexp_rec M c d e == wfrec pred_sexp
    2.43 +             (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
    2.44 +end
     3.1 --- a/src/HOL/IsaMakefile	Mon May 08 20:58:49 2000 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Mon May 08 20:59:30 2000 +0200
     3.3 @@ -31,40 +31,40 @@
     3.4  Pure:
     3.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     3.6  
     3.7 -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
     3.8 -  $(SRC)/Provers/Arith/cancel_sums.ML					\
     3.9 -  $(SRC)/Provers/Arith/assoc_fold.ML					\
    3.10 -  $(SRC)/Provers/Arith/combine_numerals.ML				\
    3.11 -  $(SRC)/Provers/Arith/cancel_numerals.ML				\
    3.12 -  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML	\
    3.13 -  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    3.14 -  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML		\
    3.15 -  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML		\
    3.16 -  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml	\
    3.17 -  $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml		\
    3.18 -  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig		\
    3.19 -  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml	\
    3.20 -  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy		\
    3.21 -  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML		\
    3.22 -  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy		\
    3.23 -  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy		\
    3.24 -  Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy	\
    3.25 -  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy		\
    3.26 -  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy	\
    3.27 -  Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML	\
    3.28 -  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML	\
    3.29 -  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML	\
    3.30 -  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy		\
    3.31 -  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy	\
    3.32 -  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML	\
    3.33 -  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML		\
    3.34 -  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML			\
    3.35 -  Tools/induct_method.ML Tools/inductive_package.ML			\
    3.36 -  Tools/numeral_syntax.ML Tools/primrec_package.ML			\
    3.37 -  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML	\
    3.38 -  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy	\
    3.39 -  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML	\
    3.40 -  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy	\
    3.41 +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
    3.42 +  $(SRC)/Provers/Arith/cancel_sums.ML		\
    3.43 +  $(SRC)/Provers/Arith/assoc_fold.ML		\
    3.44 +  $(SRC)/Provers/Arith/combine_numerals.ML	\
    3.45 +  $(SRC)/Provers/Arith/cancel_numerals.ML	\
    3.46 +  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    3.47 +  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    3.48 +  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    3.49 +  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
    3.50 +  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
    3.51 +  $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
    3.52 +  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
    3.53 +  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
    3.54 +  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
    3.55 +  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
    3.56 +  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    3.57 +  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    3.58 +  Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
    3.59 +  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
    3.60 +  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
    3.61 +  Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
    3.62 +  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
    3.63 +  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
    3.64 +  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    3.65 +  Relation.ML Relation.thy Set.ML Set.thy String.thy SVC_Oracle.ML \
    3.66 +  SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    3.67 +  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    3.68 +  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    3.69 +  Tools/induct_method.ML Tools/inductive_package.ML \
    3.70 +  Tools/numeral_syntax.ML Tools/primrec_package.ML \
    3.71 +  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
    3.72 +  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    3.73 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
    3.74 +  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
    3.75    simpdata.ML subset.ML subset.thy thy_syntax.ML
    3.76  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    3.77  
    3.78 @@ -133,11 +133,11 @@
    3.79    Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
    3.80    Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
    3.81    Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
    3.82 -  Induct/Multiset0.ML Induct/Multiset0.thy \
    3.83 -  Induct/Multiset.ML Induct/Multiset.thy \
    3.84 -  Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \
    3.85 -  Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/ABexp.ML \
    3.86 -  Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
    3.87 +  Induct/Multiset0.ML Induct/Multiset0.thy Induct/Multiset.ML \
    3.88 +  Induct/Multiset.thy Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
    3.89 +  Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
    3.90 +  Induct/SList.ML Induct/SList.thy Induct/ABexp.ML Induct/ABexp.thy \
    3.91 +  Induct/Term.ML Induct/Term.thy
    3.92  	@$(ISATOOL) usedir $(OUT)/HOL Induct
    3.93  
    3.94  
     4.1 --- a/src/HOL/PreList.thy	Mon May 08 20:58:49 2000 +0200
     4.2 +++ b/src/HOL/PreList.thy	Mon May 08 20:59:30 2000 +0200
     4.3 @@ -8,8 +8,7 @@
     4.4  *)
     4.5  
     4.6  theory PreList =
     4.7 -  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
     4.8 -  + SVC_Oracle
     4.9 +  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
    4.10  files "Integ/NatSimprocs.ML":
    4.11  
    4.12  end
     5.1 --- a/src/HOL/Sexp.ML	Mon May 08 20:58:49 2000 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,130 +0,0 @@
     5.4 -(*  Title:      HOL/Sexp
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1994  University of Cambridge
     5.8 -
     5.9 -S-expressions, general binary trees for defining recursive data structures
    5.10 -*)
    5.11 -
    5.12 -open Sexp;
    5.13 -
    5.14 -(** sexp_case **)
    5.15 -
    5.16 -Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    5.17 -by (Blast_tac 1);
    5.18 -qed "sexp_case_Leaf";
    5.19 -
    5.20 -Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    5.21 -by (Blast_tac 1);
    5.22 -qed "sexp_case_Numb";
    5.23 -
    5.24 -Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
    5.25 -by (Blast_tac 1);
    5.26 -qed "sexp_case_Scons";
    5.27 -
    5.28 -Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
    5.29 -
    5.30 -
    5.31 -(** Introduction rules for sexp constructors **)
    5.32 -
    5.33 -val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
    5.34 -by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
    5.35 -qed "sexp_In0I";
    5.36 -
    5.37 -val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
    5.38 -by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
    5.39 -qed "sexp_In1I";
    5.40 -
    5.41 -AddIs sexp.intrs;
    5.42 -
    5.43 -Goal "range(Leaf) <= sexp";
    5.44 -by (Blast_tac 1);
    5.45 -qed "range_Leaf_subset_sexp";
    5.46 -
    5.47 -val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
    5.48 -by (rtac (major RS setup_induction) 1);
    5.49 -by (etac sexp.induct 1);
    5.50 -by (ALLGOALS Blast_tac);
    5.51 -qed "Scons_D";
    5.52 -
    5.53 -(** Introduction rules for 'pred_sexp' **)
    5.54 -
    5.55 -Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
    5.56 -by (Blast_tac 1);
    5.57 -qed "pred_sexp_subset_Sigma";
    5.58 -
    5.59 -(* (a,b) : pred_sexp^+ ==> a : sexp *)
    5.60 -val trancl_pred_sexpD1 = 
    5.61 -    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
    5.62 -and trancl_pred_sexpD2 = 
    5.63 -    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
    5.64 -
    5.65 -Goalw [pred_sexp_def]
    5.66 -    "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
    5.67 -by (Blast_tac 1);
    5.68 -qed "pred_sexpI1";
    5.69 -
    5.70 -Goalw [pred_sexp_def]
    5.71 -    "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
    5.72 -by (Blast_tac 1);
    5.73 -qed "pred_sexpI2";
    5.74 -
    5.75 -(*Combinations involving transitivity and the rules above*)
    5.76 -val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
    5.77 -and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
    5.78 -
    5.79 -val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
    5.80 -and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
    5.81 -
    5.82 -(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
    5.83 -Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
    5.84 -                        pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
    5.85 -
    5.86 -val major::prems = goalw Sexp.thy [pred_sexp_def]
    5.87 -    "[| p : pred_sexp;                                       \
    5.88 -\       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
    5.89 -\       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
    5.90 -\    |] ==> R";
    5.91 -by (cut_facts_tac [major] 1);
    5.92 -by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
    5.93 -qed "pred_sexpE";
    5.94 -
    5.95 -Goal "wf(pred_sexp)";
    5.96 -by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
    5.97 -by (etac sexp.induct 1);
    5.98 -by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
    5.99 -qed "wf_pred_sexp";
   5.100 -
   5.101 -
   5.102 -(*** sexp_rec -- by wf recursion on pred_sexp ***)
   5.103 -
   5.104 -Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
   5.105 -                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
   5.106 -by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
   5.107 -
   5.108 -(* sexp_rec a c d e =
   5.109 -   sexp_case c d
   5.110 -    (%N1 N2.
   5.111 -        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
   5.112 -         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
   5.113 -*)
   5.114 -bind_thm("sexp_rec_unfold", 
   5.115 -	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
   5.116 -
   5.117 -(** conversion rules **)
   5.118 -
   5.119 -Goal "sexp_rec (Leaf a) c d h = c(a)";
   5.120 -by (stac sexp_rec_unfold 1);
   5.121 -by (rtac sexp_case_Leaf 1);
   5.122 -qed "sexp_rec_Leaf";
   5.123 -
   5.124 -Goal "sexp_rec (Numb k) c d h = d(k)";
   5.125 -by (stac sexp_rec_unfold 1);
   5.126 -by (rtac sexp_case_Numb 1);
   5.127 -qed "sexp_rec_Numb";
   5.128 -
   5.129 -Goal "[| M: sexp;  N: sexp |] ==> \
   5.130 -\    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
   5.131 -by (rtac (sexp_rec_unfold RS trans) 1);
   5.132 -by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
   5.133 -qed "sexp_rec_Scons";
     6.1 --- a/src/HOL/Sexp.thy	Mon May 08 20:58:49 2000 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,40 +0,0 @@
     6.4 -(*  Title:      HOL/Sexp
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1992  University of Cambridge
     6.8 -
     6.9 -S-expressions, general binary trees for defining recursive data structures
    6.10 -*)
    6.11 -
    6.12 -Sexp = Univ + Inductive +
    6.13 -consts
    6.14 -  sexp      :: 'a item set
    6.15 -
    6.16 -  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
    6.17 -                'a item] => 'b"
    6.18 -
    6.19 -  sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
    6.20 -                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
    6.21 -  
    6.22 -  pred_sexp :: "('a item * 'a item)set"
    6.23 -
    6.24 -inductive sexp
    6.25 -  intrs
    6.26 -    LeafI  "Leaf(a): sexp"
    6.27 -    NumbI  "Numb(i): sexp"
    6.28 -    SconsI "[| M: sexp;  N: sexp |] ==> Scons M N : sexp"
    6.29 -
    6.30 -defs
    6.31 -
    6.32 -  sexp_case_def 
    6.33 -   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
    6.34 -                            | (? k.   M=Numb(k) & z=d(k))  
    6.35 -                            | (? N1 N2. M = Scons N1 N2  & z=e N1 N2)"
    6.36 -
    6.37 -  pred_sexp_def
    6.38 -     "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
    6.39 -
    6.40 -  sexp_rec_def
    6.41 -   "sexp_rec M c d e == wfrec pred_sexp
    6.42 -             (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
    6.43 -end