made BNF compile after move to HOL
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 550626d3fad6f01c9
parent 55061 a0adf838e2d1
child 55063 6207fd64519b
made BNF compile after move to HOL
src/HOL/BNF_Comp.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_GFP.thy
src/HOL/BNF_LFP.thy
src/HOL/BNF_Util.thy
src/HOL/Basic_BNFs.thy
src/HOL/Main.thy
src/HOL/Tools/BNF/bnf_gfp.ML
     1.1 --- a/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4  lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
     1.5  by simp
     1.6  
     1.7 -ML_file "Tools/bnf_comp_tactics.ML"
     1.8 -ML_file "Tools/bnf_comp.ML"
     1.9 +ML_file "Tools/BNF/bnf_comp_tactics.ML"
    1.10 +ML_file "Tools/BNF/bnf_comp.ML"
    1.11  
    1.12  end
     2.1 --- a/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -157,7 +157,7 @@
     2.4  lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
     2.5    by clarsimp
     2.6  
     2.7 -ML_file "Tools/bnf_def_tactics.ML"
     2.8 -ML_file "Tools/bnf_def.ML"
     2.9 +ML_file "Tools/BNF/bnf_def_tactics.ML"
    2.10 +ML_file "Tools/BNF/bnf_def.ML"
    2.11  
    2.12  end
     3.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     3.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4  header {* Shared Fixed Point Operations on Bounded Natural Functors *}
     3.5  
     3.6  theory BNF_FP_Base
     3.7 -imports BNF_Comp Ctr_Sugar
     3.8 +imports Nitpick BNF_Comp Ctr_Sugar
     3.9  begin
    3.10  
    3.11  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    3.12 @@ -159,12 +159,12 @@
    3.13     (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
    3.14    unfolding Grp_def by rule auto
    3.15  
    3.16 -ML_file "Tools/bnf_fp_util.ML"
    3.17 -ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
    3.18 -ML_file "Tools/bnf_fp_def_sugar.ML"
    3.19 -ML_file "Tools/bnf_fp_n2m_tactics.ML"
    3.20 -ML_file "Tools/bnf_fp_n2m.ML"
    3.21 -ML_file "Tools/bnf_fp_n2m_sugar.ML"
    3.22 -ML_file "Tools/bnf_fp_rec_sugar_util.ML"
    3.23 +ML_file "Tools/BNF/bnf_fp_util.ML"
    3.24 +ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    3.25 +ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
    3.26 +ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
    3.27 +ML_file "Tools/BNF/bnf_fp_n2m.ML"
    3.28 +ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
    3.29 +ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
    3.30  
    3.31  end
     4.1 --- a/src/HOL/BNF_GFP.thy	Mon Jan 20 18:24:56 2014 +0100
     4.2 +++ b/src/HOL/BNF_GFP.thy	Mon Jan 20 18:24:56 2014 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4  header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
     4.5  
     4.6  theory BNF_GFP
     4.7 -imports BNF_FP_Base
     4.8 +imports BNF_FP_Base List_Prefix
     4.9  keywords
    4.10    "codatatype" :: thy_decl and
    4.11    "primcorecursive" :: thy_goal and
    4.12 @@ -266,16 +266,16 @@
    4.13  lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
    4.14  unfolding Field_card_of csum_def by auto
    4.15  
    4.16 -lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
    4.17 +lemma nat_rec_0_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
    4.18  by auto
    4.19  
    4.20 -lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    4.21 +lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    4.22  by auto
    4.23  
    4.24 -lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
    4.25 +lemma list_rec_Nil_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
    4.26  by auto
    4.27  
    4.28 -lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
    4.29 +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)"
    4.30  by auto
    4.31  
    4.32  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    4.33 @@ -349,10 +349,10 @@
    4.34    thus "univ f X \<in> B" using x PRES by simp
    4.35  qed
    4.36  
    4.37 -ML_file "Tools/bnf_gfp_rec_sugar_tactics.ML"
    4.38 -ML_file "Tools/bnf_gfp_rec_sugar.ML"
    4.39 -ML_file "Tools/bnf_gfp_util.ML"
    4.40 -ML_file "Tools/bnf_gfp_tactics.ML"
    4.41 -ML_file "Tools/bnf_gfp.ML"
    4.42 +ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
    4.43 +ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
    4.44 +ML_file "Tools/BNF/bnf_gfp_util.ML"
    4.45 +ML_file "Tools/BNF/bnf_gfp_tactics.ML"
    4.46 +ML_file "Tools/BNF/bnf_gfp.ML"
    4.47  
    4.48  end
     5.1 --- a/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     5.2 +++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     5.3 @@ -234,10 +234,10 @@
     5.4  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
     5.5    unfolding vimage2p_def by auto
     5.6  
     5.7 -ML_file "Tools/bnf_lfp_rec_sugar.ML"
     5.8 -ML_file "Tools/bnf_lfp_util.ML"
     5.9 -ML_file "Tools/bnf_lfp_tactics.ML"
    5.10 -ML_file "Tools/bnf_lfp.ML"
    5.11 -ML_file "Tools/bnf_lfp_compat.ML"
    5.12 +ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
    5.13 +ML_file "Tools/BNF/bnf_lfp_util.ML"
    5.14 +ML_file "Tools/BNF/bnf_lfp_tactics.ML"
    5.15 +ML_file "Tools/BNF/bnf_lfp.ML"
    5.16 +ML_file "Tools/BNF/bnf_lfp_compat.ML"
    5.17  
    5.18  end
     6.1 --- a/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
     6.2 +++ b/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
     6.3 @@ -30,7 +30,7 @@
     6.4  
     6.5  definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
     6.6  
     6.7 -ML_file "Tools/bnf_util.ML"
     6.8 -ML_file "Tools/bnf_tactics.ML"
     6.9 +ML_file "Tools/BNF/bnf_util.ML"
    6.10 +ML_file "Tools/BNF/bnf_tactics.ML"
    6.11  
    6.12  end
     7.1 --- a/src/HOL/Basic_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     7.2 +++ b/src/HOL/Basic_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     7.3 @@ -14,7 +14,6 @@
     7.4     (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
     7.5    Lifting_Sum
     7.6    Lifting_Product
     7.7 -  Main
     7.8  begin
     7.9  
    7.10  bnf ID: 'a
     8.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     8.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  header {* Main HOL *}
     8.5  
     8.6  theory Main
     8.7 -imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
     8.8 +imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
     8.9  begin
    8.10  
    8.11  text {*
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
     9.3 @@ -566,8 +566,8 @@
     9.4          mk_nthN n (Term.list_comb (Const (nth hset_recs (j - 1), hset_recT), args)) i
     9.5        end;
     9.6  
     9.7 -    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0} hset_rec_defs;
     9.8 -    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc} hset_rec_defs;
     9.9 +    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0_imp} hset_rec_defs;
    9.10 +    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc_imp} hset_rec_defs;
    9.11      val hset_rec_0ss' = transpose hset_rec_0ss;
    9.12      val hset_rec_Sucss' = transpose hset_rec_Sucss;
    9.13  
    9.14 @@ -1261,8 +1261,8 @@
    9.15          mk_nthN n (Term.list_comb (Const (Lev, LevT), ss) $ nat) i
    9.16        end;
    9.17  
    9.18 -    val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0} [Lev_def]);
    9.19 -    val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc} [Lev_def]);
    9.20 +    val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0_imp} [Lev_def]);
    9.21 +    val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc_imp} [Lev_def]);
    9.22  
    9.23      val rv_bind = mk_internal_b rvN;
    9.24      val rv_name = Binding.name_of rv_bind;
    9.25 @@ -1307,8 +1307,8 @@
    9.26          mk_nthN n (Term.list_comb (Const (rv, rvT), ss) $ kl) i
    9.27        end;
    9.28  
    9.29 -    val rv_Nils = flat (mk_rec_simps n @{thm list_rec_Nil} [rv_def]);
    9.30 -    val rv_Conss = flat (mk_rec_simps n @{thm list_rec_Cons} [rv_def]);
    9.31 +    val rv_Nils = flat (mk_rec_simps n @{thm list_rec_Nil_imp} [rv_def]);
    9.32 +    val rv_Conss = flat (mk_rec_simps n @{thm list_rec_Cons_imp} [rv_def]);
    9.33  
    9.34      val beh_binds = mk_internal_bs behN;
    9.35      fun beh_bind i = nth beh_binds (i - 1);