# HG changeset patch
# User blanchet
# Date 1409695579 -7200
# Node ID 967444d352b84acd592392efdd0060bf5aa23b54
# Parent  d91c1e50b36ed352404eda0d4750ed832e70374c
more compatibility functions

diff -r d91c1e50b36e -r 967444d352b8 src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Wed Sep 03 00:06:18 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Wed Sep 03 00:06:19 2014 +0200
@@ -90,20 +90,19 @@
 qed
 
 lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
-unfolding wo_rel_def card_order_on_def by blast
+  unfolding wo_rel_def card_order_on_def by blast
 
-lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
-  \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
-unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
+lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow> \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
+  unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
 
 lemma Card_order_trans:
   "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
-unfolding card_order_on_def well_order_on_def linear_order_on_def
-  partial_order_on_def preorder_on_def trans_def antisym_def by blast
+  unfolding card_order_on_def well_order_on_def linear_order_on_def
+    partial_order_on_def preorder_on_def trans_def antisym_def by blast
 
 lemma Cinfinite_limit2:
- assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
- shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
+  assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
+  shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
 proof -
   from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
     unfolding card_order_on_def well_order_on_def linear_order_on_def
@@ -132,8 +131,8 @@
   qed
 qed
 
-lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
- \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
+lemma Cinfinite_limit_finite:
+  "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk> \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
 proof (induct X rule: finite_induct)
   case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
 next
@@ -153,7 +152,7 @@
 qed
 
 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
-by auto
+  by auto
 
 lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
 
diff -r d91c1e50b36e -r 967444d352b8 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 00:06:18 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 00:06:19 2014 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2013, 2014
 
-Compatibility layer with the old datatype package. Parly based on:
+Compatibility layer with the old datatype package. Partly based on
 
     Title:      HOL/Tools/Old_Datatype/old_datatype_data.ML
     Author:     Stefan Berghofer, TU Muenchen
@@ -29,6 +29,13 @@
     string list * theory
   val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    local_theory -> (term list * thm list) * local_theory
+  val add_primrec_global: (binding * typ option * mixfix) list ->
+    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
+  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
+    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory ->
+    (term list * thm list) * theory
+  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
+    local_theory -> (string list * (term list * (int list * thm list))) * local_theory
 end;
 
 structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -358,6 +365,10 @@
   end;
 
 val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
+val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
+val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;
+val add_primrec_simple = apfst (apsnd (apsnd (apsnd flat o apfst flat))) ooo
+  BNF_LFP_Rec_Sugar.add_primrec_simple;
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "datatype_compat"}