moved old 'size' generator together with 'old_datatype'
authorblanchet
Thu Sep 18 16:47:40 2014 +0200 (2014-09-18)
changeset 58377c6f93b8d2d8e
parent 58376 c9d3074f83b3
child 58378 cf6f16bc11a7
moved old 'size' generator together with 'old_datatype'
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Basic_BNF_Least_Fixpoints.thy
src/HOL/Code_Numeral.thy
src/HOL/Fun_Def.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/Main.thy
src/HOL/Nat.thy
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Function/old_size.ML
src/HOL/Tools/Old_Datatype/old_size.ML
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 18 16:47:40 2014 +0200
     1.3 @@ -231,7 +231,6 @@
     1.4  ML_file "Tools/BNF/bnf_lfp_compat.ML"
     1.5  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
     1.6  ML_file "Tools/BNF/bnf_lfp_size.ML"
     1.7 -ML_file "Tools/Function/old_size.ML"
     1.8  
     1.9  hide_fact (open) id_transfer
    1.10  
     2.1 --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Thu Sep 18 16:47:40 2014 +0200
     2.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Thu Sep 18 16:47:40 2014 +0200
     2.3 @@ -9,32 +9,6 @@
     2.4  imports BNF_Least_Fixpoint
     2.5  begin
     2.6  
     2.7 -subsection {* Size setup (TODO: Merge with rest of file) *}
     2.8 -
     2.9 -lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    2.10 -  by (cases b) auto
    2.11 -
    2.12 -lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    2.13 -  by (induct n) simp_all
    2.14 -
    2.15 -declare prod.size[no_atp]
    2.16 -
    2.17 -lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    2.18 -  by (rule ext) (case_tac x, auto)
    2.19 -
    2.20 -lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    2.21 -  by (rule ext) auto
    2.22 -
    2.23 -setup {*
    2.24 -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    2.25 -  @{thms size_sum_o_map}
    2.26 -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    2.27 -  @{thms size_prod_o_map}
    2.28 -*}
    2.29 -
    2.30 -
    2.31 -subsection {* FP sugar setup *}
    2.32 -
    2.33  definition xtor :: "'a \<Rightarrow> 'a" where
    2.34    "xtor x = x"
    2.35  
    2.36 @@ -55,15 +29,6 @@
    2.37  
    2.38  lemmas xtor_inject = xtor_rel[of "op ="]
    2.39  
    2.40 -definition ctor_rec :: "'a \<Rightarrow> 'a" where
    2.41 -  "ctor_rec x = x"
    2.42 -
    2.43 -lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
    2.44 -  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    2.45 -
    2.46 -lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
    2.47 -  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    2.48 -
    2.49  lemma xtor_rel_induct: "(\<And>x y. vimage2p id_bnf id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
    2.50    unfolding xtor_def vimage2p_def id_bnf_def by default
    2.51  
    2.52 @@ -76,12 +41,30 @@
    2.53  lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
    2.54    unfolding xtor_def id_bnf_def by (rule reflexive)
    2.55  
    2.56 +definition ctor_rec :: "'a \<Rightarrow> 'a" where
    2.57 +  "ctor_rec x = x"
    2.58 +
    2.59 +lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
    2.60 +  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    2.61 +
    2.62 +lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
    2.63 +  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    2.64 +
    2.65 +lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
    2.66 +  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    2.67 +
    2.68  ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    2.69  
    2.70 +thm sum.rec_o_map
    2.71 +thm sum.size_o_map
    2.72 +
    2.73 +thm prod.rec_o_map
    2.74 +thm prod.size_o_map
    2.75 +
    2.76  hide_const (open) xtor ctor_rec
    2.77  
    2.78  hide_fact (open)
    2.79    xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
    2.80 -  ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
    2.81 +  ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
    2.82  
    2.83  end
     3.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 18 16:47:40 2014 +0200
     3.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 18 16:47:40 2014 +0200
     3.3 @@ -809,22 +809,6 @@
     3.4    shows P
     3.5    using assms by transfer blast
     3.6  
     3.7 -lemma [simp, code]:
     3.8 -  "size_natural = nat_of_natural"
     3.9 -proof (rule ext)
    3.10 -  fix n
    3.11 -  show "size_natural n = nat_of_natural n"
    3.12 -    by (induct n) simp_all
    3.13 -qed
    3.14 -
    3.15 -lemma [simp, code]:
    3.16 -  "size = nat_of_natural"
    3.17 -proof (rule ext)
    3.18 -  fix n
    3.19 -  show "size n = nat_of_natural n"
    3.20 -    by (induct n) simp_all
    3.21 -qed
    3.22 -
    3.23  lemma natural_decr [termination_simp]:
    3.24    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
    3.25    by transfer simp
     4.1 --- a/src/HOL/Fun_Def.thy	Thu Sep 18 16:47:40 2014 +0200
     4.2 +++ b/src/HOL/Fun_Def.thy	Thu Sep 18 16:47:40 2014 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Function Definitions and Termination Proofs *}
     4.5  
     4.6  theory Fun_Def
     4.7 -imports Partial_Function SAT
     4.8 +imports Basic_BNF_Least_Fixpoints Partial_Function SAT
     4.9  keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/Library/Old_Datatype.thy	Thu Sep 18 16:47:40 2014 +0200
     5.2 +++ b/src/HOL/Library/Old_Datatype.thy	Thu Sep 18 16:47:40 2014 +0200
     5.3 @@ -10,6 +10,10 @@
     5.4  keywords "old_datatype" :: thy_decl
     5.5  begin
     5.6  
     5.7 +ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
     5.8 +ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
     5.9 +
    5.10 +
    5.11  subsection {* The datatype universe *}
    5.12  
    5.13  definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    5.14 @@ -523,6 +527,5 @@
    5.15  
    5.16  ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
    5.17  ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
    5.18 -ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
    5.19  
    5.20  end
     6.1 --- a/src/HOL/Main.thy	Thu Sep 18 16:47:40 2014 +0200
     6.2 +++ b/src/HOL/Main.thy	Thu Sep 18 16:47:40 2014 +0200
     6.3 @@ -2,7 +2,7 @@
     6.4  
     6.5  theory Main
     6.6  imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
     6.7 -  Basic_BNF_Least_Fixpoints BNF_Greatest_Fixpoint
     6.8 +  BNF_Greatest_Fixpoint
     6.9  begin
    6.10  
    6.11  text {*
     7.1 --- a/src/HOL/Nat.thy	Thu Sep 18 16:47:40 2014 +0200
     7.2 +++ b/src/HOL/Nat.thy	Thu Sep 18 16:47:40 2014 +0200
     7.3 @@ -1185,7 +1185,7 @@
     7.4    by (fact Let_def)
     7.5  
     7.6  
     7.7 -subsubsection {* Monotonicity of Multiplication *}
     7.8 +subsubsection {* Monotonicity of multiplication *}
     7.9  
    7.10  lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
    7.11  by (simp add: mult_right_mono)
    7.12 @@ -1390,7 +1390,7 @@
    7.13  qed
    7.14  
    7.15  
    7.16 -subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
    7.17 +subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *}
    7.18  
    7.19  context semiring_1
    7.20  begin
    7.21 @@ -1512,7 +1512,7 @@
    7.22    by (auto simp add: fun_eq_iff)
    7.23  
    7.24  
    7.25 -subsection {* The Set of Natural Numbers *}
    7.26 +subsection {* The set of natural numbers *}
    7.27  
    7.28  context semiring_1
    7.29  begin
    7.30 @@ -1567,7 +1567,7 @@
    7.31  end
    7.32  
    7.33  
    7.34 -subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
    7.35 +subsection {* Further arithmetic facts concerning the natural numbers *}
    7.36  
    7.37  lemma subst_equals:
    7.38    assumes 1: "t = s" and 2: "u = t"
    7.39 @@ -1825,6 +1825,7 @@
    7.40    "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
    7.41    by (induct j arbitrary: i) (auto simp: le_Suc_eq)
    7.42   
    7.43 +
    7.44  subsection {* The divides relation on @{typ nat} *}
    7.45  
    7.46  lemma dvd_1_left [iff]: "Suc 0 dvd k"
    7.47 @@ -1962,7 +1963,7 @@
    7.48  qed
    7.49  
    7.50  
    7.51 -subsection {* aliases *}
    7.52 +subsection {* Aliases *}
    7.53  
    7.54  lemma nat_mult_1: "(1::nat) * n = n"
    7.55    by (rule mult_1_left)
    7.56 @@ -1971,13 +1972,23 @@
    7.57    by (rule mult_1_right)
    7.58  
    7.59  
    7.60 -subsection {* size of a datatype value *}
    7.61 +subsection {* Size of a datatype value *}
    7.62  
    7.63  class size =
    7.64    fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
    7.65  
    7.66 -
    7.67 -subsection {* code module namespace *}
    7.68 +instantiation nat :: size
    7.69 +begin
    7.70 +
    7.71 +definition size_nat where
    7.72 +  [simp, code]: "size (n \<Colon> nat) = n"
    7.73 +
    7.74 +instance ..
    7.75 +
    7.76 +end
    7.77 +
    7.78 +
    7.79 +subsection {* Code module namespace *}
    7.80  
    7.81  code_identifier
    7.82    code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 18 16:47:40 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 18 16:47:40 2014 +0200
     8.3 @@ -15,7 +15,6 @@
     8.4  open BNF_FP_Rec_Sugar_Util
     8.5  open BNF_FP_Util
     8.6  open BNF_FP_Def_Sugar
     8.7 -open BNF_LFP_Size
     8.8  
     8.9  fun trivial_absT_info_of fpT =
    8.10    {absT = fpT,
    8.11 @@ -38,10 +37,10 @@
    8.12     dtors = [Const (@{const_name xtor}, fpT --> fpT)],
    8.13     xtor_co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))],
    8.14     xtor_co_induct = @{thm xtor_induct},
    8.15 -   dtor_ctors = [@{thm xtor_xtor}],
    8.16 -   ctor_dtors = [@{thm xtor_xtor}],
    8.17 -   ctor_injects = [@{thm xtor_inject}],
    8.18 -   dtor_injects = [@{thm xtor_inject}],
    8.19 +   dtor_ctors = @{thms xtor_xtor},
    8.20 +   ctor_dtors = @{thms xtor_xtor},
    8.21 +   ctor_injects = @{thms xtor_inject},
    8.22 +   dtor_injects = @{thms xtor_inject},
    8.23     xtor_map_thms = [xtor_map],
    8.24     xtor_set_thmss = [xtor_sets],
    8.25     xtor_rel_thms = [xtor_rel],
    8.26 @@ -80,10 +79,10 @@
    8.27       ctr_defs = @{thms Inl_def_alt Inr_def_alt},
    8.28       ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
    8.29       co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
    8.30 -     co_rec_def = @{thm case_sum_def},
    8.31 +     co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
    8.32       maps = @{thms map_sum.simps},
    8.33 -     common_co_inducts = [@{thm sum.induct}],
    8.34 -     co_inducts = [@{thm sum.induct}],
    8.35 +     common_co_inducts = @{thms sum.induct},
    8.36 +     co_inducts = @{thms sum.induct},
    8.37       co_rec_thms = @{thms sum.case},
    8.38       co_rec_discs = [],
    8.39       co_rec_selss = [],
    8.40 @@ -118,22 +117,22 @@
    8.41       fp_nesting_bnfs = [],
    8.42       live_nesting_bnfs = [],
    8.43       ctrXs_Tss = [ctr_Ts],
    8.44 -     ctr_defs = [@{thm Pair_def_alt}],
    8.45 +     ctr_defs = @{thms Pair_def_alt},
    8.46       ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
    8.47       co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
    8.48 -     co_rec_def = @{thm case_prod_def},
    8.49 -     maps = [@{thm map_prod_simp}],
    8.50 -     common_co_inducts = [@{thm prod.induct}],
    8.51 -     co_inducts = [@{thm prod.induct}],
    8.52 -     co_rec_thms = [@{thm prod.case}],
    8.53 +     co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
    8.54 +     maps = @{thms map_prod_simp},
    8.55 +     common_co_inducts = @{thms prod.induct},
    8.56 +     co_inducts = @{thms prod.induct},
    8.57 +     co_rec_thms = @{thms prod.case},
    8.58       co_rec_discs = [],
    8.59       co_rec_selss = [],
    8.60 -     rel_injects = [@{thm rel_prod_apply}],
    8.61 +     rel_injects = @{thms rel_prod_apply},
    8.62       rel_distincts = []}
    8.63    end;
    8.64  
    8.65  val _ = Theory.setup (map_local_theory (fn lthy =>
    8.66 -  fold (BNF_FP_Def_Sugar.register_fp_sugars (fn s => s <> size_plugin) o single o (fn f => f lthy))
    8.67 +  fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy))
    8.68      [fp_sugar_of_sum, fp_sugar_of_prod] lthy));
    8.69  
    8.70  end;
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 18 16:47:40 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 18 16:47:40 2014 +0200
     9.3 @@ -67,8 +67,7 @@
     9.4  
     9.5  fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
     9.6      ctor_rec_o_map =
     9.7 -  unfold_thms_tac ctxt [rec_def] THEN
     9.8 -  HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN'
     9.9 +  HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' rtac (ctor_rec_o_map RS trans) THEN'
    9.10      CONVERSION Thm.eta_long_conversion THEN'
    9.11      asm_simp_tac (ss_only (pre_map_defs @
    9.12          distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps)
    10.1 --- a/src/HOL/Tools/Function/old_size.ML	Thu Sep 18 16:47:40 2014 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,228 +0,0 @@
    10.4 -(*  Title:      HOL/Tools/Function/old_size.ML
    10.5 -    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
    10.6 -
    10.7 -Size functions for old-style datatypes.
    10.8 -*)
    10.9 -
   10.10 -structure Old_Size: sig end =
   10.11 -struct
   10.12 -
   10.13 -fun plus (t1, t2) = Const (@{const_name Groups.plus},
   10.14 -  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
   10.15 -
   10.16 -fun size_of_type f g h (T as Type (s, Ts)) =
   10.17 -      (case f s of
   10.18 -         SOME t => SOME t
   10.19 -       | NONE => (case g s of
   10.20 -           SOME size_name =>
   10.21 -             SOME (list_comb (Const (size_name,
   10.22 -               map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
   10.23 -                 map (size_of_type' f g h) Ts))
   10.24 -         | NONE => NONE))
   10.25 -  | size_of_type _ _ h (TFree (s, _)) = h s
   10.26 -and size_of_type' f g h T = (case size_of_type f g h T of
   10.27 -      NONE => Abs ("x", T, HOLogic.zero)
   10.28 -    | SOME t => t);
   10.29 -
   10.30 -fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) =
   10.31 -      is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts
   10.32 -  | is_poly _ _ = true;
   10.33 -
   10.34 -fun constrs_of thy name =
   10.35 -  let
   10.36 -    val {descr, index, ...} = Old_Datatype_Data.the_info thy name
   10.37 -    val SOME (_, _, constrs) = AList.lookup op = descr index
   10.38 -  in constrs end;
   10.39 -
   10.40 -val app = curry (list_comb o swap);
   10.41 -
   10.42 -fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy =
   10.43 -  let
   10.44 -    val {descr, rec_names, rec_rewrites, induct, ...} = info;
   10.45 -    val l = length new_type_names;
   10.46 -    val descr' = List.take (descr, l);
   10.47 -    val tycos = map (#1 o snd) descr';
   10.48 -  in
   10.49 -    if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then
   10.50 -      (* nothing to do -- the "size" function is already defined *)
   10.51 -      thy
   10.52 -    else
   10.53 -      let
   10.54 -        val recTs = Old_Datatype_Aux.get_rec_types descr;
   10.55 -        val (recTs1, recTs2) = chop l recTs;
   10.56 -        val (_, (_, paramdts, _)) :: _ = descr;
   10.57 -        val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts;
   10.58 -        val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
   10.59 -          map (fn T as TFree (s, _) =>
   10.60 -            let
   10.61 -              val name = "f" ^ unprefix "'" s;
   10.62 -              val U = T --> HOLogic.natT
   10.63 -            in
   10.64 -              (((s, Free (name, U)), U), name)
   10.65 -            end) |> split_list |>> split_list;
   10.66 -        val param_size = AList.lookup op = param_size_fs;
   10.67 -
   10.68 -        val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
   10.69 -          map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat;
   10.70 -        val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy;
   10.71 -
   10.72 -        val (((size_names, size_fns), def_names), def_names') =
   10.73 -          recTs1 |> map (fn T as Type (s, _) =>
   10.74 -            let
   10.75 -              val s' = "size_" ^ Long_Name.base_name s;
   10.76 -              val s'' = Sign.full_bname thy s';
   10.77 -            in
   10.78 -              (s'',
   10.79 -               (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
   10.80 -                  map snd param_size_fs),
   10.81 -                (s' ^ "_def", s' ^ "_overloaded_def")))
   10.82 -            end) |> split_list ||>> split_list ||>> split_list;
   10.83 -        val overloaded_size_fns = map HOLogic.size_const recTs1;
   10.84 -
   10.85 -        (* instantiation for primrec combinator *)
   10.86 -        fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
   10.87 -          let
   10.88 -            val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
   10.89 -            val k = length (filter Old_Datatype_Aux.is_rec_type cargs);
   10.90 -            val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
   10.91 -              if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
   10.92 -              else
   10.93 -                (if b andalso is_poly thy dt' then
   10.94 -                   case size_of_type (K NONE) extra_size size_ofp T of
   10.95 -                     NONE => us | SOME sz => sz $ Bound j :: us
   10.96 -                 else us, i, j + 1))
   10.97 -                  (cargs ~~ cargs' ~~ Ts) ([], 0, k);
   10.98 -            val t =
   10.99 -              if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
  10.100 -              then HOLogic.zero
  10.101 -              else foldl1 plus (ts @ [HOLogic.Suc_zero])
  10.102 -          in
  10.103 -            fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
  10.104 -          end;
  10.105 -
  10.106 -        val fs = maps (fn (_, (name, _, constrs)) =>
  10.107 -          map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
  10.108 -        val fs' = maps (fn (n, (name, _, constrs)) =>
  10.109 -          map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
  10.110 -        val fTs = map fastype_of fs;
  10.111 -
  10.112 -        val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
  10.113 -          Const (rec_name, fTs @ [T] ---> HOLogic.natT))
  10.114 -            (recTs ~~ rec_names));
  10.115 -
  10.116 -        fun define_overloaded (def_name, eq) lthy =
  10.117 -          let
  10.118 -            val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
  10.119 -            val (thm, lthy') = lthy
  10.120 -              |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
  10.121 -              |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
  10.122 -            val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
  10.123 -            val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
  10.124 -          in (thm', lthy') end;
  10.125 -
  10.126 -        val ((size_def_thms, size_def_thms'), thy') =
  10.127 -          thy
  10.128 -          |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s),
  10.129 -              param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
  10.130 -            (size_names ~~ recTs1))
  10.131 -          |> Global_Theory.add_defs false
  10.132 -            (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
  10.133 -               (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
  10.134 -          ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size])
  10.135 -          ||>> fold_map define_overloaded
  10.136 -            (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
  10.137 -          ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
  10.138 -          ||> Local_Theory.exit_global;
  10.139 -
  10.140 -        val ctxt = Proof_Context.init_global thy';
  10.141 -
  10.142 -        val simpset1 =
  10.143 -          put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
  10.144 -            size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
  10.145 -        val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
  10.146 -
  10.147 -        fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
  10.148 -          HOLogic.mk_eq (app fs r $ Free p,
  10.149 -            the (size_of_type tab extra_size size_ofp T) $ Free p);
  10.150 -
  10.151 -        fun prove_unfolded_size_eqs size_ofp fs =
  10.152 -          if null recTs2 then []
  10.153 -          else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
  10.154 -            (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @
  10.155 -               map (mk_unfolded_size_eq (AList.lookup op =
  10.156 -                   (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
  10.157 -                 (xs ~~ recTs2 ~~ rec_combs2))))
  10.158 -            (fn _ => (Old_Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
  10.159 -
  10.160 -        val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
  10.161 -        val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
  10.162 -
  10.163 -        (* characteristic equations for size functions *)
  10.164 -        fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
  10.165 -          let
  10.166 -            val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
  10.167 -            val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts);
  10.168 -            val ts = map_filter (fn (sT as (_, T), dt) =>
  10.169 -              Option.map (fn sz => sz $ Free sT)
  10.170 -                (if p dt then size_of_type size_of extra_size size_ofp T
  10.171 -                 else NONE)) (tnames ~~ Ts ~~ cargs)
  10.172 -          in
  10.173 -            HOLogic.mk_Trueprop (HOLogic.mk_eq
  10.174 -              (size_const $ list_comb (Const (cname, Ts ---> T),
  10.175 -                 map2 (curry Free) tnames Ts),
  10.176 -               if null ts then HOLogic.zero
  10.177 -               else foldl1 plus (ts @ [HOLogic.Suc_zero])))
  10.178 -          end;
  10.179 -
  10.180 -        val simpset2 =
  10.181 -          put_simpset HOL_basic_ss ctxt
  10.182 -            addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1);
  10.183 -        val simpset3 =
  10.184 -          put_simpset HOL_basic_ss ctxt
  10.185 -            addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2);
  10.186 -
  10.187 -        fun prove_size_eqs p size_fns size_ofp simpset =
  10.188 -          maps (fn (((_, (_, _, constrs)), size_const), T) =>
  10.189 -            map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
  10.190 -              (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
  10.191 -                 size_ofp size_const T constr)
  10.192 -              (fn _ => simp_tac simpset 1))) constrs)
  10.193 -            (descr' ~~ size_fns ~~ recTs1);
  10.194 -
  10.195 -        val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
  10.196 -          prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
  10.197 -
  10.198 -        val ([(_, size_thms)], thy'') = thy'
  10.199 -          |> Global_Theory.note_thmss ""
  10.200 -            [((Binding.name "size",
  10.201 -                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
  10.202 -                 Thm.declaration_attribute (fn thm =>
  10.203 -                   Context.mapping (Code.add_default_eqn thm) I)]),
  10.204 -              [(size_eqns, [])])];
  10.205 -
  10.206 -      in
  10.207 -        fold2 (fn new_type_name => fn size_name =>
  10.208 -            BNF_LFP_Size.register_size_global new_type_name size_name size_thms [])
  10.209 -          new_type_names size_names thy''
  10.210 -      end
  10.211 -  end;
  10.212 -
  10.213 -fun add_size_thms _ (new_type_names as name :: _) thy =
  10.214 -  let
  10.215 -    val info as {descr, ...} = Old_Datatype_Data.the_info thy name;
  10.216 -    val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
  10.217 -    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
  10.218 -      Old_Datatype_Aux.is_rec_type dt andalso
  10.219 -        not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
  10.220 -  in
  10.221 -    if no_size then thy
  10.222 -    else
  10.223 -      thy
  10.224 -      |> Sign.add_path prefix
  10.225 -      |> prove_size_thms info new_type_names
  10.226 -      |> Sign.restore_naming thy
  10.227 -  end;
  10.228 -
  10.229 -val _ = Context.>> (Context.map_theory (Old_Datatype_Data.interpretation add_size_thms));
  10.230 -
  10.231 -end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/Old_Datatype/old_size.ML	Thu Sep 18 16:47:40 2014 +0200
    11.3 @@ -0,0 +1,229 @@
    11.4 +(*  Title:      HOL/Tools/Old_Datatype/old_size.ML
    11.5 +    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
    11.6 +
    11.7 +Size functions for old-style datatypes.
    11.8 +*)
    11.9 +
   11.10 +structure Old_Size: sig end =
   11.11 +struct
   11.12 +
   11.13 +fun plus (t1, t2) = Const (@{const_name Groups.plus},
   11.14 +  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
   11.15 +
   11.16 +fun size_of_type f g h (T as Type (s, Ts)) =
   11.17 +      (case f s of
   11.18 +         SOME t => SOME t
   11.19 +       | NONE => (case g s of
   11.20 +           SOME size_name =>
   11.21 +             SOME (list_comb (Const (size_name,
   11.22 +               map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
   11.23 +                 map (size_of_type' f g h) Ts))
   11.24 +         | NONE => NONE))
   11.25 +  | size_of_type _ _ h (TFree (s, _)) = h s
   11.26 +and size_of_type' f g h T = (case size_of_type f g h T of
   11.27 +      NONE => Abs ("x", T, HOLogic.zero)
   11.28 +    | SOME t => t);
   11.29 +
   11.30 +fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) =
   11.31 +      is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts
   11.32 +  | is_poly _ _ = true;
   11.33 +
   11.34 +fun constrs_of thy name =
   11.35 +  let
   11.36 +    val {descr, index, ...} = Old_Datatype_Data.the_info thy name
   11.37 +    val SOME (_, _, constrs) = AList.lookup op = descr index
   11.38 +  in constrs end;
   11.39 +
   11.40 +val app = curry (list_comb o swap);
   11.41 +
   11.42 +fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy =
   11.43 +  let
   11.44 +    val {descr, rec_names, rec_rewrites, induct, ...} = info;
   11.45 +    val l = length new_type_names;
   11.46 +    val descr' = List.take (descr, l);
   11.47 +    val tycos = map (#1 o snd) descr';
   11.48 +  in
   11.49 +    if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then
   11.50 +      (* nothing to do -- the "size" function is already defined *)
   11.51 +      thy
   11.52 +    else
   11.53 +      let
   11.54 +        val recTs = Old_Datatype_Aux.get_rec_types descr;
   11.55 +        val (recTs1, recTs2) = chop l recTs;
   11.56 +        val (_, (_, paramdts, _)) :: _ = descr;
   11.57 +        val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts;
   11.58 +        val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
   11.59 +          map (fn T as TFree (s, _) =>
   11.60 +            let
   11.61 +              val name = "f" ^ unprefix "'" s;
   11.62 +              val U = T --> HOLogic.natT
   11.63 +            in
   11.64 +              (((s, Free (name, U)), U), name)
   11.65 +            end) |> split_list |>> split_list;
   11.66 +        val param_size = AList.lookup op = param_size_fs;
   11.67 +
   11.68 +        val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
   11.69 +          map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat;
   11.70 +        val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy;
   11.71 +
   11.72 +        val (((size_names, size_fns), def_names), def_names') =
   11.73 +          recTs1 |> map (fn T as Type (s, _) =>
   11.74 +            let
   11.75 +              val s' = "size_" ^ Long_Name.base_name s;
   11.76 +              val s'' = Sign.full_bname thy s';
   11.77 +            in
   11.78 +              (s'',
   11.79 +               (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
   11.80 +                  map snd param_size_fs),
   11.81 +                (s' ^ "_def", s' ^ "_overloaded_def")))
   11.82 +            end) |> split_list ||>> split_list ||>> split_list;
   11.83 +        val overloaded_size_fns = map HOLogic.size_const recTs1;
   11.84 +
   11.85 +        (* instantiation for primrec combinator *)
   11.86 +        fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
   11.87 +          let
   11.88 +            val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
   11.89 +            val k = length (filter Old_Datatype_Aux.is_rec_type cargs);
   11.90 +            val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
   11.91 +              if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
   11.92 +              else
   11.93 +                (if b andalso is_poly thy dt' then
   11.94 +                   case size_of_type (K NONE) extra_size size_ofp T of
   11.95 +                     NONE => us | SOME sz => sz $ Bound j :: us
   11.96 +                 else us, i, j + 1))
   11.97 +                  (cargs ~~ cargs' ~~ Ts) ([], 0, k);
   11.98 +            val t =
   11.99 +              if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
  11.100 +              then HOLogic.zero
  11.101 +              else foldl1 plus (ts @ [HOLogic.Suc_zero])
  11.102 +          in
  11.103 +            fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
  11.104 +          end;
  11.105 +
  11.106 +        val fs = maps (fn (_, (name, _, constrs)) =>
  11.107 +          map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
  11.108 +        val fs' = maps (fn (n, (name, _, constrs)) =>
  11.109 +          map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
  11.110 +        val fTs = map fastype_of fs;
  11.111 +
  11.112 +        val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
  11.113 +          Const (rec_name, fTs @ [T] ---> HOLogic.natT))
  11.114 +            (recTs ~~ rec_names));
  11.115 +
  11.116 +        fun define_overloaded (def_name, eq) lthy =
  11.117 +          let
  11.118 +            val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
  11.119 +            val (thm, lthy') = lthy
  11.120 +              |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
  11.121 +              |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
  11.122 +            val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
  11.123 +            val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
  11.124 +          in (thm', lthy') end;
  11.125 +
  11.126 +        val ((size_def_thms, size_def_thms'), thy') =
  11.127 +          thy
  11.128 +          |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s),
  11.129 +              param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
  11.130 +            (size_names ~~ recTs1))
  11.131 +          |> Global_Theory.add_defs false
  11.132 +            (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
  11.133 +               (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
  11.134 +          ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size])
  11.135 +          ||>> fold_map define_overloaded
  11.136 +            (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
  11.137 +          ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
  11.138 +          ||> Local_Theory.exit_global;
  11.139 +
  11.140 +        val ctxt = Proof_Context.init_global thy';
  11.141 +
  11.142 +        val simpset1 =
  11.143 +          put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
  11.144 +            size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
  11.145 +        val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
  11.146 +
  11.147 +        fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
  11.148 +          HOLogic.mk_eq (app fs r $ Free p,
  11.149 +            the (size_of_type tab extra_size size_ofp T) $ Free p);
  11.150 +
  11.151 +        fun prove_unfolded_size_eqs size_ofp fs =
  11.152 +          if null recTs2 then []
  11.153 +          else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
  11.154 +            (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @
  11.155 +               map (mk_unfolded_size_eq (AList.lookup op =
  11.156 +                   (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
  11.157 +                 (xs ~~ recTs2 ~~ rec_combs2))))
  11.158 +            (fn _ => (Old_Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
  11.159 +
  11.160 +        val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
  11.161 +        val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
  11.162 +
  11.163 +        (* characteristic equations for size functions *)
  11.164 +        fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
  11.165 +          let
  11.166 +            val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
  11.167 +            val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts);
  11.168 +            val ts = map_filter (fn (sT as (_, T), dt) =>
  11.169 +              Option.map (fn sz => sz $ Free sT)
  11.170 +                (if p dt then size_of_type size_of extra_size size_ofp T
  11.171 +                 else NONE)) (tnames ~~ Ts ~~ cargs)
  11.172 +          in
  11.173 +            HOLogic.mk_Trueprop (HOLogic.mk_eq
  11.174 +              (size_const $ list_comb (Const (cname, Ts ---> T),
  11.175 +                 map2 (curry Free) tnames Ts),
  11.176 +               if null ts then HOLogic.zero
  11.177 +               else foldl1 plus (ts @ [HOLogic.Suc_zero])))
  11.178 +          end;
  11.179 +
  11.180 +        val simpset2 =
  11.181 +          put_simpset HOL_basic_ss ctxt
  11.182 +            addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1);
  11.183 +        val simpset3 =
  11.184 +          put_simpset HOL_basic_ss ctxt
  11.185 +            addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2);
  11.186 +
  11.187 +        fun prove_size_eqs p size_fns size_ofp simpset =
  11.188 +          maps (fn (((_, (_, _, constrs)), size_const), T) =>
  11.189 +            map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
  11.190 +              (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
  11.191 +                 size_ofp size_const T constr)
  11.192 +              (fn _ => simp_tac simpset 1))) constrs)
  11.193 +            (descr' ~~ size_fns ~~ recTs1);
  11.194 +
  11.195 +        val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
  11.196 +          prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
  11.197 +
  11.198 +        val ([(_, size_thms)], thy'') = thy'
  11.199 +          |> Global_Theory.note_thmss ""
  11.200 +            [((Binding.name "size",
  11.201 +                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
  11.202 +                 Thm.declaration_attribute (fn thm =>
  11.203 +                   Context.mapping (Code.add_default_eqn thm) I)]),
  11.204 +              [(size_eqns, [])])];
  11.205 +
  11.206 +      in
  11.207 +        fold2 (fn new_type_name => fn size_name =>
  11.208 +            BNF_LFP_Size.register_size_global new_type_name size_name size_thms [])
  11.209 +          new_type_names size_names thy''
  11.210 +      end
  11.211 +  end;
  11.212 +
  11.213 +fun add_size_thms _ (new_type_names as name :: _) thy =
  11.214 +  let
  11.215 +    val info as {descr, ...} = Old_Datatype_Data.the_info thy name;
  11.216 +    val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
  11.217 +    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
  11.218 +      Old_Datatype_Aux.is_rec_type dt andalso
  11.219 +        not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
  11.220 +val _ = tracing ("NAME: " ^ @{make_string} (name, no_size))(*###*)
  11.221 +  in
  11.222 +    if no_size then thy
  11.223 +    else
  11.224 +      thy
  11.225 +      |> Sign.add_path prefix
  11.226 +      |> prove_size_thms info new_type_names
  11.227 +      |> Sign.restore_naming thy
  11.228 +  end;
  11.229 +
  11.230 +val _ = Theory.setup (Old_Datatype_Data.interpretation add_size_thms);
  11.231 +
  11.232 +end;