# HG changeset patch # User blanchet # Date 1398241407 -7200 # Node ID 41d3596d8a64f763a6c3f2555e65e863db46f33a # Parent 15cd15f9b40c2ba2d679f1a8ec43b7c1f15c4246 move size hooks together, with new one preceding old one and sharing same theory data diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:27 2014 +0200 @@ -212,7 +212,35 @@ ML_file "Tools/BNF/bnf_lfp.ML" ML_file "Tools/BNF/bnf_lfp_compat.ML" ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" + + +subsection {* Size of a datatype value *} + ML_file "Tools/BNF/bnf_lfp_size.ML" +ML_file "Tools/Function/size.ML" +setup Size.setup + +lemma size_bool[code]: "size (b\bool) = 0" + by (cases b) auto + +lemma nat_size[simp, code]: "size (n\nat) = n" + by (induct n) simp_all + +declare prod.size[no_atp] + +lemma sum_size_o_map: "sum_size g1 g2 \ map_sum f1 f2 = sum_size (g1 \ f1) (g2 \ f2)" + by (rule ext) (case_tac x, auto) + +lemma prod_size_o_map: "prod_size g1 g2 \ map_prod f1 f2 = prod_size (g1 \ f1) (g2 \ f2)" + by (rule ext) auto + +setup {* +BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size} + @{thms sum_size_o_map} +#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size} + @{thms prod_size_o_map} +*} + hide_fact (open) id_transfer diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/Fun_Def.thy --- a/src/HOL/Fun_Def.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Fun_Def.thy Wed Apr 23 10:23:27 2014 +0200 @@ -111,7 +111,8 @@ #> Function_Fun.setup *} -subsection {* Measure Functions *} + +subsection {* Measure functions *} inductive is_measure :: "('a \ nat) \ bool" where is_measure_trivial: "is_measure f" @@ -137,7 +138,7 @@ setup Lexicographic_Order.setup -subsection {* Congruence Rules *} +subsection {* Congruence rules *} lemma let_cong [fundef_cong]: "M = N \ (\x. x = N \ f x = g x) \ Let M f = Let N g" @@ -156,22 +157,22 @@ "f (g x) = f' (g' x') \ (f o g) x = (f' o g') x'" unfolding o_apply . + subsection {* Simp rules for termination proofs *} -lemma termination_basic_simps[termination_simp]: - "x < (y::nat) \ x < y + z" - "x < z \ x < y + z" - "x \ y \ x \ y + (z::nat)" - "x \ z \ x \ y + (z::nat)" - "x < y \ x \ (y::nat)" -by arith+ - -declare le_imp_less_Suc[termination_simp] +declare + trans_less_add1[termination_simp] + trans_less_add2[termination_simp] + trans_le_add1[termination_simp] + trans_le_add2[termination_simp] + less_imp_le_nat[termination_simp] + le_imp_less_Suc[termination_simp] lemma prod_size_simp[termination_simp]: "prod_size f g p = f (fst p) + g (snd p) + Suc 0" by (induct p) auto + subsection {* Decomposition *} lemma less_by_empty: @@ -185,7 +186,7 @@ by (auto simp add: wf_comp_self[of R]) -subsection {* Reduction Pairs *} +subsection {* Reduction pairs *} definition "reduction_pair P = (wf (fst P) \ fst P O snd P \ fst P)" diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/Lazy_Sequence.thy --- a/src/HOL/Lazy_Sequence.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Lazy_Sequence.thy Wed Apr 23 10:23:27 2014 +0200 @@ -28,7 +28,7 @@ by (auto intro: lazy_sequence_eqI) lemma lazy_sequence_size_eq: - "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))" + "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))" by (cases xq) simp lemma size_lazy_sequence_eq [code]: diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/Library/IArray.thy --- a/src/HOL/Library/IArray.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Library/IArray.thy Wed Apr 23 10:23:27 2014 +0200 @@ -59,7 +59,7 @@ by (cases as) simp lemma [code]: -"iarray_size f as = Suc (list_size f (IArray.list_of as))" +"iarray_size f as = Suc (size_list f (IArray.list_of as))" by (cases as) simp lemma [code]: diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/List.thy --- a/src/HOL/List.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/List.thy Wed Apr 23 10:23:27 2014 +0200 @@ -3488,8 +3488,8 @@ "x \ set xs \ listsum (map f xs) = f x + listsum (map f (remove1 x xs))" by (induct xs) (auto simp add: ac_simps) -lemma (in monoid_add) list_size_conv_listsum: - "list_size f xs = listsum (map f xs) + size xs" +lemma (in monoid_add) size_list_conv_listsum: + "size_list f xs = listsum (map f xs) + size xs" by (induct xs) auto lemma (in monoid_add) length_concat: @@ -5945,28 +5945,28 @@ subsection {* Size function *} -lemma [measure_function]: "is_measure f \ is_measure (list_size f)" +lemma [measure_function]: "is_measure f \ is_measure (size_list f)" by (rule is_measure_trivial) -lemma [measure_function]: "is_measure f \ is_measure (option_size f)" +lemma [measure_function]: "is_measure f \ is_measure (size_option f)" by (rule is_measure_trivial) -lemma list_size_estimation[termination_simp]: - "x \ set xs \ y < f x \ y < list_size f xs" +lemma size_list_estimation[termination_simp]: + "x \ set xs \ y < f x \ y < size_list f xs" by (induct xs) auto -lemma list_size_estimation'[termination_simp]: - "x \ set xs \ y \ f x \ y \ list_size f xs" +lemma size_list_estimation'[termination_simp]: + "x \ set xs \ y \ f x \ y \ size_list f xs" by (induct xs) auto -lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs" +lemma size_list_map[simp]: "size_list f (map g xs) = size_list (f o g) xs" by (induct xs) auto -lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys" +lemma size_list_append[simp]: "size_list f (xs @ ys) = size_list f xs + size_list f ys" by (induct xs, auto) -lemma list_size_pointwise[termination_simp]: - "(\x. x \ set xs \ f x \ g x) \ list_size f xs \ list_size g xs" +lemma size_list_pointwise[termination_simp]: + "(\x. x \ set xs \ f x \ g x) \ size_list f xs \ size_list g xs" by (induct xs) force+ @@ -6757,7 +6757,7 @@ lemma length_transfer [transfer_rule]: "(list_all2 A ===> op =) length length" - unfolding list_size_overloaded_def by transfer_prover + unfolding size_list_overloaded_def size_list_def by transfer_prover lemma rotate1_transfer [transfer_rule]: "(list_all2 A ===> list_all2 A) rotate1 rotate1" diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Nitpick.thy Wed Apr 23 10:23:27 2014 +0200 @@ -113,9 +113,8 @@ declare nat.case [nitpick_simp del] -lemma list_size_simp [nitpick_simp]: -"list_size f xs = (if xs = [] then 0 - else Suc (f (hd xs) + list_size f (tl xs)))" +lemma size_list_simp [nitpick_simp]: +"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))" "size xs = (if xs = [] then 0 else Suc (size (tl xs)))" by (cases xs) auto @@ -145,8 +144,9 @@ definition Frac :: "int \ int \ bool" where "Frac \ \(a, b). b > 0 \ int_gcd a b = 1" -axiomatization Abs_Frac :: "int \ int \ 'a" - and Rep_Frac :: "'a \ int \ int" +axiomatization + Abs_Frac :: "int \ int \ 'a" and + Rep_Frac :: "'a \ int \ int" definition zero_frac :: 'a where "zero_frac \ Abs_Frac (0, 1)" @@ -244,7 +244,7 @@ hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold - list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def + size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:27 2014 +0200 @@ -8,6 +8,7 @@ signature BNF_LFP_SIZE = sig val register_size: string -> string -> thm list -> thm list -> theory -> theory + val lookup_size: theory -> string -> (string * (thm list * thm list)) option end; structure BNF_LFP_Size : BNF_LFP_SIZE = @@ -33,7 +34,9 @@ ); fun register_size T_name size_name size_simps size_o_maps = - Data.map (Symtab.update_new (T_name, (size_name, (size_simps, size_o_maps)))); + Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))); + +val lookup_size = Symtab.lookup o Data.get; val zero_nat = @{const zero_class.zero (nat)}; @@ -224,8 +227,13 @@ val maps0 = map map_of_bnf fp_bnfs; + (* This disables much of the functionality of the size extension within a locale. It is not + clear how to make the code below work with locales, given that interpretations are based on + theories. *) + val has_hyps = not (null (Thm.hyps_of (hd (hd rec_thmss)))); + val (rec_o_map_thmss, size_o_map_thmss) = - if live = 0 then + if has_hyps orelse live = 0 then `I (replicate nn []) else let @@ -306,16 +314,19 @@ val (_, thy4) = thy3 |> fold_map4 (fn T_name => fn size_simps => fn rec_o_map_thms => fn size_o_map_thms => - let val qualify = Binding.qualify true (Long_Name.base_name T_name) in - Global_Theory.note_thmss "" - ([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]), - ((qualify (Binding.name sizeN), - [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute - (fn thm => Context.mapping (Code.add_default_eqn thm) I)]), - [(size_simps, [])]), - ((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])] - |> filter_out (forall (null o fst) o snd)) - end) + if has_hyps then + pair [] + else + let val qualify = Binding.qualify true (Long_Name.base_name T_name) in + Global_Theory.note_thmss "" + ([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]), + ((qualify (Binding.name sizeN), + [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute + (fn thm => Context.mapping (Code.add_default_eqn thm) I)]), + [(size_simps, [])]), + ((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])] + |> filter_out (forall (null o fst) o snd)) + end) T_names (map2 append size_simpss overloaded_size_simpss) rec_o_map_thmss size_o_map_thmss ||> Spec_Rules.add_global Spec_Rules.Equational (size_consts, size_simps); in diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Tools/Function/size.ML Wed Apr 23 10:23:27 2014 +0200 @@ -6,23 +6,12 @@ signature SIZE = sig - val size_thms: theory -> string -> thm list val setup: theory -> theory end; structure Size: SIZE = struct -structure Data = Theory_Data -( - type T = (string * thm list) Symtab.table; - val empty = Symtab.empty; - val extend = I - fun merge data = Symtab.merge (K true) data; -); - -val lookup_size = Data.get #> Symtab.lookup; - fun plus (t1, t2) = Const (@{const_name Groups.plus}, HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; @@ -35,15 +24,13 @@ map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT), map (size_of_type' f g h) Ts)) | NONE => NONE)) - | size_of_type f g h (TFree (s, _)) = h s + | 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 (Datatype_Aux.DtType (name, dts)) = - (case lookup_size thy name of - NONE => false - | SOME _ => exists (is_poly thy) dts) + is_some (BNF_LFP_Size.lookup_size thy name) andalso exists (is_poly thy) dts | is_poly _ _ = true; fun constrs_of thy name = @@ -66,7 +53,6 @@ thy else let - val (rec_names1, rec_names2) = chop l rec_names; val recTs = Datatype_Aux.get_rec_types descr; val (recTs1, recTs2) = chop l recTs; val (_, (_, paramdts, _)) :: _ = descr; @@ -82,8 +68,8 @@ val param_size = AList.lookup op = param_size_fs; val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |> - map_filter (Option.map snd o lookup_size thy) |> flat; - val extra_size = Option.map fst o lookup_size thy; + map_filter (Option.map (fst o snd) o BNF_LFP_Size.lookup_size thy) |> flat; + val extra_size = Option.map fst o BNF_LFP_Size.lookup_size thy; val (((size_names, size_fns), def_names), def_names') = recTs1 |> map (fn T as Type (s, _) => @@ -160,7 +146,7 @@ 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 (x, T), r) = + 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); @@ -181,7 +167,7 @@ let val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs; val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts); - val ts = map_filter (fn (sT as (s, T), dt) => + 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) @@ -220,12 +206,13 @@ [(size_eqns, [])])]; in - Data.map (fold (Symtab.update_new o apsnd (rpair size_thms)) - (new_type_names ~~ size_names)) thy'' + fold2 (fn new_type_name => fn size_name => + BNF_LFP_Size.register_size new_type_name size_name [] size_thms) + new_type_names size_names thy'' end end; -fun add_size_thms config (new_type_names as name :: _) thy = +fun add_size_thms _ (new_type_names as name :: _) thy = let val info as {descr, ...} = Datatype_Data.the_info thy name; val prefix = space_implode "_" (map Long_Name.base_name new_type_names); @@ -241,8 +228,6 @@ |> Sign.restore_naming thy end; -val size_thms = snd oo (the oo lookup_size); - val setup = Datatype_Data.interpretation add_size_thms; end; diff -r 15cd15f9b40c -r 41d3596d8a64 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Wellfounded.thy Wed Apr 23 10:23:27 2014 +0200 @@ -848,20 +848,6 @@ done -subsection {* size of a datatype value *} - -ML_file "Tools/Function/size.ML" -setup Size.setup - -lemma size_bool [code]: - "size (b\bool) = 0" by (cases b) auto - -lemma nat_size [simp, code]: "size (n\nat) = n" - by (induct n) simp_all - -declare prod.size [no_atp] - - hide_const (open) acc accp end