# HG changeset patch # User traytel # Date 1385561298 -3600 # Node ID 91a1e4aa7c803ead3728ed2c6a4372f98e841596 # Parent ac54bc80a5cc15f5803d630f18b82a8238e32db3 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it diff -r ac54bc80a5cc -r 91a1e4aa7c80 src/HOL/BNF/BNF.thy --- a/src/HOL/BNF/BNF.thy Wed Nov 27 11:08:55 2013 +0100 +++ b/src/HOL/BNF/BNF.thy Wed Nov 27 15:08:18 2013 +0100 @@ -10,7 +10,7 @@ header {* Bounded Natural Functors for (Co)datatypes *} theory BNF -imports Countable_Set_Type BNF_LFP BNF_GFP +imports Countable_Set_Type BNF_LFP BNF_GFP BNF_Decl begin hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr diff -r ac54bc80a5cc -r 91a1e4aa7c80 src/HOL/BNF/BNF_Decl.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/BNF_Decl.thy Wed Nov 27 15:08:18 2013 +0100 @@ -0,0 +1,18 @@ +(* Title: HOL/BNF/BNF_Decl.thy + Author: Dmitriy Traytel, TU Muenchen + Copyright 2013 + +Axiomatic declaration of bounded natural functors. +*) + +header {* Axiomatic declaration of Bounded Natural Functors *} + +theory BNF_Decl +imports BNF_Def +keywords + "bnf_decl" :: thy_decl +begin + +ML_file "Tools/bnf_decl.ML" + +end diff -r ac54bc80a5cc -r 91a1e4aa7c80 src/HOL/BNF/Tools/bnf_decl.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/Tools/bnf_decl.ML Wed Nov 27 15:08:18 2013 +0100 @@ -0,0 +1,96 @@ +(* Title: HOL/BNF/Tools/bnf_decl.ML + Author: Dmitriy Traytel, TU Muenchen + Copyright 2013 + +Axiomatic declaration of bounded natural functors. +*) + +signature BNF_DECL = +sig + val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding -> + local_theory -> BNF_Def.bnf * local_theory +end + +structure BNF_Decl : BNF_DECL = +struct + +open BNF_Util +open BNF_Def + +fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb lthy = + let + fun prepare_type_arg (set_opt, (ty, c)) = + let val s = fst (dest_TFree (prepare_typ lthy ty)) in + (set_opt, (s, prepare_constraint lthy c)) + end; + val ((user_setbs, vars), raw_vars') = + map prepare_type_arg raw_vars + |> `split_list + |>> apfst (map_filter I); + val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; + + fun mk_b name user_b = + (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) + |> Binding.qualify false (Binding.name_of b); + val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy; + val (bd_type_Tname, lthy) = + Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy; + val T = Type (Tname, map TFree vars); + val bd_type_T = Type (bd_type_Tname, map TFree deads); + val lives = map TFree (filter_out (member (op =) deads) vars); + val live = length lives; + val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; + val (lives', _) = BNF_Util.mk_TFrees (length lives) + (fold Variable.declare_typ (map TFree vars) lthy); + val T' = Term.typ_subst_atomic (lives ~~ lives') T; + val mapT = map2 (curry op -->) lives lives' ---> T --> T'; + val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; + val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); + val mapb = mk_b BNF_Def.mapN user_mapb; + val bdb = mk_b "bd" Binding.empty; + val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs + (if live = 1 then [0] else 1 upto live); + val lthy = Local_Theory.background_theory + (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: + map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs)) + lthy; + val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); + val Fsets = map2 (fn setb => fn setT => + Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; + val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); + val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = + prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads)) + user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), []), NONE) lthy; + + fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps; + val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; + fun mk_wit_thms set_maps = + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps) + |> Conjunction.elim_balanced (length wit_goals) + |> map2 (Conjunction.elim_balanced o length) wit_goalss + |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); + + val ((_, [thms]), (lthy_old, lthy)) = Local_Theory.background_theory_result + (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), goals)]) lthy + ||> `Local_Theory.restore; + val phi = Proof_Context.export_morphism lthy_old lthy; + in + BNF_Def.register_bnf key (after_qed mk_wit_thms (map single (Morphism.fact phi thms)) lthy) + end; + +val bnf_decl = prepare_decl (K I) (K I); + +fun read_constraint _ NONE = HOLogic.typeS + | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; + +val bnf_decl_cmd = prepare_decl read_constraint Syntax.parse_typ; + +val parse_bnf_decl = + parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- Parse.opt_mixfix; + +val _ = + Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration" + (parse_bnf_decl >> + (fn (((bsTs, b), (mapb, relb)), mx) => bnf_decl_cmd bsTs b mx mapb relb #> snd)); + +end; diff -r ac54bc80a5cc -r 91a1e4aa7c80 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 27 11:08:55 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 27 15:08:18 2013 +0100 @@ -101,6 +101,15 @@ Proof.context val print_bnfs: Proof.context -> unit + val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> + (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option -> + binding -> binding -> binding list -> + (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context -> + string * term list * + ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) * + ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) * + local_theory * thm list + val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> ({prems: thm list, context: Proof.context} -> tactic) list -> ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding -> diff -r ac54bc80a5cc -r 91a1e4aa7c80 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Nov 27 11:08:55 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Nov 27 15:08:18 2013 +0100 @@ -1515,24 +1515,13 @@ val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained; +(*FIXME: use parse_type_args_named_constrained from BNF_Util and thus + allow users to kill certain arguments of a (co)datatype*) val parse_type_args_named_constrained = parse_type_arg_constrained >> (single o pair Binding.empty) || @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) || Scan.succeed []; -val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding; - -val no_map_rel = (Binding.empty, Binding.empty); - -fun extract_map_rel ("map", b) = apfst (K b) - | extract_map_rel ("rel", b) = apsnd (K b) - | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")"); - -val parse_map_rel_bindings = - @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"} - >> (fn ps => fold extract_map_rel ps no_map_rel) || - Scan.succeed no_map_rel; - val parse_ctr_spec = parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix; diff -r ac54bc80a5cc -r 91a1e4aa7c80 src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Wed Nov 27 11:08:55 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Nov 27 15:08:18 2013 +0100 @@ -136,6 +136,8 @@ val parse_binding_colon: binding parser val parse_opt_binding_colon: binding parser + val parse_type_args_named_constrained: (binding option * (string * string option)) list parser + val parse_map_rel_bindings: (binding * binding) parser val typedef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory @@ -253,6 +255,32 @@ val parse_binding_colon = parse_binding --| @{keyword ":"}; val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; +val parse_type_arg_constrained = + Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); + +val parse_type_arg_named_constrained = + (Parse.minus --| @{keyword ":"} >> K NONE || parse_opt_binding_colon >> SOME) -- + parse_type_arg_constrained; + +val parse_type_args_named_constrained = + parse_type_arg_constrained >> (single o pair (SOME Binding.empty)) || + @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) || + Scan.succeed []; + +val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding; + +val no_map_rel = (Binding.empty, Binding.empty); + +fun extract_map_rel ("map", b) = apfst (K b) + | extract_map_rel ("rel", b) = apsnd (K b) + | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")"); + +val parse_map_rel_bindings = + @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"} + >> (fn ps => fold extract_map_rel ps no_map_rel) || + Scan.succeed no_map_rel; + + (*TODO: is this really different from Typedef.add_typedef_global?*) fun typedef (b, Ts, mx) set opt_morphs tac lthy = let