# HG changeset patch
# User haftmann
# Date 1248071527 -7200
# Node ID e8e0fb5da77ae26715f00bd3b652f2b3b0d16319
# Parent  db50e76b0046374c050f005522514e19f0e134d1# Parent  76d6ba08a05f7cff95191b1aac5be092f3863167
merged

diff -r db50e76b0046 -r e8e0fb5da77a NEWS
--- a/NEWS	Sat Jul 18 22:53:02 2009 +0200
+++ b/NEWS	Mon Jul 20 08:32:07 2009 +0200
@@ -28,6 +28,14 @@
 
 * New type class boolean_algebra.
 
+* Refinements to lattices classes:
+  - added boolean_algebra type class
+  - less default intro/elim rules in locale variant, more default
+    intro/elim rules in class variant: more uniformity
+  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
+  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
+  - renamed ACI to inf_sup_aci
+
 * Class semiring_div requires superclass no_zero_divisors and proof of
 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -32,7 +32,7 @@
   \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
   "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
 
-lemma valapp_code [code, code_inline]:
+lemma valapp_code [code, code_unfold]:
   "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
   by (simp only: valapp_def fst_conv snd_conv)
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Code_Numeral.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -176,13 +176,13 @@
 
 end
 
-lemma zero_code_numeral_code [code_inline, code]:
+lemma zero_code_numeral_code [code, code_unfold]:
   "(0\<Colon>code_numeral) = Numeral0"
   by (simp add: number_of_code_numeral_def Pls_def)
 lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
   using zero_code_numeral_code ..
 
-lemma one_code_numeral_code [code_inline, code]:
+lemma one_code_numeral_code [code, code_unfold]:
   "(1\<Colon>code_numeral) = Numeral1"
   by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
 lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -812,7 +812,7 @@
 by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
 
 lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
-by (induct pred:finite) auto
+by (induct pred: finite) (auto intro: le_infI1)
 
 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
 proof(induct arbitrary: a pred:finite)
@@ -823,7 +823,7 @@
   proof cases
     assume "A = {}" thus ?thesis using insert by simp
   next
-    assume "A \<noteq> {}" thus ?thesis using insert by auto
+    assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
   qed
 qed
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/HOL.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -187,8 +187,8 @@
   True_or_False:  "(P=True) | (P=False)"
 
 defs
-  Let_def:      "Let s f == f(s)"
-  if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
+  Let_def [code]: "Let s f == f(s)"
+  if_def:         "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
 finalconsts
   "op ="
@@ -1029,8 +1029,8 @@
     "(P ~= Q) = (P = (~Q))"
     "(P | ~P) = True"    "(~P | P) = True"
     "(x = x) = True"
-  and not_True_eq_False: "(\<not> True) = False"
-  and not_False_eq_True: "(\<not> False) = True"
+  and not_True_eq_False [code]: "(\<not> True) = False"
+  and not_False_eq_True [code]: "(\<not> False) = True"
   and
     "(~P) ~= P"  "P ~= (~P)"
     "(True=P) = P"
@@ -1157,10 +1157,10 @@
 
 text {* \medskip if-then-else rules *}
 
-lemma if_True: "(if True then x else y) = x"
+lemma if_True [code]: "(if True then x else y) = x"
   by (unfold if_def) blast
 
-lemma if_False: "(if False then x else y) = y"
+lemma if_False [code]: "(if False then x else y) = y"
   by (unfold if_def) blast
 
 lemma if_P: "P ==> (if P then x else y) = x"
@@ -1722,6 +1722,7 @@
 setup {*
   Codegen.setup
   #> RecfunCodegen.setup
+  #> Codegen.map_unfold (K HOL_basic_ss)
 *}
 
 types_code
@@ -1841,13 +1842,7 @@
     and "x \<or> False \<longleftrightarrow> x"
     and "x \<or> True \<longleftrightarrow> True" by simp_all
 
-lemma [code]:
-  shows "\<not> True \<longleftrightarrow> False"
-    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
-
-lemmas [code] = Let_def if_True if_False
-
-lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
+declare imp_conv_disj [code, code_unfold_post]
 
 instantiation itself :: (type) eq
 begin
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -283,7 +283,7 @@
 where
   [code del]: "raise_exc e = raise []"
 
