# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 6d3fad6f01c98fcdcb5628d81e0dc5d4ab3102a7
# Parent  a0adf838e2d1e1cc9ce26371652e0289428a5e54
made BNF compile after move to HOL

diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -70,7 +70,7 @@
 lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
 by simp
 
-ML_file "Tools/bnf_comp_tactics.ML"
-ML_file "Tools/bnf_comp.ML"
+ML_file "Tools/BNF/bnf_comp_tactics.ML"
+ML_file "Tools/BNF/bnf_comp.ML"
 
 end
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -157,7 +157,7 @@
 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
   by clarsimp
 
-ML_file "Tools/bnf_def_tactics.ML"
-ML_file "Tools/bnf_def.ML"
+ML_file "Tools/BNF/bnf_def_tactics.ML"
+ML_file "Tools/BNF/bnf_def.ML"
 
 end
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -10,7 +10,7 @@
 header {* Shared Fixed Point Operations on Bounded Natural Functors *}
 
 theory BNF_FP_Base
-imports BNF_Comp Ctr_Sugar
+imports Nitpick BNF_Comp Ctr_Sugar
 begin
 
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
@@ -159,12 +159,12 @@
    (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
   unfolding Grp_def by rule auto
 
-ML_file "Tools/bnf_fp_util.ML"
-ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
-ML_file "Tools/bnf_fp_def_sugar.ML"
-ML_file "Tools/bnf_fp_n2m_tactics.ML"
-ML_file "Tools/bnf_fp_n2m.ML"
-ML_file "Tools/bnf_fp_n2m_sugar.ML"
-ML_file "Tools/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/BNF/bnf_fp_util.ML"
+ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
+ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
+ML_file "Tools/BNF/bnf_fp_n2m.ML"
+ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
+ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
 
 end
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -10,7 +10,7 @@
 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_GFP
-imports BNF_FP_Base
+imports BNF_FP_Base List_Prefix
 keywords
   "codatatype" :: thy_decl and
   "primcorecursive" :: thy_goal and
@@ -266,16 +266,16 @@
 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
 unfolding Field_card_of csum_def by auto
 
-lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
+lemma nat_rec_0_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
 by auto
 
-lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
+lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
 by auto
 
-lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
+lemma list_rec_Nil_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
 by auto
 
-lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
+lemma list_rec_Cons_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
 by auto
 
 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
@@ -349,10 +349,10 @@
   thus "univ f X \<in> B" using x PRES by simp
 qed
 
-ML_file "Tools/bnf_gfp_rec_sugar_tactics.ML"
-ML_file "Tools/bnf_gfp_rec_sugar.ML"
-ML_file "Tools/bnf_gfp_util.ML"
-ML_file "Tools/bnf_gfp_tactics.ML"
-ML_file "Tools/bnf_gfp.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
+ML_file "Tools/BNF/bnf_gfp_util.ML"
+ML_file "Tools/BNF/bnf_gfp_tactics.ML"
+ML_file "Tools/BNF/bnf_gfp.ML"
 
 end
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -234,10 +234,10 @@
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   unfolding vimage2p_def by auto
 
-ML_file "Tools/bnf_lfp_rec_sugar.ML"
-ML_file "Tools/bnf_lfp_util.ML"
-ML_file "Tools/bnf_lfp_tactics.ML"
-ML_file "Tools/bnf_lfp.ML"
-ML_file "Tools/bnf_lfp_compat.ML"
+ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
+ML_file "Tools/BNF/bnf_lfp_util.ML"
+ML_file "Tools/BNF/bnf_lfp_tactics.ML"
+ML_file "Tools/BNF/bnf_lfp.ML"
+ML_file "Tools/BNF/bnf_lfp_compat.ML"
 
 end
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/BNF_Util.thy
--- a/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -30,7 +30,7 @@
 
 definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
 
-ML_file "Tools/bnf_util.ML"
-ML_file "Tools/bnf_tactics.ML"
+ML_file "Tools/BNF/bnf_util.ML"
+ML_file "Tools/BNF/bnf_tactics.ML"
 
 end
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -14,7 +14,6 @@
    (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
   Lifting_Sum
   Lifting_Product
-  Main
 begin
 
 bnf ID: 'a
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
+imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
 begin
 
 text {*
diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -566,8 +566,8 @@
         mk_nthN n (Term.list_comb (Const (nth hset_recs (j - 1), hset_recT), args)) i
       end;
 
-    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0} hset_rec_defs;
-    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc} hset_rec_defs;
+    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0_imp} hset_rec_defs;
+    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc_imp} hset_rec_defs;
     val hset_rec_0ss' = transpose hset_rec_0ss;
     val hset_rec_Sucss' = transpose hset_rec_Sucss;
 
@@ -1261,8 +1261,8 @@
         mk_nthN n (Term.list_comb (Const (Lev, LevT), ss) $ nat) i
       end;
 
-    val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0} [Lev_def]);
-    val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc} [Lev_def]);
+    val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0_imp} [Lev_def]);
+    val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc_imp} [Lev_def]);
 
     val rv_bind = mk_internal_b rvN;
     val rv_name = Binding.name_of rv_bind;
@@ -1307,8 +1307,8 @@
         mk_nthN n (Term.list_comb (Const (rv, rvT), ss) $ kl) i
       end;
 
-    val rv_Nils = flat (mk_rec_simps n @{thm list_rec_Nil} [rv_def]);
-    val rv_Conss = flat (mk_rec_simps n @{thm list_rec_Cons} [rv_def]);
+    val rv_Nils = flat (mk_rec_simps n @{thm list_rec_Nil_imp} [rv_def]);
+    val rv_Conss = flat (mk_rec_simps n @{thm list_rec_Cons_imp} [rv_def]);
 
     val beh_binds = mk_internal_bs behN;
     fun beh_bind i = nth beh_binds (i - 1);