--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 {*
--- 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);