--- a/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 12:37:03 2013 +0200
@@ -11,10 +11,7 @@
theory BNF_FP_Basic
imports BNF_Comp BNF_Ctr_Sugar
keywords
- "primrec_new" :: thy_decl and
- "primcorec" :: thy_goal and
- "defaults" and
- "sequential"
+ "defaults"
begin
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
--- a/src/HOL/BNF/BNF_GFP.thy Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Fri Aug 30 12:37:03 2013 +0200
@@ -10,7 +10,9 @@
theory BNF_GFP
imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist"
keywords
- "codatatype" :: thy_decl
+ "codatatype" :: thy_decl and
+ "primcorec" :: thy_goal and
+ "sequential"
begin
lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
--- a/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:37:03 2013 +0200
@@ -13,7 +13,8 @@
imports BNF_FP_Basic
keywords
"datatype_new" :: thy_decl and
- "datatype_new_compat" :: thy_decl
+ "datatype_new_compat" :: thy_decl and
+ "primrec_new" :: thy_decl
begin
lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 12:37:03 2013 +0200
@@ -9,6 +9,9 @@
sig
val add_primrec_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> local_theory -> local_theory;
+ val add_primcorec_cmd: bool ->
+ (binding * string option * mixfix) list * (Attrib.binding * string) list -> Proof.context ->
+ Proof.state
end;
(* TODO:
@@ -34,6 +37,9 @@
val simp_attrs = @{attributes [simp]};
+
+(* Primrec *)
+
type eqn_data = {
fun_name: string,
rec_type: typ,
@@ -390,25 +396,8 @@
space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns))
-val _ = Outer_Syntax.local_theory
- @{command_spec "primrec_new"}
- "define primitive recursive functions"
- (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd);
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+(* Primcorec *)
type co_eqn_data_dtr_disc = {
fun_name: string,
@@ -734,10 +723,4 @@
else error ("primcorec error:\n " ^ str ^ "\nin\n " ^
space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns))
-val _ = Outer_Syntax.local_theory_to_proof
- @{command_spec "primcorec"}
- "define primitive corecursive functions"
- (Parse.opt_keyword "sequential" -- (Parse.fixes -- Parse_Spec.where_alt_specs) >>
- uncurry add_primcorec_cmd);
-
end;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Aug 30 12:37:03 2013 +0200
@@ -23,6 +23,7 @@
open BNF_Comp
open BNF_FP_Util
open BNF_FP_Def_Sugar
+open BNF_FP_Rec_Sugar
open BNF_GFP_Util
open BNF_GFP_Tactics
@@ -2902,4 +2903,9 @@
Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
(parse_co_datatype_cmd Greatest_FP construct_gfp);
+val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorec"}
+ "define primitive corecursive functions"
+ ((Scan.option @{keyword "sequential"} >> is_some) --
+ (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd);
+
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Aug 30 12:37:03 2013 +0200
@@ -22,6 +22,7 @@
open BNF_Comp
open BNF_FP_Util
open BNF_FP_Def_Sugar
+open BNF_FP_Rec_Sugar
open BNF_LFP_Util
open BNF_LFP_Tactics
@@ -1875,4 +1876,8 @@
Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
(parse_co_datatype_cmd Least_FP construct_lfp);
+val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"}
+ "define primitive recursive functions"
+ (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd);
+
end;