src/HOL/Sexp.ML
changeset 1475 7f5a4cd08209
parent 1465 5d7a7e439cec
child 1642 21db0cf9a1a4
     1.1 --- a/src/HOL/Sexp.ML	Mon Feb 05 14:44:09 1996 +0100
     1.2 +++ b/src/HOL/Sexp.ML	Mon Feb 05 21:27:16 1996 +0100
     1.3 @@ -17,17 +17,17 @@
     1.4                     Scons_neq_Leaf, Scons_neq_Numb];
     1.5  
     1.6  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
     1.7 -by (rtac select_equality 1);
     1.8 +by (resolve_tac [select_equality] 1);
     1.9  by (ALLGOALS (fast_tac sexp_free_cs));
    1.10  qed "sexp_case_Leaf";
    1.11  
    1.12  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    1.13 -by (rtac select_equality 1);
    1.14 +by (resolve_tac [select_equality] 1);
    1.15  by (ALLGOALS (fast_tac sexp_free_cs));
    1.16  qed "sexp_case_Numb";
    1.17  
    1.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
    1.19 -by (rtac select_equality 1);
    1.20 +by (resolve_tac [select_equality] 1);
    1.21  by (ALLGOALS (fast_tac sexp_free_cs));
    1.22  qed "sexp_case_Scons";
    1.23  
    1.24 @@ -109,9 +109,18 @@
    1.25  
    1.26  (*** sexp_rec -- by wf recursion on pred_sexp ***)
    1.27  
    1.28 +goal Sexp.thy
    1.29 +   "(%M. sexp_rec M c d e) = wfrec pred_sexp \
    1.30 +                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
    1.31 +by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
    1.32 +bind_thm("sexp_rec_unfold", wf_pred_sexp RS 
    1.33 +                            ((result() RS eq_reflection) RS def_wfrec));
    1.34  (** conversion rules **)
    1.35  
    1.36 -val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
    1.37 +(*---------------------------------------------------------------------------
    1.38 + * Old:
    1.39 + * val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
    1.40 + *---------------------------------------------------------------------------*)
    1.41  
    1.42  
    1.43  goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";