src/HOL/thy_syntax.ML
changeset 4032 4b1c69d8b767
parent 4001 b6a3c2665c45
child 4091 771b1f6422a8
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Oct 29 16:03:19 1997 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Oct 30 09:45:03 1997 +0100
     1.3 @@ -126,9 +126,10 @@
     1.4  
     1.5    (*generate string for calling add_datatype and build_record*)
     1.6    fun mk_params ((ts, tname), cons) =
     1.7 -   ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
     1.8 +   ("val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
     1.9 +    \    Datatype.add_datatype\n"
    1.10      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    1.11 -    \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
    1.12 +    \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)"
    1.13      ,
    1.14      "val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
    1.15      \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
    1.16 @@ -161,9 +162,19 @@
    1.17        tname ^ ".distinct;\n\
    1.18      \val dummy = Addsimps(map (fn (_,eqn) =>\n\
    1.19      \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
    1.20 -                     "] eqn (fn _ => [Simp_tac 1]))\n" ^
    1.21 -    tname^"_size_eqns)\n"
    1.22 +                     "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
    1.23 +    \val split_"^tname^"_case = prove_goal thy split_"^tname^"_eqn\n\
    1.24 +    \  (fn _ => [#exhaust_tac(snd(hd(!datatypes))) \""^tname^"0\" 1,\n\
    1.25 +    \            ALLGOALS Asm_simp_tac])"
    1.26     );
    1.27 +(*
    1.28 +The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
    1.29 +is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
    1.30 +specific exhaustion tactic from the theory associated with the proof
    1.31 +state. However, the exhaustion tactic for the current datatype has only just
    1.32 +been added to !datatypes (a few lines above) but is not yet associated with
    1.33 +the theory. Hope this can be simplified in the future.
    1.34 +*)
    1.35  
    1.36    (*parsers*)
    1.37    val tvars = type_args >> map (cat "dtVar");