Adapted to new inductive definition package.
authorberghofe
Tue Jun 30 20:42:47 1998 +0200 (1998-06-30)
changeset 50976c4a7ad6ebc7
parent 5096 84b00be693b4
child 5098 48e70d9fe05f
Adapted to new inductive definition package.
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jun 30 20:41:41 1998 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 30 20:42:47 1998 +0200
     1.3 @@ -42,17 +42,18 @@
     1.4    Integ/Bin.ML Integ/Bin.thy  Integ/Equiv.ML Integ/Equiv.thy \
     1.5    Integ/Integ.ML Integ/Integ.thy Integ/ROOT.ML \
     1.6    Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy \
     1.7 -  Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.ML \
     1.8 +  Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
     1.9    Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
    1.10    Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
    1.11    Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \
    1.12    RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    1.13    Sum.ML Sum.thy Tools/record_package.ML Tools/typedef_package.ML \
    1.14 +  Tools/inductive_package.ML \
    1.15    Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.16    Update.ML Update.thy Vimage.ML Vimage.thy WF.ML \
    1.17 -  WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \
    1.18 -  datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \
    1.19 -  indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \
    1.20 +  WF.thy WF_Rel.ML WF_Rel.thy arith_data.ML cladata.ML \
    1.21 +  datatype.ML equalities.ML equalities.thy hologic.ML \
    1.22 +  mono.ML mono.thy \
    1.23    simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML
    1.24  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.25  
     2.1 --- a/src/HOL/ROOT.ML	Tue Jun 30 20:41:41 1998 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Tue Jun 30 20:42:47 1998 +0200
     2.3 @@ -36,8 +36,7 @@
     2.4  use_thy "Ord";
     2.5  use_thy "subset";
     2.6  use "Tools/typedef_package.ML";
     2.7 -use_thy "Sum";
     2.8 -use_thy "Gfp";
     2.9 +use_thy "Inductive";
    2.10  
    2.11  use "Tools/record_package.ML";
    2.12  use_thy "Record";
    2.13 @@ -46,11 +45,7 @@
    2.14  use_thy "Arith";
    2.15  use "arith_data.ML";
    2.16  
    2.17 -use "ind_syntax.ML";
    2.18 -use "add_ind_def.ML";
    2.19 -use_thy "intr_elim";
    2.20 -use_thy "indrule";
    2.21 -use_thy "Inductive";
    2.22 +use "Tools/inductive_package.ML";
    2.23  
    2.24  use_thy "RelPow";
    2.25  use_thy "Finite";
     3.1 --- a/src/HOL/thy_syntax.ML	Tue Jun 30 20:41:41 1998 +0200
     3.2 +++ b/src/HOL/thy_syntax.ML	Tue Jun 30 20:42:47 1998 +0200
     3.3 @@ -44,8 +44,7 @@
     3.4  
     3.5  (** (co)inductive **)
     3.6  
     3.7 -(*co is either "" or "Co"*)
     3.8 -fun inductive_decl co =
     3.9 +fun inductive_decl coind =
    3.10    let
    3.11      fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    3.12        if Syntax.is_identifier s then "op " ^ s else "_";
    3.13 @@ -53,39 +52,28 @@
    3.14        let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
    3.15            and srec_tms = mk_list recs
    3.16            and sintrs   = mk_big_list (map snd ipairs)
    3.17 -          val intrnl_name = big_rec_name ^ "_Intrnl"
    3.18        in
    3.19 -         (";\n\n\
    3.20 -          \structure " ^ intrnl_name ^ " =\n\
    3.21 -          \  struct\n\
    3.22 -          \  val _ = writeln \"" ^ co ^
    3.23 -                     "Inductive definition " ^ big_rec_name ^ "\"\n\
    3.24 -          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
    3.25 -                           ^ srec_tms ^ "\n\
    3.26 -          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    3.27 -                           ^ sintrs ^ "\n\
    3.28 -          \  end;\n\n\
    3.29 -          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
    3.30 -             intrnl_name ^ ".rec_tms, " ^
    3.31 -             intrnl_name ^ ".intr_tms)"
    3.32 -         ,
    3.33 -          "structure " ^ big_rec_name ^ " =\n\
    3.34 -          \ let\n\
    3.35 -          \  val _ = writeln \"Proofs for " ^ co ^ 
    3.36 -                     "Inductive definition " ^ big_rec_name ^ "\"\n\
    3.37 -          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    3.38 -          \\t  (open " ^ intrnl_name ^ "\n\
    3.39 -          \\t   val thy\t\t= thy\n\
    3.40 -          \\t   val monos\t\t= " ^ monos ^ "\n\
    3.41 -          \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    3.42 -          \ in\n\
    3.43 -          \  struct\n\
    3.44 -          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    3.45 -          \  open Result\n\
    3.46 -          \  end\n\
    3.47 -          \ end;\n\n\
    3.48 -          \structure " ^ intrnl_name ^ " = struct end;\n\n"
    3.49 -         )
    3.50 +        ";\n\n\
    3.51 +        \local\n\
    3.52 +        \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
    3.53 +        \  InductivePackage.add_inductive true " ^
    3.54 +        (if coind then "true " else "false ") ^ srec_tms ^ " " ^
    3.55 +         sintrs ^ " " ^ monos ^ " " ^ con_defs ^ " thy;\n\
    3.56 +        \in\n\
    3.57 +        \structure " ^ big_rec_name ^ " =\n\
    3.58 +        \struct\n\
    3.59 +        \  val defs = defs;\n\
    3.60 +        \  val mono = mono;\n\
    3.61 +        \  val unfold = unfold;\n\
    3.62 +        \  val intrs = intrs;\n\
    3.63 +        \  val elims = elims;\n\
    3.64 +        \  val elim = hd elims;\n\
    3.65 +        \  val " ^ (if coind then "co" else "") ^ "induct = induct;\n\
    3.66 +        \  val mk_cases = mk_cases;\n\
    3.67 +        \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\
    3.68 +        \end;\n\
    3.69 +        \val thy = thy;\nend;\n\
    3.70 +        \val thy = thy\n"
    3.71        end
    3.72      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    3.73      fun optstring s = optional (s $$-- string >> trim) "[]"
    3.74 @@ -95,7 +83,6 @@
    3.75    end;
    3.76  
    3.77  
    3.78 -
    3.79  (** datatype **)
    3.80  
    3.81  local
    3.82 @@ -293,10 +280,10 @@
    3.83  val _ = ThySyn.add_syntax
    3.84   ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
    3.85   [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
    3.86 -  (section "record" "|> RecordPackage.add_record" record_decl),
    3.87 -  ("inductive", inductive_decl ""),
    3.88 -  ("coinductive", inductive_decl "Co"),
    3.89 -  (section "datatype" "" datatype_decl),
    3.90 +  section "record" "|> RecordPackage.add_record" record_decl,
    3.91 +  section "inductive" "" (inductive_decl false),
    3.92 +  section "coinductive" "" (inductive_decl true),
    3.93 +  section "datatype" "" datatype_decl,
    3.94    ("primrec", primrec_decl),
    3.95    ("recdef", rec_decl)];
    3.96