# HG changeset patch # User blanchet # Date 1411051660 -7200 # Node ID c6f93b8d2d8e6cdafd1400100abe25045e70b0c1 # Parent c9d3074f83b38c9956381733ae6767b25aca3423 moved old 'size' generator together with 'old_datatype' diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 18 16:47:40 2014 +0200 @@ -231,7 +231,6 @@ ML_file "Tools/BNF/bnf_lfp_compat.ML" ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" ML_file "Tools/BNF/bnf_lfp_size.ML" -ML_file "Tools/Function/old_size.ML" hide_fact (open) id_transfer diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Basic_BNF_Least_Fixpoints.thy --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy Thu Sep 18 16:47:40 2014 +0200 @@ -9,32 +9,6 @@ imports BNF_Least_Fixpoint begin -subsection {* Size setup (TODO: Merge with rest of file) *} - -lemma size_bool[code]: "size (b\bool) = 0" - by (cases b) auto - -lemma size_nat[simp, code]: "size (n\nat) = n" - by (induct n) simp_all - -declare prod.size[no_atp] - -lemma size_sum_o_map: "size_sum g1 g2 \ map_sum f1 f2 = size_sum (g1 \ f1) (g2 \ f2)" - by (rule ext) (case_tac x, auto) - -lemma size_prod_o_map: "size_prod g1 g2 \ map_prod f1 f2 = size_prod (g1 \ f1) (g2 \ f2)" - by (rule ext) auto - -setup {* -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} - @{thms size_sum_o_map} -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} - @{thms size_prod_o_map} -*} - - -subsection {* FP sugar setup *} - definition xtor :: "'a \ 'a" where "xtor x = x" @@ -55,15 +29,6 @@ lemmas xtor_inject = xtor_rel[of "op ="] -definition ctor_rec :: "'a \ 'a" where - "ctor_rec x = x" - -lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((id_bnf \ g \ id_bnf) x)" - unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) - -lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (id_bnf \ g \ id_bnf))" - unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) - lemma xtor_rel_induct: "(\x y. vimage2p id_bnf id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR" unfolding xtor_def vimage2p_def id_bnf_def by default @@ -76,12 +41,30 @@ lemma Pair_def_alt: "Pair \ (\a b. xtor (id_bnf (a, b)))" unfolding xtor_def id_bnf_def by (rule reflexive) +definition ctor_rec :: "'a \ 'a" where + "ctor_rec x = x" + +lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((id_bnf \ g \ id_bnf) x)" + unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) + +lemma ctor_rec_def_alt: "f = ctor_rec (f \ id_bnf)" + unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) + +lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (id_bnf \ g \ id_bnf))" + unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) + ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" +thm sum.rec_o_map +thm sum.size_o_map + +thm prod.rec_o_map +thm prod.size_o_map + hide_const (open) xtor ctor_rec hide_fact (open) xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec - ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt + ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt end diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Code_Numeral.thy Thu Sep 18 16:47:40 2014 +0200 @@ -809,22 +809,6 @@ shows P using assms by transfer blast -lemma [simp, code]: - "size_natural = nat_of_natural" -proof (rule ext) - fix n - show "size_natural n = nat_of_natural n" - by (induct n) simp_all -qed - -lemma [simp, code]: - "size = nat_of_natural" -proof (rule ext) - fix n - show "size n = nat_of_natural n" - by (induct n) simp_all -qed - lemma natural_decr [termination_simp]: "n \ 0 \ nat_of_natural n - Nat.Suc 0 < nat_of_natural n" by transfer simp diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Fun_Def.thy --- a/src/HOL/Fun_Def.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Fun_Def.thy Thu Sep 18 16:47:40 2014 +0200 @@ -5,7 +5,7 @@ header {* Function Definitions and Termination Proofs *} theory Fun_Def -imports Partial_Function SAT +imports Basic_BNF_Least_Fixpoints Partial_Function SAT keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl begin diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Library/Old_Datatype.thy --- a/src/HOL/Library/Old_Datatype.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Library/Old_Datatype.thy Thu Sep 18 16:47:40 2014 +0200 @@ -10,6 +10,10 @@ keywords "old_datatype" :: thy_decl begin +ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" +ML_file "~~/src/HOL/Tools/datatype_realizer.ML" + + subsection {* The datatype universe *} definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" @@ -523,6 +527,5 @@ ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML" ML_file "~~/src/HOL/Tools/inductive_realizer.ML" -ML_file "~~/src/HOL/Tools/datatype_realizer.ML" end diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Main.thy --- a/src/HOL/Main.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Main.thy Thu Sep 18 16:47:40 2014 +0200 @@ -2,7 +2,7 @@ theory Main imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick - Basic_BNF_Least_Fixpoints BNF_Greatest_Fixpoint + BNF_Greatest_Fixpoint begin text {* diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Nat.thy Thu Sep 18 16:47:40 2014 +0200 @@ -1185,7 +1185,7 @@ by (fact Let_def) -subsubsection {* Monotonicity of Multiplication *} +subsubsection {* Monotonicity of multiplication *} lemma mult_le_mono1: "i \ (j::nat) ==> i * k \ j * k" by (simp add: mult_right_mono) @@ -1390,7 +1390,7 @@ qed -subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *} +subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *} context semiring_1 begin @@ -1512,7 +1512,7 @@ by (auto simp add: fun_eq_iff) -subsection {* The Set of Natural Numbers *} +subsection {* The set of natural numbers *} context semiring_1 begin @@ -1567,7 +1567,7 @@ end -subsection {* Further Arithmetic Facts Concerning the Natural Numbers *} +subsection {* Further arithmetic facts concerning the natural numbers *} lemma subst_equals: assumes 1: "t = s" and 2: "u = t" @@ -1825,6 +1825,7 @@ "i \ j \ P i \ (\n. i \ n \ n < j \ P n \ P (Suc n)) \ P j" by (induct j arbitrary: i) (auto simp: le_Suc_eq) + subsection {* The divides relation on @{typ nat} *} lemma dvd_1_left [iff]: "Suc 0 dvd k" @@ -1962,7 +1963,7 @@ qed -subsection {* aliases *} +subsection {* Aliases *} lemma nat_mult_1: "(1::nat) * n = n" by (rule mult_1_left) @@ -1971,13 +1972,23 @@ by (rule mult_1_right) -subsection {* size of a datatype value *} +subsection {* Size of a datatype value *} class size = fixes size :: "'a \ nat" -- {* see further theory @{text Wellfounded} *} - -subsection {* code module namespace *} +instantiation nat :: size +begin + +definition size_nat where + [simp, code]: "size (n \ nat) = n" + +instance .. + +end + + +subsection {* Code module namespace *} code_identifier code_module Nat \ (SML) Arith and (OCaml) Arith and (Haskell) Arith diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 18 16:47:40 2014 +0200 @@ -15,7 +15,6 @@ open BNF_FP_Rec_Sugar_Util open BNF_FP_Util open BNF_FP_Def_Sugar -open BNF_LFP_Size fun trivial_absT_info_of fpT = {absT = fpT, @@ -38,10 +37,10 @@ dtors = [Const (@{const_name xtor}, fpT --> fpT)], xtor_co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))], xtor_co_induct = @{thm xtor_induct}, - dtor_ctors = [@{thm xtor_xtor}], - ctor_dtors = [@{thm xtor_xtor}], - ctor_injects = [@{thm xtor_inject}], - dtor_injects = [@{thm xtor_inject}], + dtor_ctors = @{thms xtor_xtor}, + ctor_dtors = @{thms xtor_xtor}, + ctor_injects = @{thms xtor_inject}, + dtor_injects = @{thms xtor_inject}, xtor_map_thms = [xtor_map], xtor_set_thmss = [xtor_sets], xtor_rel_thms = [xtor_rel], @@ -80,10 +79,10 @@ ctr_defs = @{thms Inl_def_alt Inr_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), - co_rec_def = @{thm case_sum_def}, + co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]}, maps = @{thms map_sum.simps}, - common_co_inducts = [@{thm sum.induct}], - co_inducts = [@{thm sum.induct}], + common_co_inducts = @{thms sum.induct}, + co_inducts = @{thms sum.induct}, co_rec_thms = @{thms sum.case}, co_rec_discs = [], co_rec_selss = [], @@ -118,22 +117,22 @@ fp_nesting_bnfs = [], live_nesting_bnfs = [], ctrXs_Tss = [ctr_Ts], - ctr_defs = [@{thm Pair_def_alt}], + ctr_defs = @{thms Pair_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), - co_rec_def = @{thm case_prod_def}, - maps = [@{thm map_prod_simp}], - common_co_inducts = [@{thm prod.induct}], - co_inducts = [@{thm prod.induct}], - co_rec_thms = [@{thm prod.case}], + co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, + maps = @{thms map_prod_simp}, + common_co_inducts = @{thms prod.induct}, + co_inducts = @{thms prod.induct}, + co_rec_thms = @{thms prod.case}, co_rec_discs = [], co_rec_selss = [], - rel_injects = [@{thm rel_prod_apply}], + rel_injects = @{thms rel_prod_apply}, rel_distincts = []} end; val _ = Theory.setup (map_local_theory (fn lthy => - fold (BNF_FP_Def_Sugar.register_fp_sugars (fn s => s <> size_plugin) o single o (fn f => f lthy)) + fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy)) [fp_sugar_of_sum, fp_sugar_of_prod] lthy)); end; diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 18 16:47:40 2014 +0200 @@ -67,8 +67,7 @@ fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses ctor_rec_o_map = - unfold_thms_tac ctxt [rec_def] THEN - HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN' + HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' rtac (ctor_rec_o_map RS trans) THEN' CONVERSION Thm.eta_long_conversion THEN' asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps) diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Tools/Function/old_size.ML --- a/src/HOL/Tools/Function/old_size.ML Thu Sep 18 16:47:40 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,228 +0,0 @@ -(* Title: HOL/Tools/Function/old_size.ML - Author: Stefan Berghofer, Florian Haftmann, TU Muenchen - -Size functions for old-style datatypes. -*) - -structure Old_Size: sig end = -struct - -fun plus (t1, t2) = Const (@{const_name Groups.plus}, - HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; - -fun size_of_type f g h (T as Type (s, Ts)) = - (case f s of - SOME t => SOME t - | NONE => (case g s of - SOME size_name => - SOME (list_comb (Const (size_name, - map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT), - map (size_of_type' f g h) Ts)) - | NONE => NONE)) - | size_of_type _ _ h (TFree (s, _)) = h s -and size_of_type' f g h T = (case size_of_type f g h T of - NONE => Abs ("x", T, HOLogic.zero) - | SOME t => t); - -fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) = - is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts - | is_poly _ _ = true; - -fun constrs_of thy name = - let - val {descr, index, ...} = Old_Datatype_Data.the_info thy name - val SOME (_, _, constrs) = AList.lookup op = descr index - in constrs end; - -val app = curry (list_comb o swap); - -fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy = - let - val {descr, rec_names, rec_rewrites, induct, ...} = info; - val l = length new_type_names; - val descr' = List.take (descr, l); - val tycos = map (#1 o snd) descr'; - in - if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then - (* nothing to do -- the "size" function is already defined *) - thy - else - let - val recTs = Old_Datatype_Aux.get_rec_types descr; - val (recTs1, recTs2) = chop l recTs; - val (_, (_, paramdts, _)) :: _ = descr; - val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts; - val ((param_size_fs, param_size_fTs), f_names) = paramTs |> - map (fn T as TFree (s, _) => - let - val name = "f" ^ unprefix "'" s; - val U = T --> HOLogic.natT - in - (((s, Free (name, U)), U), name) - end) |> split_list |>> split_list; - val param_size = AList.lookup op = param_size_fs; - - val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |> - map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat; - val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy; - - val (((size_names, size_fns), def_names), def_names') = - recTs1 |> map (fn T as Type (s, _) => - let - val s' = "size_" ^ Long_Name.base_name s; - val s'' = Sign.full_bname thy s'; - in - (s'', - (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT), - map snd param_size_fs), - (s' ^ "_def", s' ^ "_overloaded_def"))) - end) |> split_list ||>> split_list ||>> split_list; - val overloaded_size_fns = map HOLogic.size_const recTs1; - - (* instantiation for primrec combinator *) - fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) = - let - val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; - val k = length (filter Old_Datatype_Aux.is_rec_type cargs); - val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) => - if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1) - else - (if b andalso is_poly thy dt' then - case size_of_type (K NONE) extra_size size_ofp T of - NONE => us | SOME sz => sz $ Bound j :: us - else us, i, j + 1)) - (cargs ~~ cargs' ~~ Ts) ([], 0, k); - val t = - if null ts andalso (not b orelse not (exists (is_poly thy) cargs')) - then HOLogic.zero - else foldl1 plus (ts @ [HOLogic.Suc_zero]) - in - fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t - end; - - val fs = maps (fn (_, (name, _, constrs)) => - map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr; - val fs' = maps (fn (n, (name, _, constrs)) => - map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr; - val fTs = map fastype_of fs; - - val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) => - Const (rec_name, fTs @ [T] ---> HOLogic.natT)) - (recTs ~~ rec_names)); - - fun define_overloaded (def_name, eq) lthy = - let - val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq; - val (thm, lthy') = lthy - |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) - |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm); - val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); - val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; - in (thm', lthy') end; - - val ((size_def_thms, size_def_thms'), thy') = - thy - |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), - param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) - (size_names ~~ recTs1)) - |> Global_Theory.add_defs false - (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs))) - (map Binding.name def_names ~~ (size_fns ~~ rec_combs1))) - ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size]) - ||>> fold_map define_overloaded - (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1)) - ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) - ||> Local_Theory.exit_global; - - val ctxt = Proof_Context.init_global thy'; - - val simpset1 = - put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} :: - size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites; - val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2); - - fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) = - HOLogic.mk_eq (app fs r $ Free p, - the (size_of_type tab extra_size size_ofp T) $ Free p); - - fun prove_unfolded_size_eqs size_ofp fs = - if null recTs2 then [] - else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs [] - (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @ - map (mk_unfolded_size_eq (AList.lookup op = - (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) - (xs ~~ recTs2 ~~ rec_combs2)))) - (fn _ => (Old_Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); - - val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs; - val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; - - (* characteristic equations for size functions *) - fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) = - let - val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; - val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts); - val ts = map_filter (fn (sT as (_, T), dt) => - Option.map (fn sz => sz $ Free sT) - (if p dt then size_of_type size_of extra_size size_ofp T - else NONE)) (tnames ~~ Ts ~~ cargs) - in - HOLogic.mk_Trueprop (HOLogic.mk_eq - (size_const $ list_comb (Const (cname, Ts ---> T), - map2 (curry Free) tnames Ts), - if null ts then HOLogic.zero - else foldl1 plus (ts @ [HOLogic.Suc_zero]))) - end; - - val simpset2 = - put_simpset HOL_basic_ss ctxt - addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1); - val simpset3 = - put_simpset HOL_basic_ss ctxt - addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2); - - fun prove_size_eqs p size_fns size_ofp simpset = - maps (fn (((_, (_, _, constrs)), size_const), T) => - map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] [] - (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns)) - size_ofp size_const T constr) - (fn _ => simp_tac simpset 1))) constrs) - (descr' ~~ size_fns ~~ recTs1); - - val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @ - prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3; - - val ([(_, size_thms)], thy'') = thy' - |> Global_Theory.note_thmss "" - [((Binding.name "size", - [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}, - Thm.declaration_attribute (fn thm => - Context.mapping (Code.add_default_eqn thm) I)]), - [(size_eqns, [])])]; - - in - fold2 (fn new_type_name => fn size_name => - BNF_LFP_Size.register_size_global new_type_name size_name size_thms []) - new_type_names size_names thy'' - end - end; - -fun add_size_thms _ (new_type_names as name :: _) thy = - let - val info as {descr, ...} = Old_Datatype_Data.the_info thy name; - val prefix = space_implode "_" (map Long_Name.base_name new_type_names); - val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => - Old_Datatype_Aux.is_rec_type dt andalso - not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr - in - if no_size then thy - else - thy - |> Sign.add_path prefix - |> prove_size_thms info new_type_names - |> Sign.restore_naming thy - end; - -val _ = Context.>> (Context.map_theory (Old_Datatype_Data.interpretation add_size_thms)); - -end; diff -r c9d3074f83b3 -r c6f93b8d2d8e src/HOL/Tools/Old_Datatype/old_size.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Old_Datatype/old_size.ML Thu Sep 18 16:47:40 2014 +0200 @@ -0,0 +1,229 @@ +(* Title: HOL/Tools/Old_Datatype/old_size.ML + Author: Stefan Berghofer, Florian Haftmann, TU Muenchen + +Size functions for old-style datatypes. +*) + +structure Old_Size: sig end = +struct + +fun plus (t1, t2) = Const (@{const_name Groups.plus}, + HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; + +fun size_of_type f g h (T as Type (s, Ts)) = + (case f s of + SOME t => SOME t + | NONE => (case g s of + SOME size_name => + SOME (list_comb (Const (size_name, + map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT), + map (size_of_type' f g h) Ts)) + | NONE => NONE)) + | size_of_type _ _ h (TFree (s, _)) = h s +and size_of_type' f g h T = (case size_of_type f g h T of + NONE => Abs ("x", T, HOLogic.zero) + | SOME t => t); + +fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) = + is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts + | is_poly _ _ = true; + +fun constrs_of thy name = + let + val {descr, index, ...} = Old_Datatype_Data.the_info thy name + val SOME (_, _, constrs) = AList.lookup op = descr index + in constrs end; + +val app = curry (list_comb o swap); + +fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy = + let + val {descr, rec_names, rec_rewrites, induct, ...} = info; + val l = length new_type_names; + val descr' = List.take (descr, l); + val tycos = map (#1 o snd) descr'; + in + if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then + (* nothing to do -- the "size" function is already defined *) + thy + else + let + val recTs = Old_Datatype_Aux.get_rec_types descr; + val (recTs1, recTs2) = chop l recTs; + val (_, (_, paramdts, _)) :: _ = descr; + val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts; + val ((param_size_fs, param_size_fTs), f_names) = paramTs |> + map (fn T as TFree (s, _) => + let + val name = "f" ^ unprefix "'" s; + val U = T --> HOLogic.natT + in + (((s, Free (name, U)), U), name) + end) |> split_list |>> split_list; + val param_size = AList.lookup op = param_size_fs; + + val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |> + map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat; + val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy; + + val (((size_names, size_fns), def_names), def_names') = + recTs1 |> map (fn T as Type (s, _) => + let + val s' = "size_" ^ Long_Name.base_name s; + val s'' = Sign.full_bname thy s'; + in + (s'', + (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT), + map snd param_size_fs), + (s' ^ "_def", s' ^ "_overloaded_def"))) + end) |> split_list ||>> split_list ||>> split_list; + val overloaded_size_fns = map HOLogic.size_const recTs1; + + (* instantiation for primrec combinator *) + fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) = + let + val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; + val k = length (filter Old_Datatype_Aux.is_rec_type cargs); + val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) => + if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1) + else + (if b andalso is_poly thy dt' then + case size_of_type (K NONE) extra_size size_ofp T of + NONE => us | SOME sz => sz $ Bound j :: us + else us, i, j + 1)) + (cargs ~~ cargs' ~~ Ts) ([], 0, k); + val t = + if null ts andalso (not b orelse not (exists (is_poly thy) cargs')) + then HOLogic.zero + else foldl1 plus (ts @ [HOLogic.Suc_zero]) + in + fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t + end; + + val fs = maps (fn (_, (name, _, constrs)) => + map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr; + val fs' = maps (fn (n, (name, _, constrs)) => + map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr; + val fTs = map fastype_of fs; + + val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) => + Const (rec_name, fTs @ [T] ---> HOLogic.natT)) + (recTs ~~ rec_names)); + + fun define_overloaded (def_name, eq) lthy = + let + val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq; + val (thm, lthy') = lthy + |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) + |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm); + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); + val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; + in (thm', lthy') end; + + val ((size_def_thms, size_def_thms'), thy') = + thy + |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), + param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) + (size_names ~~ recTs1)) + |> Global_Theory.add_defs false + (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs))) + (map Binding.name def_names ~~ (size_fns ~~ rec_combs1))) + ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size]) + ||>> fold_map define_overloaded + (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1)) + ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) + ||> Local_Theory.exit_global; + + val ctxt = Proof_Context.init_global thy'; + + val simpset1 = + put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} :: + size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites; + val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2); + + fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) = + HOLogic.mk_eq (app fs r $ Free p, + the (size_of_type tab extra_size size_ofp T) $ Free p); + + fun prove_unfolded_size_eqs size_ofp fs = + if null recTs2 then [] + else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs [] + (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @ + map (mk_unfolded_size_eq (AList.lookup op = + (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) + (xs ~~ recTs2 ~~ rec_combs2)))) + (fn _ => (Old_Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); + + val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs; + val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; + + (* characteristic equations for size functions *) + fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) = + let + val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; + val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts); + val ts = map_filter (fn (sT as (_, T), dt) => + Option.map (fn sz => sz $ Free sT) + (if p dt then size_of_type size_of extra_size size_ofp T + else NONE)) (tnames ~~ Ts ~~ cargs) + in + HOLogic.mk_Trueprop (HOLogic.mk_eq + (size_const $ list_comb (Const (cname, Ts ---> T), + map2 (curry Free) tnames Ts), + if null ts then HOLogic.zero + else foldl1 plus (ts @ [HOLogic.Suc_zero]))) + end; + + val simpset2 = + put_simpset HOL_basic_ss ctxt + addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1); + val simpset3 = + put_simpset HOL_basic_ss ctxt + addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2); + + fun prove_size_eqs p size_fns size_ofp simpset = + maps (fn (((_, (_, _, constrs)), size_const), T) => + map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] [] + (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns)) + size_ofp size_const T constr) + (fn _ => simp_tac simpset 1))) constrs) + (descr' ~~ size_fns ~~ recTs1); + + val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @ + prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3; + + val ([(_, size_thms)], thy'') = thy' + |> Global_Theory.note_thmss "" + [((Binding.name "size", + [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}, + Thm.declaration_attribute (fn thm => + Context.mapping (Code.add_default_eqn thm) I)]), + [(size_eqns, [])])]; + + in + fold2 (fn new_type_name => fn size_name => + BNF_LFP_Size.register_size_global new_type_name size_name size_thms []) + new_type_names size_names thy'' + end + end; + +fun add_size_thms _ (new_type_names as name :: _) thy = + let + val info as {descr, ...} = Old_Datatype_Data.the_info thy name; + val prefix = space_implode "_" (map Long_Name.base_name new_type_names); + val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => + Old_Datatype_Aux.is_rec_type dt andalso + not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr +val _ = tracing ("NAME: " ^ @{make_string} (name, no_size))(*###*) + in + if no_size then thy + else + thy + |> Sign.add_path prefix + |> prove_size_thms info new_type_names + |> Sign.restore_naming thy + end; + +val _ = Theory.setup (Old_Datatype_Data.interpretation add_size_thms); + +end;