--- a/src/HOL/Library/Cardinality.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy Fri Sep 04 19:22:13 2015 +0200
@@ -410,7 +410,10 @@
possibly slow dictionary constructions.
\<close>
-definition card_UNIV' :: "'a card_UNIV"
+context
+begin
+
+qualified definition card_UNIV' :: "'a card_UNIV"
where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
lemma CARD_code [code_unfold]:
@@ -421,7 +424,7 @@
"card_UNIV' = card_UNIV"
by(simp add: card_UNIV card_UNIV'_def)
-hide_const (open) card_UNIV'
+end
lemma card_Compl:
"finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
@@ -430,7 +433,7 @@
context fixes xs :: "'a :: finite_UNIV list"
begin
-definition finite' :: "'a set \<Rightarrow> bool"
+qualified definition finite' :: "'a set \<Rightarrow> bool"
where [simp, code del, code_abbrev]: "finite' = finite"
lemma finite'_code [code]:
@@ -443,7 +446,7 @@
context fixes xs :: "'a :: card_UNIV list"
begin
-definition card' :: "'a set \<Rightarrow> nat"
+qualified definition card' :: "'a set \<Rightarrow> nat"
where [simp, code del, code_abbrev]: "card' = card"
lemma card'_code [code]:
@@ -452,7 +455,7 @@
by(simp_all add: List.card_set card_Compl card_UNIV)
-definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
lemma subset'_code [code]:
@@ -462,7 +465,7 @@
by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
(metis finite_compl finite_set rev_finite_subset)
-definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where [simp, code del, code_abbrev]: "eq_set = op ="
lemma eq_set_code [code]:
@@ -538,7 +541,4 @@
by eval
end
-hide_const (open) card' finite' subset' eq_set
-
end
-
--- a/src/HOL/Library/Code_Binary_Nat.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy Fri Sep 04 19:22:13 2015 +0200
@@ -40,6 +40,9 @@
subsection \<open>Basic arithmetic\<close>
+context
+begin
+
lemma [code, code del]:
"(plus :: nat \<Rightarrow> _) = plus" ..
@@ -51,7 +54,7 @@
text \<open>Bounded subtraction needs some auxiliary\<close>
-definition dup :: "nat \<Rightarrow> nat" where
+qualified definition dup :: "nat \<Rightarrow> nat" where
"dup n = n + n"
lemma dup_code [code]:
@@ -59,7 +62,7 @@
"dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
by (simp_all add: dup_def numeral_Bit0)
-definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
+qualified definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
"sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
lemma sub_code [code]:
@@ -139,6 +142,8 @@
"divmod_nat 0 n = (0, 0)"
by (simp_all add: prod_eq_iff nat_of_num_numeral)
+end
+
subsection \<open>Conversions\<close>
@@ -155,7 +160,4 @@
code_module Code_Binary_Nat \<rightharpoonup>
(SML) Arith and (OCaml) Arith and (Haskell) Arith
-hide_const (open) dup sub
-
end
-
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Fri Sep 04 19:22:13 2015 +0200
@@ -85,20 +85,23 @@
and (OCaml) "Pervasives.sqrt"
declare sqrt_def[code del]
-definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
+context
+begin
+
+qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
unfolding real_exp_def ..
+end
+
code_printing
- constant real_exp \<rightharpoonup>
+ constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
(SML) "Math.exp"
and (OCaml) "Pervasives.exp"
-declare real_exp_def[code del]
+declare Code_Real_Approx_By_Float.real_exp_def[code del]
declare exp_def[code del]
-hide_const (open) real_exp
-
code_printing
constant ln \<rightharpoonup>
(SML) "Math.ln"
@@ -149,7 +152,10 @@
(SML) "Real.fromInt"
and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
-definition real_of_int :: "int \<Rightarrow> real" where
+context
+begin
+
+qualified definition real_of_int :: "int \<Rightarrow> real" where
[code_abbrev]: "real_of_int = of_int"
lemma [code]:
@@ -172,7 +178,7 @@
"- numeral k \<equiv> (of_rat (- numeral k) :: real)"
by simp
-hide_const (open) real_of_int
+end
code_printing
constant Ratreal \<rightharpoonup> (SML)
--- a/src/HOL/Library/Countable.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Countable.thy Fri Sep 04 19:22:13 2015 +0200
@@ -66,15 +66,17 @@
subsection \<open>Automatically proving countability of old-style datatypes\<close>
-inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
+context
+begin
+
+qualified inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
undefined: "finite_item undefined"
| In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)"
| In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)"
| Leaf: "finite_item (Old_Datatype.Leaf a)"
| Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)"
-function
- nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
+qualified function nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
where
"nth_item 0 = undefined"
| "nth_item (Suc n) =
@@ -97,7 +99,7 @@
lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)"
unfolding sum_encode_def by simp
-termination
+qualified termination
by (relation "measure id")
(auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
@@ -193,7 +195,7 @@
end)
\<close>
-hide_const (open) finite_item nth_item
+end
subsection \<open>Automatically proving countability of datatypes\<close>
--- a/src/HOL/Library/DAList_Multiset.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Fri Sep 04 19:22:13 2015 +0200
@@ -275,10 +275,13 @@
"fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"
| "fold_impl fn e [] = e"
-definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
+context
+begin
+
+qualified definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
where "fold f e al = fold_impl f e (DAList.impl_of al)"
-hide_const (open) fold
+end
context comp_fun_commute
begin
@@ -348,7 +351,10 @@
end
-lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
+context
+begin
+
+private lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
by auto
lemma image_mset_Bag [code]:
@@ -368,7 +374,7 @@
qed
qed
-hide_const single_alist_entry
+end
(* we cannot use (\<lambda>a n. op + (a * n)) for folding, since * is not defined
in comm_monoid_add *)
--- a/src/HOL/Library/Debug.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Debug.thy Fri Sep 04 19:22:13 2015 +0200
@@ -6,37 +6,40 @@
imports Main
begin
-definition trace :: "String.literal \<Rightarrow> unit" where
+context
+begin
+
+qualified definition trace :: "String.literal \<Rightarrow> unit" where
[simp]: "trace s = ()"
-definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
+qualified definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
[simp]: "tracing s = id"
lemma [code]:
"tracing s = (let u = trace s in id)"
by simp
-definition flush :: "'a \<Rightarrow> unit" where
+qualified definition flush :: "'a \<Rightarrow> unit" where
[simp]: "flush x = ()"
-definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
[simp]: "flushing x = id"
lemma [code, code_unfold]:
"flushing x = (let u = flush x in id)"
by simp
-definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+qualified definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
[simp]: "timing s f x = f x"
+end
+
code_printing
- constant trace \<rightharpoonup> (Eval) "Output.tracing"
-| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
-| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
+ constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
+| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
+| constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
code_reserved Eval Output Timing
-hide_const (open) trace tracing flush flushing timing
-
end
--- a/src/HOL/Library/Discrete.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Discrete.thy Fri Sep 04 19:22:13 2015 +0200
@@ -8,7 +8,10 @@
subsection \<open>Discrete logarithm\<close>
-fun log :: "nat \<Rightarrow> nat"
+context
+begin
+
+qualified fun log :: "nat \<Rightarrow> nat"
where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
lemma log_zero [simp]: "log 0 = 0"
@@ -67,7 +70,7 @@
subsection \<open>Discrete square root\<close>
-definition sqrt :: "nat \<Rightarrow> nat"
+qualified definition sqrt :: "nat \<Rightarrow> nat"
where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
lemma sqrt_aux:
@@ -173,7 +176,6 @@
lemma sqrt_le: "sqrt n \<le> n"
using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
-hide_const (open) log sqrt
-
end
+end
\ No newline at end of file
--- a/src/HOL/Library/Dlist.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Dlist.thy Fri Sep 04 19:22:13 2015 +0200
@@ -46,61 +46,71 @@
text \<open>Fundamental operations:\<close>
-definition empty :: "'a dlist" where
+context
+begin
+
+qualified definition empty :: "'a dlist" where
"empty = Dlist []"
-definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
"insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
-definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
"remove x dxs = Dlist (remove1 x (list_of_dlist dxs))"
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
+qualified definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
"map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
"filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
+end
+
text \<open>Derived operations:\<close>
-definition null :: "'a dlist \<Rightarrow> bool" where
+context
+begin
+
+qualified definition null :: "'a dlist \<Rightarrow> bool" where
"null dxs = List.null (list_of_dlist dxs)"
-definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
+qualified definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
"member dxs = List.member (list_of_dlist dxs)"
-definition length :: "'a dlist \<Rightarrow> nat" where
+qualified definition length :: "'a dlist \<Rightarrow> nat" where
"length dxs = List.length (list_of_dlist dxs)"
-definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
"fold f dxs = List.fold f (list_of_dlist dxs)"
-definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
"foldr f dxs = List.foldr f (list_of_dlist dxs)"
+end
+
subsection \<open>Executable version obeying invariant\<close>
lemma list_of_dlist_empty [simp, code abstract]:
- "list_of_dlist empty = []"
- by (simp add: empty_def)
+ "list_of_dlist Dlist.empty = []"
+ by (simp add: Dlist.empty_def)
lemma list_of_dlist_insert [simp, code abstract]:
- "list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)"
- by (simp add: insert_def)
+ "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
+ by (simp add: Dlist.insert_def)
lemma list_of_dlist_remove [simp, code abstract]:
- "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
- by (simp add: remove_def)
+ "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
+ by (simp add: Dlist.remove_def)
lemma list_of_dlist_map [simp, code abstract]:
- "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
- by (simp add: map_def)
+ "list_of_dlist (Dlist.map f dxs) = remdups (List.map f (list_of_dlist dxs))"
+ by (simp add: Dlist.map_def)
lemma list_of_dlist_filter [simp, code abstract]:
- "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
- by (simp add: filter_def)
+ "list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)"
+ by (simp add: Dlist.filter_def)
text \<open>Explicit executable conversion\<close>
@@ -134,28 +144,29 @@
subsection \<open>Induction principle and case distinction\<close>
lemma dlist_induct [case_names empty insert, induct type: dlist]:
- assumes empty: "P empty"
- assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)"
+ assumes empty: "P Dlist.empty"
+ assumes insrt: "\<And>x dxs. \<not> Dlist.member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (Dlist.insert x dxs)"
shows "P dxs"
proof (cases dxs)
case (Abs_dlist xs)
- then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id)
+ then have "distinct xs" and dxs: "dxs = Dlist xs"
+ by (simp_all add: Dlist_def distinct_remdups_id)
from \<open>distinct xs\<close> have "P (Dlist xs)"
proof (induct xs)
- case Nil from empty show ?case by (simp add: empty_def)
+ case Nil from empty show ?case by (simp add: Dlist.empty_def)
next
case (Cons x xs)
- then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
- by (simp_all add: member_def List.member_def)
- with insrt have "P (insert x (Dlist xs))" .
- with Cons show ?case by (simp add: insert_def distinct_remdups_id)
+ then have "\<not> Dlist.member (Dlist xs) x" and "P (Dlist xs)"
+ by (simp_all add: Dlist.member_def List.member_def)
+ with insrt have "P (Dlist.insert x (Dlist xs))" .
+ with Cons show ?case by (simp add: Dlist.insert_def distinct_remdups_id)
qed
with dxs show "P dxs" by simp
qed
lemma dlist_case [cases type: dlist]:
- obtains (empty) "dxs = empty"
- | (insert) x dys where "\<not> member dys x" and "dxs = insert x dys"
+ obtains (empty) "dxs = Dlist.empty"
+ | (insert) x dys where "\<not> Dlist.member dys x" and "dxs = Dlist.insert x dys"
proof (cases dxs)
case (Abs_dlist xs)
then have dxs: "dxs = Dlist xs" and distinct: "distinct xs"
@@ -163,13 +174,13 @@
show thesis
proof (cases xs)
case Nil with dxs
- have "dxs = empty" by (simp add: empty_def)
+ have "dxs = Dlist.empty" by (simp add: Dlist.empty_def)
with empty show ?thesis .
next
case (Cons x xs)
- with dxs distinct have "\<not> member (Dlist xs) x"
- and "dxs = insert x (Dlist xs)"
- by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
+ with dxs distinct have "\<not> Dlist.member (Dlist xs) x"
+ and "dxs = Dlist.insert x (Dlist xs)"
+ by (simp_all add: Dlist.member_def List.member_def Dlist.insert_def distinct_remdups_id)
with insert show ?thesis .
qed
qed
@@ -178,14 +189,11 @@
subsection \<open>Functorial structure\<close>
functor map: map
- by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
+ by (simp_all add: remdups_map_remdups fun_eq_iff dlist_eq_iff)
subsection \<open>Quickcheck generators\<close>
-quickcheck_generator dlist predicate: distinct constructors: empty, insert
-
-
-hide_const (open) member fold foldr empty insert remove map filter null member length fold
+quickcheck_generator dlist predicate: distinct constructors: Dlist.empty, Dlist.insert
end
--- a/src/HOL/Library/IArray.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/IArray.thy Fri Sep 04 19:22:13 2015 +0200
@@ -13,36 +13,35 @@
lists first. Arrays could be converted back into lists for printing if they
were wrapped up in an additional constructor.\<close>
+context
+begin
+
datatype 'a iarray = IArray "'a list"
-primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
+qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
"list_of (IArray xs) = xs"
-hide_const (open) list_of
-definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
+qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
[simp]: "of_fun f n = IArray (map f [0..<n])"
-hide_const (open) of_fun
-definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
[simp]: "as !! n = IArray.list_of as ! n"
-hide_const (open) sub
-definition length :: "'a iarray \<Rightarrow> nat" where
+qualified definition length :: "'a iarray \<Rightarrow> nat" where
[simp]: "length as = List.length (IArray.list_of as)"
-hide_const (open) length
-fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
"all p (IArray as) = (ALL a : set as. p a)"
-hide_const (open) all
-fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
"exists p (IArray as) = (EX a : set as. p a)"
-hide_const (open) exists
lemma list_of_code [code]:
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
by (cases as) (simp add: map_nth)
+end
+
subsection "Code Generation"
@@ -86,10 +85,13 @@
"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
by (cases as, cases bs) (simp add: equal)
-primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
+context
+begin
+
+qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
"tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
-hide_const (open) tabulate
+end
lemma [code]:
"IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
@@ -98,10 +100,13 @@
code_printing
constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
-primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
+context
+begin
+
+qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
[code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
-hide_const (open) sub'
+end
lemma [code]:
"IArray.sub' (IArray as, n) = as ! nat_of_integer n"
@@ -114,10 +119,13 @@
code_printing
constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
-definition length' :: "'a iarray \<Rightarrow> integer" where
+context
+begin
+
+qualified definition length' :: "'a iarray \<Rightarrow> integer" where
[code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
-hide_const (open) length'
+end
lemma [code]:
"IArray.length' (IArray as) = integer_of_nat (List.length as)"
--- a/src/HOL/Library/While_Combinator.thy Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy Fri Sep 04 19:22:13 2015 +0200
@@ -314,10 +314,10 @@
and x :: 'a
begin
-fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
-fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
+qualified fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
where "rtrancl_while_step (ws, Z) =
(let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
in (new @ tl ws, set new \<union> Z))"
@@ -325,12 +325,12 @@
definition rtrancl_while :: "('a list * 'a set) option"
where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
-fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
where "rtrancl_while_invariant (ws, Z) =
(x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
-lemma rtrancl_while_invariant:
+qualified lemma rtrancl_while_invariant:
assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
shows "rtrancl_while_invariant (rtrancl_while_step st)"
proof (cases st)
@@ -392,7 +392,4 @@
end
-hide_const (open) rtrancl_while_test rtrancl_while_step rtrancl_while_invariant
-hide_fact (open) rtrancl_while_invariant
-
end