kill old size infrastructure
authorblanchet
Wed Jan 03 11:06:13 2018 +0100 (17 months ago)
changeset 67332cb96edae56ef
parent 67331 a8770603a269
child 67333 ac0b81ca3ed5
kill old size infrastructure
src/HOL/Basic_BNF_LFPs.thy
src/HOL/Code_Numeral.thy
src/HOL/Library/Multiset.thy
src/HOL/Nat.thy
src/HOL/Tools/Old_Datatype/old_size.ML
     1.1 --- a/src/HOL/Basic_BNF_LFPs.thy	Tue Jan 02 23:04:15 2018 +0100
     1.2 +++ b/src/HOL/Basic_BNF_LFPs.thy	Wed Jan 03 11:06:13 2018 +0100
     1.3 @@ -104,14 +104,7 @@
     1.4  
     1.5  ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
     1.6  
     1.7 -ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
     1.8 -
     1.9 -lemma size_bool[code]: "size (b :: bool) = 0"
    1.10 -  by (cases b) auto
    1.11 -
    1.12 -declare prod.size[no_atp]
    1.13 -
    1.14 -lemmas size_nat = size_nat_def
    1.15 +declare prod.size [no_atp]
    1.16  
    1.17  hide_const (open) xtor ctor_rec
    1.18  
     2.1 --- a/src/HOL/Code_Numeral.thy	Tue Jan 02 23:04:15 2018 +0100
     2.2 +++ b/src/HOL/Code_Numeral.thy	Wed Jan 03 11:06:13 2018 +0100
     2.3 @@ -938,19 +938,14 @@
     2.4    shows P
     2.5    using assms by transfer blast
     2.6  
     2.7 -lemma [simp, code]: "size_natural = nat_of_natural"
     2.8 -proof (rule ext)
     2.9 -  fix n
    2.10 -  show "size_natural n = nat_of_natural n"
    2.11 -    by (induct n) simp_all
    2.12 -qed
    2.13 +instantiation natural :: size
    2.14 +begin
    2.15  
    2.16 -lemma [simp, code]: "size = nat_of_natural"
    2.17 -proof (rule ext)
    2.18 -  fix n
    2.19 -  show "size n = nat_of_natural n"
    2.20 -    by (induct n) simp_all
    2.21 -qed
    2.22 +definition size_nat where [simp, code]: "size_nat = nat_of_natural"
    2.23 +
    2.24 +instance ..
    2.25 +
    2.26 +end
    2.27  
    2.28  lemma natural_decr [termination_simp]:
    2.29    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
     3.1 --- a/src/HOL/Library/Multiset.thy	Tue Jan 02 23:04:15 2018 +0100
     3.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jan 03 11:06:13 2018 +0100
     3.3 @@ -3869,7 +3869,7 @@
     3.4  
     3.5  subsection \<open>Size setup\<close>
     3.6  
     3.7 -lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
     3.8 +lemma size_multiset_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
     3.9    apply (rule ext)
    3.10    subgoal for x by (induct x) auto
    3.11    done
    3.12 @@ -3879,7 +3879,7 @@
    3.13      @{thm size_multiset_overloaded_def}
    3.14      @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single
    3.15        size_union}
    3.16 -    @{thms multiset_size_o_map}
    3.17 +    @{thms size_multiset_o_map}
    3.18  \<close>
    3.19  
    3.20  subsection \<open>Lemmas about Size\<close>
     4.1 --- a/src/HOL/Nat.thy	Tue Jan 02 23:04:15 2018 +0100
     4.2 +++ b/src/HOL/Nat.thy	Wed Jan 03 11:06:13 2018 +0100
     4.3 @@ -2456,6 +2456,8 @@
     4.4  
     4.5  end
     4.6  
     4.7 +lemmas size_nat = size_nat_def
     4.8 +
     4.9  
    4.10  subsection \<open>Code module namespace\<close>
    4.11  
     5.1 --- a/src/HOL/Tools/Old_Datatype/old_size.ML	Tue Jan 02 23:04:15 2018 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,228 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/Old_Datatype/old_size.ML
     5.5 -    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
     5.6 -
     5.7 -Size functions for old-style datatypes.
     5.8 -*)
     5.9 -
    5.10 -structure Old_Size: sig end =
    5.11 -struct
    5.12 -
    5.13 -fun plus (t1, t2) = Const (@{const_name Groups.plus},
    5.14 -  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    5.15 -
    5.16 -fun size_of_type f g h (T as Type (s, Ts)) =
    5.17 -      (case f s of
    5.18 -         SOME t => SOME t
    5.19 -       | NONE => (case g s of
    5.20 -           SOME size_name =>
    5.21 -             SOME (list_comb (Const (size_name,
    5.22 -               map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
    5.23 -                 map (size_of_type' f g h) Ts))
    5.24 -         | NONE => NONE))
    5.25 -  | size_of_type _ _ h (TFree (s, _)) = h s
    5.26 -and size_of_type' f g h T = (case size_of_type f g h T of
    5.27 -      NONE => Abs ("x", T, HOLogic.zero)
    5.28 -    | SOME t => t);
    5.29 -
    5.30 -fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) =
    5.31 -      is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts
    5.32 -  | is_poly _ _ = true;
    5.33 -
    5.34 -fun constrs_of thy name =
    5.35 -  let
    5.36 -    val {descr, index, ...} = Old_Datatype_Data.the_info thy name
    5.37 -    val SOME (_, _, constrs) = AList.lookup op = descr index
    5.38 -  in constrs end;
    5.39 -
    5.40 -val app = curry (list_comb o swap);
    5.41 -
    5.42 -fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy =
    5.43 -  let
    5.44 -    val {descr, rec_names, rec_rewrites, induct, ...} = info;
    5.45 -    val l = length new_type_names;
    5.46 -    val descr' = List.take (descr, l);
    5.47 -    val tycos = map (#1 o snd) descr';
    5.48 -  in
    5.49 -    if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then
    5.50 -      (* nothing to do -- the "size" function is already defined *)
    5.51 -      thy
    5.52 -    else
    5.53 -      let
    5.54 -        val recTs = Old_Datatype_Aux.get_rec_types descr;
    5.55 -        val (recTs1, recTs2) = chop l recTs;
    5.56 -        val (_, (_, paramdts, _)) :: _ = descr;
    5.57 -        val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts;
    5.58 -        val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
    5.59 -          map (fn T as TFree (s, _) =>
    5.60 -            let
    5.61 -              val name = "f" ^ unprefix "'" s;
    5.62 -              val U = T --> HOLogic.natT
    5.63 -            in
    5.64 -              (((s, Free (name, U)), U), name)
    5.65 -            end) |> split_list |>> split_list;
    5.66 -        val param_size = AList.lookup op = param_size_fs;
    5.67 -
    5.68 -        val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
    5.69 -          map_filter (Option.map (#2 o snd) o BNF_LFP_Size.size_of_global thy) |> flat;
    5.70 -        val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy;
    5.71 -
    5.72 -        val (((size_names, size_fns), def_names), def_names') =
    5.73 -          recTs1 |> map (fn T as Type (s, _) =>
    5.74 -            let
    5.75 -              val s' = "size_" ^ Long_Name.base_name s;
    5.76 -              val s'' = Sign.full_bname thy s';
    5.77 -            in
    5.78 -              (s'',
    5.79 -               (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
    5.80 -                  map snd param_size_fs),
    5.81 -                (s' ^ "_def", s' ^ "_overloaded_def")))
    5.82 -            end) |> split_list ||>> split_list ||>> split_list;
    5.83 -        val overloaded_size_fns = map HOLogic.size_const recTs1;
    5.84 -
    5.85 -        (* instantiation for primrec combinator *)
    5.86 -        fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
    5.87 -          let
    5.88 -            val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
    5.89 -            val k = length (filter Old_Datatype_Aux.is_rec_type cargs);
    5.90 -            val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
    5.91 -              if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
    5.92 -              else
    5.93 -                (if b andalso is_poly thy dt' then
    5.94 -                   case size_of_type (K NONE) extra_size size_ofp T of
    5.95 -                     NONE => us | SOME sz => sz $ Bound j :: us
    5.96 -                 else us, i, j + 1))
    5.97 -                  (cargs ~~ cargs' ~~ Ts) ([], 0, k);
    5.98 -            val t =
    5.99 -              if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
   5.100 -              then HOLogic.zero
   5.101 -              else foldl1 plus (ts @ [HOLogic.Suc_zero])
   5.102 -          in
   5.103 -            fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
   5.104 -          end;
   5.105 -
   5.106 -        val fs = maps (fn (_, (name, _, constrs)) =>
   5.107 -          map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
   5.108 -        val fs' = maps (fn (n, (name, _, constrs)) =>
   5.109 -          map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
   5.110 -        val fTs = map fastype_of fs;
   5.111 -
   5.112 -        val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
   5.113 -          Const (rec_name, fTs @ [T] ---> HOLogic.natT))
   5.114 -            (recTs ~~ rec_names));
   5.115 -
   5.116 -        fun define_overloaded (def_name, eq) lthy =
   5.117 -          let
   5.118 -            val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
   5.119 -            val (thm, lthy') = lthy
   5.120 -              |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
   5.121 -              |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
   5.122 -            val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
   5.123 -            val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
   5.124 -          in (thm', lthy') end;
   5.125 -
   5.126 -        val ((size_def_thms, size_def_thms'), thy') =
   5.127 -          thy
   5.128 -          |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s),
   5.129 -              param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
   5.130 -            (size_names ~~ recTs1))
   5.131 -          |> Global_Theory.add_defs false
   5.132 -            (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
   5.133 -               (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
   5.134 -          ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size])
   5.135 -          ||>> fold_map define_overloaded
   5.136 -            (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
   5.137 -          ||> Class.prove_instantiation_instance (fn ctxt => Class.intro_classes_tac ctxt [])
   5.138 -          ||> Local_Theory.exit_global;
   5.139 -
   5.140 -        val ctxt = Proof_Context.init_global thy';
   5.141 -
   5.142 -        val simpset1 =
   5.143 -          put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
   5.144 -            size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
   5.145 -        val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
   5.146 -
   5.147 -        fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
   5.148 -          HOLogic.mk_eq (app fs r $ Free p,
   5.149 -            the (size_of_type tab extra_size size_ofp T) $ Free p);
   5.150 -
   5.151 -        fun prove_unfolded_size_eqs size_ofp fs =
   5.152 -          if null recTs2 then []
   5.153 -          else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
   5.154 -            (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @
   5.155 -               map (mk_unfolded_size_eq (AList.lookup op =
   5.156 -                   (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
   5.157 -                 (xs ~~ recTs2 ~~ rec_combs2))))
   5.158 -            (fn _ => (Old_Datatype_Aux.ind_tac ctxt induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
   5.159 -
   5.160 -        val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
   5.161 -        val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
   5.162 -
   5.163 -        (* characteristic equations for size functions *)
   5.164 -        fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
   5.165 -          let
   5.166 -            val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
   5.167 -            val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts);
   5.168 -            val ts = map_filter (fn (sT as (_, T), dt) =>
   5.169 -              Option.map (fn sz => sz $ Free sT)
   5.170 -                (if p dt then size_of_type size_of extra_size size_ofp T
   5.171 -                 else NONE)) (tnames ~~ Ts ~~ cargs)
   5.172 -          in
   5.173 -            HOLogic.mk_Trueprop (HOLogic.mk_eq
   5.174 -              (size_const $ list_comb (Const (cname, Ts ---> T),
   5.175 -                 map2 (curry Free) tnames Ts),
   5.176 -               if null ts then HOLogic.zero
   5.177 -               else foldl1 plus (ts @ [HOLogic.Suc_zero])))
   5.178 -          end;
   5.179 -
   5.180 -        val simpset2 =
   5.181 -          put_simpset HOL_basic_ss ctxt
   5.182 -            addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1);
   5.183 -        val simpset3 =
   5.184 -          put_simpset HOL_basic_ss ctxt
   5.185 -            addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2);
   5.186 -
   5.187 -        fun prove_size_eqs p size_fns size_ofp simpset =
   5.188 -          maps (fn (((_, (_, _, constrs)), size_const), T) =>
   5.189 -            map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
   5.190 -              (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
   5.191 -                 size_ofp size_const T constr)
   5.192 -              (fn _ => simp_tac simpset 1))) constrs)
   5.193 -            (descr' ~~ size_fns ~~ recTs1);
   5.194 -
   5.195 -        val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
   5.196 -          prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
   5.197 -
   5.198 -        val ([(_, size_thms)], thy'') = thy'
   5.199 -          |> Global_Theory.note_thmss ""
   5.200 -            [((Binding.name "size",
   5.201 -                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}]),
   5.202 -              [(size_eqns, [])])];
   5.203 -
   5.204 -      in
   5.205 -        thy''
   5.206 -        |> fold2 (fn new_type_name => fn size_name =>
   5.207 -            BNF_LFP_Size.register_size_global new_type_name size_name refl(*dummy*) size_thms [])
   5.208 -          new_type_names size_names 
   5.209 -        |> Code.declare_default_eqns_global (map (rpair true) size_thms)
   5.210 -      end
   5.211 -  end;
   5.212 -
   5.213 -fun add_size_thms _ (new_type_names as name :: _) thy =
   5.214 -  let
   5.215 -    val info as {descr, ...} = Old_Datatype_Data.the_info thy name;
   5.216 -    val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
   5.217 -    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
   5.218 -      Old_Datatype_Aux.is_rec_type dt andalso
   5.219 -        not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
   5.220 -  in
   5.221 -    if no_size then thy
   5.222 -    else
   5.223 -      thy
   5.224 -      |> Sign.add_path prefix
   5.225 -      |> prove_size_thms info new_type_names
   5.226 -      |> Sign.restore_naming thy
   5.227 -  end;
   5.228 -
   5.229 -val _ = Theory.setup (Old_Datatype_Data.interpretation add_size_thms);
   5.230 -
   5.231 -end;