merged
authorwenzelm
Thu, 14 Feb 2013 17:06:15 +0100
changeset 51123 e51e76ffaedd
parent 51117 47af65ef228e (diff)
parent 51122 386a117925db (current diff)
child 51125 f90874d3a246
merged
--- a/NEWS	Thu Feb 14 16:36:21 2013 +0100
+++ b/NEWS	Thu Feb 14 17:06:15 2013 +0100
@@ -10,6 +10,15 @@
 (lin)order_topology. Allows to generalize theorems about limits and
 order. Instances are reals and extended reals.
 
+*** HOL ***
+
+* Consolidation of library theories on product orders:
+
+    Product_Lattice ~> Product_Order -- pointwise order on products
+    Product_ord ~> Product_Lexorder -- lexicographic order on products
+
+INCOMPATIBILITY.
+
 
 New in Isabelle2013 (February 2013)
 -----------------------------------
--- a/src/HOL/Big_Operators.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -6,7 +6,7 @@
 header {* Big operators and finite (non-empty) sets *}
 
 theory Big_Operators
-imports Plain
+imports Finite_Set Metis
 begin
 
 subsection {* Generic monoid operation over a set *}
--- a/src/HOL/Code_Evaluation.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Evaluation
-imports Plain Typerep New_DSequence
+imports Typerep New_DSequence
 begin
 
 subsection {* Term representation *}
--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -22,23 +22,13 @@
 lemma [code, code del]:
   "pred_of_set = pred_of_set" ..
 
-
-lemma [code, code del]:
-  "Cardinality.card' = Cardinality.card'" ..
-
-lemma [code, code del]:
-  "Cardinality.finite' = Cardinality.finite'" ..
-
-lemma [code, code del]:
-  "Cardinality.subset' = Cardinality.subset'" ..
-
-lemma [code, code del]:
-  "Cardinality.eq_set = Cardinality.eq_set" ..
-
-
 lemma [code, code del]:
   "acc = acc" ..
 
