# HG changeset patch # User traytel # Date 1456909332 -3600 # Node ID 5b5b704f4811c3bf6e554d4508bb88dfa3e0cac7 # Parent f187aaf602c4f9cc29a010d5b71b1fade062f1f4 respect qualification when noting theorems in prim(co)rec diff -r f187aaf602c4 -r 5b5b704f4811 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Mar 02 10:01:31 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Mar 02 10:02:12 2016 +0100 @@ -1098,6 +1098,7 @@ val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts); val fun_names = map Binding.name_of bs; + val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs; val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; val frees = map (fst #>> Binding.name_of #> Free) fixes; val has_call = Term.exists_subterm (member (op =) frees); @@ -1520,6 +1521,7 @@ val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss; val common_name = mk_common_name fun_names; + val common_qualify = fold_rev I qualifys; val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; @@ -1532,7 +1534,8 @@ (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], common_coinduct_attrs)] |> filter_out (null o #2) |> map (fn (thmN, thms, attrs) => - ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); + ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs), + [(thms, [])])); val notes = [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs), @@ -1547,9 +1550,10 @@ (selN, sel_thmss, simp_attrs), (simpsN, simp_thmss, [])] |> maps (fn (thmN, thmss, attrs) => - map2 (fn fun_name => fn thms => - ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])])) - fun_names (take actual_nn thmss)) + @{map 3} (fn fun_name => fn qualify => fn thms => + ((qualify (Binding.qualify true fun_name (Binding.name thmN)), attrs), + [(thms, [])])) + fun_names qualifys (take actual_nn thmss)) |> filter_out (null o fst o hd o snd); val fun_ts0 = map fst def_infos; diff -r f187aaf602c4 -r 5b5b704f4811 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Mar 02 10:01:31 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Mar 02 10:02:12 2016 +0100 @@ -537,7 +537,8 @@ val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec; val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global; val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded; -val primrec_simple = apfst (apsnd (old_of_new (flat o snd))) ooo BNF_LFP_Rec_Sugar.primrec_simple; +val primrec_simple = apfst (apfst fst o apsnd (old_of_new (flat o snd))) ooo + BNF_LFP_Rec_Sugar.primrec_simple; val _ = Outer_Syntax.local_theory @{command_keyword datatype_compat} diff -r f187aaf602c4 -r 5b5b704f4811 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Mar 02 10:01:31 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Mar 02 10:02:12 2016 +0100 @@ -73,7 +73,8 @@ (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory -> - (string list * (term list * thm list * (int list list * thm list list))) * local_theory + ((string list * (binding -> binding) list) * + (term list * thm list * (int list list * thm list list))) * local_theory end; structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR = @@ -509,6 +510,7 @@ val (bs, mxs) = map_split (apfst fst) fixes; val fun_names = map Binding.name_of bs; + val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs; val eqns_data = map (dissect_eqn lthy0 fun_names) specs; val funs_data = eqns_data |> partition_eq (op = o apply2 #fun_name) @@ -569,21 +571,23 @@ val notes = (if n2m then - map2 (fn name => fn thm => (name, inductN, [thm], induct_attrs)) fun_names - (take actual_nn inducts) + @{map 3} (fn name => fn qualify => fn thm => (name, qualify, inductN, [thm], induct_attrs)) + fun_names qualifys (take actual_nn inducts) else []) - |> map (fn (prefix, thmN, thms, attrs) => - ((Binding.qualify true prefix (Binding.name thmN), attrs), [(thms, [])])); + |> map (fn (prefix, qualify, thmN, thms, attrs) => + ((qualify (Binding.qualify true prefix (Binding.name thmN)), attrs), [(thms, [])])); val common_name = mk_common_name fun_names; + val common_qualify = fold_rev I qualifys; val common_notes = (if n2m then [(inductN, [common_induct], [])] else []) |> map (fn (thmN, thms, attrs) => - ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); + ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs), + [(thms, [])])); in - (((fun_names, defs), + (((fun_names, qualifys, defs), fn lthy => fn defs => let val def_thms = map (snd o snd) defs; @@ -606,14 +610,14 @@ val nonexhaustives = replicate actual_nn nonexhaustive; val transfers = replicate actual_nn transfer; - val (((names, defs), prove), lthy') = + val (((names, qualifys, defs), prove), lthy') = prepare_primrec plugins nonexhaustives transfers fixes ts lthy; in lthy' |> fold_map Local_Theory.define defs |-> (fn defs => fn lthy => let val ((jss, simpss), lthy) = prove lthy defs in - ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) + (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) end) end; @@ -621,7 +625,8 @@ primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy handle OLD_PRIMREC () => Old_Primrec.primrec_simple fixes ts lthy - |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single; + |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single + |>> apfst (map_split (rpair I)); fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy = let @@ -638,7 +643,7 @@ val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy); val mk_notes = - flat ooo @{map 3} (fn js => fn prefix => fn thms => + flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms => let val (bs, attrss) = map_split (fst o nth specs) js; val notes = @@ -647,14 +652,14 @@ [([thm], [])])) bs attrss thms; in - ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes + ((qualify (Binding.qualify true prefix (Binding.name simpsN)), []), [(thms, [])]) :: notes end); in lthy |> primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs) - |-> (fn (names, (ts, defs, (jss, simpss))) => + |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) => Spec_Rules.add Spec_Rules.Equational (ts, flat simpss) - #> Local_Theory.notes (mk_notes jss names simpss) + #> Local_Theory.notes (mk_notes jss names qualifys simpss) #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes))) end handle OLD_PRIMREC () =>