removed dependency of BNF package on Nitpick
authorblanchet
Mon Jan 20 19:05:25 2014 +0100 (2014-01-20)
changeset 55079ec08a67e993b
parent 55078 558c9ceabaa1
child 55080 b7c41accbff2
removed dependency of BNF package on Nitpick
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_GFP.thy
src/HOL/Main.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:59:53 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 19:05:25 2014 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  header {* Shared Fixed Point Operations on Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_FP_Base
     1.7 -imports Nitpick BNF_Comp Ctr_Sugar
     1.8 +imports BNF_Comp Ctr_Sugar
     1.9  begin
    1.10  
    1.11  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
     2.1 --- a/src/HOL/BNF_GFP.thy	Mon Jan 20 18:59:53 2014 +0100
     2.2 +++ b/src/HOL/BNF_GFP.thy	Mon Jan 20 19:05:25 2014 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4  header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
     2.5  
     2.6  theory BNF_GFP
     2.7 -imports BNF_FP_Base List_Prefix
     2.8 +imports BNF_FP_Base List_Prefix String
     2.9  keywords
    2.10    "codatatype" :: thy_decl and
    2.11    "primcorecursive" :: thy_goal and
     3.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:59:53 2014 +0100
     3.2 +++ b/src/HOL/Main.thy	Mon Jan 20 19:05:25 2014 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  header {* Main HOL *}
     3.5  
     3.6  theory Main
     3.7 -imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
     3.8 +imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_LFP BNF_GFP
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 18:59:53 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 19:05:25 2014 +0100
     4.3 @@ -1447,17 +1447,6 @@
     4.4             (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
     4.5             (unfoldN, unfold_thmss, K coiter_attrs)]
     4.6            |> massage_multi_notes;
     4.7 -
     4.8 -        fun is_codatatype (Type (s, _)) =
     4.9 -            (case fp_sugar_of lthy s of SOME {fp = Greatest_FP, ...} => true | _ => false)
    4.10 -          | is_codatatype _ = false;
    4.11 -
    4.12 -        val nitpick_supported = forall (is_codatatype o T_of_bnf) nested_bnfs;
    4.13 -
    4.14 -        fun register_nitpick fpT ({ctrs, casex, ...} : ctr_sugar) =
    4.15 -          Nitpick_HOL.register_codatatype fpT (fst (dest_Const casex))
    4.16 -            (map (dest_Const o mk_ctr As) ctrs)
    4.17 -          |> Generic_Target.theory_declaration;
    4.18        in
    4.19          lthy
    4.20          |> Local_Theory.notes (common_notes @ notes) |> snd
    4.21 @@ -1465,7 +1454,6 @@
    4.22            ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
    4.23            (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
    4.24            (transpose [sel_unfold_thmsss, sel_corec_thmsss])
    4.25 -        |> nitpick_supported ? fold2 register_nitpick fpTs ctr_sugars
    4.26        end;
    4.27  
    4.28      val lthy'' = lthy'