src/HOL/Tools/datatype_abs_proofs.ML
changeset 24699 c6674504103f
parent 24589 d3fca349736c
child 24712 64ed05609568
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 25 10:27:43 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 25 12:16:08 2007 +0200
     1.3 @@ -10,8 +10,7 @@
     1.4   - characteristic equations for primrec combinators
     1.5   - characteristic equations for case combinators
     1.6   - equations for splitting "P (case ...)" expressions
     1.7 - - datatype size function
     1.8 - - "nchotomy" and "case_cong" theorems for TFL
     1.9 +  - "nchotomy" and "case_cong" theorems for TFL
    1.10  
    1.11  *)
    1.12  
    1.13 @@ -31,9 +30,6 @@
    1.14      DatatypeAux.descr list -> (string * sort) list ->
    1.15        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.16          (thm * thm) list * theory
    1.17 -  val prove_size_thms : bool -> string list ->
    1.18 -    DatatypeAux.descr list -> (string * sort) list ->
    1.19 -      string list -> thm list -> theory -> thm list * theory
    1.20    val prove_nchotomys : string list -> DatatypeAux.descr list ->
    1.21      (string * sort) list -> thm list -> theory -> thm list * theory
    1.22    val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
    1.23 @@ -381,83 +377,6 @@
    1.24      |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
    1.25    end;
    1.26  
    1.27 -(******************************* size functions *******************************)
    1.28 -
    1.29 -fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
    1.30 -  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
    1.31 -    is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
    1.32 -      (List.concat descr)
    1.33 -  then
    1.34 -    ([], thy)
    1.35 -  else
    1.36 -  let
    1.37 -    val _ = message "Proving equations for size function ...";
    1.38 -
    1.39 -    val big_name = space_implode "_" new_type_names;
    1.40 -    val thy1 = add_path flat_names big_name thy;
    1.41 -
    1.42 -    val descr' = flat descr;
    1.43 -    val recTs = get_rec_types descr' sorts;
    1.44 -
    1.45 -    val Const (size_name, _) = HOLogic.size_const dummyT;
    1.46 -    val size_names = replicate (length (hd descr)) size_name @
    1.47 -      map (Sign.full_name thy1) (DatatypeProp.indexify_names
    1.48 -        (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
    1.49 -    val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
    1.50 -      (map (fn T => name_of_typ T ^ "_size") recTs));
    1.51 -
    1.52 -    fun plus (t1, t2) =
    1.53 -      Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    1.54 -
    1.55 -    fun make_sizefun (_, cargs) =
    1.56 -      let
    1.57 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.58 -        val k = length (filter is_rec_type cargs);
    1.59 -        val t = if k = 0 then HOLogic.zero else
    1.60 -          foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.Suc_zero])
    1.61 -      in
    1.62 -        foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
    1.63 -      end;
    1.64 -
    1.65 -    val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr';
    1.66 -    val fTs = map fastype_of fs;
    1.67 -
    1.68 -    fun instance_size_class tyco thy =
    1.69 -      let
    1.70 -        val n = Sign.arity_number thy tyco;
    1.71 -      in
    1.72 -        thy
    1.73 -        |> Class.prove_instance (Class.intro_classes_tac [])
    1.74 -            [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    1.75 -        |> snd
    1.76 -      end
    1.77 -
    1.78 -    val (size_def_thms, thy') =
    1.79 -      thy1
    1.80 -      |> Theory.add_consts_i (map (fn (s, T) =>
    1.81 -           (Sign.base_name s, T --> HOLogic.natT, NoSyn))
    1.82 -           (Library.drop (length (hd descr), size_names ~~ recTs)))
    1.83 -      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
    1.84 -      |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) =>
    1.85 -           (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
    1.86 -            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))))
    1.87 -            (size_names ~~ recTs ~~ def_names ~~ reccomb_names))
    1.88 -      ||> parent_path flat_names;
    1.89 -
    1.90 -    val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
    1.91 -
    1.92 -    val size_thms = map (fn t => Goal.prove_global thy' [] [] t
    1.93 -      (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))
    1.94 -        (DatatypeProp.make_size descr sorts thy')
    1.95 -
    1.96 -  in
    1.97 -    thy'
    1.98 -    |> Theory.add_path big_name
    1.99 -    |> PureThy.add_thmss [(("size", size_thms), [])]
   1.100 -    ||> Theory.parent_path
   1.101 -    |-> (fn thmss => pair (flat thmss))
   1.102 -  end;
   1.103 -
   1.104  fun prove_weak_case_congs new_type_names descr sorts thy =
   1.105    let
   1.106      fun prove_weak_case_cong t =