# HG changeset patch # User traytel # Date 1399965682 -7200 # Node ID 5fff4dc31d34f28c4da8cddc83b7c933ae6330b3 # Parent 952833323c997ca5a1db01dbd4eed7e77fabace6 bnf_decl -> bnf_axiomatization diff -r 952833323c99 -r 5fff4dc31d34 NEWS --- a/NEWS Mon May 12 17:17:32 2014 +0200 +++ b/NEWS Tue May 13 09:21:22 2014 +0200 @@ -291,7 +291,7 @@ New theories: Wellorder_Extension.thy (split from Zorn.thy) Library/Cardinal_Notations.thy - Library/BNF_Decl.thy + Library/BNF_Axomatization.thy BNF_Examples/Misc_Primcorec.thy BNF_Examples/Stream_Processor.thy Discontinued theories: diff -r 952833323c99 -r 5fff4dc31d34 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon May 12 17:17:32 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue May 13 09:21:22 2014 +0200 @@ -10,7 +10,7 @@ theory Datatypes imports Setup - "~~/src/HOL/Library/BNF_Decl" + "~~/src/HOL/Library/BNF_Axiomatization" "~~/src/HOL/Library/Cardinal_Notations" "~~/src/HOL/Library/FSet" "~~/src/HOL/Library/Simps_Case_Conv" @@ -80,7 +80,7 @@ infinite branching. The package is part of @{theory Main}. Additional functionality is provided by -the theory @{theory BNF_Decl}, located in the directory +the theory @{theory BNF_Axiomatization}, located in the directory \verb|~~/src/HOL/Library|. The package, like its predecessor, fully adheres to the LCF philosophy @@ -2477,7 +2477,7 @@ for further examples of BNF registration, some of which feature custom witnesses. -The next example declares a BNF axiomatically. The @{command bnf_decl} command +The next example declares a BNF axiomatically. The @{command bnf_axiomatization} command introduces a type @{text "('a, 'b, 'c) F"}, three set constants, a map function, a relator, and a nonemptiness witness that depends only on @{typ 'a}. (The type @{text "'a \ ('a, 'b, 'c) F"} of @@ -2486,7 +2486,7 @@ properties are postulated as axioms. *} - bnf_decl (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \ ('a, 'b, 'c) F"] + bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \ ('a, 'b, 'c) F"] text {* \blankline *} @@ -2533,11 +2533,11 @@ text {* \begin{matharray}{rcl} - @{command_def "bnf_decl"} & : & @{text "local_theory \ local_theory"} + @{command_def "bnf_axiomatization"} & : & @{text "local_theory \ local_theory"} \end{matharray} @{rail \ - @@{command bnf_decl} target? @{syntax tyargs}? name @{syntax map_rel}? \ + @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax map_rel}? \ @{syntax wit_types}? mixfix? ; @{syntax_def wit_types}: '[' 'wits' ':' types ']' @@ -2546,7 +2546,7 @@ \medskip \noindent -The @{command bnf_decl} command declares a new type and associated constants +The @{command bnf_axiomatization} command declares a new type and associated constants (map, set, relator, and cardinal bound) and asserts the BNF properties for these constants as axioms. @@ -2558,12 +2558,12 @@ Type arguments are live by default; they can be marked as dead by entering ``-'' (hyphen) instead of an identifier for the corresponding set function. Witnesses can be specified by their types. Otherwise, the syntax of -@{command bnf_decl} is identical to the left-hand side of a +@{command bnf_axiomatization} is identical to the left-hand side of a @{command datatype_new} or @{command codatatype} definition. The command is useful to reason abstractly about BNFs. The axioms are safe because there exists BNFs of arbitrary large arities. Applications must import -the theory @{theory BNF_Decl}, located in the directory +the theory @{theory BNF_Axiomatization}, located in the directory \verb|~~/src/HOL/Library|, to use this functionality. *} diff -r 952833323c99 -r 5fff4dc31d34 src/HOL/BNF_Examples/Stream_Processor.thy --- a/src/HOL/BNF_Examples/Stream_Processor.thy Mon May 12 17:17:32 2014 +0200 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy Tue May 13 09:21:22 2014 +0200 @@ -9,7 +9,7 @@ header {* Stream Processors *} theory Stream_Processor -imports Stream "~~/src/HOL/Library/BNF_Decl" +imports Stream "~~/src/HOL/Library/BNF_Axiomatization" begin section {* Continuous Functions on Streams *} @@ -150,7 +150,7 @@ section {* Generalization to an Arbitrary BNF as Codomain *} -bnf_decl ('a, 'b) F (map: F) +bnf_axiomatization ('a, 'b) F (map: F) notation BNF_Def.convol ("<_ , _>") diff -r 952833323c99 -r 5fff4dc31d34 src/HOL/Library/BNF_Axiomatization.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/BNF_Axiomatization.thy Tue May 13 09:21:22 2014 +0200 @@ -0,0 +1,18 @@ +(* Title: HOL/Library/BNF_Axiomatization.thy + Author: Dmitriy Traytel, TU Muenchen + Copyright 2013 + +Axiomatic declaration of bounded natural functors. +*) + +header {* Axiomatic declaration of Bounded Natural Functors *} + +theory BNF_Axiomatization +imports Main +keywords + "bnf_axiomatization" :: thy_decl +begin + +ML_file "bnf_axiomatization.ML" + +end diff -r 952833323c99 -r 5fff4dc31d34 src/HOL/Library/BNF_Decl.thy --- a/src/HOL/Library/BNF_Decl.thy Mon May 12 17:17:32 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/Library/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 Main -keywords - "bnf_decl" :: thy_decl -begin - -ML_file "bnf_decl.ML" - -end diff -r 952833323c99 -r 5fff4dc31d34 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon May 12 17:17:32 2014 +0200 +++ b/src/HOL/Library/Library.thy Tue May 13 09:21:22 2014 +0200 @@ -4,7 +4,7 @@ AList BigO Bit - BNF_Decl + BNF_Axiomatization Boolean_Algebra Char_ord ContNotDenum diff -r 952833323c99 -r 5fff4dc31d34 src/HOL/Library/bnf_axiomatization.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/bnf_axiomatization.ML Tue May 13 09:21:22 2014 +0200 @@ -0,0 +1,120 @@ +(* Title: HOL/Library/bnf_axiomatization.ML + Author: Dmitriy Traytel, TU Muenchen + Copyright 2013 + +Axiomatic declaration of bounded natural functors. +*) + +signature BNF_AXIOMATIZATION = +sig + val bnf_axiomatization: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> + binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory +end + +structure BNF_Axiomatization : BNF_AXIOMATIZATION = +struct + +open BNF_Util +open BNF_Def + +fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs 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 witTs = map (prepare_typ lthy) user_witTs; + val nwits = length witTs; + val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty) + (if nwits = 1 then [0] else 1 upto nwits); + + val lthy = Local_Theory.background_theory + (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: + map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ + map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) + 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 Fwits = map2 (fn witb => fn witT => + Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; + val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = + prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads)) + user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE) + lthy; + + fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; + val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; + val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); + + val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result + (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy + ||> `Local_Theory.restore; + + fun mk_wit_thms set_maps = + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) + (fn {context = ctxt, prems = _} => mk_wits_tac ctxt 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 phi = Proof_Context.export_morphism lthy_old lthy; + val thms = unflat all_goalss (Morphism.fact phi raw_thms); + + val (bnf, lthy') = after_qed mk_wit_thms thms lthy + in + (bnf, BNF_Def.register_bnf key bnf lthy') + end; + +val bnf_axiomatization = prepare_decl (K I) (K I); + +fun read_constraint _ NONE = @{sort type} + | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; + +val bnf_axiomatization_cmd = prepare_decl read_constraint Syntax.read_typ; + +val parse_witTs = + @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ + >> (fn ("wits", Ts) => Ts + | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| + @{keyword "]"} || Scan.succeed []; + +val parse_bnf_axiomatization = + parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- + parse_witTs -- Parse.opt_mixfix; + +val _ = + Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration" + (parse_bnf_axiomatization >> + (fn ((((bsTs, b), (mapb, relb)), witTs), mx) => + bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd)); + +end; diff -r 952833323c99 -r 5fff4dc31d34 src/HOL/Library/bnf_decl.ML --- a/src/HOL/Library/bnf_decl.ML Mon May 12 17:17:32 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,120 +0,0 @@ -(* Title: HOL/Library/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 -> - typ list -> 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 user_witTs 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 witTs = map (prepare_typ lthy) user_witTs; - val nwits = length witTs; - val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty) - (if nwits = 1 then [0] else 1 upto nwits); - - val lthy = Local_Theory.background_theory - (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: - map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ - map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) - 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 Fwits = map2 (fn witb => fn witT => - Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; - val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = - prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads)) - user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE) - lthy; - - fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; - val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; - val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); - - val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result - (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy - ||> `Local_Theory.restore; - - fun mk_wit_thms set_maps = - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) - (fn {context = ctxt, prems = _} => mk_wits_tac ctxt 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 phi = Proof_Context.export_morphism lthy_old lthy; - val thms = unflat all_goalss (Morphism.fact phi raw_thms); - - val (bnf, lthy') = after_qed mk_wit_thms thms lthy - in - (bnf, BNF_Def.register_bnf key bnf lthy') - end; - -val bnf_decl = prepare_decl (K I) (K I); - -fun read_constraint _ NONE = @{sort type} - | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; - -val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ; - -val parse_witTs = - @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ - >> (fn ("wits", Ts) => Ts - | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| - @{keyword "]"} || Scan.succeed []; - -val parse_bnf_decl = - parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- - parse_witTs -- Parse.opt_mixfix; - -val _ = - Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration" - (parse_bnf_decl >> - (fn ((((bsTs, b), (mapb, relb)), witTs), mx) => - bnf_decl_cmd bsTs b mx mapb relb witTs #> snd)); - -end;