# HG changeset patch
# User haftmann
# Date 1497956867 -7200
# Node ID 5e60c2d0a1f156a0d0f006084f1278f7d55f60fe
# Parent  9225370db5f035b22715b24bae2b8d2bce850c27
avoid ancient [code, code del] antipattern

diff -r 9225370db5f0 -r 5e60c2d0a1f1 src/HOL/Imperative_HOL/Heap_Monad.thy
--- 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"
diff -r 9225370db5f0 -r 5e60c2d0a1f1 src/HOL/Library/Code_Binary_Nat.thy
--- 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"
diff -r 9225370db5f0 -r 5e60c2d0a1f1 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- 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)
diff -r 9225370db5f0 -r 5e60c2d0a1f1 src/HOL/Library/DAList_Multiset.thy
--- 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>
 
diff -r 9225370db5f0 -r 5e60c2d0a1f1 src/HOL/Library/RBT_Set.thy
--- 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"
diff -r 9225370db5f0 -r 5e60c2d0a1f1 src/HOL/Quickcheck_Narrowing.thy
--- 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>
diff -r 9225370db5f0 -r 5e60c2d0a1f1 src/HOL/Unix/Nested_Environment.thy
--- 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"