-lemma raise_raise_exc [code, code_inline]:
+lemma raise_raise_exc [code, code_unfold]:
   "raise s = raise_exc (Fail (STR s))"
   unfolding Fail_def raise_exc_def raise_def ..
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Int.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -2126,11 +2126,11 @@
 
 hide (open) const nat_aux
 
-lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
+lemma zero_is_num_zero [code, code_unfold_post]:
   "(0\<Colon>int) = Numeral0" 
   by simp
 
-lemma one_is_num_one [code, code_inline, symmetric, code_post]:
+lemma one_is_num_one [code, code_unfold_post]:
   "(1\<Colon>int) = Numeral1" 
   by simp
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/IntDiv.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -36,7 +36,7 @@
 
 text{*algorithm for the general case @{term "b\<noteq>0"}*}
 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
-  [code_inline]: "negateSnd = apsnd uminus"
+  [code_unfold]: "negateSnd = apsnd uminus"
 
 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     --{*The full division algorithm considers all possible signs for a, b
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Lattices.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -44,38 +44,27 @@
 context lower_semilattice
 begin
 
-lemma le_infI1[intro]:
-  assumes "a \<sqsubseteq> x"
-  shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
-  from assms show "a \<sqsubseteq> x" .
-  show "a \<sqinter> b \<sqsubseteq> a" by simp 
-qed
-lemmas (in -) [rule del] = le_infI1
+lemma le_infI1:
+  "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+  by (rule order_trans) auto
 
-lemma le_infI2[intro]:
-  assumes "b \<sqsubseteq> x"
-  shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
-  from assms show "b \<sqsubseteq> x" .
-  show "a \<sqinter> b \<sqsubseteq> b" by simp
-qed
-lemmas (in -) [rule del] = le_infI2
+lemma le_infI2:
+  "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+  by (rule order_trans) auto
 
-lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
-by(blast intro: inf_greatest)
-lemmas (in -) [rule del] = le_infI
+lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+  by (blast intro: inf_greatest)
 
-lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
-  by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_infE
+lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+  by (blast intro: order_trans le_infI1 le_infI2)
 
 lemma le_inf_iff [simp]:
-  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
-by blast
+  "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
+  by (blast intro: le_infI elim: le_infE)
 
-lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
-  by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_inf:
+  "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
+  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
 
 lemma mono_inf:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
@@ -87,28 +76,29 @@
 context upper_semilattice
 begin
 
-lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1:
+  "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   by (rule order_trans) auto
-lemmas (in -) [rule del] = le_supI1
 
-lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2:
+  "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   by (rule order_trans) auto 
-lemmas (in -) [rule del] = le_supI2
 
-lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI:
+  "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   by (blast intro: sup_least)
-lemmas (in -) [rule del] = le_supI
 
-lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
-  by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_supE
+lemma le_supE:
+  "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+  by (blast intro: le_supI1 le_supI2 order_trans)
 
-lemma ge_sup_conv[simp]:
-  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
-by blast
+lemma le_sup_iff [simp]:
+  "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+  by (blast intro: le_supI elim: le_supE)
 
-lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
-  by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_sup:
+  "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
+  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
 
 lemma mono_sup:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
@@ -118,62 +108,61 @@
 end
 
 
-subsubsection{* Equational laws *}
+subsubsection {* Equational laws *}
 
 context lower_semilattice
 begin
 
 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_infI1 le_infI2)
 
 lemma inf_idem[simp]: "x \<sqinter> x = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_infI2)
 
 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
-  by (blast intro: antisym)
-
-lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
+  by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
+  
+lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
 
 end
 
-
 context upper_semilattice
 begin
 
 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_supI1 le_supI2)
 
 lemma sup_idem[simp]: "x \<squnion> x = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_supI2)
 
 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
-  by (blast intro: antisym)
+  by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
 
-lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
+lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
 
 end
 
@@ -191,18 +180,17 @@
 lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
   by (blast intro: antisym sup_ge1 sup_least inf_le1)
 
-lemmas ACI = inf_ACI sup_ACI
+lemmas inf_sup_aci = inf_aci sup_aci
 
 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
 
 text{* Towards distributivity *}
 
 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
