1.1 --- a/NEWS Mon May 12 17:17:32 2014 +0200
1.2 +++ b/NEWS Tue May 13 09:21:22 2014 +0200
1.3 @@ -291,7 +291,7 @@
1.4 New theories:
1.5 Wellorder_Extension.thy (split from Zorn.thy)
1.6 Library/Cardinal_Notations.thy
1.7 - Library/BNF_Decl.thy
1.8 + Library/BNF_Axomatization.thy
1.9 BNF_Examples/Misc_Primcorec.thy
1.10 BNF_Examples/Stream_Processor.thy
1.11 Discontinued theories:
2.1 --- a/src/Doc/Datatypes/Datatypes.thy Mon May 12 17:17:32 2014 +0200
2.2 +++ b/src/Doc/Datatypes/Datatypes.thy Tue May 13 09:21:22 2014 +0200
2.3 @@ -10,7 +10,7 @@
2.4 theory Datatypes
2.5 imports
2.6 Setup
2.7 - "~~/src/HOL/Library/BNF_Decl"
2.8 + "~~/src/HOL/Library/BNF_Axiomatization"
2.9 "~~/src/HOL/Library/Cardinal_Notations"
2.10 "~~/src/HOL/Library/FSet"
2.11 "~~/src/HOL/Library/Simps_Case_Conv"
2.12 @@ -80,7 +80,7 @@
2.13 infinite branching.
2.14
2.15 The package is part of @{theory Main}. Additional functionality is provided by
2.16 -the theory @{theory BNF_Decl}, located in the directory
2.17 +the theory @{theory BNF_Axiomatization}, located in the directory
2.18 \verb|~~/src/HOL/Library|.
2.19
2.20 The package, like its predecessor, fully adheres to the LCF philosophy
2.21 @@ -2477,7 +2477,7 @@
2.22 for further examples of BNF registration, some of which feature custom
2.23 witnesses.
2.24
2.25 -The next example declares a BNF axiomatically. The @{command bnf_decl} command
2.26 +The next example declares a BNF axiomatically. The @{command bnf_axiomatization} command
2.27 introduces a type @{text "('a, 'b, 'c) F"}, three set constants, a map
2.28 function, a relator, and a nonemptiness witness that depends only on
2.29 @{typ 'a}. (The type @{text "'a \<Rightarrow> ('a, 'b, 'c) F"} of
2.30 @@ -2486,7 +2486,7 @@
2.31 properties are postulated as axioms.
2.32 *}
2.33
2.34 - bnf_decl (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
2.35 + bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
2.36
2.37 text {* \blankline *}
2.38
2.39 @@ -2533,11 +2533,11 @@
2.40
2.41 text {*
2.42 \begin{matharray}{rcl}
2.43 - @{command_def "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
2.44 + @{command_def "bnf_axiomatization"} & : & @{text "local_theory \<rightarrow> local_theory"}
2.45 \end{matharray}
2.46
2.47 @{rail \<open>
2.48 - @@{command bnf_decl} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
2.49 + @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
2.50 @{syntax wit_types}? mixfix?
2.51 ;
2.52 @{syntax_def wit_types}: '[' 'wits' ':' types ']'
2.53 @@ -2546,7 +2546,7 @@
2.54 \medskip
2.55
2.56 \noindent
2.57 -The @{command bnf_decl} command declares a new type and associated constants
2.58 +The @{command bnf_axiomatization} command declares a new type and associated constants
2.59 (map, set, relator, and cardinal bound) and asserts the BNF properties for
2.60 these constants as axioms.
2.61
2.62 @@ -2558,12 +2558,12 @@
2.63 Type arguments are live by default; they can be marked as dead by entering
2.64 ``-'' (hyphen) instead of an identifier for the corresponding set function.
2.65 Witnesses can be specified by their types. Otherwise, the syntax of
2.66 -@{command bnf_decl} is identical to the left-hand side of a
2.67 +@{command bnf_axiomatization} is identical to the left-hand side of a
2.68 @{command datatype_new} or @{command codatatype} definition.
2.69
2.70 The command is useful to reason abstractly about BNFs. The axioms are safe
2.71 because there exists BNFs of arbitrary large arities. Applications must import
2.72 -the theory @{theory BNF_Decl}, located in the directory
2.73 +the theory @{theory BNF_Axiomatization}, located in the directory
2.74 \verb|~~/src/HOL/Library|, to use this functionality.
2.75 *}
2.76
3.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy Mon May 12 17:17:32 2014 +0200
3.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy Tue May 13 09:21:22 2014 +0200
3.3 @@ -9,7 +9,7 @@
3.4 header {* Stream Processors *}
3.5
3.6 theory Stream_Processor
3.7 -imports Stream "~~/src/HOL/Library/BNF_Decl"
3.8 +imports Stream "~~/src/HOL/Library/BNF_Axiomatization"
3.9 begin
3.10
3.11 section {* Continuous Functions on Streams *}
3.12 @@ -150,7 +150,7 @@
3.13
3.14 section {* Generalization to an Arbitrary BNF as Codomain *}
3.15
3.16 -bnf_decl ('a, 'b) F (map: F)
3.17 +bnf_axiomatization ('a, 'b) F (map: F)
3.18
3.19 notation BNF_Def.convol ("<_ , _>")
3.20
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Library/BNF_Axiomatization.thy Tue May 13 09:21:22 2014 +0200
4.3 @@ -0,0 +1,18 @@
4.4 +(* Title: HOL/Library/BNF_Axiomatization.thy
4.5 + Author: Dmitriy Traytel, TU Muenchen
4.6 + Copyright 2013
4.7 +
4.8 +Axiomatic declaration of bounded natural functors.
4.9 +*)
4.10 +
4.11 +header {* Axiomatic declaration of Bounded Natural Functors *}
4.12 +
4.13 +theory BNF_Axiomatization
4.14 +imports Main
4.15 +keywords
4.16 + "bnf_axiomatization" :: thy_decl
4.17 +begin
4.18 +
4.19 +ML_file "bnf_axiomatization.ML"
4.20 +
4.21 +end
5.1 --- a/src/HOL/Library/BNF_Decl.thy Mon May 12 17:17:32 2014 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,18 +0,0 @@
5.4 -(* Title: HOL/Library/BNF_Decl.thy
5.5 - Author: Dmitriy Traytel, TU Muenchen
5.6 - Copyright 2013
5.7 -
5.8 -Axiomatic declaration of bounded natural functors.
5.9 -*)
5.10 -
5.11 -header {* Axiomatic declaration of Bounded Natural Functors *}
5.12 -
5.13 -theory BNF_Decl
5.14 -imports Main
5.15 -keywords
5.16 - "bnf_decl" :: thy_decl
5.17 -begin
5.18 -
5.19 -ML_file "bnf_decl.ML"
5.20 -
5.21 -end
6.1 --- a/src/HOL/Library/Library.thy Mon May 12 17:17:32 2014 +0200
6.2 +++ b/src/HOL/Library/Library.thy Tue May 13 09:21:22 2014 +0200
6.3 @@ -4,7 +4,7 @@
6.4 AList
6.5 BigO
6.6 Bit
6.7 - BNF_Decl
6.8 + BNF_Axiomatization
6.9 Boolean_Algebra
6.10 Char_ord
6.11 ContNotDenum
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Library/bnf_axiomatization.ML Tue May 13 09:21:22 2014 +0200
7.3 @@ -0,0 +1,120 @@
7.4 +(* Title: HOL/Library/bnf_axiomatization.ML
7.5 + Author: Dmitriy Traytel, TU Muenchen
7.6 + Copyright 2013
7.7 +
7.8 +Axiomatic declaration of bounded natural functors.
7.9 +*)
7.10 +
7.11 +signature BNF_AXIOMATIZATION =
7.12 +sig
7.13 + val bnf_axiomatization: (binding option * (typ * sort)) list -> binding -> mixfix -> binding ->
7.14 + binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory
7.15 +end
7.16 +
7.17 +structure BNF_Axiomatization : BNF_AXIOMATIZATION =
7.18 +struct
7.19 +
7.20 +open BNF_Util
7.21 +open BNF_Def
7.22 +
7.23 +fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
7.24 + let
7.25 + fun prepare_type_arg (set_opt, (ty, c)) =
7.26 + let val s = fst (dest_TFree (prepare_typ lthy ty)) in
7.27 + (set_opt, (s, prepare_constraint lthy c))
7.28 + end;
7.29 + val ((user_setbs, vars), raw_vars') =
7.30 + map prepare_type_arg raw_vars
7.31 + |> `split_list
7.32 + |>> apfst (map_filter I);
7.33 + val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
7.34 +
7.35 + fun mk_b name user_b =
7.36 + (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
7.37 + |> Binding.qualify false (Binding.name_of b);
7.38 + val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
7.39 + val (bd_type_Tname, lthy) =
7.40 + Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
7.41 + val T = Type (Tname, map TFree vars);
7.42 + val bd_type_T = Type (bd_type_Tname, map TFree deads);
7.43 + val lives = map TFree (filter_out (member (op =) deads) vars);
7.44 + val live = length lives;
7.45 + val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
7.46 + val (lives', _) = BNF_Util.mk_TFrees (length lives)
7.47 + (fold Variable.declare_typ (map TFree vars) lthy);
7.48 + val T' = Term.typ_subst_atomic (lives ~~ lives') T;
7.49 + val mapT = map2 (curry op -->) lives lives' ---> T --> T';
7.50 + val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
7.51 + val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
7.52 + val mapb = mk_b BNF_Def.mapN user_mapb;
7.53 + val bdb = mk_b "bd" Binding.empty;
7.54 + val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
7.55 + (if live = 1 then [0] else 1 upto live);
7.56 +
7.57 + val witTs = map (prepare_typ lthy) user_witTs;
7.58 + val nwits = length witTs;
7.59 + val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
7.60 + (if nwits = 1 then [0] else 1 upto nwits);
7.61 +
7.62 + val lthy = Local_Theory.background_theory
7.63 + (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
7.64 + map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
7.65 + map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
7.66 + lthy;
7.67 + val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
7.68 + val Fsets = map2 (fn setb => fn setT =>
7.69 + Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
7.70 + val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
7.71 + val Fwits = map2 (fn witb => fn witT =>
7.72 + Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
7.73 + val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
7.74 + prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
7.75 + user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
7.76 + lthy;
7.77 +
7.78 + fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
7.79 + val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
7.80 + val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
7.81 +
7.82 + val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
7.83 + (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
7.84 + ||> `Local_Theory.restore;
7.85 +
7.86 + fun mk_wit_thms set_maps =
7.87 + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
7.88 + (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
7.89 + |> Conjunction.elim_balanced (length wit_goals)
7.90 + |> map2 (Conjunction.elim_balanced o length) wit_goalss
7.91 + |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
7.92 + val phi = Proof_Context.export_morphism lthy_old lthy;
7.93 + val thms = unflat all_goalss (Morphism.fact phi raw_thms);
7.94 +
7.95 + val (bnf, lthy') = after_qed mk_wit_thms thms lthy
7.96 + in
7.97 + (bnf, BNF_Def.register_bnf key bnf lthy')
7.98 + end;
7.99 +
7.100 +val bnf_axiomatization = prepare_decl (K I) (K I);
7.101 +
7.102 +fun read_constraint _ NONE = @{sort type}
7.103 + | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
7.104 +
7.105 +val bnf_axiomatization_cmd = prepare_decl read_constraint Syntax.read_typ;
7.106 +
7.107 +val parse_witTs =
7.108 + @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
7.109 + >> (fn ("wits", Ts) => Ts
7.110 + | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
7.111 + @{keyword "]"} || Scan.succeed [];
7.112 +
7.113 +val parse_bnf_axiomatization =
7.114 + parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
7.115 + parse_witTs -- Parse.opt_mixfix;
7.116 +
7.117 +val _ =
7.118 + Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
7.119 + (parse_bnf_axiomatization >>
7.120 + (fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
7.121 + bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd));
7.122 +
7.123 +end;
8.1 --- a/src/HOL/Library/bnf_decl.ML Mon May 12 17:17:32 2014 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,120 +0,0 @@
8.4 -(* Title: HOL/Library/bnf_decl.ML
8.5 - Author: Dmitriy Traytel, TU Muenchen
8.6 - Copyright 2013
8.7 -
8.8 -Axiomatic declaration of bounded natural functors.
8.9 -*)
8.10 -
8.11 -signature BNF_DECL =
8.12 -sig
8.13 - val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding ->
8.14 - typ list -> local_theory -> BNF_Def.bnf * local_theory
8.15 -end
8.16 -
8.17 -structure BNF_Decl : BNF_DECL =
8.18 -struct
8.19 -
8.20 -open BNF_Util
8.21 -open BNF_Def
8.22 -
8.23 -fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
8.24 - let
8.25 - fun prepare_type_arg (set_opt, (ty, c)) =
8.26 - let val s = fst (dest_TFree (prepare_typ lthy ty)) in
8.27 - (set_opt, (s, prepare_constraint lthy c))
8.28 - end;
8.29 - val ((user_setbs, vars), raw_vars') =
8.30 - map prepare_type_arg raw_vars
8.31 - |> `split_list
8.32 - |>> apfst (map_filter I);
8.33 - val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
8.34 -
8.35 - fun mk_b name user_b =
8.36 - (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
8.37 - |> Binding.qualify false (Binding.name_of b);
8.38 - val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
8.39 - val (bd_type_Tname, lthy) =
8.40 - Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
8.41 - val T = Type (Tname, map TFree vars);
8.42 - val bd_type_T = Type (bd_type_Tname, map TFree deads);
8.43 - val lives = map TFree (filter_out (member (op =) deads) vars);
8.44 - val live = length lives;
8.45 - val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
8.46 - val (lives', _) = BNF_Util.mk_TFrees (length lives)
8.47 - (fold Variable.declare_typ (map TFree vars) lthy);
8.48 - val T' = Term.typ_subst_atomic (lives ~~ lives') T;
8.49 - val mapT = map2 (curry op -->) lives lives' ---> T --> T';
8.50 - val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
8.51 - val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
8.52 - val mapb = mk_b BNF_Def.mapN user_mapb;
8.53 - val bdb = mk_b "bd" Binding.empty;
8.54 - val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
8.55 - (if live = 1 then [0] else 1 upto live);
8.56 -
8.57 - val witTs = map (prepare_typ lthy) user_witTs;
8.58 - val nwits = length witTs;
8.59 - val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
8.60 - (if nwits = 1 then [0] else 1 upto nwits);
8.61 -
8.62 - val lthy = Local_Theory.background_theory
8.63 - (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
8.64 - map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
8.65 - map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
8.66 - lthy;
8.67 - val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
8.68 - val Fsets = map2 (fn setb => fn setT =>
8.69 - Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
8.70 - val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
8.71 - val Fwits = map2 (fn witb => fn witT =>
8.72 - Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
8.73 - val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
8.74 - prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
8.75 - user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
8.76 - lthy;
8.77 -
8.78 - fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
8.79 - val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
8.80 - val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
8.81 -
8.82 - val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
8.83 - (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
8.84 - ||> `Local_Theory.restore;
8.85 -
8.86 - fun mk_wit_thms set_maps =
8.87 - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
8.88 - (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
8.89 - |> Conjunction.elim_balanced (length wit_goals)
8.90 - |> map2 (Conjunction.elim_balanced o length) wit_goalss
8.91 - |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
8.92 - val phi = Proof_Context.export_morphism lthy_old lthy;
8.93 - val thms = unflat all_goalss (Morphism.fact phi raw_thms);
8.94 -
8.95 - val (bnf, lthy') = after_qed mk_wit_thms thms lthy
8.96 - in
8.97 - (bnf, BNF_Def.register_bnf key bnf lthy')
8.98 - end;
8.99 -
8.100 -val bnf_decl = prepare_decl (K I) (K I);
8.101 -
8.102 -fun read_constraint _ NONE = @{sort type}
8.103 - | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
8.104 -
8.105 -val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
8.106 -
8.107 -val parse_witTs =
8.108 - @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
8.109 - >> (fn ("wits", Ts) => Ts
8.110 - | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
8.111 - @{keyword "]"} || Scan.succeed [];
8.112 -
8.113 -val parse_bnf_decl =
8.114 - parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
8.115 - parse_witTs -- Parse.opt_mixfix;
8.116 -
8.117 -val _ =
8.118 - Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration"
8.119 - (parse_bnf_decl >>
8.120 - (fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
8.121 - bnf_decl_cmd bsTs b mx mapb relb witTs #> snd));
8.122 -
8.123 -end;