+lemmas [code del] =
+  finite_set_code finite_coset_code 
+  equal_set_code
+
 (*
   If the code generation ends with an exception with the following message:
   '"List.set" is not a constructor, on left hand side of equation: ...',
--- a/src/HOL/Equiv_Relations.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
 header {* Equivalence Relations in Higher-Order Set Theory *}
 
 theory Equiv_Relations
-imports Big_Operators Relation Plain
+imports Big_Operators Relation
 begin
 
 subsection {* Equivalence relations -- set version *}
--- a/src/HOL/Int.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Int.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -6,7 +6,7 @@
 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
 
 theory Int
-imports Equiv_Relations Wellfounded Quotient
+imports Equiv_Relations Wellfounded Quotient FunDef
 begin
 
 subsection {* Definition of integers as a quotient type *}
--- a/src/HOL/Library/Cardinality.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Cardinality.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -199,7 +199,7 @@
 subsection {* A type class for computing the cardinality of types *}
 
 definition is_list_UNIV :: "'a list \<Rightarrow> bool"
-where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
+where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
 
 lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
 by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
@@ -211,15 +211,6 @@
   fixes card_UNIV :: "'a card_UNIV"
   assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
 
-lemma card_UNIV_code [code_unfold]: 
-  "CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)"
-by(simp add: card_UNIV)
-
-lemma is_list_UNIV_code [code]:
-  "is_list_UNIV (xs :: 'a list) = 
-  (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
-by(rule is_list_UNIV_def)
-
 subsection {* Instantiations for @{text "card_UNIV"} *}
 
 instantiation nat :: card_UNIV begin
@@ -396,80 +387,66 @@
 
 subsection {* Code setup for sets *}
 
+text {*
+  Implement operations @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, and @{term "op ="} 
+  for sets using @{term "finite_UNIV"} and @{term "card_UNIV"}.
+*}
+
 lemma card_Compl:
   "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
 by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
 
-context fixes xs :: "'a :: card_UNIV list"
-begin
+lemma card_coset_code [code]:
+  fixes xs :: "'a :: card_UNIV list" 
+  shows "card (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
+by(simp add: List.card_set card_Compl card_UNIV)
 
-definition card' :: "'a set \<Rightarrow> nat" 
-where [simp, code del, code_abbrev]: "card' = card"
-
-lemma card'_code [code]:
-  "card' (set xs) = length (remdups xs)"
-  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
-by(simp_all add: List.card_set card_Compl card_UNIV)
+lemma [code, code del]: "finite = finite" ..
 
-lemma card'_UNIV [code_unfold]: 
-  "card' (UNIV :: 'a :: card_UNIV set) = of_phantom (card_UNIV :: 'a card_UNIV)"
-by(simp add: card_UNIV)
-
-definition finite' :: "'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "finite' = finite"
-
-lemma finite'_code [code]:
-  "finite' (set xs) \<longleftrightarrow> True"
-  "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
+lemma [code]:
+  fixes xs :: "'a :: card_UNIV list" 
+  shows finite_set_code:
+  "finite (set xs) = True" 
+  and finite_coset_code:
+  "finite (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
 by(simp_all add: card_gt_0_iff finite_UNIV)
 
-definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
-
-lemma subset'_code [code]:
-  "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
-  "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
-  "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
+lemma coset_subset_code [code]:
+  fixes xs :: "'a list" shows
+  "List.coset xs \<subseteq> set ys \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card (set (xs @ ys)) = n)"
 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"
-where [simp, code del, code_abbrev]: "eq_set = op ="
-
-lemma eq_set_code [code]:
-  fixes ys
+lemma equal_set_code [code]:
+  fixes xs ys :: "'a :: equal list"
   defines "rhs \<equiv> 
   let n = CARD('a)
   in if n = 0 then False else 
         let xs' = remdups xs; ys' = remdups ys 
         in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
-  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
-  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
-  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
-  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
+  shows "equal_class.equal (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
+  and "equal_class.equal (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
+  and "equal_class.equal (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
+  and "equal_class.equal (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
 proof -
   show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
   proof
     assume ?lhs thus ?rhs
-      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
+      by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
   next
     assume ?rhs
     moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
     ultimately show ?lhs
-      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
+      by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
   qed
-  thus ?thesis2 unfolding eq_set_def by blast
-  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
+  thus ?thesis2 unfolding equal_eq by blast
+  show ?thesis3 ?thesis4 unfolding equal_eq List.coset_def by blast+
 qed
 
-end
-
 notepad begin (* test code setup *)
 have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])"
   by eval
 end
 
-hide_const (open) card' finite' subset' eq_set
-
 end
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -0,0 +1,113 @@
+(*  Title:      HOL/Library/Code_Abstract_Nat.thy
+    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
+*)
+
+header {* Avoidance of pattern matching on natural numbers *}
+
+theory Code_Abstract_Nat
+imports Main
+begin
+
+text {*
+  When natural numbers are implemented in another than the
+  conventional inductive @{term "0::nat"}/@{term Suc} representation,
+  it is necessary to avoid all pattern matching on natural numbers
+  altogether.  This is accomplished by this theory (up to a certain
+  extent).
+*}
+
+subsection {* Case analysis *}
+
+text {*
+  Case analysis on natural numbers is rephrased using a conditional
+  expression:
+*}
+
+lemma [code, code_unfold]:
+  "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+  by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
+
+
+subsection {* Preprocessors *}
+
+text {*
+  The term @{term "Suc n"} is no longer a valid pattern.  Therefore,
+  all occurrences of this term in a position where a pattern is
+  expected (i.e.~on the left-hand side of a code equation) must be
+  eliminated.  This can be accomplished – as far as possible – by
+  applying the following transformation rule:
+*}
+
+lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
+  f n \<equiv> if n = 0 then g else h (n - 1)"
+  by (rule eq_reflection) (cases n, simp_all)
+
+text {*
+  The rule above is built into a preprocessor that is plugged into
+  the code generator.
+*}
+
+setup {*
+let
+
+fun remove_suc thy thms =
+  let
+    val vname = singleton (Name.variant_list (map fst
+      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
+    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
+    fun lhs_of th = snd (Thm.dest_comb
+      (fst (Thm.dest_comb (cprop_of th))));
+    fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
+    fun find_vars ct = (case term_of ct of
+        (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
+      | _ $ _ =>
+        let val (ct1, ct2) = Thm.dest_comb ct
+        in 
+          map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
+          map (apfst (Thm.apply ct1)) (find_vars ct2)
+        end
+      | _ => []);
+    val eqs = maps
+      (fn th => map (pair th) (find_vars (lhs_of th))) thms;
+    fun mk_thms (th, (ct, cv')) =
+      let
+        val th' =
+          Thm.implies_elim
+           (Conv.fconv_rule (Thm.beta_conversion true)
+             (Drule.instantiate'
+               [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
+                 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
+               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
+      in
+        case map_filter (fn th'' =>
+            SOME (th'', singleton
+              (Variable.trade (K (fn [th'''] => [th''' RS th']))
+                (Variable.global_thm_context th'')) th'')
+          handle THM _ => NONE) thms of
+            [] => NONE
+          | thps =>
+              let val (ths1, ths2) = split_list thps
+              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
+      end
+  in get_first mk_thms eqs end;
+
+fun eqn_suc_base_preproc thy thms =
+  let
+    val dest = fst o Logic.dest_equals o prop_of;
+    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
+  in
+    if forall (can dest) thms andalso exists (contains_suc o dest) thms
+      then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
+       else NONE
+  end;
+
+val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
+
+in
+
+  Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
+
+end;
+*}
+
+end
--- a/src/HOL/Library/Code_Binary_Nat.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -1,11 +1,11 @@
 (*  Title:      HOL/Library/Code_Binary_Nat.thy
-    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
+    Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Implementation of natural numbers as binary numerals *}
 
 theory Code_Binary_Nat
-imports Main
+imports Code_Abstract_Nat
 begin
 
 text {*
@@ -146,104 +146,6 @@
   by (simp_all add: nat_of_num_numeral)
 
 
-subsection {* Case analysis *}
-
-text {*
-  Case analysis on natural numbers is rephrased using a conditional
-  expression:
-*}
-
-lemma [code, code_unfold]:
-  "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
-  by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
-
-
-subsection {* Preprocessors *}
-
-text {*
-  The term @{term "Suc n"} is no longer a valid pattern.
-  Therefore, all occurrences of this term in a position
-  where a pattern is expected (i.e.~on the left-hand side of a recursion
-  equation) must be eliminated.
-  This can be accomplished by applying the following transformation rules:
-*}
-
-lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
-  f n \<equiv> if n = 0 then g else h (n - 1)"
-  by (rule eq_reflection) (cases n, simp_all)
-
-text {*
-  The rules above are built into a preprocessor that is plugged into
-  the code generator. Since the preprocessor for introduction rules
-  does not know anything about modes, some of the modes that worked
-  for the canonical representation of natural numbers may no longer work.
-*}
-
-(*<*)
-setup {*
-let
-
-fun remove_suc thy thms =
-  let
-    val vname = singleton (Name.variant_list (map fst
-      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
-    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
-    fun lhs_of th = snd (Thm.dest_comb
-      (fst (Thm.dest_comb (cprop_of th))));
-    fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
-    fun find_vars ct = (case term_of ct of
-        (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
-      | _ $ _ =>
-        let val (ct1, ct2) = Thm.dest_comb ct
-        in 
-          map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
-          map (apfst (Thm.apply ct1)) (find_vars ct2)
-        end
-      | _ => []);
-    val eqs = maps
-      (fn th => map (pair th) (find_vars (lhs_of th))) thms;
-    fun mk_thms (th, (ct, cv')) =
-      let
-        val th' =
-          Thm.implies_elim
-           (Conv.fconv_rule (Thm.beta_conversion true)
-             (Drule.instantiate'
-               [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
-                 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
-               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
-      in
-        case map_filter (fn th'' =>
-            SOME (th'', singleton
-              (Variable.trade (K (fn [th'''] => [th''' RS th']))
-                (Variable.global_thm_context th'')) th'')
-          handle THM _ => NONE) thms of
-            [] => NONE
-          | thps =>
-              let val (ths1, ths2) = split_list thps
-              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
-      end
-  in get_first mk_thms eqs end;
-
-fun eqn_suc_base_preproc thy thms =
-  let
-    val dest = fst o Logic.dest_equals o prop_of;
-    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
-  in
-    if forall (can dest) thms andalso exists (contains_suc o dest) thms
-      then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
-       else NONE
-  end;
-
-val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
-
-in
-
-  Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
-
-end;
-*}
-(*>*)
-
 code_modulename SML
   Code_Binary_Nat Arith
 
--- a/src/HOL/Library/Code_Numeral_Types.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Numeral_Types.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -13,9 +13,11 @@
 typedef integer = "UNIV \<Colon> int set"
   morphisms int_of_integer integer_of_int ..
 
+setup_lifting (no_code) type_definition_integer
+
 lemma integer_eq_iff:
   "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
-  using int_of_integer_inject [of k l] ..
+  by transfer rule
 
 lemma integer_eqI:
   "int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
@@ -23,172 +25,199 @@
 
 lemma int_of_integer_integer_of_int [simp]:
   "int_of_integer (integer_of_int k) = k"
-  using integer_of_int_inverse [of k] by simp
+  by transfer rule
 
 lemma integer_of_int_int_of_integer [simp]:
   "integer_of_int (int_of_integer k) = k"
-  using int_of_integer_inverse [of k] by simp
+  by transfer rule
 
 instantiation integer :: ring_1
 begin
 
-definition
-  "0 = integer_of_int 0"
+lift_definition zero_integer :: integer
+  is "0 :: int"
+  .
 
-lemma int_of_integer_zero [simp]:
-  "int_of_integer 0 = 0"
-  by (simp add: zero_integer_def)
-
-definition
-  "1 = integer_of_int 1"
+declare zero_integer.rep_eq [simp]
 
-lemma int_of_integer_one [simp]:
-  "int_of_integer 1 = 1"
-  by (simp add: one_integer_def)
+lift_definition one_integer :: integer
+  is "1 :: int"
+  .
+
+declare one_integer.rep_eq [simp]
 
-definition
-  "k + l = integer_of_int (int_of_integer k + int_of_integer l)"
+lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "plus :: int \<Rightarrow> int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_plus [simp]:
-  "int_of_integer (k + l) = int_of_integer k + int_of_integer l"
-  by (simp add: plus_integer_def)
+declare plus_integer.rep_eq [simp]
 
-definition
-  "- k = integer_of_int (- int_of_integer k)"
+lift_definition uminus_integer :: "integer \<Rightarrow> integer"
+  is "uminus :: int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_uminus [simp]:
-  "int_of_integer (- k) = - int_of_integer k"
-  by (simp add: uminus_integer_def)
-
-definition
-  "k - l = integer_of_int (int_of_integer k - int_of_integer l)"
+declare uminus_integer.rep_eq [simp]
 
-lemma int_of_integer_minus [simp]:
-  "int_of_integer (k - l) = int_of_integer k - int_of_integer l"
-  by (simp add: minus_integer_def)
+lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "minus :: int \<Rightarrow> int \<Rightarrow> int"
+  .
+
+declare minus_integer.rep_eq [simp]
 
-definition
-  "k * l = integer_of_int (int_of_integer k * int_of_integer l)"
+lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "times :: int \<Rightarrow> int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_times [simp]:
-  "int_of_integer (k * l) = int_of_integer k * int_of_integer l"
-  by (simp add: times_integer_def)
+declare times_integer.rep_eq [simp]
 
 instance proof
-qed (auto simp add: integer_eq_iff algebra_simps)
+qed (transfer, simp add: algebra_simps)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+  by (unfold of_nat_def [abs_def])  transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+proof -
+  have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+    by (unfold of_int_of_nat [abs_def]) transfer_prover
+  then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
+proof -
+  have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
+    by transfer_prover
+  then show ?thesis by simp
+qed
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
+  by (unfold neg_numeral_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold Num.sub_def [abs_def]) transfer_prover
+
 lemma int_of_integer_of_nat [simp]:
   "int_of_integer (of_nat n) = of_nat n"
-  by (induct n) simp_all
+  by transfer rule
 
-definition integer_of_nat :: "nat \<Rightarrow> integer"
-where
-  "integer_of_nat = of_nat"
+lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
+  is "of_nat :: nat \<Rightarrow> int"
+  .
 
 lemma int_of_integer_integer_of_nat [simp]:
   "int_of_integer (integer_of_nat n) = of_nat n"
-  by (simp add: integer_of_nat_def)
-  
-definition nat_of_integer :: "integer \<Rightarrow> nat"
-where
-  "nat_of_integer k = Int.nat (int_of_integer k)"
+  by transfer rule
+
+lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
+  is Int.nat
+  .
 
 lemma nat_of_integer_of_nat [simp]:
   "nat_of_integer (of_nat n) = n"
-  by (simp add: nat_of_integer_def)
+  by transfer simp
 
 lemma int_of_integer_of_int [simp]:
   "int_of_integer (of_int k) = k"
-  by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one)
+  by transfer simp
 
 lemma nat_of_integer_integer_of_nat [simp]:
   "nat_of_integer (integer_of_nat n) = n"
-  by (simp add: integer_of_nat_def)
+  by transfer simp
 
 lemma integer_of_int_eq_of_int [simp, code_abbrev]:
   "integer_of_int = of_int"
-  by rule (simp add: integer_eq_iff)
+  by transfer (simp add: fun_eq_iff)
 
 lemma of_int_integer_of [simp]:
   "of_int (int_of_integer k) = (k :: integer)"
-  by (simp add: integer_eq_iff)
+  by transfer rule
 
 lemma int_of_integer_numeral [simp]:
   "int_of_integer (numeral k) = numeral k"
-  using int_of_integer_of_int [of "numeral k"] by simp
+  by transfer rule
 
 lemma int_of_integer_neg_numeral [simp]:
   "int_of_integer (neg_numeral k) = neg_numeral k"
-  by (simp only: neg_numeral_def int_of_integer_uminus) simp
+  by transfer rule
 
 lemma int_of_integer_sub [simp]:
   "int_of_integer (Num.sub k l) = Num.sub k l"
-  by (simp only: Num.sub_def int_of_integer_minus int_of_integer_numeral)
+  by transfer rule
 
 instantiation integer :: "{ring_div, equal, linordered_idom}"
 begin
 
-definition
-  "k div l = of_int (int_of_integer k div int_of_integer l)"
+lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_div [simp]:
-  "int_of_integer (k div l) = int_of_integer k div int_of_integer l"
-  by (simp add: div_integer_def)
+declare div_integer.rep_eq [simp]
 
-definition
-  "k mod l = of_int (int_of_integer k mod int_of_integer l)"
+lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
+  .
+
+declare mod_integer.rep_eq [simp]
 
-lemma int_of_integer_mod [simp]:
-  "int_of_integer (k mod l) = int_of_integer k mod int_of_integer l"
-  by (simp add: mod_integer_def)
+lift_definition abs_integer :: "integer \<Rightarrow> integer"
+  is "abs :: int \<Rightarrow> int"
+  .
 
-definition
-  "\<bar>k\<bar> = of_int \<bar>int_of_integer k\<bar>"
+declare abs_integer.rep_eq [simp]
 
-lemma int_of_integer_abs [simp]:
-  "int_of_integer \<bar>k\<bar> = \<bar>int_of_integer k\<bar>"
-  by (simp add: abs_integer_def)
+lift_definition sgn_integer :: "integer \<Rightarrow> integer"
+  is "sgn :: int \<Rightarrow> int"
+  .
 
-definition
-  "sgn k = of_int (sgn (int_of_integer k))"
+declare sgn_integer.rep_eq [simp]
 
-lemma int_of_integer_sgn [simp]:
-  "int_of_integer (sgn k) = sgn (int_of_integer k)"
-  by (simp add: sgn_integer_def)
+lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+  is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
+  .
 
-definition
-  "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
+lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+  is "less :: int \<Rightarrow> int \<Rightarrow> bool"
+  .
 
-definition
-  "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
-
-definition
-  "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of_integer k) (int_of_integer l)"
+lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+  is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
+  .
 
 instance proof
-qed (auto simp add: integer_eq_iff algebra_simps
-  less_eq_integer_def less_integer_def equal_integer_def equal
-  intro: mult_strict_right_mono)
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold max_def [abs_def]) transfer_prover
+
 lemma int_of_integer_min [simp]:
   "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
-  by (simp add: min_def less_eq_integer_def)
+  by transfer rule
 
 lemma int_of_integer_max [simp]:
   "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
-  by (simp add: max_def less_eq_integer_def)
+  by transfer rule
 
 lemma nat_of_integer_non_positive [simp]:
   "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
-  by (simp add: nat_of_integer_def less_eq_integer_def)
+  by transfer simp
 
 lemma of_nat_of_integer [simp]:
   "of_nat (nat_of_integer k) = max 0 k"
-  by (simp add: nat_of_integer_def integer_eq_iff less_eq_integer_def max_def)
+  by transfer auto
 
 
 subsection {* Code theorems for target language integers *}
@@ -199,29 +228,36 @@
 where
   [simp, code_abbrev]: "Pos = numeral"
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer numeral Pos"
+  by simp transfer_prover
+
 definition Neg :: "num \<Rightarrow> integer"
 where
   [simp, code_abbrev]: "Neg = neg_numeral"
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer neg_numeral Neg"
+  by simp transfer_prover
+
 code_datatype "0::integer" Pos Neg
 
 
 text {* Auxiliary operations *}
 
-definition dup :: "integer \<Rightarrow> integer"
-where
-  [simp]: "dup k = k + k"
+lift_definition dup :: "integer \<Rightarrow> integer"
+  is "\<lambda>k::int. k + k"
+  .
 
 lemma dup_code [code]:
   "dup 0 = 0"
   "dup (Pos n) = Pos (Num.Bit0 n)"
   "dup (Neg n) = Neg (Num.Bit0 n)"
-  unfolding Pos_def Neg_def neg_numeral_def
-  by (simp_all add: numeral_Bit0)
+  by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
 
-definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
-where
-  [simp]: "sub m n = numeral m - numeral n"
+lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
+  is "\<lambda>m n. numeral m - numeral n :: int"
+  .
 
 lemma sub_code [code]:
   "sub Num.One Num.One = 0"
@@ -233,9 +269,7 @@
   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
-  unfolding sub_def dup_def numeral.simps Pos_def Neg_def
-    neg_numeral_def numeral_BitM
-  by (simp_all only: algebra_simps add.comm_neutral)
+  by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
 
 
 text {* Implementations *}
@@ -251,7 +285,7 @@
   "Pos m + Neg n = sub m n"
   "Neg m + Pos n = sub n m"
   "Neg m + Neg n = Neg (m + n)"
-  by simp_all
+  by (transfer, simp)+
 
 lemma uminus_integer_code [code]:
   "uminus 0 = (0::integer)"
@@ -266,7 +300,7 @@
   "Pos m - Neg n = Pos (m + n)"
   "Neg m - Pos n = Neg (m + n)"
   "Neg m - Neg n = sub n m"
-  by simp_all
+  by (transfer, simp)+
 
 lemma abs_integer_code [code]:
   "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
@@ -322,15 +356,18 @@
     (let j = sub k l in
        if j < 0 then (0, Pos k)
        else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
-  by (auto simp add: prod_eq_iff integer_eq_iff Let_def prod_case_beta
-    sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
+  apply (simp add: prod_eq_iff Let_def prod_case_beta)
+  apply transfer
+  apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
+  done
 
-lemma divmod_integer_code [code]: "divmod_integer k l =
-  (if k = 0 then (0, 0) else if l = 0 then (0, k) else
-  (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
-    then divmod_abs k l
-    else (let (r, s) = divmod_abs k l in
-      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+lemma divmod_integer_code [code]:
+  "divmod_integer k l =
+    (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+    (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
+      then divmod_abs k l
+      else (let (r, s) = divmod_abs k l in
+        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
 proof -
   have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0"
     by (auto simp add: sgn_if)
@@ -358,7 +395,7 @@
   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
-  by (simp_all add: equal integer_eq_iff)
+  by (simp_all add: equal)
 
 lemma equal_integer_refl [code nbe]:
   "HOL.equal (k::integer) k \<longleftrightarrow> True"
@@ -374,7 +411,7 @@
   "Neg k \<le> 0 \<longleftrightarrow> True"
   "Neg k \<le> Pos l \<longleftrightarrow> True"
   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
-  by (simp_all add: less_eq_integer_def)
+  by simp_all
 
 lemma less_integer_code [code]:
   "0 < (0::integer) \<longleftrightarrow> False"
@@ -386,21 +423,21 @@
   "Neg k < 0 \<longleftrightarrow> True"
   "Neg k < Pos l \<longleftrightarrow> True"
   "Neg k < Neg l \<longleftrightarrow> l < k"
-  by (simp_all add: less_integer_def)
+  by simp_all
 
-definition integer_of_num :: "num \<Rightarrow> integer"
-where
-  "integer_of_num = numeral"
+lift_definition integer_of_num :: "num \<Rightarrow> integer"
+  is "numeral :: num \<Rightarrow> int"
+  .
 
 lemma integer_of_num [code]:
   "integer_of_num num.One = 1"
   "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
   "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
-  by (simp_all only: Let_def) (simp_all only: integer_of_num_def numeral.simps)
+  by (transfer, simp only: numeral.simps Let_def)+
 
-definition num_of_integer :: "integer \<Rightarrow> num"
-where
-  "num_of_integer = num_of_nat \<circ> nat_of_integer"
+lift_definition num_of_integer :: "integer \<Rightarrow> num"
+  is "num_of_nat \<circ> nat"
+  .
 
 lemma num_of_integer_code [code]:
   "num_of_integer k = (if k \<le> 1 then Num.One
@@ -587,9 +624,11 @@
 typedef natural = "UNIV \<Colon> nat set"
   morphisms nat_of_natural natural_of_nat ..
 
+setup_lifting (no_code) type_definition_natural
+
 lemma natural_eq_iff [termination_simp]:
   "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
-  using nat_of_natural_inject [of m n] ..
+  by transfer rule
 
 lemma natural_eqI:
   "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
@@ -597,168 +636,179 @@
 
 lemma nat_of_natural_of_nat_inverse [simp]:
   "nat_of_natural (natural_of_nat n) = n"
-  using natural_of_nat_inverse [of n] by simp
+  by transfer rule
 
 lemma natural_of_nat_of_natural_inverse [simp]:
   "natural_of_nat (nat_of_natural n) = n"
-  using nat_of_natural_inverse [of n] by simp
+  by transfer rule
 
 instantiation natural :: "{comm_monoid_diff, semiring_1}"
 begin
 
-definition
-  "0 = natural_of_nat 0"
+lift_definition zero_natural :: natural
+  is "0 :: nat"
+  .
 
-lemma nat_of_natural_zero [simp]:
-  "nat_of_natural 0 = 0"
-  by (simp add: zero_natural_def)
+declare zero_natural.rep_eq [simp]
 
-definition
-  "1 = natural_of_nat 1"
+lift_definition one_natural :: natural
+  is "1 :: nat"
+  .
 
-lemma nat_of_natural_one [simp]:
-  "nat_of_natural 1 = 1"
-  by (simp add: one_natural_def)
-
-definition
-  "m + n = natural_of_nat (nat_of_natural m + nat_of_natural n)"
+declare one_natural.rep_eq [simp]
 
-lemma nat_of_natural_plus [simp]:
-  "nat_of_natural (m + n) = nat_of_natural m + nat_of_natural n"
-  by (simp add: plus_natural_def)
+lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
 
-definition
-  "m - n = natural_of_nat (nat_of_natural m - nat_of_natural n)"
+declare plus_natural.rep_eq [simp]
 
-lemma nat_of_natural_minus [simp]:
-  "nat_of_natural (m - n) = nat_of_natural m - nat_of_natural n"
-  by (simp add: minus_natural_def)
+lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
+
+declare minus_natural.rep_eq [simp]
 
-definition
-  "m * n = natural_of_nat (nat_of_natural m * nat_of_natural n)"
+lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
 
-lemma nat_of_natural_times [simp]:
-  "nat_of_natural (m * n) = nat_of_natural m * nat_of_natural n"
-  by (simp add: times_natural_def)
+declare times_natural.rep_eq [simp]
 
 instance proof
-qed (auto simp add: natural_eq_iff algebra_simps)
+qed (transfer, simp add: algebra_simps)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+proof -
+  have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
+    by (unfold of_nat_def [abs_def]) transfer_prover
+  then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+proof -
+  have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+    by transfer_prover
+  then show ?thesis by simp
+qed
+
 lemma nat_of_natural_of_nat [simp]:
   "nat_of_natural (of_nat n) = n"
-  by (induct n) simp_all
+  by transfer rule
 
 lemma natural_of_nat_of_nat [simp, code_abbrev]:
   "natural_of_nat = of_nat"
-  by rule (simp add: natural_eq_iff)
+  by transfer rule
 
 lemma of_nat_of_natural [simp]:
   "of_nat (nat_of_natural n) = n"
-  using natural_of_nat_of_natural_inverse [of n] by simp
+  by transfer rule
 
 lemma nat_of_natural_numeral [simp]:
   "nat_of_natural (numeral k) = numeral k"
-  using nat_of_natural_of_nat [of "numeral k"] by simp
+  by transfer rule
 
 instantiation natural :: "{semiring_div, equal, linordered_semiring}"
 begin
 
-definition
-  "m div n = natural_of_nat (nat_of_natural m div nat_of_natural n)"
+lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
+
+declare div_natural.rep_eq [simp]
 
-lemma nat_of_natural_div [simp]:
-  "nat_of_natural (m div n) = nat_of_natural m div nat_of_natural n"
-  by (simp add: div_natural_def)
+lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
 
-definition
-  "m mod n = natural_of_nat (nat_of_natural m mod nat_of_natural n)"
+declare mod_natural.rep_eq [simp]
 
-lemma nat_of_natural_mod [simp]:
-  "nat_of_natural (m mod n) = nat_of_natural m mod nat_of_natural n"
-  by (simp add: mod_natural_def)
+lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+  is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  .
+
+declare less_eq_natural.rep_eq [termination_simp]
 
-definition
-  [termination_simp]: "m \<le> n \<longleftrightarrow> nat_of_natural m \<le> nat_of_natural n"
+lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+  is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  .
 
-definition
-  [termination_simp]: "m < n \<longleftrightarrow> nat_of_natural m < nat_of_natural n"
+declare less_natural.rep_eq [termination_simp]
 
-definition
-  "HOL.equal m n \<longleftrightarrow> HOL.equal (nat_of_natural m) (nat_of_natural n)"
+lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+  is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  .
 
 instance proof
-qed (auto simp add: natural_eq_iff algebra_simps
-  less_eq_natural_def less_natural_def equal_natural_def equal)
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold max_def [abs_def]) transfer_prover
+
 lemma nat_of_natural_min [simp]:
   "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
-  by (simp add: min_def less_eq_natural_def)
+  by transfer rule
 
 lemma nat_of_natural_max [simp]:
   "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
-  by (simp add: max_def less_eq_natural_def)
+  by transfer rule
 
-definition natural_of_integer :: "integer \<Rightarrow> natural"
-where
-  "natural_of_integer = of_nat \<circ> nat_of_integer"
+lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
+  is "nat :: int \<Rightarrow> nat"
+  .
 
-definition integer_of_natural :: "natural \<Rightarrow> integer"
-where
-  "integer_of_natural = of_nat \<circ> nat_of_natural"
+lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
+  is "of_nat :: nat \<Rightarrow> int"
+  .
 
 lemma natural_of_integer_of_natural [simp]:
   "natural_of_integer (integer_of_natural n) = n"
-  by (simp add: natural_of_integer_def integer_of_natural_def natural_eq_iff)
+  by transfer simp
 
 lemma integer_of_natural_of_integer [simp]:
   "integer_of_natural (natural_of_integer k) = max 0 k"
-  by (simp add: natural_of_integer_def integer_of_natural_def integer_eq_iff)
+  by transfer auto
 
 lemma int_of_integer_of_natural [simp]:
   "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
-  by (simp add: integer_of_natural_def)
+  by transfer rule
 
 lemma integer_of_natural_of_nat [simp]:
   "integer_of_natural (of_nat n) = of_nat n"
-  by (simp add: integer_eq_iff)
+  by transfer rule
 
 lemma [measure_function]:
-  "is_measure nat_of_natural" by (rule is_measure_trivial)
+  "is_measure nat_of_natural"
+  by (rule is_measure_trivial)
 
 
 subsection {* Inductive represenation of target language naturals *}
 
-definition Suc :: "natural \<Rightarrow> natural"
-where
-  "Suc = natural_of_nat \<circ> Nat.Suc \<circ> nat_of_natural"
+lift_definition Suc :: "natural \<Rightarrow> natural"
+  is Nat.Suc
+  .
 
-lemma nat_of_natural_Suc [simp]:
-  "nat_of_natural (Suc n) = Nat.Suc (nat_of_natural n)"
-  by (simp add: Suc_def)
+declare Suc.rep_eq [simp]
 
 rep_datatype "0::natural" Suc
-proof -
-  fix P :: "natural \<Rightarrow> bool"
-  fix n :: natural
-  assume "P 0" then have init: "P (natural_of_nat 0)" by simp
-  assume "\<And>n. P n \<Longrightarrow> P (Suc n)"
-    then have "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (Suc (natural_of_nat n))" .
-    then have step: "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (natural_of_nat (Nat.Suc n))"
-      by (simp add: Suc_def)
-  from init step have "P (natural_of_nat (nat_of_natural n))"
-    by (rule nat.induct)
-  with natural_of_nat_of_natural_inverse show "P n" by simp
-qed (simp_all add: natural_eq_iff)
+  by (transfer, fact nat.induct nat.inject nat.distinct)+
 
 lemma natural_case [case_names nat, cases type: natural]:
   fixes m :: natural
   assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
   shows P
-  by (rule assms [of "nat_of_natural m"]) simp
+  using assms by transfer blast
 
 lemma [simp, code]:
   "natural_size = nat_of_natural"
@@ -778,7 +828,7 @@
 
 lemma natural_decr [termination_simp]:
   "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
-  by (simp add: natural_eq_iff)
+  by transfer simp
 
 lemma natural_zero_minus_one:
   "(0::natural) - 1 = 0"
@@ -786,26 +836,26 @@
 
 lemma Suc_natural_minus_one:
   "Suc n - 1 = n"
-  by (simp add: natural_eq_iff)
+  by transfer simp
 
 hide_const (open) Suc
 
 
 subsection {* Code refinement for target language naturals *}
 
-definition Nat :: "integer \<Rightarrow> natural"
-where
-  "Nat = natural_of_integer"
+lift_definition Nat :: "integer \<Rightarrow> natural"
+  is nat
+  .
 
 lemma [code_post]:
   "Nat 0 = 0"
   "Nat 1 = 1"
   "Nat (numeral k) = numeral k"
-  by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def)
+  by (transfer, simp)+
 
 lemma [code abstype]:
   "Nat (integer_of_natural n) = n"
-  by (unfold Nat_def) (fact natural_of_integer_of_natural)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (natural_of_nat n) = of_nat n"
@@ -817,23 +867,23 @@
 
 lemma [code_abbrev]:
   "natural_of_integer (Code_Numeral_Types.Pos k) = numeral k"
-  by (simp add: nat_of_integer_def natural_of_integer_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural 0 = 0"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural 1 = 1"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (Code_Numeral_Types.Suc n) = integer_of_natural n + 1"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code]:
   "nat_of_natural = nat_of_integer \<circ> integer_of_natural"
-  by (simp add: integer_of_natural_def fun_eq_iff)
+  by transfer (simp add: fun_eq_iff)
 
 lemma [code, code_unfold]:
   "natural_case f g n = (if n = 0 then f else g (n - 1))"
@@ -843,39 +893,39 @@
 
 lemma [code abstract]:
   "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
-  by (simp add: integer_eq_iff of_nat_mult)
+  by transfer (simp add: of_nat_mult)
 
 lemma [code abstract]:
   "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
-  by (simp add: integer_eq_iff zdiv_int)
+  by transfer (simp add: zdiv_int)
 
 lemma [code abstract]:
   "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
-  by (simp add: integer_eq_iff zmod_int)
+  by transfer (simp add: zmod_int)
 
 lemma [code]:
   "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
-  by (simp add: equal natural_eq_iff integer_eq_iff)
+  by transfer (simp add: equal)
 
 lemma [code nbe]:
   "HOL.equal n (n::natural) \<longleftrightarrow> True"
   by (simp add: equal)
 
 lemma [code]:
-  "m \<le> n \<longleftrightarrow> (integer_of_natural m) \<le> integer_of_natural n"
-  by (simp add: less_eq_natural_def less_eq_integer_def)
+  "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
+  by transfer simp
 
 lemma [code]:
-  "m < n \<longleftrightarrow> (integer_of_natural m) < integer_of_natural n"
-  by (simp add: less_natural_def less_integer_def)
+  "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
+  by transfer simp
 
 hide_const (open) Nat
 
--- a/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -15,47 +15,47 @@
 
 lemma [code]:
   "integer_of_int (int_of_integer k) = k"
-  by (simp add: integer_eq_iff)
+  by transfer rule
 
 lemma [code]:
   "Int.Pos = int_of_integer \<circ> integer_of_num"
-  by (simp add: integer_of_num_def fun_eq_iff)
+  by transfer (simp add: fun_eq_iff) 
 
 lemma [code]:
   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
-  by (simp add: integer_of_num_def fun_eq_iff)
+  by transfer (simp add: fun_eq_iff) 
 
 lemma [code_abbrev]:
   "int_of_integer (numeral k) = Int.Pos k"
-  by simp
+  by transfer simp
 
 lemma [code_abbrev]:
   "int_of_integer (neg_numeral k) = Int.Neg k"
-  by simp
+  by transfer simp
   
 lemma [code, symmetric, code_post]:
   "0 = int_of_integer 0"
-  by simp
+  by transfer simp
 
 lemma [code, symmetric, code_post]:
   "1 = int_of_integer 1"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "k + l = int_of_integer (of_int k + of_int l)"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "- k = int_of_integer (- of_int k)"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "k - l = int_of_integer (of_int k - of_int l)"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
-  by simp
+  by transfer simp
 
 lemma [code, code del]:
   "Int.sub = Int.sub" ..
@@ -79,15 +79,15 @@
 
 lemma [code]:
   "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
-  by (simp add: equal integer_eq_iff)
+  by transfer (simp add: equal)
 
 lemma [code]:
   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
-  by (simp add: less_eq_int_def)
+  by transfer rule
 
 lemma [code]:
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
-  by (simp add: less_int_def)
+  by transfer rule
 
 lemma (in ring_1) of_int_code:
   "of_int k = (if k = 0 then 0
@@ -107,7 +107,7 @@
 
 lemma [code]:
   "nat = nat_of_integer \<circ> of_int"
-  by (simp add: fun_eq_iff nat_of_integer_def)
+  by transfer (simp add: fun_eq_iff)
 
 code_modulename SML
   Code_Target_Int Arith
--- a/src/HOL/Library/Code_Target_Nat.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -1,83 +1,80 @@
 (*  Title:      HOL/Library/Code_Target_Nat.thy
-    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
+    Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Implementation of natural numbers by target-language integers *}
 
 theory Code_Target_Nat
-imports Main Code_Numeral_Types Code_Binary_Nat
+imports Code_Abstract_Nat Code_Numeral_Types
 begin
 
 subsection {* Implementation for @{typ nat} *}
 
-definition Nat :: "integer \<Rightarrow> nat"
-where
-  "Nat = nat_of_integer"
+lift_definition Nat :: "integer \<Rightarrow> nat"
+  is nat
+  .
 
 lemma [code_post]:
   "Nat 0 = 0"
   "Nat 1 = 1"
   "Nat (numeral k) = numeral k"
-  by (simp_all add: Nat_def nat_of_integer_def)
+  by (transfer, simp)+
 
 lemma [code_abbrev]:
   "integer_of_nat = of_nat"
-  by (fact integer_of_nat_def)
+  by transfer rule
 
 lemma [code_unfold]:
   "Int.nat (int_of_integer k) = nat_of_integer k"
-  by (simp add: nat_of_integer_def)
+  by transfer rule
 
 lemma [code abstype]:
   "Code_Target_Nat.Nat (integer_of_nat n) = n"
-  by (simp add: Nat_def integer_of_nat_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat (nat_of_integer k) = max 0 k"
-  by (simp add: integer_of_nat_def)
+  by transfer auto
 
 lemma [code_abbrev]:
   "nat_of_integer (numeral k) = nat_of_num k"
-  by (simp add: nat_of_integer_def nat_of_num_numeral)
+  by transfer (simp add: nat_of_num_numeral)
 
 lemma [code abstract]:
   "integer_of_nat (nat_of_num n) = integer_of_num n"
-  by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral)
+  by transfer (simp add: nat_of_num_numeral)
 
 lemma [code abstract]:
   "integer_of_nat 0 = 0"
-  by (simp add: integer_eq_iff integer_of_nat_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat 1 = 1"
-  by (simp add: integer_eq_iff integer_of_nat_def)
+  by transfer simp
+
+lemma [code]:
+  "Suc n = n + 1"
+  by simp
 
 lemma [code abstract]:
   "integer_of_nat (m + n) = of_nat m + of_nat n"
-  by (simp add: integer_eq_iff integer_of_nat_def)
-
-lemma [code abstract]:
-  "integer_of_nat (Code_Binary_Nat.dup n) = Code_Numeral_Types.dup (of_nat n)"
-  by (simp add: integer_eq_iff Code_Binary_Nat.dup_def integer_of_nat_def)
-
-lemma [code, code del]:
-  "Code_Binary_Nat.sub = Code_Binary_Nat.sub" ..
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
-  by (simp add: integer_eq_iff integer_of_nat_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat (m * n) = of_nat m * of_nat n"
-  by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def)
+  by transfer (simp add: of_nat_mult)
 
 lemma [code abstract]:
   "integer_of_nat (m div n) = of_nat m div of_nat n"
-  by (simp add: integer_eq_iff zdiv_int integer_of_nat_def)
+  by transfer (simp add: zdiv_int)
 
 lemma [code abstract]:
   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
-  by (simp add: integer_eq_iff zmod_int integer_of_nat_def)
+  by transfer (simp add: zmod_int)
 
 lemma [code]:
   "Divides.divmod_nat m n = (m div n, m mod n)"
@@ -85,7 +82,7 @@
 
 lemma [code]:
   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
-  by (simp add: equal integer_eq_iff)
+  by transfer (simp add: equal)
 
 lemma [code]:
   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
@@ -97,7 +94,7 @@
 
 lemma num_of_nat_code [code]:
   "num_of_nat = num_of_integer \<circ> of_nat"
-  by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def)
+  by transfer (simp add: fun_eq_iff)
 
 lemma (in semiring_1) of_nat_code:
   "of_nat n = (if n = 0 then 0
@@ -124,7 +121,7 @@
 
 lemma [code abstract]:
   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
-  by (simp add: integer_of_nat_def of_int_of_nat max_def)
+  by transfer auto
 
 code_modulename SML
   Code_Target_Nat Arith
--- a/src/HOL/Library/Finite_Lattice.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Finite_Lattice.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -1,7 +1,7 @@
 (* Author: Alessandro Coglio *)
 
 theory Finite_Lattice
-imports Product_Lattice
+imports Product_Order
 begin
 
 text {* A non-empty finite lattice is a complete lattice.
--- a/src/HOL/Library/Product_Lattice.thy	Thu Feb 14 16:36:21 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,238 +0,0 @@
-(*  Title:      HOL/Library/Product_Lattice.thy
-    Author:     Brian Huffman
-*)
-
-header {* Lattice operations on product types *}
-
-theory Product_Lattice
-imports "~~/src/HOL/Library/Product_plus"
-begin
-
-subsection {* Pointwise ordering *}
-
-instantiation prod :: (ord, ord) ord
-begin
-
-definition
-  "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
-
-definition
-  "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
-
-instance ..
-
-end
-
-lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
-  unfolding less_eq_prod_def by simp
-
-lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
-  unfolding less_eq_prod_def by simp
-
-lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
-  unfolding less_eq_prod_def by simp
-
-lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
-  unfolding less_eq_prod_def by simp
-
-instance prod :: (preorder, preorder) preorder
-proof
-  fix x y z :: "'a \<times> 'b"
-  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
-    by (rule less_prod_def)
-  show "x \<le> x"
-    unfolding less_eq_prod_def
-    by fast
-  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
-    unfolding less_eq_prod_def
-    by (fast elim: order_trans)
-qed
-
-instance prod :: (order, order) order
-  by default auto
-
-
-subsection {* Binary infimum and supremum *}
-
-instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
-begin
-
-definition
-  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
-
-lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
-  unfolding inf_prod_def by simp
-
-lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
-  unfolding inf_prod_def by simp
-
-lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
-  unfolding inf_prod_def by simp
-
-instance
-  by default auto
-
-end
-
-instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
-begin
-
-definition
-  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
-
-lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
-  unfolding sup_prod_def by simp
-
-lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
-  unfolding sup_prod_def by simp
-
-lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
-  unfolding sup_prod_def by simp
-
-instance
-  by default auto
-
-end
-
-instance prod :: (lattice, lattice) lattice ..
-
-instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
-  by default (auto simp add: sup_inf_distrib1)
-
-
-subsection {* Top and bottom elements *}
-
-instantiation prod :: (top, top) top
-begin
-
-definition
-  "top = (top, top)"
-
-lemma fst_top [simp]: "fst top = top"
-  unfolding top_prod_def by simp
-
-lemma snd_top [simp]: "snd top = top"
-  unfolding top_prod_def by simp
-
-lemma Pair_top_top: "(top, top) = top"
-  unfolding top_prod_def by simp
-
-instance
-  by default (auto simp add: top_prod_def)
-
-end
-
-instantiation prod :: (bot, bot) bot
-begin
-
-definition
-  "bot = (bot, bot)"
-
-lemma fst_bot [simp]: "fst bot = bot"
-  unfolding bot_prod_def by simp
-
-lemma snd_bot [simp]: "snd bot = bot"
-  unfolding bot_prod_def by simp
-
-lemma Pair_bot_bot: "(bot, bot) = bot"
-  unfolding bot_prod_def by simp
-
-instance
-  by default (auto simp add: bot_prod_def)
-
-end
-
-instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
-
-instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
-  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
-
-
-subsection {* Complete lattice operations *}
-
-instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
-begin
-
-definition
-  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
-
-definition
-  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
-
-instance
-  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
-    INF_lower SUP_upper le_INF_iff SUP_le_iff)
-
-end
-
-lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
-  unfolding Sup_prod_def by simp
-
-lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
-  unfolding Sup_prod_def by simp
-
-lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
-  unfolding Inf_prod_def by simp
-
-lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
-  unfolding Inf_prod_def by simp
-
-lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
-  by (simp add: SUP_def fst_Sup image_image)
-
-lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
-  by (simp add: SUP_def snd_Sup image_image)
-
-lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
-  by (simp add: INF_def fst_Inf image_image)
-
-lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
-  by (simp add: INF_def snd_Inf image_image)
-
-lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
-  by (simp add: SUP_def Sup_prod_def image_image)
-
-lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
-  by (simp add: INF_def Inf_prod_def image_image)
-
-
-text {* Alternative formulations for set infima and suprema over the product
-of two complete lattices: *}
-
-lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
-by (auto simp: Inf_prod_def INF_def)
-
-lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
-by (auto simp: Sup_prod_def SUP_def)
-
-lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
-by (auto simp: INF_def Inf_prod_def image_compose)
-
-lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
-by (auto simp: SUP_def Sup_prod_def image_compose)
-
-lemma INF_prod_alt_def:
-  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
-by (metis fst_INF snd_INF surjective_pairing)
-
-lemma SUP_prod_alt_def:
-  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
-by (metis fst_SUP snd_SUP surjective_pairing)
-
-
-subsection {* Complete distributive lattices *}
-
-(* Contribution: Alessandro Coglio *)
-
-instance prod ::
-  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof
-  case goal1 thus ?case
-    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
-next
-  case goal2 thus ?case
-    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
-qed
-
-
-end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Product_Lexorder.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -0,0 +1,125 @@
+(*  Title:      HOL/Library/Product_Lexorder.thy
+    Author:     Norbert Voelker
+*)
+
+header {* Lexicographic order on product types *}
+
+theory Product_Lexorder
+imports Main
+begin
+
+instantiation prod :: (ord, ord) ord
+begin
+
+definition
+  "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
+
+definition
+  "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
+
+instance ..
+
+end
+
+lemma less_eq_prod_simp [simp, code]:
+  "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+  by (simp add: less_eq_prod_def)
+
+lemma less_prod_simp [simp, code]:
+  "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
+  by (simp add: less_prod_def)
+
+text {* A stronger version for partial orders. *}
+
+lemma less_prod_def':
+  fixes x y :: "'a::order \<times> 'b::ord"
+  shows "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+  by (auto simp add: less_prod_def le_less)
+
+instance prod :: (preorder, preorder) preorder
+  by default (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
+
+instance prod :: (order, order) order
+  by default (auto simp add: less_eq_prod_def)
+
+instance prod :: (linorder, linorder) linorder
+  by default (auto simp: less_eq_prod_def)
+
+instantiation prod :: (linorder, linorder) distrib_lattice
+begin
+
+definition
+  "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+
+definition
+  "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
+
+instance
+  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+
+end
+
+instantiation prod :: (bot, bot) bot
+begin
+
+definition
+  "bot = (bot, bot)"
+
+instance
+  by default (auto simp add: bot_prod_def)
+
+end
+
+instantiation prod :: (top, top) top
+begin
+
+definition
+  "top = (top, top)"
+
+instance
+  by default (auto simp add: top_prod_def)
+
+end
+
+instance prod :: (wellorder, wellorder) wellorder
+proof
+  fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
+  assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  show "P z"
+  proof (induct z)
+    case (Pair a b)
+    show "P (a, b)"
+    proof (induct a arbitrary: b rule: less_induct)
+      case (less a\<^isub>1) note a\<^isub>1 = this
+      show "P (a\<^isub>1, b)"
+      proof (induct b rule: less_induct)
+        case (less b\<^isub>1) note b\<^isub>1 = this
+        show "P (a\<^isub>1, b\<^isub>1)"
+        proof (rule P)
+          fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
+          show "P p"
+          proof (cases "fst p < a\<^isub>1")
+            case True
+            then have "P (fst p, snd p)" by (rule a\<^isub>1)
+            then show ?thesis by simp
+          next
+            case False
+            with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
+              by (simp_all add: less_prod_def')
+            from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
+            with 1 show ?thesis by simp
+          qed
+        qed
+      qed
+    qed
+  qed
+qed
+
+text {* Legacy lemma bindings *}
+
+lemmas prod_le_def = less_eq_prod_def
+lemmas prod_less_def = less_prod_def
+lemmas prod_less_eq = less_prod_def'
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Product_Order.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -0,0 +1,238 @@
+(*  Title:      HOL/Library/Product_Order.thy
+    Author:     Brian Huffman
+*)
+
+header {* Pointwise order on product types *}
+
+theory Product_Order
+imports "~~/src/HOL/Library/Product_plus"
+begin
+
+subsection {* Pointwise ordering *}
+
+instantiation prod :: (ord, ord) ord
+begin
+
+definition
+  "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
+
+definition
+  "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+
+instance ..
+
+end
+
+lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
+  unfolding less_eq_prod_def by simp
+
+lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
+  unfolding less_eq_prod_def by simp
+
+lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
+  unfolding less_eq_prod_def by simp
+
+lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
+  unfolding less_eq_prod_def by simp
+
+instance prod :: (preorder, preorder) preorder
+proof
+  fix x y z :: "'a \<times> 'b"
+  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+    by (rule less_prod_def)
+  show "x \<le> x"
+    unfolding less_eq_prod_def
+    by fast
+  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
+    unfolding less_eq_prod_def
+    by (fast elim: order_trans)
+qed
+
+instance prod :: (order, order) order
+  by default auto
+
+
+subsection {* Binary infimum and supremum *}
+
+instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
+begin
+
+definition
+  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
+
+lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
+  unfolding inf_prod_def by simp
+
+lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
+  unfolding inf_prod_def by simp
+
+lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
+  unfolding inf_prod_def by simp
+
+instance
+  by default auto
+
+end
+
+instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
+begin
+
+definition
+  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
+
+lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
+  unfolding sup_prod_def by simp
+
+lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
+  unfolding sup_prod_def by simp
+
+lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
+  unfolding sup_prod_def by simp
+
+instance
+  by default auto
+
+end
+
+instance prod :: (lattice, lattice) lattice ..
+
+instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
+  by default (auto simp add: sup_inf_distrib1)
+
+
+subsection {* Top and bottom elements *}
+
+instantiation prod :: (top, top) top
+begin
+
+definition
+  "top = (top, top)"
+
+lemma fst_top [simp]: "fst top = top"
+  unfolding top_prod_def by simp
+
+lemma snd_top [simp]: "snd top = top"
+  unfolding top_prod_def by simp
+
+lemma Pair_top_top: "(top, top) = top"
+  unfolding top_prod_def by simp
+
+instance
+  by default (auto simp add: top_prod_def)
+
+end
+
+instantiation prod :: (bot, bot) bot
+begin
+
+definition
+  "bot = (bot, bot)"
+
+lemma fst_bot [simp]: "fst bot = bot"
+  unfolding bot_prod_def by simp
+
+lemma snd_bot [simp]: "snd bot = bot"
+  unfolding bot_prod_def by simp
+
+lemma Pair_bot_bot: "(bot, bot) = bot"
+  unfolding bot_prod_def by simp
+
+instance
+  by default (auto simp add: bot_prod_def)
+
+end
+
+instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
+
+instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
+  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
+
+
+subsection {* Complete lattice operations *}
+
+instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
+begin
+
+definition
+  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
+
+definition
+  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+
+instance
+  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
+    INF_lower SUP_upper le_INF_iff SUP_le_iff)
+
+end
+
+lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
+  unfolding Sup_prod_def by simp
+
+lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
+  unfolding Sup_prod_def by simp
+
+lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
+  unfolding Inf_prod_def by simp
+
+lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
+  unfolding Inf_prod_def by simp
+
+lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
+  by (simp add: SUP_def fst_Sup image_image)
+
+lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
+  by (simp add: SUP_def snd_Sup image_image)
+
+lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
+  by (simp add: INF_def fst_Inf image_image)
+
+lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
+  by (simp add: INF_def snd_Inf image_image)
+
+lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
+  by (simp add: SUP_def Sup_prod_def image_image)
+
+lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
+  by (simp add: INF_def Inf_prod_def image_image)
+
+
+text {* Alternative formulations for set infima and suprema over the product
+of two complete lattices: *}
+
+lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
+by (auto simp: Inf_prod_def INF_def)
+
+lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
+by (auto simp: Sup_prod_def SUP_def)
+
+lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
+by (auto simp: INF_def Inf_prod_def image_compose)
+
+lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
+by (auto simp: SUP_def Sup_prod_def image_compose)
+
+lemma INF_prod_alt_def:
+  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
+by (metis fst_INF snd_INF surjective_pairing)
+
+lemma SUP_prod_alt_def:
+  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
+by (metis fst_SUP snd_SUP surjective_pairing)
+
+
+subsection {* Complete distributive lattices *}
+
+(* Contribution: Alessandro Coglio *)
+
+instance prod ::
+  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
+proof
+  case goal1 thus ?case
+    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
+next
+  case goal2 thus ?case
+    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
+qed
+
+end
+
--- a/src/HOL/Library/Product_ord.thy	Thu Feb 14 16:36:21 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-(*  Title:      HOL/Library/Product_ord.thy
-    Author:     Norbert Voelker
-*)
-
-header {* Order on product types *}
-
-theory Product_ord
-imports Main
-begin
-
-instantiation prod :: (ord, ord) ord
-begin
-
-definition
-  prod_le_def: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
-
-definition
-  prod_less_def: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
-
-instance ..
-
-end
-
-lemma [code]:
-  "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
-  "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
-  unfolding prod_le_def prod_less_def by simp_all
-
-instance prod :: (preorder, preorder) preorder
-  by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
-
-instance prod :: (order, order) order
-  by default (auto simp add: prod_le_def)
-
-instance prod :: (linorder, linorder) linorder
-  by default (auto simp: prod_le_def)
-
-instantiation prod :: (linorder, linorder) distrib_lattice
-begin
-
-definition
-  inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
-
-definition
-  sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
-
-instance
-  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
-
-end
-
-instantiation prod :: (bot, bot) bot
-begin
-
-definition
-  bot_prod_def: "bot = (bot, bot)"
-
-instance
-  by default (auto simp add: bot_prod_def prod_le_def)
-
-end
-
-instantiation prod :: (top, top) top
-begin
-
-definition
-  top_prod_def: "top = (top, top)"
-
-instance
-  by default (auto simp add: top_prod_def prod_le_def)
-
-end
-
-text {* A stronger version of the definition holds for partial orders. *}
-
-lemma prod_less_eq:
-  fixes x y :: "'a::order \<times> 'b::ord"
-  shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)"
-  unfolding prod_less_def fst_conv snd_conv le_less by auto
-
-instance prod :: (wellorder, wellorder) wellorder
-proof
-  fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
-  assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
-  show "P z"
-  proof (induct z)
-    case (Pair a b)
-    show "P (a, b)"
-    proof (induct a arbitrary: b rule: less_induct)
-      case (less a\<^isub>1) note a\<^isub>1 = this
-      show "P (a\<^isub>1, b)"
-      proof (induct b rule: less_induct)
-        case (less b\<^isub>1) note b\<^isub>1 = this
-        show "P (a\<^isub>1, b\<^isub>1)"
-        proof (rule P)
-          fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
-          show "P p"
-          proof (cases "fst p < a\<^isub>1")
-            case True
-            then have "P (fst p, snd p)" by (rule a\<^isub>1)
-            then show ?thesis by simp
-          next
-            case False
-            with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
-              by (simp_all add: prod_less_eq)
-            from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
-            with 1 show ?thesis by simp
-          qed
-        qed
-      qed
-    qed
-  qed
-qed
-
-end
--- a/src/HOL/Library/RBT_Set.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
 header {* Implementation of sets using RBT trees *}
 
 theory RBT_Set
-imports RBT Product_ord
+imports RBT Product_Lexorder
 begin
 
 (*
--- a/src/HOL/Lifting.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Lifting.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -6,7 +6,7 @@
 header {* Lifting package *}
 
 theory Lifting
-imports Plain Equiv_Relations Transfer
+imports Equiv_Relations Transfer
 keywords
   "print_quotmaps" "print_quotients" :: diag and
   "lift_definition" :: thy_goal and
--- a/src/HOL/List.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/List.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Plain Presburger Code_Numeral Quotient ATP
+imports Presburger Code_Numeral Quotient ATP
 begin
 
 datatype 'a list =
--- a/src/HOL/Main.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Main.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Predicate_Compile Nitpick
+imports Predicate_Compile Nitpick Extraction
 begin
 
 text {*
@@ -11,4 +11,18 @@
 
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf (infixl "\<sqinter>" 70) and
+  sup (infixl "\<squnion>" 65) and
+  Inf ("\<Sqinter>_" [900] 900) and
+  Sup ("\<Squnion>_" [900] 900)
+
+no_syntax (xsymbols)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
 end
--- a/src/HOL/Plain.thy	Thu Feb 14 16:36:21 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-header {* Plain HOL *}
-
-theory Plain
-imports Datatype FunDef Extraction Metis Num
-begin
-
-text {*
-  Plain bootstrap of fundamental HOL tools and packages; does not
-  include @{text Hilbert_Choice}.
-*}
-
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900)
-
-no_syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-end
--- a/src/HOL/Predicate.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Predicate.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -8,20 +8,6 @@
 imports List
 begin
 
-notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900)
-
-syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
 subsection {* The type of predicate enumerations (a monad) *}
 
 datatype 'a pred = Pred "'a \<Rightarrow> bool"
@@ -729,20 +715,8 @@
   by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
 
 no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900) and
   bind (infixl "\<guillemotright>=" 70)
 
-no_syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
 hide_type (open) pred seq
 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
--- a/src/HOL/Quotient.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Quotient.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
 header {* Definition of Quotient Types *}
 
 theory Quotient
-imports Plain Hilbert_Choice Equiv_Relations Lifting
+imports Hilbert_Choice Equiv_Relations Lifting
 keywords
   "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
   "quotient_type" :: thy_goal and "/" and
--- a/src/HOL/ROOT	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/ROOT	Thu Feb 14 17:06:15 2013 +0100
@@ -26,6 +26,8 @@
     Finite_Lattice
     Code_Char_chr
     Code_Char_ord
+    Product_Lexorder
+    Product_Order
     Code_Integer
     Efficient_Nat
     (* Code_Prolog  FIXME cf. 76965c356d2a *)
--- a/src/HOL/Record.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Record.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -9,7 +9,7 @@
 header {* Extensible records with structural subtyping *}
 
 theory Record
-imports Plain Quickcheck_Narrowing
+imports Quickcheck_Narrowing
 keywords "record" :: thy_decl
 begin
 
--- a/src/HOL/Transfer.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Transfer.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
 header {* Generic theorem transfer using relations *}
 
 theory Transfer
-imports Plain Hilbert_Choice
+imports Hilbert_Choice
 begin
 
 subsection {* Relator for function space *}
--- a/src/HOL/Typerep.thy	Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Typerep.thy	Thu Feb 14 17:06:15 2013 +0100
@@ -3,7 +3,7 @@
 header {* Reflecting Pure types into HOL *}
 
 theory Typerep
-imports Plain String
+imports String
 begin
 
 datatype typerep = Typerep String.literal "typerep list"