-  by blast
+  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
-  by blast
-
+  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 text{* If you have one of them, you have them all. *}
 
@@ -230,10 +218,6 @@
   finally show ?thesis .
 qed
 
-(* seems unused *)
-lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
-by blast
-
 end
 
 
@@ -247,7 +231,7 @@
 
 lemma sup_inf_distrib2:
  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
-by(simp add:ACI sup_inf_distrib1)
+by(simp add: inf_sup_aci sup_inf_distrib1)
 
 lemma inf_sup_distrib1:
  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -255,7 +239,7 @@
 
 lemma inf_sup_distrib2:
  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
-by(simp add:ACI inf_sup_distrib1)
+by(simp add: inf_sup_aci inf_sup_distrib1)
 
 lemma dual_distrib_lattice:
   "distrib_lattice (op \<ge>) (op >) sup inf"
@@ -458,16 +442,6 @@
 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
 
-text {*
-  Now we have inherited antisymmetry as an intro-rule on all
-  linear orders. This is a problem because it applies to bool, which is
-  undesirable.
-*}
-
-lemmas [rule del] = min_max.le_infI min_max.le_supI
-  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
-  min_max.le_infI1 min_max.le_infI2
-
 
 subsection {* Bool as lattice *}
 
@@ -548,8 +522,6 @@
 
 text {* redundant bindings *}
 
-lemmas inf_aci = inf_ACI
-lemmas sup_aci = sup_ACI
 
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -24,11 +24,11 @@
 
 lemmas [code del] = char.recs char.cases char.size
 
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
   "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
   by (cases c) (auto simp add: nibble_pair_of_nat_char)
 
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
   "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
   by (cases c) (auto simp add: nibble_pair_of_nat_char)
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -26,15 +26,13 @@
 
 code_datatype number_nat_inst.number_of_nat
 
-lemma zero_nat_code [code, code_inline]:
+lemma zero_nat_code [code, code_unfold_post]:
   "0 = (Numeral0 :: nat)"
   by simp
-lemmas [code_post] = zero_nat_code [symmetric]
 
-lemma one_nat_code [code, code_inline]:
+lemma one_nat_code [code, code_unfold_post]:
   "1 = (Numeral1 :: nat)"
   by simp
-lemmas [code_post] = one_nat_code [symmetric]
 
 lemma Suc_code [code]:
   "Suc n = n + 1"
@@ -302,7 +300,7 @@
   Natural numerals.
 *}
 
-lemma [code_inline, symmetric, code_post]:
+lemma [code_unfold_post]:
   "nat (number_of i) = number_nat_inst.number_of_nat i"
   -- {* this interacts as desired with @{thm nat_number_of_def} *}
   by (simp add: number_nat_inst.number_of_nat)
@@ -322,9 +320,7 @@
   returns @{text "0"}.
 *}
 
-definition
-  int :: "nat \<Rightarrow> int"
-where
+definition int :: "nat \<Rightarrow> int" where
   [code del]: "int = of_nat"
 
 lemma int_code' [code]:
@@ -335,9 +331,12 @@
   "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   unfolding nat_number_of_def number_of_is_id neg_def by simp
 
-lemma of_nat_int [code_unfold]:
+lemma of_nat_int [code_unfold_post]:
   "of_nat = int" by (simp add: int_def)
-declare of_nat_int [symmetric, code_post]
+
+lemma of_nat_aux_int [code_unfold]:
+  "of_nat_aux (\<lambda>i. i + 1) k 0 = int k"
+  by (simp add: int_def Nat.of_nat_code)
 
 code_const int
   (SML "_")
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Library/Float.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -42,7 +42,7 @@
 instance ..
 end
 
-lemma number_of_float_Float [code_inline, symmetric, code_post]:
+lemma number_of_float_Float [code_unfold_post]:
   "number_of k = Float (number_of k) 0"
   by (simp add: number_of_float_def number_of_is_id)
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -40,10 +40,10 @@
   "0 = Fin 0"
 
 definition
-  [code_inline]: "1 = Fin 1"
+  [code_unfold]: "1 = Fin 1"
 
 definition
