--- 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:
--- 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 \<Rightarrow> ('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 \<Rightarrow> ('a, 'b, 'c) F"]
+ bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
text {* \blankline *}
@@ -2533,11 +2533,11 @@
text {*
\begin{matharray}{rcl}
- @{command_def "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
+ @{command_def "bnf_axiomatization"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}
@{rail \<open>
- @@{command bnf_decl} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
+ @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
@{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.
*}
--- 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 ("<_ , _>")
--- /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
--- 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
--- 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
--- /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;
--- 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;