disable datatype 'plugins' for internal types
authorblanchet
Sun Sep 14 22:59:30 2014 +0200 (2014-09-14)
changeset 583347553a1bcecb7
parent 58333 ec949d7206bb
child 58335 a5a3b576fcfb
disable datatype 'plugins' for internal types
src/HOL/Code_Evaluation.thy
src/HOL/Enum.thy
src/HOL/Extraction.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Nitpick.thy
src/HOL/Predicate.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Sat Sep 13 18:08:45 2014 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Sun Sep 14 22:59:30 2014 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  subsubsection {* Terms and class @{text term_of} *}
     1.6  
     1.7 -datatype "term" = dummy_term
     1.8 +datatype (plugins only: code) "term" = dummy_term
     1.9  
    1.10  definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    1.11    "Const _ _ = dummy_term"
    1.12 @@ -113,7 +113,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
    1.17 +declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
    1.18    "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
    1.19    "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
    1.20  
     2.1 --- a/src/HOL/Enum.thy	Sat Sep 13 18:08:45 2014 +0200
     2.2 +++ b/src/HOL/Enum.thy	Sun Sep 14 22:59:30 2014 +0200
     2.3 @@ -491,9 +491,9 @@
     2.4  
     2.5  subsection {* Small finite types *}
     2.6  
     2.7 -text {* We define small finite types for the use in Quickcheck *}
     2.8 +text {* We define small finite types for use in Quickcheck *}
     2.9  
    2.10 -datatype finite_1 = a\<^sub>1
    2.11 +datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
    2.12  
    2.13  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.14  
    2.15 @@ -595,7 +595,7 @@
    2.16  declare [[simproc del: finite_1_eq]]
    2.17  hide_const (open) a\<^sub>1
    2.18  
    2.19 -datatype finite_2 = a\<^sub>1 | a\<^sub>2
    2.20 +datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
    2.21  
    2.22  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.23  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.24 @@ -701,7 +701,7 @@
    2.25  
    2.26  hide_const (open) a\<^sub>1 a\<^sub>2
    2.27  
    2.28 -datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    2.29 +datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    2.30  
    2.31  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.32  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.33 @@ -825,7 +825,7 @@
    2.34  
    2.35  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    2.36  
    2.37 -datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    2.38 +datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    2.39  
    2.40  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.41  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.42 @@ -926,8 +926,7 @@
    2.43  
    2.44  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    2.45  
    2.46 -
    2.47 -datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    2.48 +datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    2.49  
    2.50  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.51  notation (output) a\<^sub>2  ("a\<^sub>2")
     3.1 --- a/src/HOL/Extraction.thy	Sat Sep 13 18:08:45 2014 +0200
     3.2 +++ b/src/HOL/Extraction.thy	Sun Sep 14 22:59:30 2014 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     3.5    induct_true_def induct_false_def
     3.6  
     3.7 -datatype sumbool = Left | Right
     3.8 +datatype (plugins only: code) sumbool = Left | Right
     3.9  
    3.10  subsection {* Type of extracted program *}
    3.11  
     4.1 --- a/src/HOL/Lazy_Sequence.thy	Sat Sep 13 18:08:45 2014 +0200
     4.2 +++ b/src/HOL/Lazy_Sequence.thy	Sun Sep 14 22:59:30 2014 +0200
     4.3 @@ -1,4 +1,3 @@
     4.4 -
     4.5  (* Author: Lukas Bulwahn, TU Muenchen *)
     4.6  
     4.7  header {* Lazy sequences *}
     4.8 @@ -9,7 +8,7 @@
     4.9  
    4.10  subsection {* Type of lazy sequences *}
    4.11  
    4.12 -datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
    4.13 +datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
    4.14  
    4.15  primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
    4.16  where
    4.17 @@ -27,11 +26,6 @@
    4.18    "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
    4.19    by (auto intro: lazy_sequence_eqI)
    4.20  
    4.21 -lemma size_lazy_sequence_eq [code]:
    4.22 -  "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
    4.23 -  "size xq = Suc (length (list_of_lazy_sequence xq))"
    4.24 -  by (cases xq, simp)+
    4.25 -
    4.26  lemma case_lazy_sequence [simp]:
    4.27    "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    4.28    by (cases xq) auto
    4.29 @@ -72,12 +66,6 @@
    4.30    case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
    4.31    by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
    4.32  
    4.33 -lemma size_lazy_sequence_code [code]:
    4.34 -  "size_lazy_sequence s xq = (case yield xq of
    4.35 -    None \<Rightarrow> 1
    4.36 -  | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
    4.37 -  by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
    4.38 -
    4.39  lemma equal_lazy_sequence_code [code]:
    4.40    "HOL.equal xq yq = (case (yield xq, yield yq) of
    4.41      (None, None) \<Rightarrow> True
     5.1 --- a/src/HOL/Nitpick.thy	Sat Sep 13 18:08:45 2014 +0200
     5.2 +++ b/src/HOL/Nitpick.thy	Sun Sep 14 22:59:30 2014 +0200
     5.3 @@ -14,9 +14,9 @@
     5.4    "nitpick_params" :: thy_decl
     5.5  begin
     5.6  
     5.7 -datatype (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
     5.8 -datatype (dead 'a, dead 'b) pair_box = PairBox 'a 'b
     5.9 -datatype (dead 'a) word = Word "'a set"
    5.10 +datatype (plugins only: code) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
    5.11 +datatype (plugins only: code) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
    5.12 +datatype (plugins only: code) (dead 'a) word = Word "'a set"
    5.13  
    5.14  typedecl bisim_iterator
    5.15  typedecl unsigned_bit
     6.1 --- a/src/HOL/Predicate.thy	Sat Sep 13 18:08:45 2014 +0200
     6.2 +++ b/src/HOL/Predicate.thy	Sun Sep 14 22:59:30 2014 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  
     6.5  subsection {* The type of predicate enumerations (a monad) *}
     6.6  
     6.7 -datatype 'a pred = Pred "'a \<Rightarrow> bool"
     6.8 +datatype (plugins only: code) (dead 'a) pred = Pred "'a \<Rightarrow> bool"
     6.9  
    6.10  primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
    6.11    eval_pred: "eval (Pred f) = f"
    6.12 @@ -402,7 +402,10 @@
    6.13  
    6.14  subsection {* Implementation *}
    6.15  
    6.16 -datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
    6.17 +datatype (plugins only: code) (dead 'a) seq =
    6.18 +  Empty
    6.19 +| Insert "'a" "'a pred"
    6.20 +| Join "'a pred" "'a seq"
    6.21  
    6.22  primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
    6.23    "pred_of_seq Empty = \<bottom>"
    6.24 @@ -494,12 +497,6 @@
    6.25      by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
    6.26  qed
    6.27  
    6.28 -lemma [code]:
    6.29 -  "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
    6.30 -
    6.31 -lemma [code]:
    6.32 -  "size_pred f P = 0" by (cases P) simp
    6.33 -
    6.34  primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
    6.35    "contained Empty Q \<longleftrightarrow> True"
    6.36  | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
     7.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sat Sep 13 18:08:45 2014 +0200
     7.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Sep 14 22:59:30 2014 +0200
     7.3 @@ -574,8 +574,8 @@
     7.4  where
     7.5    "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
     7.6  
     7.7 -datatype (dead 'a) unknown = Unknown | Known 'a
     7.8 -datatype (dead 'a) three_valued = Unknown_value | Value 'a | No_value
     7.9 +datatype (plugins only: code) (dead 'a) unknown = Unknown | Known 'a
    7.10 +datatype (plugins only: code) (dead 'a) three_valued = Unknown_value | Value 'a | No_value
    7.11  
    7.12  type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
    7.13  
     8.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sat Sep 13 18:08:45 2014 +0200
     8.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Sep 14 22:59:30 2014 +0200
     8.3 @@ -26,14 +26,14 @@
     8.4  
     8.5  subsubsection {* Narrowing's deep representation of types and terms *}
     8.6  
     8.7 -datatype narrowing_type =
     8.8 +datatype (plugins only: code) narrowing_type =
     8.9    Narrowing_sum_of_products "narrowing_type list list"
    8.10  
    8.11 -datatype narrowing_term =
    8.12 +datatype (plugins only: code) narrowing_term =
    8.13    Narrowing_variable "integer list" narrowing_type
    8.14  | Narrowing_constructor integer "narrowing_term list"
    8.15  
    8.16 -datatype (dead 'a) narrowing_cons =
    8.17 +datatype (plugins only: code) (dead 'a) narrowing_cons =
    8.18    Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
    8.19  
    8.20  primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
    8.21 @@ -127,7 +127,10 @@
    8.22  class narrowing =
    8.23    fixes narrowing :: "integer => 'a narrowing_cons"
    8.24  
    8.25 -datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    8.26 +datatype (plugins only: code) property =
    8.27 +  Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
    8.28 +| Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
    8.29 +| Property bool
    8.30  
    8.31  (* FIXME: hard-wired maximal depth of 100 here *)
    8.32  definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
    8.33 @@ -155,7 +158,9 @@
    8.34  
    8.35  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
    8.36  
    8.37 -datatype (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
    8.38 +datatype (plugins only: code quickcheck_narrowing) (dead 'a, dead 'b) ffun =
    8.39 +  Constant 'b
    8.40 +| Update 'a 'b "('a, 'b) ffun"
    8.41  
    8.42  primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
    8.43  where
    8.44 @@ -165,7 +170,7 @@
    8.45  hide_type (open) ffun
    8.46  hide_const (open) Constant Update eval_ffun
    8.47  
    8.48 -datatype (dead 'b) cfun = Constant 'b
    8.49 +datatype (plugins only: code quickcheck_narrowing) (dead 'b) cfun = Constant 'b
    8.50  
    8.51  primrec eval_cfun :: "'b cfun => 'a => 'b"
    8.52  where