src/HOL/thy_syntax.ML
changeset 4106 01fa6e7e7196
parent 4091 771b1f6422a8
child 4184 23a09f2fd687
     1.1 --- a/src/HOL/thy_syntax.ML	Mon Nov 03 21:12:40 1997 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon Nov 03 21:13:24 1997 +0100
     1.3 @@ -3,9 +3,6 @@
     1.4      Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
     1.5  
     1.6  Additional theory file sections for HOL.
     1.7 -
     1.8 -TODO:
     1.9 -  move datatype / primrec stuff to pre_datatype.ML (?)
    1.10  *)
    1.11  
    1.12  (*the kind of distinctiveness axioms depends on number of constructors*)
    1.13 @@ -126,12 +123,11 @@
    1.14  
    1.15    (*generate string for calling add_datatype and build_record*)
    1.16    fun mk_params ((ts, tname), cons) =
    1.17 -   ("val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
    1.18 +    "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
    1.19      \    Datatype.add_datatype\n"
    1.20      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    1.21 -    \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)"
    1.22 -    ,
    1.23 -    "val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
    1.24 +    \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
    1.25 +    \val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
    1.26      \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
    1.27      \structure " ^ tname ^ " =\n\
    1.28      \struct\n\
    1.29 @@ -151,10 +147,12 @@
    1.30      \ val simps = inject @ distinct @ cases @ recs;\n\
    1.31      \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
    1.32      \end;\n\
    1.33 -    \val dummy = datatypes := Dtype.build_record (thy, " ^
    1.34 -      mk_pair ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
    1.35 -        mk_list (map (fst o fst) cons)) ^
    1.36 -      ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
    1.37 +    \val thy = thy |> Dtype.add_record " ^
    1.38 +      mk_triple
    1.39 +        ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
    1.40 +          mk_list (map (fst o fst) cons),
    1.41 +          tname ^ ".induct_tac") ^ ";\n\
    1.42 +    \val dummy = context thy;\n\
    1.43      \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
    1.44      \val dummy = AddIffs " ^ tname ^ ".inject;\n\
    1.45      \val dummy = " ^
    1.46 @@ -164,9 +162,11 @@
    1.47      \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
    1.48                       "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
    1.49      \val split_"^tname^"_case = prove_goal thy split_"^tname^"_eqn\n\
    1.50 -    \  (fn _ => [#exhaust_tac(snd(hd(!datatypes))) \""^tname^"0\" 1,\n\
    1.51 -    \            ALLGOALS Asm_simp_tac])"
    1.52 -   );
    1.53 +    \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
    1.54 +      ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
    1.55 +    \            ALLGOALS Asm_simp_tac]);\n\
    1.56 +    \val thy = thy\n";
    1.57 +
    1.58  (*
    1.59  The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
    1.60  is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
    1.61 @@ -291,7 +291,7 @@
    1.62    (section "record" "|> Record.add_record" record_decl),
    1.63    ("inductive", inductive_decl ""),
    1.64    ("coinductive", inductive_decl "Co"),
    1.65 -  ("datatype", datatype_decl),
    1.66 +  (section "datatype" "" datatype_decl),
    1.67    ("primrec", primrec_decl),
    1.68    ("recdef", rec_decl)];
    1.69