replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
authorbulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231d85a2fdc586c
parent 45230 1b08942bb86f
child 45232 eb56e1774c26
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
src/HOL/Divides.thy
src/HOL/HOL.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Transitive_Closure_Table.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/MicroJava/J/SystemClasses.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Divides.thy	Fri Oct 21 11:17:12 2011 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Oct 21 11:17:14 2011 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4    note that ultimately show thesis by blast
     1.5  qed
     1.6  
     1.7 -lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.8 +lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.9  proof
    1.10    assume "b mod a = 0"
    1.11    with mod_div_equality [of b a] have "b div a * a = b" by simp
     2.1 --- a/src/HOL/HOL.thy	Fri Oct 21 11:17:12 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Oct 21 11:17:14 2011 +0200
     2.3 @@ -1729,7 +1729,7 @@
     2.4    assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
     2.5  begin
     2.6  
     2.7 -lemma equal [code_unfold, code_inline del]: "equal = (op =)"
     2.8 +lemma equal: "equal = (op =)"
     2.9    by (rule ext equal_eq)+
    2.10  
    2.11  lemma equal_refl: "equal x x \<longleftrightarrow> True"
     3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 21 11:17:12 2011 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 21 11:17:14 2011 +0200
     3.3 @@ -495,7 +495,7 @@
     3.4  lemma [code_post]: "raise' (STR s) = raise s"
     3.5  unfolding raise'_def by (simp add: STR_inverse)
     3.6  
     3.7 -lemma raise_raise' [code_inline]:
     3.8 +lemma raise_raise' [code_unfold]:
     3.9    "raise s = raise' (STR s)"
    3.10    unfolding raise'_def by (simp add: STR_inverse)
    3.11  
     4.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Oct 21 11:17:12 2011 +0200
     4.2 +++ b/src/HOL/Library/Executable_Set.thy	Fri Oct 21 11:17:14 2011 +0200
     4.3 @@ -67,7 +67,7 @@
     4.4    "{} = empty"
     4.5    by simp
     4.6  
     4.7 -lemma [code_unfold, code_inline del]:
     4.8 +lemma
     4.9    "empty = Set []"
    4.10    by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
    4.11  
     5.1 --- a/src/HOL/Library/Mapping.thy	Fri Oct 21 11:17:12 2011 +0200
     5.2 +++ b/src/HOL/Library/Mapping.thy	Fri Oct 21 11:17:14 2011 +0200
     5.3 @@ -90,7 +90,7 @@
     5.4  
     5.5  subsection {* Properties *}
     5.6  
     5.7 -lemma keys_is_none_lookup [code_inline]:
     5.8 +lemma keys_is_none_lookup [code_unfold]:
     5.9    "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
    5.10    by (auto simp add: keys_def is_none_def)
    5.11  
     6.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Oct 21 11:17:12 2011 +0200
     6.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Oct 21 11:17:14 2011 +0200
     6.3 @@ -84,7 +84,7 @@
     6.4  
     6.5  definition subtract
     6.6  where
     6.7 -  [code_inline]: "subtract x y = y - x"
     6.8 +  [code_unfold]: "subtract x y = y - x"
     6.9  
    6.10  setup {*
    6.11  let
     7.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 11:17:12 2011 +0200
     7.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 11:17:14 2011 +0200
     7.3 @@ -185,8 +185,6 @@
     7.4      by (auto simp add: rtranclp_eq_rtrancl_path)
     7.5  qed
     7.6  
     7.7 -declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
     7.8 -
     7.9  declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
    7.10  
    7.11  code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
     8.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Fri Oct 21 11:17:12 2011 +0200
     8.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Oct 21 11:17:14 2011 +0200
     8.3 @@ -118,12 +118,12 @@
     8.4  
     8.5  definition undefined_cname :: cname 
     8.6    where [code del]: "undefined_cname = undefined"
     8.7 -declare undefined_cname_def[symmetric, code_inline]
     8.8 +declare undefined_cname_def[symmetric, code_unfold]
     8.9  code_datatype Object Xcpt Cname undefined_cname
    8.10  
    8.11  definition undefined_val :: val
    8.12    where [code del]: "undefined_val = undefined"
    8.13 -declare undefined_val_def[symmetric, code_inline]
    8.14 +declare undefined_val_def[symmetric, code_unfold]
    8.15  code_datatype Unit Null Bool Intg Addr undefined_val
    8.16  
    8.17  definition E where 
     9.1 --- a/src/HOL/MicroJava/J/SystemClasses.thy	Fri Oct 21 11:17:12 2011 +0200
     9.2 +++ b/src/HOL/MicroJava/J/SystemClasses.thy	Fri Oct 21 11:17:14 2011 +0200
     9.3 @@ -13,18 +13,18 @@
     9.4  *}
     9.5  
     9.6  definition ObjectC :: "'c cdecl" where
     9.7 -  [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
     9.8 +  [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
     9.9  
    9.10  definition NullPointerC :: "'c cdecl" where
    9.11 -  [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
    9.12 +  [code_unfold]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
    9.13  
    9.14  definition ClassCastC :: "'c cdecl" where
    9.15 -  [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
    9.16 +  [code_unfold]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
    9.17  
    9.18  definition OutOfMemoryC :: "'c cdecl" where
    9.19 -  [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
    9.20 +  [code_unfold]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
    9.21  
    9.22  definition SystemClasses :: "'c cdecl list" where
    9.23 -  [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
    9.24 +  [code_unfold]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
    9.25  
    9.26  end
    10.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 11:17:12 2011 +0200
    10.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 11:17:14 2011 +0200
    10.3 @@ -97,7 +97,7 @@
    10.4    [inductify]
    10.5    subcls'
    10.6  .
    10.7 -lemma subcls_conv_subcls' [code_inline]:
    10.8 +lemma subcls_conv_subcls' [code_unfold]:
    10.9    "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
   10.10  by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
   10.11  
    11.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 21 11:17:12 2011 +0200
    11.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 21 11:17:14 2011 +0200
    11.3 @@ -125,11 +125,11 @@
    11.4  definition undefined_cname :: cname 
    11.5    where [code del]: "undefined_cname = undefined"
    11.6  code_datatype Object Xcpt Cname undefined_cname
    11.7 -declare undefined_cname_def[symmetric, code_inline]
    11.8 +declare undefined_cname_def[symmetric, code_unfold]
    11.9  
   11.10  definition undefined_val :: val
   11.11    where [code del]: "undefined_val = undefined"
   11.12 -declare undefined_val_def[symmetric, code_inline]
   11.13 +declare undefined_val_def[symmetric, code_unfold]
   11.14  code_datatype Unit Null Bool Intg Addr undefined_val
   11.15  
   11.16  definition
    12.1 --- a/src/HOL/Nat.thy	Fri Oct 21 11:17:12 2011 +0200
    12.2 +++ b/src/HOL/Nat.thy	Fri Oct 21 11:17:14 2011 +0200
    12.3 @@ -1301,7 +1301,7 @@
    12.4  
    12.5  end
    12.6  
    12.7 -declare of_nat_code [code, code_unfold, code_inline del]
    12.8 +declare of_nat_code [code]
    12.9  
   12.10  text{*Class for unital semirings with characteristic zero.
   12.11   Includes non-ordered rings like the complex numbers.*}
    13.1 --- a/src/HOL/Orderings.thy	Fri Oct 21 11:17:12 2011 +0200
    13.2 +++ b/src/HOL/Orderings.thy	Fri Oct 21 11:17:14 2011 +0200
    13.3 @@ -305,13 +305,13 @@
    13.4  
    13.5  text {* Explicit dictionaries for code generation *}
    13.6  
    13.7 -lemma min_ord_min [code, code_unfold, code_inline del]:
    13.8 +lemma min_ord_min [code]:
    13.9    "min = ord.min (op \<le>)"
   13.10    by (rule ext)+ (simp add: min_def ord.min_def)
   13.11  
   13.12  declare ord.min_def [code]
   13.13  
   13.14 -lemma max_ord_max [code, code_unfold, code_inline del]:
   13.15 +lemma max_ord_max [code]:
   13.16    "max = ord.max (op \<le>)"
   13.17    by (rule ext)+ (simp add: max_def ord.max_def)
   13.18  
    14.1 --- a/src/HOL/Power.thy	Fri Oct 21 11:17:12 2011 +0200
    14.2 +++ b/src/HOL/Power.thy	Fri Oct 21 11:17:14 2011 +0200
    14.3 @@ -460,7 +460,7 @@
    14.4  
    14.5  subsection {* Code generator tweak *}
    14.6  
    14.7 -lemma power_power_power [code, code_unfold, code_inline del]:
    14.8 +lemma power_power_power [code]:
    14.9    "power = power.power (1::'a::{power}) (op *)"
   14.10    unfolding power_def power.power_def ..
   14.11