src/HOL/Sexp.ML
changeset 4521 c7f56322a84b
parent 4089 96fba19bcbe2
child 4535 f24cebc299e4
     1.1 --- a/src/HOL/Sexp.ML	Wed Jan 07 13:55:54 1998 +0100
     1.2 +++ b/src/HOL/Sexp.ML	Thu Jan 08 11:21:45 1998 +0100
     1.3 @@ -22,6 +22,8 @@
     1.4  by (blast_tac (claset() addSIs [select_equality]) 1);
     1.5  qed "sexp_case_Scons";
     1.6  
     1.7 +Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
     1.8 +
     1.9  
    1.10  (** Introduction rules for sexp constructors **)
    1.11  
    1.12 @@ -100,6 +102,13 @@
    1.13     "(%M. sexp_rec M c d e) = wfrec pred_sexp \
    1.14                         \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
    1.15  by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
    1.16 +
    1.17 +(* sexp_rec a c d e =
    1.18 +   sexp_case c d
    1.19 +    (%N1 N2.
    1.20 +        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
    1.21 +         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
    1.22 +*)
    1.23  bind_thm("sexp_rec_unfold", 
    1.24  	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
    1.25  
    1.26 @@ -118,6 +127,5 @@
    1.27  goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
    1.28  \    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
    1.29  by (rtac (sexp_rec_unfold RS trans) 1);
    1.30 -by (asm_simp_tac (simpset() addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
    1.31 -    1);
    1.32 +by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
    1.33  qed "sexp_rec_Scons";