--- a/src/HOL/Code_Evaluation.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Sun Sep 14 22:59:30 2014 +0200
@@ -13,7 +13,7 @@
subsubsection {* Terms and class @{text term_of} *}
-datatype "term" = dummy_term
+datatype (plugins only: code) "term" = dummy_term
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
"Const _ _ = dummy_term"
@@ -113,7 +113,7 @@
end
-declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
+declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
"term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
"term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
--- a/src/HOL/Enum.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Enum.thy Sun Sep 14 22:59:30 2014 +0200
@@ -491,9 +491,9 @@
subsection {* Small finite types *}
-text {* We define small finite types for the use in Quickcheck *}
+text {* We define small finite types for use in Quickcheck *}
-datatype finite_1 = a\<^sub>1
+datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -595,7 +595,7 @@
declare [[simproc del: finite_1_eq]]
hide_const (open) a\<^sub>1
-datatype finite_2 = a\<^sub>1 | a\<^sub>2
+datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -701,7 +701,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2
-datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -825,7 +825,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
-datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -926,8 +926,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
-
-datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
--- a/src/HOL/Extraction.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Extraction.thy Sun Sep 14 22:59:30 2014 +0200
@@ -37,7 +37,7 @@
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
induct_true_def induct_false_def
-datatype sumbool = Left | Right
+datatype (plugins only: code) sumbool = Left | Right
subsection {* Type of extracted program *}
--- a/src/HOL/Lazy_Sequence.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy Sun Sep 14 22:59:30 2014 +0200
@@ -1,4 +1,3 @@
-
(* Author: Lukas Bulwahn, TU Muenchen *)
header {* Lazy sequences *}
@@ -9,7 +8,7 @@
subsection {* Type of lazy sequences *}
-datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
+datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
where
@@ -27,11 +26,6 @@
"xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
by (auto intro: lazy_sequence_eqI)
-lemma size_lazy_sequence_eq [code]:
- "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
- "size xq = Suc (length (list_of_lazy_sequence xq))"
- by (cases xq, simp)+
-
lemma case_lazy_sequence [simp]:
"case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
by (cases xq) auto
@@ -72,12 +66,6 @@
case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
-lemma size_lazy_sequence_code [code]:
- "size_lazy_sequence s xq = (case yield xq of
- None \<Rightarrow> 1
- | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
- by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
-
lemma equal_lazy_sequence_code [code]:
"HOL.equal xq yq = (case (yield xq, yield yq) of
(None, None) \<Rightarrow> True
--- a/src/HOL/Nitpick.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Nitpick.thy Sun Sep 14 22:59:30 2014 +0200
@@ -14,9 +14,9 @@
"nitpick_params" :: thy_decl
begin
-datatype (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
-datatype (dead 'a, dead 'b) pair_box = PairBox 'a 'b
-datatype (dead 'a) word = Word "'a set"
+datatype (plugins only: code) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
+datatype (plugins only: code) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
+datatype (plugins only: code) (dead 'a) word = Word "'a set"
typedecl bisim_iterator
typedecl unsigned_bit
--- a/src/HOL/Predicate.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Predicate.thy Sun Sep 14 22:59:30 2014 +0200
@@ -10,7 +10,7 @@
subsection {* The type of predicate enumerations (a monad) *}
-datatype 'a pred = Pred "'a \<Rightarrow> bool"
+datatype (plugins only: code) (dead 'a) pred = Pred "'a \<Rightarrow> bool"
primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
eval_pred: "eval (Pred f) = f"
@@ -402,7 +402,10 @@
subsection {* Implementation *}
-datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
+datatype (plugins only: code) (dead 'a) seq =
+ Empty
+| Insert "'a" "'a pred"
+| Join "'a pred" "'a seq"
primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
"pred_of_seq Empty = \<bottom>"
@@ -494,12 +497,6 @@
by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
qed
-lemma [code]:
- "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
-
-lemma [code]:
- "size_pred f P = 0" by (cases P) simp
-
primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
"contained Empty Q \<longleftrightarrow> True"
| "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
--- a/src/HOL/Quickcheck_Exhaustive.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Sep 14 22:59:30 2014 +0200
@@ -574,8 +574,8 @@
where
"pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
-datatype (dead 'a) unknown = Unknown | Known 'a
-datatype (dead 'a) three_valued = Unknown_value | Value 'a | No_value
+datatype (plugins only: code) (dead 'a) unknown = Unknown | Known 'a
+datatype (plugins only: code) (dead 'a) three_valued = Unknown_value | Value 'a | No_value
type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
--- a/src/HOL/Quickcheck_Narrowing.thy Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Sun Sep 14 22:59:30 2014 +0200
@@ -26,14 +26,14 @@
subsubsection {* Narrowing's deep representation of types and terms *}
-datatype narrowing_type =
+datatype (plugins only: code) narrowing_type =
Narrowing_sum_of_products "narrowing_type list list"
-datatype narrowing_term =
+datatype (plugins only: code) narrowing_term =
Narrowing_variable "integer list" narrowing_type
| Narrowing_constructor integer "narrowing_term list"
-datatype (dead 'a) narrowing_cons =
+datatype (plugins only: code) (dead 'a) narrowing_cons =
Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
@@ -127,7 +127,10 @@
class narrowing =
fixes narrowing :: "integer => 'a narrowing_cons"
-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
+datatype (plugins only: code) 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
(* FIXME: hard-wired maximal depth of 100 here *)
definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
@@ -155,7 +158,9 @@
subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
-datatype (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
+datatype (plugins only: code quickcheck_narrowing) (dead 'a, dead 'b) ffun =
+ Constant 'b
+| Update 'a 'b "('a, 'b) ffun"
primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
where
@@ -165,7 +170,7 @@
hide_type (open) ffun
hide_const (open) Constant Update eval_ffun
-datatype (dead 'b) cfun = Constant 'b
+datatype (plugins only: code quickcheck_narrowing) (dead 'b) cfun = Constant 'b
primrec eval_cfun :: "'b cfun => 'a => 'b"
where