# HG changeset patch # User traytel # Date 1347952553 -7200 # Node ID 433dc7e028c8b06c7937efcc6fa7e13460dca8b2 # Parent 1095f240146a3539502d7fa13a038ebe9d673609 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands) diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/Basic_BNFs.thy --- a/src/HOL/Codatatype/Basic_BNFs.thy Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/Basic_BNFs.thy Tue Sep 18 09:15:53 2012 +0200 @@ -24,7 +24,7 @@ lemma natLeq_cinfinite: "cinfinite natLeq" unfolding cinfinite_def Field_natLeq by (rule nat_infinite) -bnf_def ID = "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" ["id :: 'a \ 'a"] +bnf_def ID: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" ["id :: 'a \ 'a"] apply auto apply (rule natLeq_card_order) apply (rule natLeq_cinfinite) @@ -52,7 +52,7 @@ lemma ID_pred[simp]: "ID_pred \ = \" unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto -bnf_def DEADID = "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] +bnf_def DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] apply (auto simp add: wpull_id) apply (rule card_order_csum) apply (rule natLeq_card_order) @@ -86,8 +86,8 @@ structure Basic_BNFs : BASIC_BNFS = struct -val ID_bnf = the (BNF_Def.bnf_of @{context} "ID"); -val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID"); +val ID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.ID"); +val DEADID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.DEADID"); val rel_def = BNF_Def.rel_def_of_bnf ID_bnf; val ID_rel_def = rel_def RS sym; @@ -104,7 +104,7 @@ lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def] -bnf_def sum = sum_map [sum_setl, sum_setr] "\_::'a + 'b. natLeq" [Inl, Inr] +bnf_def sum_map [sum_setl, sum_setr] "\_::'a + 'b. natLeq" [Inl, Inr] proof - show "sum_map id id = id" by (rule sum_map.id) next @@ -240,7 +240,7 @@ lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] -bnf_def prod = map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] +bnf_def map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] proof (unfold prod_set_defs) show "map_pair id id = id" by (rule map_pair.id) next @@ -358,7 +358,7 @@ ultimately show ?thesis using card_of_ordLeq by fast qed -bnf_def "fun" = "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" +bnf_def "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"] proof fix f show "id \ f = id f" by simp diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/More_BNFs.thy --- a/src/HOL/Codatatype/More_BNFs.thy Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/More_BNFs.thy Tue Sep 18 09:15:53 2012 +0200 @@ -22,7 +22,7 @@ lemma option_rec_conv_option_case: "option_rec = option_case" by (simp add: fun_eq_iff split: option.split) -bnf_def option = Option.map [Option.set] "\_::'a option. natLeq" ["None"] +bnf_def Option.map [Option.set] "\_::'a option. natLeq" ["None"] proof - show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split) next @@ -190,7 +190,7 @@ qed qed -bnf_def list = map [set] "\_::'a list. natLeq" ["[]"] +bnf_def map [set] "\_::'a list. natLeq" ["[]"] proof - show "map id = id" by (rule List.map.id) next @@ -355,7 +355,7 @@ lemma fset_to_fset: "finite A \ fset (the_inv fset A) = A" by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset) -bnf_def fset = map_fset [fset] "\_::'a fset. natLeq" ["{||}"] +bnf_def map_fset [fset] "\_::'a fset. natLeq" ["{||}"] proof - show "map_fset id = id" unfolding map_fset_def2 map_id o_id afset_rfset_id .. @@ -511,7 +511,7 @@ finally show ?thesis . qed -bnf_def cset = cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] +bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] proof - show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto next @@ -1134,7 +1134,7 @@ definition mset_map :: "('a \ 'b) \ 'a multiset \ 'b multiset" where "mset_map h = Abs_multiset \ mmap h \ count" -bnf_def mset = mset_map [set_of] "\_::'a multiset. natLeq" ["{#}"] +bnf_def mset_map [set_of] "\_::'a multiset. natLeq" ["{#}"] unfolding mset_map_def proof - show "Abs_multiset \ mmap id \ count = id" unfolding mmap_id by (auto simp: count_inverse) diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 18 09:15:53 2012 +0200 @@ -12,6 +12,8 @@ type nonemptiness_witness = {I: int list, wit: term, prop: thm list} val bnf_of: Proof.context -> string -> BNF option + val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory) + val name_of_bnf: BNF -> binding val T_of_bnf: BNF -> typ val live_of_bnf: BNF -> int @@ -540,6 +542,18 @@ | _ => error "Bad bound constant"); val wit_rhss = map (prep_term no_defs_lthy) raw_wits; + fun err T = + error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ + " as unnamed BNF"); + + val (b, key) = + if Binding.eq_name (b, Binding.empty) then + (case bd_rhsT of + Type (C, Ts) => if forall (is_some o try dest_TFree) Ts + then (Binding.qualified_name C, C) else err bd_rhsT + | T => err T) + else (b, Local_Theory.full_name no_defs_lthy b); + val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs); val set_binds_defs = let @@ -624,12 +638,6 @@ | SOME Ds => map (Morphism.typ phi) Ds); val dead = length deads; - (*FIXME: check DUP here, not in after_qed*) - val key = - (case (CA, Binding.eq_name (qualify b, b)) of - (Type (C, _), true) => C - | _ => Name_Space.full_name Name_Space.default_naming b); - (*TODO: further checks of type of bnf_map*) (*TODO: check types of bnf_sets*) (*TODO: check type of bnf_bd*) @@ -1152,18 +1160,20 @@ [(thms, [])])); in Local_Theory.notes notes #> snd - #> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) end else I)) end; in - (goals, wit_goalss, after_qed, lthy', one_step_defs) + (key, goals, wit_goalss, after_qed, lthy', one_step_defs) end; +fun register_bnf key (bnf, lthy) = + (bnf, Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy); + fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds = - (fn (goals, wit_goalss, after_qed, lthy, defs) => + (fn (_, goals, wit_goalss, after_qed, lthy, defs) => let val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac; val wit_goals = wit_goalss |> map Logic.mk_conjunction_balanced; @@ -1179,9 +1189,9 @@ |> (fn thms => after_qed (map single thms @ wit_thms) lthy) end) oo prepare_def const_policy fact_policy qualify (K I) Ds; -val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) => +val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) => Proof.unfolding ([[(defs, [])]]) - (Proof.theorem NONE (snd oo after_qed) + (Proof.theorem NONE (snd o register_bnf key oo after_qed) (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo prepare_def Do_Inline user_policy I Syntax.read_term NONE; @@ -1216,7 +1226,7 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type" - (((Parse.binding --| @{keyword "="}) -- Parse.term -- + ((parse_opt_binding_colon -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd); diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 18 09:15:53 2012 +0200 @@ -805,12 +805,9 @@ val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term; -val parse_binding_colon = Parse.binding --| @{keyword ":"}; -val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding; - val parse_ctr_arg = @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} || - (Parse.typ >> pair no_binding); + (Parse.typ >> pair Binding.empty); val parse_defaults = @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"}; diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 18 09:15:53 2012 +0200 @@ -2855,9 +2855,10 @@ val wit_tac = mk_wit_tac n unf_fld_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); val (Jbnfs, lthy) = - fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => + fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy => bnf_def Dont_Inline user_policy I tacs (wit_tac thms) (SOME deads) - ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits)) + ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy + |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts all_witss lthy; val fold_maps = Local_Defs.fold lthy (map (fn bnf => diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 18 09:15:53 2012 +0200 @@ -1701,9 +1701,10 @@ fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); val (Ibnfs, lthy) = - fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => + fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy => bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads) - ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits)) + ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy + |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts fld_witss lthy; val fold_maps = Local_Defs.fold lthy (map (fn bnf => diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/Tools/bnf_util.ML --- a/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 18 09:15:53 2012 +0200 @@ -128,6 +128,9 @@ val certifyT: Proof.context -> typ -> ctyp val certify: Proof.context -> term -> cterm + val parse_binding_colon: Token.T list -> binding * Token.T list + val parse_opt_binding_colon: Token.T list -> binding * Token.T list + val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory @@ -250,6 +253,9 @@ fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); +val parse_binding_colon = Parse.binding --| @{keyword ":"}; +val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; + (*TODO: is this really different from Typedef.add_typedef_global?*) fun typedef def opt_name typ set opt_morphs tac lthy = let diff -r 1095f240146a -r 433dc7e028c8 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 18 03:33:53 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 18 09:15:53 2012 +0200 @@ -7,7 +7,6 @@ signature BNF_WRAP = sig - val no_binding: binding val mk_half_pairss: 'a list -> ('a * 'a) list list val mk_ctr: typ list -> term -> term val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list -> @@ -45,7 +44,6 @@ val split_asmN = "split_asm"; val weak_case_cong_thmsN = "weak_case_cong"; -val no_binding = @{binding ""}; val std_binding = @{binding _}; val induct_simp_attrs = @{attributes [induct_simp]}; @@ -111,10 +109,11 @@ val ms = map length ctr_Tss; - val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings; + val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings; fun can_really_rely_on_disc k = - not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0; + not (Binding.eq_name (nth raw_disc_bindings' (k - 1), Binding.empty)) orelse + nth ms (k - 1) = 0; fun can_rely_on_disc k = can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2)); fun can_omit_disc_binding k m = @@ -127,7 +126,7 @@ raw_disc_bindings' |> map4 (fn k => fn m => fn ctr => fn disc => Option.map (Binding.qualify false (Binding.name_of data_b)) - (if Binding.eq_name (disc, no_binding) then + (if Binding.eq_name (disc, Binding.empty) then if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr) else if Binding.eq_name (disc, std_binding) then SOME (std_disc_binding ctr) @@ -143,10 +142,10 @@ pad_list [] n raw_sel_bindingss |> map3 (fn ctr => fn m => map2 (fn l => fn sel => Binding.qualify false (Binding.name_of data_b) - (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then + (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then std_sel_binding m l ctr else - sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms; + sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms; fun mk_case Ts T = let