-  [code_inline, code del]: "number_of k = Fin (number_of k)"
+  [code_unfold, code del]: "number_of k = Fin (number_of k)"
 
 instance ..
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/List.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -3760,7 +3760,7 @@
   "xs = [] \<longleftrightarrow> null xs"
 by (cases xs) simp_all
 
-lemma [code_inline]:
+lemma [code_unfold]:
   "eq_class.eq xs [] \<longleftrightarrow> null xs"
 by (simp add: eq empty_null)
 
@@ -3808,7 +3808,7 @@
   "map_filter f P xs = map f (filter P xs)"
 by (induct xs) auto
 
-lemma length_remdups_length_unique [code_inline]:
+lemma length_remdups_length_unique [code_unfold]:
   "length (remdups xs) = length_unique xs"
   by (induct xs) simp_all
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -20,7 +20,7 @@
 begin
 
 definition
-  nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
+  nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
 
 instance ..
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Option.thy
--- a/src/HOL/Option.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Option.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -105,7 +105,7 @@
   "is_none x \<longleftrightarrow> x = None"
   by (simp add: is_none_def)
 
-lemma [code_inline]:
+lemma [code_unfold]:
   "eq_class.eq x None \<longleftrightarrow> is_none x"
   by (simp add: eq is_none_none)
 
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -1075,16 +1075,16 @@
 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
 
 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
 
 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
 
 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
 
 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
 
 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
 proof -
@@ -1120,7 +1120,7 @@
   assume "0 <= a + a"
   hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
   have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
-    by (simp add: add_sup_inf_distribs inf_ACI)
+    by (simp add: add_sup_inf_distribs inf_aci)
   hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
   hence "inf a 0 = 0" by (simp only: add_right_cancel)
   then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
@@ -1206,10 +1206,10 @@
 by (simp add: le_iff_inf nprt_def inf_commute)
 
 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
-by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
+by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
 
 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
-by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
+by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
 
 end
 
@@ -1230,7 +1230,7 @@
   then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   then show ?thesis
