Improving space efficiency of inductive/datatype definitions.
authorpaulson
Tue Jan 02 10:46:50 1996 +0100 (1996-01-02)
changeset 1430439e1476a7f8
parent 1429 1f0009009219
child 1431 be7c6d77e19c
Improving space efficiency of inductive/datatype definitions.
Reduce usage of "open" and change struct open X; D end to
let open X in struct D end end whenever possible -- removes X from the final
structure. Especially needed for functors Intr_elim and Indrule.
src/HOL/Inductive.ML
src/HOL/ind_syntax.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Inductive.ML	Mon Jan 01 11:54:36 1996 +0100
     1.2 +++ b/src/HOL/Inductive.ML	Tue Jan 02 10:46:50 1996 +0100
     1.3 @@ -12,11 +12,8 @@
     1.4  Products are used only to derive "streamlined" induction rules for relations
     1.5  *)
     1.6  
     1.7 -local open Ind_Syntax
     1.8 -in
     1.9 -
    1.10  fun gen_fp_oper a (X,T,t) = 
    1.11 -    let val setT = mk_setT T
    1.12 +    let val setT = Ind_Syntax.mk_setT T
    1.13      in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t)  end;
    1.14  
    1.15  structure Lfp_items =
    1.16 @@ -33,19 +30,25 @@
    1.17    val induct	= def_Collect_coinduct
    1.18    end;
    1.19  
    1.20 -end;
    1.21 -
    1.22  
    1.23  functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    1.24    : sig include INTR_ELIM INDRULE end =
    1.25 -struct
    1.26 -structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
    1.27 -				    Fp=Lfp_items);
    1.28 +let
    1.29 +  structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
    1.30 +					  Fp=Lfp_items);
    1.31  
    1.32 -structure Indrule = Indrule_Fun
    1.33 -    (structure Inductive=Inductive and Intr_elim=Intr_elim);
    1.34 -
    1.35 -open Intr_elim Indrule
    1.36 +  structure Indrule = Indrule_Fun
    1.37 +      (structure Inductive=Inductive and Intr_elim=Intr_elim);
    1.38 +in 
    1.39 +   struct 
    1.40 +   val thy	= Intr_elim.thy
    1.41 +   val defs	= Intr_elim.defs
    1.42 +   val mono	= Intr_elim.mono
    1.43 +   val intrs	= Intr_elim.intrs
    1.44 +   val elim	= Intr_elim.elim
    1.45 +   val mk_cases	= Intr_elim.mk_cases
    1.46 +   open Indrule 
    1.47 +   end
    1.48  end;
    1.49  
    1.50  
     2.1 --- a/src/HOL/ind_syntax.ML	Mon Jan 01 11:54:36 1996 +0100
     2.2 +++ b/src/HOL/ind_syntax.ML	Tue Jan 02 10:46:50 1996 +0100
     2.3 @@ -121,4 +121,9 @@
     2.4  val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
     2.5       (fn _ => [assume_tac 1]);
     2.6  
     2.7 +(*Includes rules for Suc and Pair since they are common constructions*)
     2.8 +val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
     2.9 +		make_elim Suc_inject, 
    2.10 +		refl_thin, conjE, exE, disjE];
    2.11 +
    2.12  end;
     3.1 --- a/src/HOL/thy_syntax.ML	Mon Jan 01 11:54:36 1996 +0100
     3.2 +++ b/src/HOL/thy_syntax.ML	Tue Jan 02 10:46:50 1996 +0100
     3.3 @@ -51,30 +51,34 @@
     3.4        in
     3.5           (";\n\n\
     3.6            \structure " ^ stri_name ^ " =\n\
     3.7 -          \ let open Ind_Syntax in\n\
     3.8            \  struct\n\
     3.9            \  val _ = writeln \"" ^ co ^
    3.10                       "Inductive definition " ^ big_rec_name ^ "\"\n\
    3.11 -          \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
    3.12 +          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
    3.13                             ^ srec_tms ^ "\n\
    3.14            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    3.15                             ^ sintrs ^ "\n\
    3.16 -          \  end\n\
    3.17 -          \ end;\n\n\
    3.18 +          \  end;\n\n\
    3.19            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
    3.20               stri_name ^ ".rec_tms, " ^
    3.21               stri_name ^ ".intr_tms)"
    3.22           ,
    3.23            "structure " ^ big_rec_name ^ " =\n\
    3.24 -          \  struct\n\
    3.25 +          \ let\n\
    3.26 +          \  val _ = writeln \"Proofs for " ^ co ^ 
    3.27 +                     "Inductive definition " ^ big_rec_name ^ "\"\n\
    3.28            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    3.29 -          \  (open " ^ stri_name ^ "\n\
    3.30 -          \   val thy\t\t= thy\n\
    3.31 -          \   val monos\t\t= " ^ monos ^ "\n\
    3.32 -          \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    3.33 +          \\t  (open " ^ stri_name ^ "\n\
    3.34 +          \\t   val thy\t\t= thy\n\
    3.35 +          \\t   val monos\t\t= " ^ monos ^ "\n\
    3.36 +          \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    3.37 +	  \ in\n\
    3.38 +          \  struct\n\
    3.39            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    3.40            \  open Result\n\
    3.41 -          \  end\n"
    3.42 +          \  end\n\
    3.43 +          \ end;\n\n\
    3.44 +          \structure " ^ stri_name ^ " = struct end;\n\n"
    3.45           )
    3.46        end
    3.47      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)