--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 20 13:07:47 2017 +0200
@@ -18,9 +18,7 @@
and transform the heap, or fail\<close>
datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
-lemma [code, code del]:
- "(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
- ..
+declare [[code drop: "Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term"]]
primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
[code del]: "execute (Heap f) = f"
--- a/src/HOL/Library/Code_Binary_Nat.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy Tue Jun 20 13:07:47 2017 +0200
@@ -43,8 +43,7 @@
context
begin
-lemma [code, code del]:
- "(plus :: nat \<Rightarrow> _) = plus" ..
+declare [[code drop: "plus :: nat \<Rightarrow> _"]]
lemma plus_nat_code [code]:
"nat_of_num k + nat_of_num l = nat_of_num (k + l)"
@@ -83,8 +82,7 @@
apply (simp_all add: sub_non_negative [symmetric, where ?'a = int])
done
-lemma [code, code del]:
- "(minus :: nat \<Rightarrow> _) = minus" ..
+declare [[code drop: "minus :: nat \<Rightarrow> _"]]
lemma minus_nat_code [code]:
"nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
@@ -92,8 +90,7 @@
"0 - n = (0::nat)"
by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
-lemma [code, code del]:
- "(times :: nat \<Rightarrow> _) = times" ..
+declare [[code drop: "times :: nat \<Rightarrow> _"]]
lemma times_nat_code [code]:
"nat_of_num k * nat_of_num l = nat_of_num (k * l)"
@@ -101,8 +98,7 @@
"0 * n = (0::nat)"
by (simp_all add: nat_of_num_numeral)
-lemma [code, code del]:
- "(HOL.equal :: nat \<Rightarrow> _) = HOL.equal" ..
+declare [[code drop: "HOL.equal :: nat \<Rightarrow> _"]]
lemma equal_nat_code [code]:
"HOL.equal 0 (0::nat) \<longleftrightarrow> True"
@@ -115,8 +111,7 @@
"HOL.equal (n::nat) n \<longleftrightarrow> True"
by (rule equal_refl)
-lemma [code, code del]:
- "(less_eq :: nat \<Rightarrow> _) = less_eq" ..
+declare [[code drop: "less_eq :: nat \<Rightarrow> _"]]
lemma less_eq_nat_code [code]:
"0 \<le> (n::nat) \<longleftrightarrow> True"
@@ -124,8 +119,7 @@
"nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l"
by (simp_all add: nat_of_num_numeral)
-lemma [code, code del]:
- "(less :: nat \<Rightarrow> _) = less" ..
+declare [[code drop: "less :: nat \<Rightarrow> _"]]
lemma less_nat_code [code]:
"(m::nat) < 0 \<longleftrightarrow> False"
@@ -133,8 +127,7 @@
"nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
by (simp_all add: nat_of_num_numeral)
-lemma [code, code del]:
- "Divides.divmod_nat = Divides.divmod_nat" ..
+declare [[code drop: Divides.divmod_nat]]
lemma divmod_nat_code [code]:
"Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
@@ -147,8 +140,7 @@
subsection \<open>Conversions\<close>
-lemma [code, code del]:
- "of_nat = of_nat" ..
+declare [[code drop: of_nat]]
lemma of_nat_code [code]:
"of_nat 0 = 0"
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Jun 20 13:07:47 2017 +0200
@@ -194,23 +194,12 @@
lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
-lemma [code, code del]: "(HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool) = (HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool)"
- ..
-
-lemma [code, code del]: "(plus :: real \<Rightarrow> real \<Rightarrow> real) = plus"
- ..
-
-lemma [code, code del]: "(uminus :: real \<Rightarrow> real) = uminus"
- ..
-
-lemma [code, code del]: "(minus :: real \<Rightarrow> real \<Rightarrow> real) = minus"
- ..
-
-lemma [code, code del]: "(times :: real \<Rightarrow> real \<Rightarrow> real) = times"
- ..
-
-lemma [code, code del]: "(divide :: real \<Rightarrow> real \<Rightarrow> real) = divide"
- ..
+declare [[code drop: "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
+ "plus :: real \<Rightarrow> real \<Rightarrow> real"
+ "uminus :: real \<Rightarrow> real"
+ "minus :: real \<Rightarrow> real \<Rightarrow> real"
+ "times :: real \<Rightarrow> real \<Rightarrow> real"
+ "divide :: real \<Rightarrow> real \<Rightarrow> real"]]
lemma [code]: "inverse r = 1 / r" for r :: real
by (fact inverse_eq_divide)
--- a/src/HOL/Library/DAList_Multiset.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Tue Jun 20 13:07:47 2017 +0200
@@ -10,42 +10,13 @@
text \<open>Delete prexisting code equations\<close>
-lemma [code, code del]: "{#} = {#}" ..
-
-lemma [code, code del]: "Multiset.is_empty = Multiset.is_empty" ..
-
-lemma [code, code del]: "add_mset = add_mset" ..
-
-lemma [code, code del]: "plus = (plus :: 'a multiset \<Rightarrow> _)" ..
-
-lemma [code, code del]: "minus = (minus :: 'a multiset \<Rightarrow> _)" ..
-
-lemma [code, code del]: "inf_subset_mset = (inf_subset_mset :: 'a multiset \<Rightarrow> _)" ..
-
-lemma [code, code del]: "sup_subset_mset = (sup_subset_mset :: 'a multiset \<Rightarrow> _)" ..
-
-lemma [code, code del]: "image_mset = image_mset" ..
-
-lemma [code, code del]: "filter_mset = filter_mset" ..
-
-lemma [code, code del]: "count = count" ..
-
-lemma [code, code del]: "size = (size :: _ multiset \<Rightarrow> nat)" ..
-
-lemma [code, code del]: "sum_mset = sum_mset" ..
-
-lemma [code, code del]: "prod_mset = prod_mset" ..
-
-lemma [code, code del]: "set_mset = set_mset" ..
-
-lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
-
-lemma [code, code del]: "subset_mset = subset_mset" ..
-
-lemma [code, code del]: "subseteq_mset = subseteq_mset" ..
-
-lemma [code, code del]: "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset" ..
-
+declare [[code drop: "{#}" Multiset.is_empty add_mset
+ "plus :: 'a multiset \<Rightarrow> _" "minus :: 'a multiset \<Rightarrow> _"
+ inf_subset_mset sup_subset_mset image_mset filter_mset count
+ "size :: _ multiset \<Rightarrow> nat" sum_mset prod_mset
+ set_mset sorted_list_of_multiset subset_mset subseteq_mset
+ equal_multiset_inst.equal_multiset]]
+
text \<open>Raw operations on lists\<close>
--- a/src/HOL/Library/RBT_Set.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Library/RBT_Set.thy Tue Jun 20 13:07:47 2017 +0200
@@ -27,123 +27,17 @@
section \<open>Deletion of already existing code equations\<close>
-lemma [code, code del]:
- "Set.empty = Set.empty" ..
-
-lemma [code, code del]:
- "Set.is_empty = Set.is_empty" ..
-
-lemma [code, code del]:
- "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..
-
-lemma [code, code del]:
- "Set.member = Set.member" ..
-
-lemma [code, code del]:
- "Set.insert = Set.insert" ..
-
-lemma [code, code del]:
- "Set.remove = Set.remove" ..
-
-lemma [code, code del]:
- "UNIV = UNIV" ..
-
-lemma [code, code del]:
- "Set.filter = Set.filter" ..
-
-lemma [code, code del]:
- "image = image" ..
-
-lemma [code, code del]:
- "Set.subset_eq = Set.subset_eq" ..
-
-lemma [code, code del]:
- "Ball = Ball" ..
-
-lemma [code, code del]:
- "Bex = Bex" ..
-
-lemma [code, code del]:
- "can_select = can_select" ..
-
-lemma [code, code del]:
- "Set.union = Set.union" ..
-
-lemma [code, code del]:
- "minus_set_inst.minus_set = minus_set_inst.minus_set" ..
-
-lemma [code, code del]:
- "Set.inter = Set.inter" ..
-
-lemma [code, code del]:
- "card = card" ..
-
-lemma [code, code del]:
- "the_elem = the_elem" ..
-
-lemma [code, code del]:
- "Pow = Pow" ..
+declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set
+ Set.member Set.insert Set.remove UNIV Set.filter image
+ Set.subset_eq Ball Bex can_select Set.union minus_set_inst.minus_set Set.inter
+ card the_elem Pow sum prod Product_Type.product Id_on
+ Image trancl relcomp wf Min Inf_fin Max Sup_fin
+ "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"
+ sorted_list_of_set List.map_project List.Bleast]]
-lemma [code, code del]:
- "sum = sum" ..
-
-lemma [code, code del]:
- "prod = prod" ..
-
-lemma [code, code del]:
- "Product_Type.product = Product_Type.product" ..
-
-lemma [code, code del]:
- "Id_on = Id_on" ..
-
-lemma [code, code del]:
- "Image = Image" ..
-
-lemma [code, code del]:
- "trancl = trancl" ..
-
-lemma [code, code del]:
- "relcomp = relcomp" ..
-
-lemma [code, code del]:
- "wf = wf" ..
-
-lemma [code, code del]:
- "Min = Min" ..
-
-lemma [code, code del]:
- "Inf_fin = Inf_fin" ..
-
-lemma [code, code del]:
- "INFIMUM = INFIMUM" ..
-
-lemma [code, code del]:
- "Max = Max" ..
-
-lemma [code, code del]:
- "Sup_fin = Sup_fin" ..
-
-lemma [code, code del]:
- "SUPREMUM = SUPREMUM" ..
-
-lemma [code, code del]:
- "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
-
-lemma [code, code del]:
- "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..
-
-lemma [code, code del]:
- "sorted_list_of_set = sorted_list_of_set" ..
-
-lemma [code, code del]:
- "List.map_project = List.map_project" ..
-
-lemma [code, code del]:
- "List.Bleast = List.Bleast" ..
section \<open>Lemmas\<close>
-
subsection \<open>Auxiliary lemmas\<close>
lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
--- a/src/HOL/Quickcheck_Narrowing.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Tue Jun 20 13:07:47 2017 +0200
@@ -260,8 +260,7 @@
end
-lemma [code, code del]: "partial_term_of (ty :: int itself) t \<equiv> undefined"
- by (rule partial_term_of_anything)+
+declare [[code drop: "partial_term_of :: int itself \<Rightarrow> _"]]
lemma [code]:
"partial_term_of (ty :: int itself) (Narrowing_variable p t) \<equiv>
@@ -283,8 +282,7 @@
end
-lemma [code, code del]: "partial_term_of (ty :: integer itself) t \<equiv> undefined"
- by (rule partial_term_of_anything)+
+declare [[code drop: "partial_term_of :: integer itself \<Rightarrow> _"]]
lemma [code]:
"partial_term_of (ty :: integer itself) (Narrowing_variable p t) \<equiv>
--- a/src/HOL/Unix/Nested_Environment.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy Tue Jun 20 13:07:47 2017 +0200
@@ -522,9 +522,6 @@
subsection \<open>Code generation\<close>
-lemma [code, code del]:
- "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
-
lemma equal_env_code [code]:
fixes x y :: "'a::equal"
and f g :: "'c::{equal, finite} \<Rightarrow> ('b::equal, 'a, 'c) env option"