# HG changeset patch # User traytel # Date 1384336416 -3600 # Node ID 632be352a5a3152c76d0d912bed77a087d8a6037 # Parent 1e6412c82837207d0f154fa3237d7010285d931e more explicit syntax for defining a bnf diff -r 1e6412c82837 -r 632be352a5a3 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Nov 13 09:37:00 2013 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Nov 13 10:53:36 2013 +0100 @@ -2280,10 +2280,9 @@ \end{matharray} @{rail " - @@{command bnf} target? (name ':')? term \\ - term_list term term_list? term? - ; - X_list: '[' (X + ',') ']' + @@{command bnf} target? (name ':')? typ \\ + 'map:' term ('sets:' (term +))? 'bd:' term \\ + ('wits:' (term +))? ('rel:' term)? "} *} @@ -2364,6 +2363,8 @@ @{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )? ; @{syntax_def name_term}: (name ':' term) + ; + X_list: '[' (X + ',') ']' "} % options: no_discs_sels rep_compat diff -r 1e6412c82837 -r 632be352a5a3 src/HOL/BNF/BNF_Def.thy --- a/src/HOL/BNF/BNF_Def.thy Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/BNF_Def.thy Wed Nov 13 10:53:36 2013 +0100 @@ -202,5 +202,4 @@ ML_file "Tools/bnf_def_tactics.ML" ML_file "Tools/bnf_def.ML" - end diff -r 1e6412c82837 -r 632be352a5a3 src/HOL/BNF/Basic_BNFs.thy --- a/src/HOL/BNF/Basic_BNFs.thy Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/Basic_BNFs.thy Wed Nov 13 10:53:36 2013 +0100 @@ -27,14 +27,20 @@ lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \ Grp B1 f1 OO (Grp B2 f2)\\ \ (Grp A p1)\\ OO Grp A p2" unfolding wpull_def Grp_def by auto -bnf ID: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" - "id :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" +bnf ID: 'a + map: "id :: ('a \ 'b) \ 'a \ 'b" + sets: "\x. {x}" + bd: natLeq + rel: "id :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] done -bnf DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" "op = :: 'a \ 'a \ bool" +bnf DEADID: 'a + map: "id :: 'a \ 'a" + bd: "natLeq +c |UNIV :: 'a set|" + rel: "op = :: 'a \ 'a \ bool" by (auto simp add: wpull_Grp_def Grp_def card_order_csum natLeq_card_order card_of_card_order_on cinfinite_csum natLeq_cinfinite) @@ -47,7 +53,12 @@ lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] -bnf sum_map [setl, setr] "\_::'a + 'b. natLeq" [Inl, Inr] sum_rel +bnf "'a + 'b" + map: sum_map + sets: setl setr + bd: natLeq + wits: Inl Inr + rel: sum_rel proof - show "sum_map id id = id" by (rule sum_map.id) next @@ -147,7 +158,11 @@ lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] -bnf map_pair [fsts, snds] "\_::'a \ 'b. natLeq" prod_rel +bnf "'a \ 'b" + map: map_pair + sets: fsts snds + bd: natLeq + rel: prod_rel proof (unfold prod_set_defs) show "map_pair id id = id" by (rule map_pair.id) next @@ -230,8 +245,11 @@ ultimately show ?thesis using card_of_ordLeq by fast qed -bnf "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" - "fun_rel op =" +bnf "'a \ 'b" + map: "op \" + sets: range + bd: "natLeq +c |UNIV :: 'a set|" + rel: "fun_rel op =" proof fix f show "id \ f = id f" by simp next diff -r 1e6412c82837 -r 632be352a5a3 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/More_BNFs.thy Wed Nov 13 10:53:36 2013 +0100 @@ -21,7 +21,12 @@ lemma option_rec_conv_option_case: "option_rec = option_case" by (simp add: fun_eq_iff split: option.split) -bnf Option.map [Option.set] "\_::'a option. natLeq" ["None"] option_rel +bnf "'a option" + map: Option.map + sets: Option.set + bd: natLeq + wits: None + rel: option_rel proof - show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split) next @@ -94,7 +99,11 @@ (\zs \ ?A. map p1 zs = as \ map p2 zs = bs)" by blast qed -bnf map [set] "\_::'a list. natLeq" ["[]"] +bnf "'a list" + map: map + sets: set + bd: natLeq + wits: Nil proof - show "map id = id" by (rule List.map.id) next @@ -214,7 +223,12 @@ using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, blast)+ qed -bnf fimage [fset] "\_::'a fset. natLeq" ["{||}"] fset_rel +bnf "'a fset" + map: fimage + sets: fset + bd: natLeq + wits: "{||}" + rel: fset_rel apply - apply transfer' apply simp apply transfer' apply force @@ -300,7 +314,12 @@ by transfer force qed -bnf cimage [rcset] "\_::'a cset. natLeq" ["cempty"] cset_rel +bnf "'a cset" + map: cimage + sets: rcset + bd: natLeq + wits: "cempty" + rel: cset_rel proof - show "cimage id = id" by transfer' simp next @@ -874,7 +893,11 @@ by transfer (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def) -bnf mmap [set_of] "\_::'a multiset. natLeq" ["{#}"] +bnf "'a multiset" + map: mmap + sets: set_of + bd: natLeq + wits: "{#}" by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd intro: mmap_cong wpull_mmap) diff -r 1e6412c82837 -r 632be352a5a3 src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Nov 13 10:53:36 2013 +0100 @@ -147,7 +147,7 @@ val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1); (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) - val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd); + val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd; fun map_id0_tac _ = mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer) @@ -257,7 +257,7 @@ val (bnf', lthy') = bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty - Binding.empty [] (((((b, mapx), sets), bd), wits), SOME rel) lthy; + Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -351,7 +351,7 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty - Binding.empty [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; + Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -433,7 +433,7 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty - [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; + [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -506,7 +506,7 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty - [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; + [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -643,7 +643,7 @@ val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads) Binding.empty Binding.empty [] - (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy; + ((((((b, T), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy; in ((bnf', deads), lthy') end; diff -r 1e6412c82837 -r 632be352a5a3 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 13 10:53:36 2013 +0100 @@ -105,7 +105,7 @@ ({prems: thm list, context: Proof.context} -> tactic) list -> ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding -> binding -> binding list -> - ((((binding * term) * term list) * term) * term list) * term option -> + (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory -> bnf * local_theory end; @@ -651,18 +651,18 @@ (* Define new BNFs *) -fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs - (((((raw_bnf_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy = +fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs + ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt) + no_defs_lthy = let val fact_policy = mk_fact_policy no_defs_lthy; val bnf_b = qualify raw_bnf_b; val live = length raw_sets; + val bnf_rhs_T = prep_typ no_defs_lthy raw_bnf_T; val map_rhs = prep_term no_defs_lthy raw_map; val set_rhss = map (prep_term no_defs_lthy) raw_sets; - val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of - Abs (_, T, t) => (T, t) - | _ => error "Bad bound constant"); + val bd_rhs = prep_term no_defs_lthy raw_bd; fun err T = error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ @@ -670,9 +670,9 @@ val (bnf_b, key) = if Binding.eq_name (bnf_b, Binding.empty) then - (case bd_rhsT of + (case bnf_rhs_T of Type (C, Ts) => if forall (can dest_TFree) Ts - then (Binding.qualified_name C, C) else err bd_rhsT + then (Binding.qualified_name C, C) else err bnf_rhs_T | T => err T) else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b); @@ -745,9 +745,9 @@ val CA_params = map TVar (Term.add_tvarsT CA []); val bnf_sets = map2 (normalize_set CA_params) alphas (map (Morphism.term phi) bnf_set_terms); - val bdT = Morphism.typ phi bd_rhsT; + val bnf_T = Morphism.typ phi bnf_rhs_T; val bnf_bd = - Term.subst_TVars (Term.add_tvar_namesT bdT [] ~~ CA_params) (Morphism.term phi bnf_bd_term); + Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ CA_params) (Morphism.term phi bnf_bd_term); (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*) val deads = (case Ds_opt of @@ -1334,7 +1334,7 @@ map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] []) goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs) |> (fn thms => after_qed mk_wit_thms (map single thms) lthy) - end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs; + end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs; val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) => let @@ -1353,7 +1353,7 @@ Proof.unfolding ([[(defs, [])]]) (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms) (map (single o rpair []) goals @ nontriv_wit_goals) lthy) - end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE + end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE Binding.empty Binding.empty []; fun print_bnfs ctxt = @@ -1389,11 +1389,14 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "bnf"} "register a type as a bounded natural functor" - ((parse_opt_binding_colon -- Parse.term -- - (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- - (Scan.option ((@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) - >> the_default []) -- - Scan.option Parse.term) + (parse_opt_binding_colon -- Parse.typ --| + (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term -- + (Scan.option ((Parse.reserved "sets" -- @{keyword ":"}) |-- + Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) >> the_default []) --| + (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term -- + (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |-- + Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) -- + Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) >> bnf_cmd); end; diff -r 1e6412c82837 -r 632be352a5a3 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Nov 13 10:53:36 2013 +0100 @@ -2678,7 +2678,7 @@ fn T => fn (thms, wits) => fn lthy => bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b rel_b set_bs - (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy + ((((((b, T), fold_rev Term.absfree fs' mapx), sets), bd), wits), NONE) lthy |> register_bnf (Local_Theory.full_name lthy b)) tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy; diff -r 1e6412c82837 -r 632be352a5a3 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Nov 13 10:53:36 2013 +0100 @@ -1749,7 +1749,7 @@ fn T => fn wits => fn lthy => bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b rel_b set_bs - (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) + ((((((b, T), fold_rev Term.absfree fs' mapx), sets), bd), wits), NONE) lthy |> register_bnf (Local_Theory.full_name lthy b)) tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;