-    by (simp add: add_sup_inf_distribs sup_ACI
+    by (simp add: add_sup_inf_distribs sup_aci
       pprt_def nprt_def diff_minus abs_lattice)
 qed
 
@@ -1254,7 +1254,7 @@
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   proof -
     have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
-      by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
+      by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
     have a:"a+b <= sup ?m ?n" by (simp)
     have b:"-a-b <= ?n" by (simp) 
     have c:"?n <= sup ?m ?n" by (simp)
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Rational.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -1003,7 +1003,7 @@
 
 definition (in term_syntax)
   valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+  [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/RealDef.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -946,7 +946,7 @@
 
 end
 
-lemma [code_unfold, symmetric, code_post]:
+lemma [code_unfold_post]:
   "number_of k = real_of_int (number_of k)"
   unfolding number_of_is_id real_number_of_def ..
 
@@ -1129,7 +1129,7 @@
 
 definition (in term_syntax)
   valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+  [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/SEQ.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -113,8 +113,8 @@
 lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
 unfolding Bfun_def eventually_sequentially
 apply (rule iffI)
-apply (simp add: Bseq_def, fast)
-apply (fast intro: BseqI2')
+apply (simp add: Bseq_def)
+apply (auto intro: BseqI2')
 done
 
 
@@ -762,13 +762,25 @@
 lemma lemma_NBseq_def:
      "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
       (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
-apply auto
- prefer 2 apply force
-apply (cut_tac x = K in reals_Archimedean2, clarify)
-apply (rule_tac x = n in exI, clarify)
-apply (drule_tac x = na in spec)
-apply (auto simp add: real_of_nat_Suc)
-done
+proof auto
+  fix K :: real
+  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
+  then have "K \<le> real (Suc n)" by auto
+  assume "\<forall>m. norm (X m) \<le> K"
+  have "\<forall>m. norm (X m) \<le> real (Suc n)"
+  proof
+    fix m :: 'a
+    from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
+    with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
+  qed
+  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
+next
+  fix N :: nat
+  have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
+  moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
+  ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
+qed
+
 
 text{* alternative definition for Bseq *}
 lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
@@ -1105,7 +1117,7 @@
 lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
 proof (rule reals_complete)
   obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
-    using CauchyD [OF X zero_less_one] by fast
+    using CauchyD [OF X zero_less_one] by auto
   hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
   show "\<exists>x. x \<in> S"
   proof
@@ -1129,7 +1141,7 @@
   fix r::real assume "0 < r"
   hence r: "0 < r/2" by simp
   obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
-    using CauchyD [OF X r] by fast
+    using CauchyD [OF X r] by auto
   hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
   hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
     by (simp only: real_norm_def real_abs_diff_less_iff)
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/Set.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -2249,10 +2249,10 @@
   unfolding Inf_Sup by auto
 
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
-  by (auto intro: antisym Inf_greatest Inf_lower)
+  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
-  by (auto intro: antisym Sup_least Sup_upper)
+  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
 lemma Inf_singleton [simp]:
   "\<Sqinter>{a} = a"
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/String.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -58,11 +58,11 @@
 end
 *}
 
-lemma char_case_nibble_pair [code, code_inline]:
+lemma char_case_nibble_pair [code, code_unfold]:
   "char_case f = split f o nibble_pair_of_char"
   by (simp add: expand_fun_eq split: char.split)
 
-lemma char_rec_nibble_pair [code, code_inline]:
+lemma char_rec_nibble_pair [code, code_unfold]:
   "char_rec f = split f o nibble_pair_of_char"
   unfolding char_case_nibble_pair [symmetric]
   by (simp add: expand_fun_eq split: char.split)
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -3,7 +3,7 @@
 header {* Small examples for evaluation mechanisms *}
 
 theory Eval_Examples
-imports Code_Eval Rational
+imports Complex_Main
 begin
 
 text {* evaluation oracle *}
diff -r db50e76b0046 -r e8e0fb5da77a src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/HOL/ex/Numeral.thy	Mon Jul 20 08:32:07 2009 +0200
@@ -758,7 +758,7 @@
 
 code_datatype "0::int" Pls Mns
 
-lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
+lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
 
 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   [simp, code del]: "sub m n = (of_num m - of_num n)"
@@ -874,10 +874,10 @@
   using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   by (simp_all add: of_num_less_iff)
 
-lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
-lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
-declare zero_is_num_zero [code_inline del]
-declare one_is_num_one [code_inline del]
+lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
+lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
+declare zero_is_num_zero [code_unfold del]
+declare one_is_num_one [code_unfold del]
 
 hide (open) const sub dup
 
diff -r db50e76b0046 -r e8e0fb5da77a src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Mon Jul 20 08:32:07 2009 +0200
@@ -242,15 +242,16 @@
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
-    val deps_witss = case some_dep_morph
-     of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
-      | NONE => []
+    val add_dependency = case some_dep_morph
+     of SOME dep_morph => Locale.add_dependency sub
+          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
+      | NONE => I
   in
     thy
     |> AxClass.add_classrel classrel
     |> ClassData.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)
-    |> Locale.add_dependencies sub deps_witss export
+    |> add_dependency
   end;
 
 
diff -r db50e76b0046 -r e8e0fb5da77a src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jul 20 08:32:07 2009 +0200
@@ -886,7 +886,9 @@
  of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   | NONE => thy;
 
-structure Code_Attr = TheoryDataFun (
+(* c.f. src/HOL/Tools/recfun_codegen.ML *)
+
+structure Code_Target_Attr = TheoryDataFun (
   type T = (string -> thm -> theory -> theory) option;
   val empty = NONE;
   val copy = I;
@@ -895,7 +897,14 @@
     | merge _ (f1, _) = f1;
 );
 
-fun set_code_target_attr f = Code_Attr.map (K (SOME f));
+fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
+
+fun code_target_attr prefix thm thy =
+  let
+    val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
+  in thy |> add_warning_eqn thm |> attr prefix thm end;
+
+(* setup *)
 
 val _ = Context.>> (Context.map_theory
   (let
@@ -904,9 +913,7 @@
       Args.del |-- Scan.succeed (mk_attribute del_eqn)
       || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
       || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
-           (fn prefix => mk_attribute (fn thm => fn thy => thy
-             |> add_warning_eqn thm
-             |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
+           (mk_attribute o code_target_attr))
       || Scan.succeed (mk_attribute add_warning_eqn);
   in
     Type_Interpretation.init
diff -r db50e76b0046 -r e8e0fb5da77a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Mon Jul 20 08:32:07 2009 +0200
@@ -788,27 +788,6 @@
 
 (*** Interpretation ***)
 
-(** Interpretation between locales: declaring sublocale relationships **)
-
-local
-
-fun gen_sublocale prep_expr intern raw_target expression thy =
-  let
-    val target = intern thy raw_target;
-    val target_ctxt = Locale.init target thy;
-    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-    fun after_qed witss = ProofContext.theory
-      (Locale.add_dependencies target (deps ~~ witss) export);
-  in Element.witness_proof after_qed propss goal_ctxt end;
-
-in
-
-fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
-fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
-
-end;
-
-
 (** Interpretation in theories **)
 
 local
@@ -816,46 +795,31 @@
 fun gen_interpretation prep_expr parse_prop prep_attr
     expression equations theory =
   let
-    val ((propss, regs, export), expr_ctxt) = ProofContext.init theory
+    val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
       |> prep_expr expression;
 
     val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
-    val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations;
+    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
-    fun store_reg ((name, morph), wits) thy =
+    fun note_eqns raw_eqns thy =
       let
-        val wits' = map (Element.morph_witness export') wits;
-        val morph' = morph $> Element.satisfy_morphism wits';
+        val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
+        val eqn_attrss = map2 (fn attrs => fn eqn =>
+          ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
+        fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+          Drule.abs_def) o maps snd;
       in
         thy
-        |> Locale.add_registration (name, (morph', export))
-        |> pair (name, morph')
+        |> PureThy.note_thmss Thm.lemmaK eqn_attrss
+        |-> (fn facts => `(fn thy => meta_rewrite thy facts))
       end;
 
-    fun store_eqns_activate regs [] thy =
-          thy
-          |> fold (fn (name, morph) =>
-               Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
-      | store_eqns_activate regs eqs thy =
-          let
-            val eqs' = eqs |> map (Morphism.thm (export' $> export));
-            val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
-              Drule.abs_def);
-            val eq_morph = Element.eq_morphism thy morph_eqs;
-            val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
-          in
-            thy
-            |> fold (fn (name, morph) =>
-                Locale.amend_registration eq_morph (name, morph) #>
-                Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
-            |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
-            |> snd
-          end;
-
-    fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
-      #-> (fn regs => store_eqns_activate regs eqs));
+    fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
+      #-> (fn eqns => fold (fn ((dep, morph), wits) =>
+        Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism
+          (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
@@ -868,12 +832,33 @@
 end;
 
 
+(** Interpretation between locales: declaring sublocale relationships **)
+
+local
+
+fun gen_sublocale prep_expr intern raw_target expression thy =
+  let
+    val target = intern thy raw_target;
+    val target_ctxt = Locale.init target thy;
+    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
+    fun after_qed witss = ProofContext.theory
+      (fold (fn ((dep, morph), wits) => Locale.add_dependency
+        target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
+  in Element.witness_proof after_qed propss goal_ctxt end;
+
+in
+
+fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
+fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
+
+end;
+
+
 (** Interpretation in proof contexts **)
 
 local
 
-fun gen_interpret prep_expr
-    expression int state =
+fun gen_interpret prep_expr expression int state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
diff -r db50e76b0046 -r e8e0fb5da77a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Jul 20 08:32:07 2009 +0200
@@ -70,8 +70,8 @@
   (* Registrations and dependencies *)
   val add_registration: string * (morphism * morphism) -> theory -> theory
   val amend_registration: morphism -> string * morphism -> theory -> theory
-  val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
-    morphism  -> theory -> theory
+  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
+  val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
   val print_locales: theory -> unit
@@ -368,14 +368,22 @@
       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   end;
 
+fun add_registration_eqs (dep, proto_morph) eqns export thy =
+  let
+    val morph = if null eqns then proto_morph
+      else proto_morph $> Element.eq_morphism thy eqns;
+  in
+    thy
+    |> add_registration (dep, (morph, export))
+    |> Context.theory_map (activate_facts (dep, morph $> export))
+  end;
+
 
 (*** Dependencies ***)
 
-fun add_dependencies loc deps_witss export thy =
+fun add_dependency loc (dep, morph) export thy =
   thy
-  |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
-      (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
-        deps_witss
+  |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
   |> (fn thy => fold_rev (Context.theory_map o activate_facts)
       (all_registrations thy) thy);
 
diff -r db50e76b0046 -r e8e0fb5da77a src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/Pure/codegen.ML	Mon Jul 20 08:32:07 2009 +0200
@@ -85,7 +85,9 @@
   val num_args_of: 'a mixfix list -> int
   val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
   val mk_deftab: theory -> deftab
+  val map_unfold: (simpset -> simpset) -> theory -> theory
   val add_unfold: thm -> theory -> theory
+  val del_unfold: thm -> theory -> theory
 
   val get_node: codegr -> string -> node
   val add_edge: string * string -> codegr -> codegr
@@ -296,13 +298,9 @@
   fun merge _ = merge_ss;
 );
 
-fun add_unfold eqn =
-  let
-    val ctxt = ProofContext.init (Thm.theory_of_thm eqn);
-    val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn;
-  in
-    UnfoldData.map (fn ss => ss addsimps [eqn'])
-  end;
+val map_unfold = UnfoldData.map;
+val add_unfold = map_unfold o MetaSimplifier.add_simp;
+val del_unfold = map_unfold o MetaSimplifier.del_simp;
 
 fun unfold_preprocessor thy =
   let val ss = Simplifier.theory_context thy (UnfoldData.get thy)
diff -r db50e76b0046 -r e8e0fb5da77a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sat Jul 18 22:53:02 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Jul 20 08:32:07 2009 +0200
@@ -9,7 +9,7 @@
 sig
   val map_pre: (simpset -> simpset) -> theory -> theory
   val map_post: (simpset -> simpset) -> theory -> theory
-  val add_inline: thm -> theory -> theory
+  val add_unfold: thm -> theory -> theory
   val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
   val del_functrans: string -> theory -> theory
   val simple_functrans: (theory -> thm list -> thm list option)
@@ -77,14 +77,24 @@
   |> Code.purge_data
   |> (Code_Preproc_Data.map o map_thmproc) f;
 
-val map_pre = map_data o apfst o apfst;
-val map_post = map_data o apfst o apsnd;
+val map_pre_post = map_data o apfst;
+val map_pre = map_pre_post o apfst;
+val map_post = map_pre_post o apsnd;
 
-val add_inline = map_pre o MetaSimplifier.add_simp;
-val del_inline = map_pre o MetaSimplifier.del_simp;
+val add_unfold = map_pre o MetaSimplifier.add_simp;
+val del_unfold = map_pre o MetaSimplifier.del_simp;
 val add_post = map_post o MetaSimplifier.add_simp;
 val del_post = map_post o MetaSimplifier.del_simp;
-  
+
+fun add_unfold_post raw_thm thy =
+  let
+    val thm = LocalDefs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+    val thm_sym = Thm.symmetric thm;
+  in
+    thy |> map_pre_post (fn (pre, post) =>
+      (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym))
+  end;
+
 fun add_functrans (name, f) = (map_data o apsnd)
   (AList.update (op =) (name, (serial (), f)));
 
@@ -526,16 +536,19 @@
 val setup = 
   let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-    fun add_del_attribute_parser (add, del) =
+    fun add_del_attribute_parser add del =
       Attrib.add_del (mk_attribute add) (mk_attribute del);
+    fun both f g thm = f thm #> g thm;
   in
-    Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
+    Attrib.setup @{binding code_unfold} (add_del_attribute_parser 
+       (both Codegen.add_unfold add_unfold) (both Codegen.del_unfold del_unfold))
+        "preprocessing equations for code generators"
+    #> Attrib.setup @{binding code_inline} (add_del_attribute_parser add_unfold del_unfold)
         "preprocessing equations for code generator"
-    #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
+    #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
         "postprocessing equations for code generator"
-    #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
-       (fn thm => Codegen.add_unfold thm #> add_inline thm)))
-        "preprocessing equations for code generators"
+    #> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))
+        "pre- and postprocessing equations for code generator"
   end;
 
 val _ =