src/HOL/Induct/Sexp.thy
changeset 18413 50c0c118e96d
parent 16417 9bc16273c2d4
child 19736 d8d0f8f51d69
equal deleted inserted replaced
18412:9f6b3e1da352 18413:50c0c118e96d
    63 
    63 
    64 lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp"
    64 lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp"
    65 by blast
    65 by blast
    66 
    66 
    67 lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp"
    67 lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp"
    68 apply (erule setup_induction)
    68   by (induct S == "Scons M N" set: sexp) auto
    69 apply (erule sexp.induct, blast+)
       
    70 done
       
    71 
    69 
    72 (** Introduction rules for 'pred_sexp' **)
    70 (** Introduction rules for 'pred_sexp' **)
    73 
    71 
    74 lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
    72 lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
    75 by (simp add: pred_sexp_def, blast)
    73 by (simp add: pred_sexp_def, blast)