# HG changeset patch
# User haftmann
# Date 1330807898 -3600
# Node ID f0285e69d70497c870a673899cd0602e88dd22aa
# Parent  150f37dad503c84c7272e2404d5e173b57317ab7
distribution of compatibility theories

diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOL4/Compatibility.thy
--- a/src/HOL/Import/HOL4/Compatibility.thy	Sat Mar 03 21:42:41 2012 +0100
+++ b/src/HOL/Import/HOL4/Compatibility.thy	Sat Mar 03 21:51:38 2012 +0100
@@ -1,5 +1,504 @@
+(*  Title:      HOL/Import/HOL4/Compatibility.thy
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory Compatibility
-imports Main
+imports
+  Complex_Main
+  "~~/src/HOL/Old_Number_Theory/Primes"
+  "~~/src/HOL/Library/ContNotDenum"
+  "~~/src/HOL/Import/HOL4Setup"
 begin
 
+abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
+no_notation differentiable (infixl "differentiable" 60)
+no_notation sums (infixr "sums" 80)
+
+lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
+  by auto
+
+lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))"
+  by auto
+
+definition LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b" where
+  "LET f s == f s"
+
+lemma [hol4rew]: "LET f s = Let s f"
+  by (simp add: LET_def Let_def)
+
+lemmas [hol4rew] = ONE_ONE_rew
+
+lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
+  by simp
+
+lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
+  by safe
+
+(*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
+  by simp*)
+
+primrec ISL :: "'a + 'b => bool" where
+  "ISL (Inl x) = True"
+| "ISL (Inr x) = False"
+
+primrec ISR :: "'a + 'b => bool" where
+  "ISR (Inl x) = False"
+| "ISR (Inr x) = True"
+
+lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
+  by simp
+
+lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
+  by simp
+
+primrec OUTL :: "'a + 'b => 'a" where
+  "OUTL (Inl x) = x"
+
+primrec OUTR :: "'a + 'b => 'b" where
+  "OUTR (Inr x) = x"
+
+lemma OUTL: "OUTL (Inl x) = x"
+  by simp
+
+lemma OUTR: "OUTR (Inr x) = x"
+  by simp
+
+lemma sum_axiom: "EX! h. h o Inl = f & h o Inr = g"
+  apply (intro allI ex1I[of _ "sum_case f g"] conjI)
+  apply (simp_all add: o_def fun_eq_iff)
+  apply (rule)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
+  by simp
+
+lemma one: "ALL v. v = ()"
+  by simp
+
+lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
+  by simp
+
+lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
+  by simp
+
+primrec IS_SOME :: "'a option => bool" where
+  "IS_SOME (Some x) = True"
+| "IS_SOME None = False"
+
+primrec IS_NONE :: "'a option => bool" where
+  "IS_NONE (Some x) = False"
+| "IS_NONE None = True"
+
+lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
+  by simp
+
+lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
+  by simp
+
+primrec OPTION_JOIN :: "'a option option => 'a option" where
+  "OPTION_JOIN None = None"
+| "OPTION_JOIN (Some x) = x"
+
+lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
+  by simp
+
+lemma PAIR: "(fst x,snd x) = x"
+  by simp
+
+lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
+  by (simp add: map_pair_def split_def)
+
+lemma pair_case_def: "split = split"
+  ..
+
+lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
+  by auto
+
+definition nat_gt :: "nat => nat => bool" where
+  "nat_gt == %m n. n < m"
+
+definition nat_ge :: "nat => nat => bool" where
+  "nat_ge == %m n. nat_gt m n | m = n"
+
+lemma [hol4rew]: "nat_gt m n = (n < m)"
+  by (simp add: nat_gt_def)
+
+lemma [hol4rew]: "nat_ge m n = (n <= m)"
+  by (auto simp add: nat_ge_def nat_gt_def)
+
+lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)"
+  by simp
+
+lemma GREATER_OR_EQ: "ALL m n. n <= (m::nat) = (n < m | m = n)"
+  by auto
+
+lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
+proof safe
+  assume 1: "m < n"
+  def P == "%n. n <= m"
+  have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
+  proof (auto simp add: P_def)
+    assume "n <= m"
+    with 1
+    show False
+      by auto
+  qed
+  thus "? P. (!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
+    by auto
+next
+  fix P
+  assume alln: "!n. P (Suc n) \<longrightarrow> P n"
+  assume pm: "P m"
+  assume npn: "~P n"
+  have "!k q. q + k = m \<longrightarrow> P q"
+  proof
+    fix k
+    show "!q. q + k = m \<longrightarrow> P q"
+    proof (induct k,simp_all)
+      show "P m" by fact
+    next
+      fix k
+      assume ind: "!q. q + k = m \<longrightarrow> P q"
+      show "!q. Suc (q + k) = m \<longrightarrow> P q"
+      proof (rule+)
+        fix q
+        assume "Suc (q + k) = m"
+        hence "(Suc q) + k = m"
+          by simp
+        with ind
+        have psq: "P (Suc q)"
+          by simp
+        from alln
+        have "P (Suc q) --> P q"
+          ..
+        with psq
+        show "P q"
+          by simp
+      qed
+    qed
+  qed
+  hence "!q. q + (m - n) = m \<longrightarrow> P q"
+    ..
+  hence hehe: "n + (m - n) = m \<longrightarrow> P n"
+    ..
+  show "m < n"
+  proof (rule classical)
+    assume "~(m<n)"
+    hence "n <= m"
+      by simp
+    with hehe
+    have "P n"
+      by simp
+    with npn
+    show "m < n"
+      ..
+  qed
+qed
+
+definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where
+  "FUNPOW f n == f ^^ n"
+
+lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) &
+  (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))"
+  by (simp add: funpow_swap1)
+
+lemma [hol4rew]: "FUNPOW f n = f ^^ n"
+  by (simp add: FUNPOW_def)
+
+lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
+  by simp
+
+lemma MULT: "(!n. (0::nat) * n = 0) & (!m n. Suc m * n = m * n + n)"
+  by simp
+
+lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
+  by (simp) arith
+
+lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
+  by (simp add: max_def)
+
+lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)"
+  by (simp add: min_def)
+
+lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)"
+  by simp
+
+definition ALT_ZERO :: nat where 
+  "ALT_ZERO == 0"
+
+definition NUMERAL_BIT1 :: "nat \<Rightarrow> nat" where 
+  "NUMERAL_BIT1 n == n + (n + Suc 0)"
+
+definition NUMERAL_BIT2 :: "nat \<Rightarrow> nat" where 
+  "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
+
+definition NUMERAL :: "nat \<Rightarrow> nat" where 
+  "NUMERAL x == x"
+
+lemma [hol4rew]: "NUMERAL ALT_ZERO = 0"
+  by (simp add: ALT_ZERO_def NUMERAL_def)
+
+lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1"
+  by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def)
+
+lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2"
+  by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def)
+
+lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)"
+  by auto
+
+lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
+  by simp
+
+lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
+  by (auto simp add: dvd_def)
+
+lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
+  by simp
+
+primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
+  "list_size f [] = 0"
+| "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
+
+lemma list_size_def': "(!f. list_size f [] = 0) &
+         (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
+  by simp
+
+lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \<longrightarrow>  v = v') &
+           (!a0 a1. (M' = a0#a1) \<longrightarrow> (f a0 a1 = f' a0 a1)) -->
+           (list_case v f M = list_case v' f' M')"
+proof clarify
+  fix M M' v f
+  assume 1: "M' = [] \<longrightarrow> v = v'"
+    and 2: "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
+  show "list_case v f M' = list_case v' f' M'"
+  proof (rule List.list.case_cong)
+    show "M' = M'"
+      ..
+  next
+    assume "M' = []"
+    with 1 2
+    show "v = v'"
+      by auto
+  next
+    fix a0 a1
+    assume "M' = a0 # a1"
+    with 1 2
+    show "f a0 a1 = f' a0 a1"
+      by auto
+  qed
+qed
+
+lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))"
+proof safe
+  fix f0 f1
+  def fn == "list_rec f0 f1"
+  have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
+    by (simp add: fn_def)
+  thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
+    by auto
+qed
+
+lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)"
+proof safe
+  def fn == "list_rec x (%h t r. f r h t)"
+  have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
+    by (simp add: fn_def)
+  thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
+    by auto
+next
+  fix fn1 fn2
+  assume 1: "ALL h t. fn1 (h # t) = f (fn1 t) h t"
+  assume 2: "ALL h t. fn2 (h # t) = f (fn2 t) h t"
+  assume 3: "fn2 [] = fn1 []"
+  show "fn1 = fn2"
+  proof
+    fix xs
+    show "fn1 xs = fn2 xs"
+      by (induct xs) (simp_all add: 1 2 3) 
+  qed
+qed
+
+lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
+  by (simp add: null_def)
+
+definition sum :: "nat list \<Rightarrow> nat" where
+  "sum l == foldr (op +) l 0"
+
+lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)"
+  by (simp add: sum_def)
+
+lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)"
+  by simp
+
+lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))"
+  by simp
+
+lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))"
+  by simp
+
+lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
+  by simp
+
+lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
+  by (simp add: member_def)
+
+lemma FILTER: "(!P. filter P [] = []) & (!P h t.
+           filter P (h#t) = (if P h then h#filter P t else filter P t))"
+  by simp
+
+lemma REPLICATE: "(ALL x. replicate 0 x = []) &
+  (ALL n x. replicate (Suc n) x = x # replicate n x)"
+  by simp
+
+definition FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b" where
+  "FOLDR f e l == foldr f l e"
+
+lemma [hol4rew]: "FOLDR f e l = foldr f l e"
+  by (simp add: FOLDR_def)
+
+lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))"
+  by simp
+
+lemma FOLDL: "(!f e. foldl f e [] = e) & (!f e x l. foldl f e (x#l) = foldl f (f e x) l)"
+  by simp
+
+lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
+  by simp
+
+lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
+  by simp
+
+primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where
+  map2_Nil: "map2 f [] l2 = []"
+| map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
+
+lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
+  by simp
+
+lemma list_INDUCT: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !l. P l"
+proof
+  fix l
+  assume "P []"
+  assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
+  show "P l"
+  proof (induct l)
+    show "P []" by fact
+  next
+    fix h t
+    assume "P t"
+    with allt
+    have "!h. P (h # t)"
+      by auto
+    thus "P (h # t)"
+      ..
+  qed
+qed
+
+lemma list_CASES: "(l = []) | (? t h. l = h#t)"
+  by (induct l,auto)
+
+definition ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list" where
+  "ZIP == %(a,b). zip a b"
+
+lemma ZIP: "(zip [] [] = []) &
+  (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)"
+  by simp
+
+lemma [hol4rew]: "ZIP (a,b) = zip a b"
+  by (simp add: ZIP_def)
+
+primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where
+  unzip_Nil: "unzip [] = ([],[])"
+| unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
+
+lemma UNZIP: "(unzip [] = ([],[])) &
+         (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
+  by (simp add: Let_def)
+
+lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
+  by simp
+
+lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)"
+proof safe
+  fix x z
+  assume allx: "ALL x. P x \<longrightarrow> 0 < x"
+  assume px: "P x"
+  assume allx': "ALL x. P x \<longrightarrow> x < z"
+  have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
+  proof (rule posreal_complete)
+    from px
+    show "EX x. x : Collect P"
+      by auto
+  next
+    from allx'
+    show "EX y. ALL x : Collect P. x < y"
+      apply simp
+      ..
+  qed
+  thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)"
+    by simp
+qed
+
+lemma REAL_10: "~((1::real) = 0)"
+  by simp
+
+lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
+  by simp
+
+lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
+  by simp
+
+lemma REAL_ADD_LINV:  "-x + x = (0::real)"
+  by simp
+
+lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1"
+  by simp
+
+lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
+  by auto
+
+lemma [hol4rew]: "real (0::nat) = 0"
+  by simp
+
+lemma [hol4rew]: "real (1::nat) = 1"
+  by simp
+
+lemma [hol4rew]: "real (2::nat) = 2"
+  by simp
+
+lemma real_lte: "((x::real) <= y) = (~(y < x))"
+  by auto
+
+lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)"
+  by (simp add: real_of_nat_Suc)
+
+lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
+  by (simp add: abs_if)
+
+lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
+  by simp
+
+definition real_gt :: "real => real => bool" where 
+  "real_gt == %x y. y < x"
+
+lemma [hol4rew]: "real_gt x y = (y < x)"
+  by (simp add: real_gt_def)
+
+lemma real_gt: "ALL x (y::real). (y < x) = (y < x)"
+  by simp
+
+definition real_ge :: "real => real => bool" where
+  "real_ge x y == y <= x"
+
+lemma [hol4rew]: "real_ge x y = (y <= x)"
+  by (simp add: real_ge_def)
+
+lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
+  by simp
+
+definition [hol4rew]: "list_mem x xs = List.member xs x"
+
 end
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Sat Mar 03 21:42:41 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,504 +0,0 @@
-(*  Title:      HOL/Import/HOL4Compat.thy
-    Author:     Sebastian Skalberg (TU Muenchen)
-*)
-
-theory HOL4Compat
-imports
-  HOL4Setup
-  Complex_Main
-  "~~/src/HOL/Old_Number_Theory/Primes"
-  "~~/src/HOL/Library/ContNotDenum"
-begin
-
-abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
-no_notation differentiable (infixl "differentiable" 60)
-no_notation sums (infixr "sums" 80)
-
-lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
-  by auto
-
-lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))"
-  by auto
-
-definition LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b" where
-  "LET f s == f s"
-
-lemma [hol4rew]: "LET f s = Let s f"
-  by (simp add: LET_def Let_def)
-
-lemmas [hol4rew] = ONE_ONE_rew
-
-lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
-  by simp
-
-lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
-  by safe
-
-(*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
-  by simp*)
-
-primrec ISL :: "'a + 'b => bool" where
-  "ISL (Inl x) = True"
-| "ISL (Inr x) = False"
-
-primrec ISR :: "'a + 'b => bool" where
-  "ISR (Inl x) = False"
-| "ISR (Inr x) = True"
-
-lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
-  by simp
-
-lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
-  by simp
-
-primrec OUTL :: "'a + 'b => 'a" where
-  "OUTL (Inl x) = x"
-
-primrec OUTR :: "'a + 'b => 'b" where
-  "OUTR (Inr x) = x"
-
-lemma OUTL: "OUTL (Inl x) = x"
-  by simp
-
-lemma OUTR: "OUTR (Inr x) = x"
-  by simp
-
-lemma sum_axiom: "EX! h. h o Inl = f & h o Inr = g"
-  apply (intro allI ex1I[of _ "sum_case f g"] conjI)
-  apply (simp_all add: o_def fun_eq_iff)
-  apply (rule)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
-  by simp
-
-lemma one: "ALL v. v = ()"
-  by simp
-
-lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
-  by simp
-
-lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
-  by simp
-
-primrec IS_SOME :: "'a option => bool" where
-  "IS_SOME (Some x) = True"
-| "IS_SOME None = False"
-
-primrec IS_NONE :: "'a option => bool" where
-  "IS_NONE (Some x) = False"
-| "IS_NONE None = True"
-
-lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
-  by simp
-
-lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
-  by simp
-
-primrec OPTION_JOIN :: "'a option option => 'a option" where
-  "OPTION_JOIN None = None"
-| "OPTION_JOIN (Some x) = x"
-
-lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
-  by simp
-
-lemma PAIR: "(fst x,snd x) = x"
-  by simp
-
-lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
-  by (simp add: map_pair_def split_def)
-
-lemma pair_case_def: "split = split"
-  ..
-
-lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
-  by auto
-
-definition nat_gt :: "nat => nat => bool" where
-  "nat_gt == %m n. n < m"
-
-definition nat_ge :: "nat => nat => bool" where
-  "nat_ge == %m n. nat_gt m n | m = n"
-
-lemma [hol4rew]: "nat_gt m n = (n < m)"
-  by (simp add: nat_gt_def)
-
-lemma [hol4rew]: "nat_ge m n = (n <= m)"
-  by (auto simp add: nat_ge_def nat_gt_def)
-
-lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)"
-  by simp
-
-lemma GREATER_OR_EQ: "ALL m n. n <= (m::nat) = (n < m | m = n)"
-  by auto
-
-lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
-proof safe
-  assume 1: "m < n"
-  def P == "%n. n <= m"
-  have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
-  proof (auto simp add: P_def)
-    assume "n <= m"
-    with 1
-    show False
-      by auto
-  qed
-  thus "? P. (!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
-    by auto
-next
-  fix P
-  assume alln: "!n. P (Suc n) \<longrightarrow> P n"
-  assume pm: "P m"
-  assume npn: "~P n"
-  have "!k q. q + k = m \<longrightarrow> P q"
-  proof
-    fix k
-    show "!q. q + k = m \<longrightarrow> P q"
-    proof (induct k,simp_all)
-      show "P m" by fact
-    next
-      fix k
-      assume ind: "!q. q + k = m \<longrightarrow> P q"
-      show "!q. Suc (q + k) = m \<longrightarrow> P q"
-      proof (rule+)
-        fix q
-        assume "Suc (q + k) = m"
-        hence "(Suc q) + k = m"
-          by simp
-        with ind
-        have psq: "P (Suc q)"
-          by simp
-        from alln
-        have "P (Suc q) --> P q"
-          ..
-        with psq
-        show "P q"
-          by simp
-      qed
-    qed
-  qed
-  hence "!q. q + (m - n) = m \<longrightarrow> P q"
-    ..
-  hence hehe: "n + (m - n) = m \<longrightarrow> P n"
-    ..
-  show "m < n"
-  proof (rule classical)
-    assume "~(m<n)"
-    hence "n <= m"
-      by simp
-    with hehe
-    have "P n"
-      by simp
-    with npn
-    show "m < n"
-      ..
-  qed
-qed
-
-definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where
-  "FUNPOW f n == f ^^ n"
-
-lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) &
-  (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))"
-  by (simp add: funpow_swap1)
-
-lemma [hol4rew]: "FUNPOW f n = f ^^ n"
-  by (simp add: FUNPOW_def)
-
-lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
-  by simp
-
-lemma MULT: "(!n. (0::nat) * n = 0) & (!m n. Suc m * n = m * n + n)"
-  by simp
-
-lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
-  by (simp) arith
-
-lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
-  by (simp add: max_def)
-
-lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)"
-  by (simp add: min_def)
-
-lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)"
-  by simp
-
-definition ALT_ZERO :: nat where 
-  "ALT_ZERO == 0"
-
-definition NUMERAL_BIT1 :: "nat \<Rightarrow> nat" where 
-  "NUMERAL_BIT1 n == n + (n + Suc 0)"
-
-definition NUMERAL_BIT2 :: "nat \<Rightarrow> nat" where 
-  "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
-
-definition NUMERAL :: "nat \<Rightarrow> nat" where 
-  "NUMERAL x == x"
-
-lemma [hol4rew]: "NUMERAL ALT_ZERO = 0"
-  by (simp add: ALT_ZERO_def NUMERAL_def)
-
-lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1"
-  by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def)
-
-lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2"
-  by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def)
-
-lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)"
-  by auto
-
-lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
-  by simp
-
-lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
-  by (auto simp add: dvd_def)
-
-lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
-  by simp
-
-primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
-  "list_size f [] = 0"
-| "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
-
-lemma list_size_def': "(!f. list_size f [] = 0) &
-         (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
-  by simp
-
-lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \<longrightarrow>  v = v') &
-           (!a0 a1. (M' = a0#a1) \<longrightarrow> (f a0 a1 = f' a0 a1)) -->
-           (list_case v f M = list_case v' f' M')"
-proof clarify
-  fix M M' v f
-  assume 1: "M' = [] \<longrightarrow> v = v'"
-    and 2: "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
-  show "list_case v f M' = list_case v' f' M'"
-  proof (rule List.list.case_cong)
-    show "M' = M'"
-      ..
-  next
-    assume "M' = []"
-    with 1 2
-    show "v = v'"
-      by auto
-  next
-    fix a0 a1
-    assume "M' = a0 # a1"
-    with 1 2
-    show "f a0 a1 = f' a0 a1"
-      by auto
-  qed
-qed
-
-lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))"
-proof safe
-  fix f0 f1
-  def fn == "list_rec f0 f1"
-  have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
-    by (simp add: fn_def)
-  thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
-    by auto
-qed
-
-lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)"
-proof safe
-  def fn == "list_rec x (%h t r. f r h t)"
-  have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
-    by (simp add: fn_def)
-  thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
-    by auto
-next
-  fix fn1 fn2
-  assume 1: "ALL h t. fn1 (h # t) = f (fn1 t) h t"
-  assume 2: "ALL h t. fn2 (h # t) = f (fn2 t) h t"
-  assume 3: "fn2 [] = fn1 []"
-  show "fn1 = fn2"
-  proof
-    fix xs
-    show "fn1 xs = fn2 xs"
-      by (induct xs) (simp_all add: 1 2 3) 
-  qed
-qed
-
-lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
-  by (simp add: null_def)
-
-definition sum :: "nat list \<Rightarrow> nat" where
-  "sum l == foldr (op +) l 0"
-
-lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)"
-  by (simp add: sum_def)
-
-lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)"
-  by simp
-
-lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))"
-  by simp
-
-lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))"
-  by simp
-
-lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
-  by simp
-
-lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
-  by (simp add: member_def)
-
-lemma FILTER: "(!P. filter P [] = []) & (!P h t.
-           filter P (h#t) = (if P h then h#filter P t else filter P t))"
-  by simp
-
-lemma REPLICATE: "(ALL x. replicate 0 x = []) &
-  (ALL n x. replicate (Suc n) x = x # replicate n x)"
-  by simp
-
-definition FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b" where
-  "FOLDR f e l == foldr f l e"
-
-lemma [hol4rew]: "FOLDR f e l = foldr f l e"
-  by (simp add: FOLDR_def)
-
-lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))"
-  by simp
-
-lemma FOLDL: "(!f e. foldl f e [] = e) & (!f e x l. foldl f e (x#l) = foldl f (f e x) l)"
-  by simp
-
-lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
-  by simp
-
-lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
-  by simp
-
-primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where
-  map2_Nil: "map2 f [] l2 = []"
-| map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
-
-lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
-  by simp
-
-lemma list_INDUCT: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !l. P l"
-proof
-  fix l
-  assume "P []"
-  assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
-  show "P l"
-  proof (induct l)
-    show "P []" by fact
-  next
-    fix h t
-    assume "P t"
-    with allt
-    have "!h. P (h # t)"
-      by auto
-    thus "P (h # t)"
-      ..
-  qed
-qed
-
-lemma list_CASES: "(l = []) | (? t h. l = h#t)"
-  by (induct l,auto)
-
-definition ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list" where
-  "ZIP == %(a,b). zip a b"
-
-lemma ZIP: "(zip [] [] = []) &
-  (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)"
-  by simp
-
-lemma [hol4rew]: "ZIP (a,b) = zip a b"
-  by (simp add: ZIP_def)
-
-primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where
-  unzip_Nil: "unzip [] = ([],[])"
-| unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
-
-lemma UNZIP: "(unzip [] = ([],[])) &
-         (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
-  by (simp add: Let_def)
-
-lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
-  by simp
-
-lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)"
-proof safe
-  fix x z
-  assume allx: "ALL x. P x \<longrightarrow> 0 < x"
-  assume px: "P x"
-  assume allx': "ALL x. P x \<longrightarrow> x < z"
-  have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
-  proof (rule posreal_complete)
-    from px
-    show "EX x. x : Collect P"
-      by auto
-  next
-    from allx'
-    show "EX y. ALL x : Collect P. x < y"
-      apply simp
-      ..
-  qed
-  thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)"
-    by simp
-qed
-
-lemma REAL_10: "~((1::real) = 0)"
-  by simp
-
-lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
-  by simp
-
-lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
-  by simp
-
-lemma REAL_ADD_LINV:  "-x + x = (0::real)"
-  by simp
-
-lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1"
-  by simp
-
-lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
-  by auto
-
-lemma [hol4rew]: "real (0::nat) = 0"
-  by simp
-
-lemma [hol4rew]: "real (1::nat) = 1"
-  by simp
-
-lemma [hol4rew]: "real (2::nat) = 2"
-  by simp
-
-lemma real_lte: "((x::real) <= y) = (~(y < x))"
-  by auto
-
-lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)"
-  by (simp add: real_of_nat_Suc)
-
-lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
-  by (simp add: abs_if)
-
-lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
-  by simp
-
-definition real_gt :: "real => real => bool" where 
-  "real_gt == %x y. y < x"
-
-lemma [hol4rew]: "real_gt x y = (y < x)"
-  by (simp add: real_gt_def)
-
-lemma real_gt: "ALL x (y::real). (y < x) = (y < x)"
-  by simp
-
-definition real_ge :: "real => real => bool" where
-  "real_ge x y == y <= x"
-
-lemma [hol4rew]: "real_ge x y = (y <= x)"
-  by (simp add: real_ge_def)
-
-lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
-  by simp
-
-definition [hol4rew]: "list_mem x xs = List.member xs x"
-
-end
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOLLightCompat.thy
--- a/src/HOL/Import/HOLLightCompat.thy	Sat Mar 03 21:42:41 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,350 +0,0 @@
-(*  Title:      HOL/Import/HOLLightCompat.thy
-    Author:     Steven Obua and Sebastian Skalberg, TU Muenchen
-    Author:     Cezary Kaliszyk
-*)
-
-theory HOLLightCompat
-imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set"
-  HOLLightList HOLLightReal HOLLightInt HOL4Setup
-begin
-
-(* list *)
-lemmas [hol4rew] = list_el_def member_def list_mem_def
-(* int *)
-lemmas [hol4rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def
-(* real *)
-lemma [hol4rew]:
-  "real (0::nat) = 0" "real (1::nat) = 1" "real (2::nat) = 2"
-  by simp_all
-
-lemma one:
-  "\<forall>v. v = ()"
-  by simp
-
-lemma num_Axiom:
-  "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
-  apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma SUC_INJ:
-  "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
-  by simp
-
-lemma PAIR:
-  "(fst x, snd x) = x"
-  by simp
-
-lemma EXISTS_UNIQUE_THM:
-  "(Ex1 P) = (Ex P & (\<forall>x y. P x & P y --> (x = y)))"
-  by auto
-
-lemma DEF__star_:
-  "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac x)
-  apply auto
-  done
-
-lemma DEF__slash__backslash_:
-  "(t1 \<and> t2) = ((\<lambda>f. f t1 t2 :: bool) = (\<lambda>f. f True True))"
-  unfolding fun_eq_iff
-  by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \<and> b)"], simp)
-
-lemma DEF__lessthan__equal_:
-  "op \<le> = (SOME u. (\<forall>m. u m 0 = (m = 0)) \<and> (\<forall>m n. u m (Suc n) = (m = Suc n \<or> u m n)))"
-  apply (rule some_equality[symmetric])
-  apply auto[1]
-  apply (simp add: fun_eq_iff)
-  apply (intro allI)
-  apply (induct_tac xa)
-  apply auto
-  done
-
-lemma DEF__lessthan_:
-  "op < = (SOME u. (\<forall>m. u m 0 = False) \<and> (\<forall>m n. u m (Suc n) = (m = n \<or> u m n)))"
-  apply (rule some_equality[symmetric])
-  apply auto[1]
-  apply (simp add: fun_eq_iff)
-  apply (intro allI)
-  apply (induct_tac xa)
-  apply auto
-  done
-
-lemma DEF__greaterthan__equal_:
-  "(op \<ge>) = (%u ua. ua \<le> u)"
-  by (simp)
-
-lemma DEF__greaterthan_:
-  "(op >) = (%u ua. ua < u)"
-  by (simp)
-
-lemma DEF__equal__equal__greaterthan_:
-  "(t1 \<longrightarrow> t2) = ((t1 \<and> t2) = t1)"
-  by auto
-
-lemma DEF_WF:
-  "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
-  unfolding fun_eq_iff
-proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
-  fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
-  assume "P xa"
-  then show "xa \<in> Collect P" by simp
-next
-  fix x P xa z
-  assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
-  then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
-next
-  fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
-  assume a: "xa \<in> Q"
-  assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
-  then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
-  then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
-qed
-
-lemma DEF_UNIV: "top = (%x. True)"
-  by (rule ext) (simp add: top1I)
-
-lemma DEF_UNIONS:
-  "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
-  by (auto simp add: Union_eq)
-
-lemma DEF_UNION:
-  "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
-  by auto
-
-lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
-  by (metis set_rev_mp subsetI)
-
-lemma DEF_SND:
-  "snd = (\<lambda>p. SOME x. EX y. p = (y, x))"
-  unfolding fun_eq_iff
-  by (rule someI2) (auto intro: snd_conv[symmetric] someI2)
-
-definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
-
-lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
-  by (metis psubset_eq)
-
-definition [hol4rew]: "Pred n = n - (Suc 0)"
-
-lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\<forall>n. PRE (Suc n) = n))"
-  apply (rule some_equality[symmetric])
-  apply (simp add: Pred_def)
-  apply (rule ext)
-  apply (induct_tac x)
-  apply (auto simp add: Pred_def)
-  done
-
-lemma DEF_ONE_ONE:
-  "inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
-  by (simp add: inj_on_def)
-
-definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
-
-lemma DEF_ODD:
-  "odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> ODD n)))"
-  apply (rule some_equality[symmetric])
-  apply simp
-  unfolding fun_eq_iff
-  apply (intro allI)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-definition [hol4rew, simp]: "NUMERAL (x :: nat) = x"
-
-lemma DEF_MOD:
-  "op mod = (SOME r. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
-     r m n = m else m = m div n * n + r m n \<and> r m n < n)"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (case_tac "xa = 0")
-  apply auto
-  apply (drule_tac x="x" in spec)
-  apply (drule_tac x="xa" in spec)
-  apply auto
-  by (metis mod_less mod_mult_self2 nat_add_commute nat_mult_commute)
-
-definition "MEASURE = (%u x y. (u x :: nat) < u y)"
-
-lemma [hol4rew]:
-  "MEASURE u = (%a b. (a, b) \<in> measure u)"
-  unfolding MEASURE_def measure_def
-  by simp
-
-definition
-  "LET f s = f s"
-
-lemma [hol4rew]:
-  "LET f s = Let s f"
-  by (simp add: LET_def Let_def)
-
-lemma DEF_INTERS:
-  "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
-  by auto
-
-lemma DEF_INTER:
-  "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
-  by auto
-
-lemma DEF_INSERT:
-  "insert = (\<lambda>u ua. {y. y \<in> ua | y = u})"
-  by auto
-
-lemma DEF_IMAGE:
-  "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
-  by (simp add: fun_eq_iff image_def Bex_def)
-
-lemma DEF_GEQ:
-  "(op =) = (op =)"
-  by simp
-
-lemma DEF_GABS:
-  "Eps = Eps"
-  by simp
-
-lemma DEF_FST:
-  "fst = (%p. SOME x. EX y. p = (x, y))"
-  unfolding fun_eq_iff
-  by (rule someI2) (auto intro: fst_conv[symmetric] someI2)
-
-lemma DEF_FINITE:
-  "finite = (\<lambda>a. \<forall>FP. (\<forall>a. a = {} \<or> (\<exists>x s. a = insert x s \<and> FP s) \<longrightarrow> FP a) \<longrightarrow> FP a)"
-  unfolding fun_eq_iff
-  apply (intro allI iffI impI)
-  apply (erule finite_induct)
-  apply auto[2]
-  apply (drule_tac x="finite" in spec)
-  by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
-
-lemma DEF_FACT:
-  "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
-  apply (rule some_equality[symmetric])
-  apply (simp_all)
-  unfolding fun_eq_iff
-  apply (intro allI)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma DEF_EXP:
-  "power = (SOME EXP. (\<forall>m. EXP m 0 = 1) \<and> (\<forall>m n. EXP m (Suc n) = m * EXP m n))"
-  apply (rule some_equality[symmetric])
-  apply (simp_all)
-  unfolding fun_eq_iff
-  apply (intro allI)
-  apply (induct_tac xa)
-  apply simp_all
-  done
-
-lemma DEF_EVEN:
-  "even = (SOME EVEN. EVEN 0 = True \<and> (\<forall>n. EVEN (Suc n) = (\<not> EVEN n)))"
-  apply (rule some_equality[symmetric])
-  apply simp
-  unfolding fun_eq_iff
-  apply (intro allI)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma DEF_EMPTY: "bot = (%x. False)"
-  by (rule ext) auto
-  
-lemma DEF_DIV:
-  "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
-     else m = q m n * n + r m n \<and> r m n < n)"
-  apply (rule some_equality[symmetric])
-  apply (rule_tac x="op mod" in exI)
-  apply (auto simp add: fun_eq_iff)
-  apply (case_tac "xa = 0")
-  apply auto
-  apply (drule_tac x="x" in spec)
-  apply (drule_tac x="xa" in spec)
-  apply auto
-  by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less
-      nat_add_commute nat_mult_commute plus_nat.add_0)
-
-definition [hol4rew]: "DISJOINT a b \<longleftrightarrow> a \<inter> b = {}"
-
-lemma DEF_DISJOINT:
-  "DISJOINT = (%u ua. u \<inter> ua = {})"
-  by (auto simp add: DISJOINT_def_raw)
-
-lemma DEF_DIFF:
-  "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
-  by (metis set_diff_eq)
-
-definition [hol4rew]: "DELETE s e = s - {e}"
-
-lemma DEF_DELETE:
-  "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
-  by (auto simp add: DELETE_def_raw)
-
-lemma COND_DEF:
-  "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
-  by auto
-
-definition [simp]: "NUMERAL_BIT1 n = n + (n + Suc 0)"
-
-lemma BIT1_DEF:
-  "NUMERAL_BIT1 = (%u. Suc (2 * u))"
-  by (auto)
-
-definition [simp]: "NUMERAL_BIT0 (n :: nat) = n + n"
-
-lemma BIT0_DEF:
-  "NUMERAL_BIT0 = (SOME BIT0. BIT0 0 = 0 \<and> (\<forall>n. BIT0 (Suc n) = Suc (Suc (BIT0 n))))"
-  apply (rule some_equality[symmetric])
-  apply auto
-  apply (rule ext)
-  apply (induct_tac x)
-  apply auto
-  done
-
-lemma [hol4rew]:
-  "NUMERAL_BIT0 n = 2 * n"
-  "NUMERAL_BIT1 n = 2 * n + 1"
-  "2 * 0 = (0 :: nat)"
-  "2 * 1 = (2 :: nat)"
-  "0 + 1 = (1 :: nat)"
-  by simp_all
-
-lemma DEF_MINUS: "op - = (SOME sub. (\<forall>m. sub m 0 = m) & (\<forall>m n. sub m (Suc n) = sub m n - Suc 0))"
-  apply (rule some_equality[symmetric])
-  apply auto
-  apply (rule ext)+
-  apply (induct_tac xa)
-  apply auto
-  done
-
-lemma DEF_PLUS: "op + = (SOME add. (\<forall>n. add 0 n = n) & (\<forall>m n. add (Suc m) n = Suc (add m n)))"
-  apply (rule some_equality[symmetric])
-  apply auto
-  apply (rule ext)+
-  apply (induct_tac x)
-  apply auto
-  done
-
-lemmas [hol4rew] = id_apply
-
-lemma DEF_CHOICE: "Eps = (%u. SOME x. u x)"
-  by simp
-
-definition dotdot :: "nat => nat => nat set"
-  where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
-
-lemma [hol4rew]: "dotdot a b = {a..b}"
-  unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
-  by (simp add: Collect_conj_eq)
-
-definition [hol4rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
-
-lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
-  by (simp add: INFINITE_def_raw)
-
-end
-
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOLLightInt.thy
--- a/src/HOL/Import/HOLLightInt.thy	Sat Mar 03 21:42:41 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,208 +0,0 @@
-(*  Title:      HOL/Import/HOLLightInt.thy
-    Author:     Cezary Kaliszyk
-*)
-
-header {* Compatibility theorems for HOL Light integers *}
-
-theory HOLLightInt imports Main Real GCD begin
-
-fun int_coprime where "int_coprime ((a :: int), (b :: int)) = coprime a b"
-
-lemma DEF_int_coprime:
-  "int_coprime = (\<lambda>u. \<exists>x y. ((fst u) * x) + ((snd u) * y) = int 1)"
-  apply (auto simp add: fun_eq_iff)
-  apply (metis bezout_int mult_commute)
-  by (metis coprime_divisors_nat dvd_triv_left gcd_1_int gcd_add2_int)
-
-lemma INT_FORALL_POS:
-  "(\<forall>n. P (int n)) = (\<forall>i\<ge>(int 0). P i)"
-  by (auto, drule_tac x="nat i" in spec) simp
-
-lemma INT_LT_DISCRETE:
-  "(x < y) = (x + int 1 \<le> y)"
-  by auto
-
-lemma INT_ABS_MUL_1:
-  "(abs (x * y) = int 1) = (abs x = int 1 \<and> abs y = int 1)"
-  by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult mult_1_right)
-
-lemma dest_int_rep:
-  "\<exists>(n :: nat). real (i :: int) = real n \<or> real i = - real n"
-  by (metis (full_types) of_int_of_nat real_eq_of_int real_of_nat_def)
-
-lemma DEF_int_add:
-  "op + = (\<lambda>u ua. floor (real u + real ua))"
-  by simp
-
-lemma DEF_int_sub:
-  "op - = (\<lambda>u ua. floor (real u - real ua))"
-  by simp
-
-lemma DEF_int_mul:
-  "op * = (\<lambda>u ua. floor (real u * real ua))"
-  by (metis floor_number_of number_of_is_id number_of_real_def real_eq_of_int real_of_int_mult)
-
-lemma DEF_int_abs:
-  "abs = (\<lambda>u. floor (abs (real u)))"
-  by (metis floor_real_of_int real_of_int_abs)
-
-lemma DEF_int_sgn:
-  "sgn = (\<lambda>u. floor (sgn (real u)))"
-  by (simp add: sgn_if fun_eq_iff)
-
-lemma int_sgn_th:
-  "real (sgn (x :: int)) = sgn (real x)"
-  by (simp add: sgn_if)
-
-lemma DEF_int_max:
-  "max = (\<lambda>u ua. floor (max (real u) (real ua)))"
-  by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max linorder_linear)
-
-lemma int_max_th:
-  "real (max (x :: int) y) = max (real x) (real y)"
-  by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff linorder_linear)
-
-lemma DEF_int_min:
-  "min = (\<lambda>u ua. floor (min (real u) (real ua)))"
-  by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
-
-lemma int_min_th:
-  "real (min (x :: int) y) = min (real x) (real y)"
-  by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
-
-lemma INT_IMAGE:
-  "(\<exists>n. x = int n) \<or> (\<exists>n. x = - int n)"
-  by (metis number_of_eq number_of_is_id of_int_of_nat)
-
-lemma DEF_int_pow:
-  "op ^ = (\<lambda>u ua. floor (real u ^ ua))"
-  by (simp add: floor_power)
-
-lemma DEF_int_divides:
-  "op dvd = (\<lambda>(u :: int) ua. \<exists>x. ua = u * x)"
-  by (metis dvdE dvdI)
-
-lemma DEF_int_divides':
-  "(a :: int) dvd b = (\<exists>x. b = a * x)"
-  by (metis dvdE dvdI)
-
-definition "int_mod (u :: int) ua ub = (u dvd (ua - ub))"
-
-lemma int_mod_def':
-  "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
-  by (simp add: int_mod_def_raw)
-
-lemma int_congruent:
-  "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
-  unfolding int_mod_def'
-  by (auto simp add: DEF_int_divides')
-
-lemma int_congruent':
-  "\<forall>(x :: int) y n. (n dvd x - y) = (\<exists>d. x - y = n * d)"
-  using int_congruent[unfolded int_mod_def] .
-
-fun int_gcd where
-  "int_gcd ((a :: int), (b :: int)) = gcd a b"
-
-definition "hl_mod (k\<Colon>int) (l\<Colon>int) = (if 0 \<le> l then k mod l else k mod - l)"
-
-lemma hl_mod_nonneg:
-  "b \<noteq> 0 \<Longrightarrow> hl_mod a b \<ge> 0"
-  by (simp add: hl_mod_def)
-
-lemma hl_mod_lt_abs:
-  "b \<noteq> 0 \<Longrightarrow> hl_mod a b < abs b"
-  by (simp add: hl_mod_def)
-
-definition "hl_div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
-
-lemma hl_mod_div:
-  "n \<noteq> (0\<Colon>int) \<Longrightarrow> m = hl_div m n * n + hl_mod m n"
-  unfolding hl_div_def hl_mod_def
-  by auto (metis zmod_zdiv_equality mult_commute mult_minus_left)
-
-lemma sth:
-  "(\<forall>(x :: int) y z. x + (y + z) = x + y + z) \<and>
-   (\<forall>(x :: int) y. x + y = y + x) \<and>
-   (\<forall>(x :: int). int 0 + x = x) \<and>
-   (\<forall>(x :: int) y z. x * (y * z) = x * y * z) \<and>
-   (\<forall>(x :: int) y. x * y = y * x) \<and>
-   (\<forall>(x :: int). int 1 * x = x) \<and>
-   (\<forall>(x :: int). int 0 * x = int 0) \<and>
-   (\<forall>(x :: int) y z. x * (y + z) = x * y + x * z) \<and>
-   (\<forall>(x :: int). x ^ 0 = int 1) \<and> (\<forall>(x :: int) n. x ^ Suc n = x * x ^ n)"
-  by (simp_all add: right_distrib)
-
-lemma INT_DIVISION:
-  "n ~= int 0 \<Longrightarrow> m = hl_div m n * n + hl_mod m n \<and> int 0 \<le> hl_mod m n \<and> hl_mod m n < abs n"
-  by (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
-
-lemma INT_DIVMOD_EXIST_0:
-  "\<exists>q r. if n = int 0 then q = int 0 \<and> r = m
-         else int 0 \<le> r \<and> r < abs n \<and> m = q * n + r"
-  apply (rule_tac x="hl_div m n" in exI)
-  apply (rule_tac x="hl_mod m n" in exI)
-  apply (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
-  unfolding hl_div_def hl_mod_def
-  by auto
-
-lemma DEF_div:
-  "hl_div = (SOME q. \<exists>r. \<forall>m n. if n = int 0 then q m n = int 0 \<and> r m n = m
-     else (int 0) \<le> (r m n) \<and> (r m n) < (abs n) \<and> m = ((q m n) * n) + (r m n))"
-  apply (rule some_equality[symmetric])
-  apply (rule_tac x="hl_mod" in exI)
-  apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
-  apply (simp add: hl_div_def)
-  apply (simp add: hl_mod_def)
-  apply (drule_tac x="x" in spec)
-  apply (drule_tac x="xa" in spec)
-  apply (case_tac "0 = xa")
-  apply (simp add: hl_mod_def hl_div_def)
-  apply (case_tac "xa > 0")
-  apply (simp add: hl_mod_def hl_div_def)
-  apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le add_0 zdiv_eq_0_iff mult_commute)
-  apply (simp add: hl_mod_def hl_div_def)
-  by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2)
-
-lemma DEF_rem:
-  "hl_mod = (SOME r. \<forall>m n. if n = int 0 then
-     (if 0 \<le> n then m div n else - (m div - n)) = int 0 \<and> r m n = m
-     else int 0 \<le> r m n \<and> r m n < abs n \<and>
-            m = (if 0 \<le> n then m div n else - (m div - n)) * n + r m n)"
-  apply (rule some_equality[symmetric])
-  apply (fold hl_div_def)
-  apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
-  apply (simp add: hl_div_def)
-  apply (simp add: hl_mod_def)
-  apply (drule_tac x="x" in spec)
-  apply (drule_tac x="xa" in spec)
-  apply (case_tac "0 = xa")
-  apply (simp add: hl_mod_def hl_div_def)
-  apply (case_tac "xa > 0")
-  apply (simp add: hl_mod_def hl_div_def)
-  apply (metis add_left_cancel mod_div_equality)
-  apply (simp add: hl_mod_def hl_div_def)
-  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
-
-lemma DEF_int_gcd:
-  "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
-       (d (a, b)) dvd b \<and> (\<exists>x y. d (a, b) = (a * x) + (b * y)))"
-  apply (rule some_equality[symmetric])
-  apply auto
-  apply (metis bezout_int mult_commute)
-  apply (auto simp add: fun_eq_iff)
-  apply (drule_tac x="a" in spec)
-  apply (drule_tac x="b" in spec)
-  using gcd_greatest_int zdvd_antisym_nonneg
-  by auto
-
-definition "eqeq x y (r :: 'a \<Rightarrow> 'b \<Rightarrow> bool) = r x y"
-
-lemma INT_INTEGRAL:
-  "(\<forall>x. int 0 * x = int 0) \<and>
-   (\<forall>(x :: int) y z. (x + y = x + z) = (y = z)) \<and>
-   (\<forall>(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \<or> y = z))"
-  by (auto simp add: crossproduct_eq)
-
-end
-
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOLLightList.thy
--- a/src/HOL/Import/HOLLightList.thy	Sat Mar 03 21:42:41 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,340 +0,0 @@
-(*  Title:      HOL/Import/HOLLightList.thy
-    Author:     Cezary Kaliszyk
-*)
-
-header {* Compatibility theorems for HOL Light lists *}
-
-theory HOLLightList
-imports List
-begin
-
-lemma FINITE_SET_OF_LIST:
-  "finite (set l)"
-  by simp
-
-lemma AND_ALL2:
-  "(list_all2 P l m \<and> list_all2 Q l m) = list_all2 (\<lambda>x y. P x y \<and> Q x y) l m"
-  by (induct l m rule: list_induct2') auto
-
-lemma MEM_EXISTS_EL:
-  "(x \<in> set l) = (\<exists>i<length l. x = l ! i)"
-  by (auto simp add: in_set_conv_nth)
-
-lemma INJECTIVE_MAP:
-  "(\<forall>l m. map f l = map f m --> l = m) = (\<forall>x y. f x = f y --> x = y)"
-proof (intro iffI allI impI)
-  fix x y
-  assume "\<forall>l m. map f l = map f m \<longrightarrow> l = m" "f x = f y"
-  then show "x = y"
-    by (drule_tac x="[x]" in spec) (drule_tac x="[y]" in spec, simp)
-next
-  fix l m
-  assume a: "\<forall>x y. f x = f y \<longrightarrow> x = y"
-  assume "map f l = map f m"
-  then show "l = m"
-    by (induct l m rule: list_induct2') (simp_all add: a)
-qed
-
-lemma SURJECTIVE_MAP:
-  "(\<forall>m. EX l. map f l = m) = (\<forall>y. EX x. f x = y)"
-  apply (intro iffI allI)
-  apply (drule_tac x="[y]" in spec)
-  apply (elim exE)
-  apply (case_tac l)
-  apply simp
-  apply (rule_tac x="a" in exI)
-  apply simp
-  apply (induct_tac m)
-  apply simp
-  apply (drule_tac x="a" in spec)
-  apply (elim exE)
-  apply (rule_tac x="x # l" in exI)
-  apply simp
-  done
-
-lemma LENGTH_TL:
-  "l \<noteq> [] \<longrightarrow> length (tl l) = length l - 1"
-  by simp
-
-lemma DEF_APPEND:
-  "op @ = (SOME APPEND. (\<forall>l. APPEND [] l = l) \<and> (\<forall>h t l. APPEND (h # t) l = h # APPEND t l))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma DEF_REVERSE:
-  "rev = (SOME REVERSE. REVERSE [] = [] \<and> (\<forall>l x. REVERSE (x # l) = (REVERSE l) @ [x]))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma DEF_LENGTH:
-  "length = (SOME LENGTH. LENGTH [] = 0 \<and> (\<forall>h t. LENGTH (h # t) = Suc (LENGTH t)))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma DEF_MAP:
-  "map = (SOME MAP. (\<forall>f. MAP f [] = []) \<and> (\<forall>f h t. MAP f (h # t) = f h # MAP f t))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac xa)
-  apply simp_all
-  done
-
-lemma DEF_REPLICATE:
-  "replicate =
-    (SOME REPLICATE. (\<forall>x. REPLICATE 0 x = []) \<and> (\<forall>n x. REPLICATE (Suc n) x = x # REPLICATE n x))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma DEF_ITLIST:
-  "foldr = (SOME ITLIST. (\<forall>f b. ITLIST f [] b = b) \<and> (\<forall>h f t b. ITLIST f (h # t) b = f h (ITLIST f t b)))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac xa)
-  apply simp_all
-  done
-
-lemma DEF_ALL2: "list_all2 =
-  (SOME ALL2.
-    (\<forall>P l2. ALL2 P [] l2 = (l2 = [])) \<and>
-    (\<forall>h1 P t1 l2.
-      ALL2 P (h1 # t1) l2 = (if l2 = [] then False else P h1 (hd l2) \<and> ALL2 P t1 (tl l2))))"
-  apply (rule some_equality[symmetric])
-  apply (auto)
-  apply (case_tac l2, simp_all)
-  apply (case_tac l2, simp_all)
-  apply (case_tac l2, simp_all)
-  apply (simp add: fun_eq_iff)
-  apply (intro allI)
-  apply (induct_tac xa xb rule: list_induct2')
-  apply simp_all
-  done
-
-lemma ALL2:
- "list_all2 P [] [] = True \<and>
-  list_all2 P (h1 # t1) [] = False \<and>
-  list_all2 P [] (h2 # t2) = False \<and>
-  list_all2 P (h1 # t1) (h2 # t2) = (P h1 h2 \<and> list_all2 P t1 t2)"
-  by simp
-
-lemma DEF_FILTER:
-  "filter = (SOME FILTER. (\<forall>P. FILTER P [] = []) \<and>
-     (\<forall>h P t. FILTER P (h # t) = (if P h then h # FILTER P t else FILTER P t)))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac xa)
-  apply simp_all
-  done
-
-fun map2 where
-  "map2 f [] [] = []"
-| "map2 f (h1 # t1) (h2 # t2) = (f h1 h2) # (map2 f t1 t2)"
-
-lemma MAP2:
-  "map2 f [] [] = [] \<and> map2 f (h1 # t1) (h2 # t2) = f h1 h2 # map2 f t1 t2"
-  by simp
-
-fun fold2 where
-  "fold2 f [] [] b = b"
-| "fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
-
-lemma ITLIST2:
-  "fold2 f [] [] b = b \<and> fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
-  by simp
-
-definition [simp]: "list_el x xs = nth xs x"
-
-lemma ZIP:
-  "zip [] [] = [] \<and> zip (h1 # t1) (h2 # t2) = (h1, h2) # (zip t1 t2)"
-  by simp
-
-lemma LAST_CLAUSES:
-  "last [h] = h \<and> last (h # k # t) = last (k # t)"
-  by simp
-
-lemma DEF_NULL:
-  "List.null = (SOME NULL. NULL [] = True \<and> (\<forall>h t. NULL (h # t) = False))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff null_def)
-  apply (case_tac x)
-  apply simp_all
-  done
-
-lemma DEF_ALL:
-  "list_all = (SOME u. (\<forall>P. u P [] = True) \<and> (\<forall>h P t. u P (h # t) = (P h \<and> u P t)))"
-  apply (rule some_equality[symmetric])
-  apply auto[1]
-  apply (simp add: fun_eq_iff)
-  apply (intro allI)
-  apply (induct_tac xa)
-  apply simp_all
-  done
-
-lemma MAP_EQ:
-  "list_all (\<lambda>x. f x = g x) l \<longrightarrow> map f l = map g l"
-  by (induct l) auto
-
-definition [simp]: "list_mem x xs = List.member xs x"
-
-lemma DEF_MEM:
-  "list_mem = (SOME MEM. (\<forall>x. MEM x [] = False) \<and> (\<forall>h x t. MEM x (h # t) = (x = h \<or> MEM x t)))"
-  apply (rule some_equality[symmetric])
-  apply (auto simp add: member_def)[1]
-  apply (simp add: fun_eq_iff)
-  apply (intro allI)
-  apply (induct_tac xa)
-  apply (simp_all add: member_def)
-  done
-
-lemma DEF_EX:
-  "list_ex = (SOME u. (\<forall>P. u P [] = False) \<and> (\<forall>h P t. u P (h # t) = (P h \<or> u P t)))"
-  apply (rule some_equality[symmetric])
-  apply (auto)
-  apply (simp add: fun_eq_iff)
-  apply (intro allI)
-  apply (induct_tac xa)
-  apply (simp_all)
-  done
-
-lemma ALL_IMP:
-  "(\<forall>x. x \<in> set l \<and> P x \<longrightarrow> Q x) \<and> list_all P l \<longrightarrow> list_all Q l"
-  by (simp add: list_all_iff)
-
-lemma NOT_EX: "(\<not> list_ex P l) = list_all (\<lambda>x. \<not> P x) l"
-  by (simp add: list_all_iff list_ex_iff)
-
-lemma NOT_ALL: "(\<not> list_all P l) = list_ex (\<lambda>x. \<not> P x) l"
-  by (simp add: list_all_iff list_ex_iff)
-
-lemma ALL_MAP: "list_all P (map f l) = list_all (P o f) l"
-  by (simp add: list_all_iff)
-
-lemma ALL_T: "list_all (\<lambda>x. True) l"
-  by (simp add: list_all_iff)
-
-lemma MAP_EQ_ALL2: "list_all2 (\<lambda>x y. f x = f y) l m \<longrightarrow> map f l = map f m"
-  by (induct l m rule: list_induct2') simp_all
-
-lemma ALL2_MAP: "list_all2 P (map f l) l = list_all (\<lambda>a. P (f a) a) l"
-  by (induct l) simp_all
-
-lemma MAP_EQ_DEGEN: "list_all (\<lambda>x. f x = x) l --> map f l = l"
-  by (induct l) simp_all
-
-lemma ALL2_AND_RIGHT:
-   "list_all2 (\<lambda>x y. P x \<and> Q x y) l m = (list_all P l \<and> list_all2 Q l m)"
-  by (induct l m rule: list_induct2') auto
-
-lemma ITLIST_EXTRA:
-  "foldr f (l @ [a]) b = foldr f l (f a b)"
-  by simp
-
-lemma ALL_MP:
-  "list_all (\<lambda>x. P x \<longrightarrow> Q x) l \<and> list_all P l \<longrightarrow> list_all Q l"
-  by (simp add: list_all_iff)
-
-lemma AND_ALL:
-  "(list_all P l \<and> list_all Q l) = list_all (\<lambda>x. P x \<and> Q x) l"
-  by (auto simp add: list_all_iff)
-
-lemma EX_IMP:
-  "(\<forall>x. x\<in>set l \<and> P x \<longrightarrow> Q x) \<and> list_ex P l \<longrightarrow> list_ex Q l"
-  by (auto simp add: list_ex_iff)
-
-lemma ALL_MEM:
-  "(\<forall>x. x\<in>set l \<longrightarrow> P x) = list_all P l"
-  by (auto simp add: list_all_iff)
-
-lemma EX_MAP:
-  "ALL P f l. list_ex P (map f l) = list_ex (P o f) l"
-  by (simp add: list_ex_iff)
-
-lemma EXISTS_EX:
-  "\<forall>P l. (EX x. list_ex (P x) l) = list_ex (\<lambda>s. EX x. P x s) l"
-  by (auto simp add: list_ex_iff)
-
-lemma FORALL_ALL:
-  "\<forall>P l. (\<forall>x. list_all (P x) l) = list_all (\<lambda>s. \<forall>x. P x s) l"
-  by (auto simp add: list_all_iff)
-
-lemma MEM_APPEND: "\<forall>x l1 l2. (x\<in>set (l1 @ l2)) = (x\<in>set l1 \<or> x\<in>set l2)"
-  by simp
-
-lemma MEM_MAP: "\<forall>f y l. (y\<in>set (map f l)) = (EX x. x\<in>set l \<and> y = f x)"
-  by auto
-
-lemma MEM_FILTER: "\<forall>P l x. (x\<in>set (filter P l)) = (P x \<and> x\<in>set l)"
-  by auto
-
-lemma EX_MEM: "(EX x. P x \<and> x\<in>set l) = list_ex P l"
-  by (auto simp add: list_ex_iff)
-
-lemma ALL2_MAP2:
-  "list_all2 P (map f l) (map g m) = list_all2 (\<lambda>x y. P (f x) (g y)) l m"
-  by (simp add: list_all2_map1 list_all2_map2)
-
-lemma ALL2_ALL:
-  "list_all2 P l l = list_all (\<lambda>x. P x x) l"
-  by (induct l) simp_all
-
-lemma LENGTH_MAP2:
-  "length l = length m \<longrightarrow> length (map2 f l m) = length m"
-  by (induct l m rule: list_induct2') simp_all
-
-lemma DEF_set_of_list:
-  "set = (SOME sol. sol [] = {} \<and> (\<forall>h t. sol (h # t) = insert h (sol t)))"
-  apply (rule some_equality[symmetric])
-  apply (simp_all)
-  apply (rule ext)
-  apply (induct_tac x)
-  apply simp_all
-  done
-
-lemma IN_SET_OF_LIST:
-  "(x : set l) = (x : set l)"
-  by simp
-
-lemma DEF_BUTLAST:
-  "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))"
-  apply (rule some_equality[symmetric])
-  apply auto
-  apply (rule ext)
-  apply (induct_tac x)
-  apply auto
-  done
-
-lemma MONO_ALL:
-  "(ALL x. P x \<longrightarrow> Q x) \<longrightarrow> list_all P l \<longrightarrow> list_all Q l"
-  by (simp add: list_all_iff)
-
-lemma EL_TL: "l \<noteq> [] \<Longrightarrow> tl l ! x = l ! (x + 1)"
-  by (induct l) (simp_all)
-
-(* Assume the same behaviour outside of the usual domain.
-   For HD, LAST, EL it follows from "undefined = SOME _. False".
-
-   The definitions of TL and ZIP are different for empty lists.
- *)
-axiomatization where
-  DEF_HD: "hd = (SOME HD. \<forall>t h. HD (h # t) = h)"
-
-axiomatization where
-  DEF_LAST: "last =
-    (SOME LAST. \<forall>h t. LAST (h # t) = (if t = [] then h else LAST t))"
-
-axiomatization where
-  DEF_EL: "list_el =
-    (SOME EL. (\<forall>l. EL 0 l = hd l) \<and> (\<forall>n l. EL (Suc n) l = EL n (tl l)))"
-
-end
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOLLightReal.thy
--- a/src/HOL/Import/HOLLightReal.thy	Sat Mar 03 21:42:41 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,329 +0,0 @@
-(*  Title:      HOL/Import/HOLLightReal.thy
-    Author:     Cezary Kaliszyk
-*)
-
-header {* Compatibility theorems for HOL Light reals *}
-
-theory HOLLightReal imports Real begin
-
-lemma REAL_OF_NUM_MAX:
-  "max (real (m :: nat)) (real n) = real (max m n)"
-  by simp
-
-lemma REAL_OF_NUM_MIN:
-  "min (real (m :: nat)) (real n) = real (min m n)"
-  by simp
-
-lemma REAL_POLY_NEG_CLAUSES:
-  "(\<forall>(x :: real). - x = - 1 * x) \<and> (\<forall>(x :: real) y. x - y = x + - 1 * y)"
-  by simp
-
-lemma REAL_MUL_AC:
-  "(m :: real) * n = n * m \<and> m * n * p = m * (n * p) \<and> m * (n * p) = n * (m * p)"
-  by simp
-
-lemma REAL_EQ_ADD_LCANCEL_0:
-  "((x :: real) + y = x) = (y = 0)"
-  by simp
-
-lemma REAL_EQ_ADD_RCANCEL_0:
-  "((x :: real) + y = y) = (x = 0)"
-  by simp
-
-lemma REAL_LT_ANTISYM:
-  "\<not> ((x :: real) < y \<and> y < x)"
-  by simp
-
-lemma REAL_LET_ANTISYM:
-  "\<not> ((x :: real) \<le> y \<and> y < x)"
-  by simp
-
-lemma REAL_LT_NEGTOTAL:
-  "(x :: real) = 0 \<or> 0 < x \<or> 0 < - x"
-  by auto
-
-lemma REAL_LT_ADDNEG:
-  "((y :: real) < x + - z) = (y + z < x)"
-  by auto
-
-lemma REAL_LT_ADDNEG2:
-  "((x :: real) + - y < z) = (x < z + y)"
-  by auto
-
-lemma REAL_LT_ADD1:
-  "(x :: real) \<le> y \<longrightarrow> x < y + 1"
-  by simp
-
-lemma REAL_SUB_ADD2:
-  "(y :: real) + (x - y) = x"
-  by simp
-
-lemma REAL_ADD_SUB:
-  "(x :: real) + y - x = y"
-  by simp
-
-lemma REAL_NEG_EQ:
-  "(- (x :: real) = y) = (x = - y)"
-  by auto
-
-lemma REAL_LE_ADDR:
-  "((x :: real) \<le> x + y) = (0 \<le> y)"
-  by simp
-
-lemma REAL_LE_ADDL:
-  "((y :: real) \<le> x + y) = (0 \<le> x)"
-  by simp
-
-lemma REAL_LT_ADDR:
-  "((x :: real) < x + y) = (0 < y)"
-  by simp
-
-lemma REAL_LT_ADDL:
-  "((y :: real) < x + y) = (0 < x)"
-  by simp
-
-lemma REAL_SUB_SUB:
-  "(x :: real) - y - x = - y"
-  by simp
-
-lemma REAL_SUB_LNEG:
-  "- (x :: real) - y = - (x + y)"
-  by simp
-
-lemma REAL_SUB_NEG2:
-  "- (x :: real) - - y = y - x"
-  by simp
-
-lemma REAL_SUB_TRIANGLE:
-  "(a :: real) - b + (b - c) = a - c"
-  by simp
-
-lemma REAL_SUB_SUB2:
-  "(x :: real) - (x - y) = y"
-  by simp
-
-lemma REAL_ADD_SUB2:
-  "(x :: real) - (x + y) = - y"
-  by simp
-
-lemma REAL_POS_NZ:
-  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
-  by simp
-
-lemma REAL_DIFFSQ:
-  "((x :: real) + y) * (x - y) = x * x - y * y"
-  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
-
-lemma REAL_ABS_TRIANGLE_LE:
-  "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
-  by auto
-
-lemma REAL_ABS_TRIANGLE_LT:
-  "abs (x :: real) + abs (y - x) < z \<longrightarrow> abs y < z"
-  by auto
-
-lemma REAL_ABS_REFL:
-  "(abs (x :: real) = x) = (0 \<le> x)"
-  by auto
-
-lemma REAL_ABS_BETWEEN:
-  "(0 < (d :: real) \<and> x - d < y \<and> y < x + d) = (abs (y - x) < d)"
-  by auto
-
-lemma REAL_ABS_BOUND:
-  "abs ((x :: real) - y) < d \<longrightarrow> y < x + d"
-  by auto
-
-lemma REAL_ABS_STILLNZ:
-  "abs ((x :: real) - y) < abs y \<longrightarrow> x \<noteq> 0"
-  by auto
-
-lemma REAL_ABS_CASES:
-  "(x :: real) = 0 \<or> 0 < abs x"
-  by simp
-
-lemma REAL_ABS_BETWEEN1:
-  "(x :: real) < z \<and> abs (y - x) < z - x \<longrightarrow> y < z"
-  by auto
-
-lemma REAL_ABS_SIGN:
-  "abs ((x :: real) - y) < y \<longrightarrow> 0 < x"
-  by auto
-
-lemma REAL_ABS_SIGN2:
-  "abs ((x :: real) - y) < - y \<longrightarrow> x < 0"
-  by auto
-
-lemma REAL_ABS_CIRCLE:
-  "abs (h :: real) < abs y - abs x \<longrightarrow> abs (x + h) < abs y"
-  by auto
-
-lemma REAL_BOUNDS_LT:
-  "(- (k :: real) < x \<and> x < k) = (abs x < k)"
-  by auto
-
-lemma REAL_MIN_MAX:
-  "min (x :: real) y = - max (- x) (- y)"
-  by auto
-
-lemma REAL_MAX_MIN:
-  "max (x :: real) y = - min (- x) (- y)"
-  by auto
-
-lemma REAL_MAX_MAX:
-  "(x :: real) \<le> max x y \<and> y \<le> max x y"
-  by simp
-
-lemma REAL_MIN_MIN:
-  "min (x :: real) y \<le> x \<and> min x y \<le> y"
-  by simp
-
-lemma REAL_MAX_ACI:
-  "max (x :: real) y = max y x \<and>
-   max (max x y) z = max x (max y z) \<and>
-   max x (max y z) = max y (max x z) \<and> max x x = x \<and> max x (max x y) = max x y"
-  by auto
-
-
-lemma REAL_MIN_ACI:
-  "min (x :: real) y = min y x \<and>
-   min (min x y) z = min x (min y z) \<and>
-   min x (min y z) = min y (min x z) \<and> min x x = x \<and> min x (min x y) = min x y"
-  by auto
-
-lemma REAL_EQ_MUL_RCANCEL:
-  "((x :: real) * z = y * z) = (x = y \<or> z = 0)"
-  by auto
-
-lemma REAL_MUL_LINV_UNIQ:
-  "(x :: real) * y = 1 \<longrightarrow> inverse y = x"
-  by (metis inverse_inverse_eq inverse_unique)
-
-lemma REAL_DIV_RMUL:
-  "(y :: real) \<noteq> 0 \<longrightarrow> x / y * y = x"
-  by simp
-
-lemma REAL_DIV_LMUL:
-  "(y :: real) \<noteq> 0 \<longrightarrow> y * (x / y) = x"
-  by simp
-
-lemma REAL_LT_IMP_NZ:
-  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
-  by simp
-
-lemma REAL_LT_LCANCEL_IMP:
-  "0 < (x :: real) \<and> x * y < x * z \<longrightarrow> y < z"
-  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
-
-lemma REAL_LT_RCANCEL_IMP:
-  "0 < (z :: real) \<and> x * z < y * z \<longrightarrow> x < y"
-  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
-
-lemma REAL_MUL_POS_LE:
-  "(0 \<le> (x :: real) * y) = (x = 0 \<or> y = 0 \<or> 0 < x \<and> 0 < y \<or> x < 0 \<and> y < 0)"
-  by (metis less_eq_real_def mult_eq_0_iff zero_le_mult_iff)
-
-lemma REAL_EQ_RDIV_EQ:
-  "0 < (z :: real) \<longrightarrow> (x = y / z) = (x * z = y)"
-  by auto
-
-lemma REAL_EQ_LDIV_EQ:
-  "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)"
-  by auto
-
-lemma REAL_SUB_INV:
-  "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
-  by (simp add: division_ring_inverse_diff divide_real_def)
-
-lemma REAL_DOWN:
-  "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
-  by (intro impI exI[of _ "d / 2"]) simp
-
-lemma REAL_POW_MONO_LT:
-  "1 < (x :: real) \<and> m < n \<longrightarrow> x ^ m < x ^ n"
-  by simp
-
-lemma REAL_POW_MONO:
-  "1 \<le> (x :: real) \<and> m \<le> n \<longrightarrow> x ^ m \<le> x ^ n"
-  by (cases "m < n", cases "x = 1") auto
-
-lemma REAL_EQ_LCANCEL_IMP:
-  "(z :: real) \<noteq> 0 \<and> z * x = z * y \<longrightarrow> x = y"
-  by auto
-
-lemma REAL_LE_DIV:
-  "0 \<le> (x :: real) \<and> 0 \<le> y \<longrightarrow> 0 \<le> x / y"
-  by (simp add: zero_le_divide_iff)
-
-lemma REAL_10: "(1::real) \<noteq> 0"
-  by simp
-
-lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
-  by simp
-
-lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
-  by simp
-
-lemma REAL_ADD_LINV:  "-x + x = (0::real)"
-  by simp
-
-lemma REAL_MUL_LINV: "x \<noteq> (0::real) \<Longrightarrow> inverse x * x = 1"
-  by simp
-
-lemma REAL_LT_TOTAL: "((x::real) = y) \<or> x < y \<or> y < x"
-  by auto
-
-lemma real_lte: "((x::real) \<le> y) = (\<not>(y < x))"
-  by auto
-
-lemma real_of_num: "((0::real) = 0) \<and> (!n. real (Suc n) = real n + 1)"
-  by (simp add: real_of_nat_Suc)
-
-lemma abs: "abs (x::real) = (if 0 \<le> x then x else -x)"
-  by (simp add: abs_if)
-
-lemma pow: "(!x::real. x ^ 0 = 1) \<and> (!x::real. \<forall>n. x ^ (Suc n) = x * x ^ n)"
-  by simp
-
-lemma REAL_POLY_CLAUSES:
-  "(\<forall>(x :: real) y z. x + (y + z) = x + y + z) \<and>
-   (\<forall>(x :: real) y. x + y = y + x) \<and>
-   (\<forall>(x :: real). 0 + x = x) \<and>
-   (\<forall>(x :: real) y z. x * (y * z) = x * y * z) \<and>
-   (\<forall>(x :: real) y. x * y = y * x) \<and>
-   (\<forall>(x :: real). 1 * x = x) \<and>
-   (\<forall>(x :: real). 0 * x = 0) \<and>
-   (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
-   (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
-  by (auto simp add: right_distrib)
-
-lemma REAL_COMPLETE:
-  "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
-   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
-          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
-  using complete_real[unfolded Ball_def, of "Collect P"] by auto
-
-lemma REAL_COMPLETE_SOMEPOS:
-  "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
-   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
-          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
-  using REAL_COMPLETE by auto
-
-lemma REAL_ADD_AC:
-  "(m :: real) + n = n + m \<and> m + n + p = m + (n + p) \<and> m + (n + p) = n + (m + p)"
-  by simp
-
-lemma REAL_LE_RNEG:
-  "((x :: real) \<le> - y) = (x + y \<le> 0)"
-  by auto
-
-lemma REAL_LE_NEGTOTAL:
-  "0 \<le> (x :: real) \<or> 0 \<le> - x"
-  by auto
-
-lemma DEF_real_sgn:
-  "sgn = (\<lambda>u. if (0 :: real) < u then 1 else if u < 0 then - 1 else 0)"
-  by (simp add: ext)
-
-end
-
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOL_Light/Compatibility.thy
--- a/src/HOL/Import/HOL_Light/Compatibility.thy	Sat Mar 03 21:42:41 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Compatibility.thy	Sat Mar 03 21:51:38 2012 +0100
@@ -1,5 +1,349 @@
+(*  Title:      HOL/Import/HOL_Light/Compatibility.thy
+    Author:     Steven Obua and Sebastian Skalberg, TU Muenchen
+    Author:     Cezary Kaliszyk
+*)
+
 theory Compatibility
-imports Main
+imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set"
+  HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/HOL4Setup"
 begin
 
+(* list *)
+lemmas [hol4rew] = list_el_def member_def list_mem_def
+(* int *)
+lemmas [hol4rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def
+(* real *)
+lemma [hol4rew]:
+  "real (0::nat) = 0" "real (1::nat) = 1" "real (2::nat) = 2"
+  by simp_all
+
+lemma one:
+  "\<forall>v. v = ()"
+  by simp
+
+lemma num_Axiom:
+  "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
+  apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma SUC_INJ:
+  "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
+  by simp
+
+lemma PAIR:
+  "(fst x, snd x) = x"
+  by simp
+
+lemma EXISTS_UNIQUE_THM:
+  "(Ex1 P) = (Ex P & (\<forall>x y. P x & P y --> (x = y)))"
+  by auto
+
+lemma DEF__star_:
+  "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac x)
+  apply auto
+  done
+
+lemma DEF__slash__backslash_:
+  "(t1 \<and> t2) = ((\<lambda>f. f t1 t2 :: bool) = (\<lambda>f. f True True))"
+  unfolding fun_eq_iff
+  by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \<and> b)"], simp)
+
+lemma DEF__lessthan__equal_:
+  "op \<le> = (SOME u. (\<forall>m. u m 0 = (m = 0)) \<and> (\<forall>m n. u m (Suc n) = (m = Suc n \<or> u m n)))"
+  apply (rule some_equality[symmetric])
+  apply auto[1]
+  apply (simp add: fun_eq_iff)
+  apply (intro allI)
+  apply (induct_tac xa)
+  apply auto
+  done
+
+lemma DEF__lessthan_:
+  "op < = (SOME u. (\<forall>m. u m 0 = False) \<and> (\<forall>m n. u m (Suc n) = (m = n \<or> u m n)))"
+  apply (rule some_equality[symmetric])
+  apply auto[1]
+  apply (simp add: fun_eq_iff)
+  apply (intro allI)
+  apply (induct_tac xa)
+  apply auto
+  done
+
+lemma DEF__greaterthan__equal_:
+  "(op \<ge>) = (%u ua. ua \<le> u)"
+  by (simp)
+
+lemma DEF__greaterthan_:
+  "(op >) = (%u ua. ua < u)"
+  by (simp)
+
+lemma DEF__equal__equal__greaterthan_:
+  "(t1 \<longrightarrow> t2) = ((t1 \<and> t2) = t1)"
+  by auto
+
+lemma DEF_WF:
+  "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
+  unfolding fun_eq_iff
+proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
+  fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
+  assume "P xa"
+  then show "xa \<in> Collect P" by simp
+next
+  fix x P xa z
+  assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
+  then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
+next
+  fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
+  assume a: "xa \<in> Q"
+  assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
+  then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
+  then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
+qed
+
+lemma DEF_UNIV: "top = (%x. True)"
+  by (rule ext) (simp add: top1I)
+
+lemma DEF_UNIONS:
+  "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
+  by (auto simp add: Union_eq)
+
+lemma DEF_UNION:
+  "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
+  by auto
+
+lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
+  by (metis set_rev_mp subsetI)
+
+lemma DEF_SND:
+  "snd = (\<lambda>p. SOME x. EX y. p = (y, x))"
+  unfolding fun_eq_iff
+  by (rule someI2) (auto intro: snd_conv[symmetric] someI2)
+
+definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
+
+lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
+  by (metis psubset_eq)
+
+definition [hol4rew]: "Pred n = n - (Suc 0)"
+
+lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\<forall>n. PRE (Suc n) = n))"
+  apply (rule some_equality[symmetric])
+  apply (simp add: Pred_def)
+  apply (rule ext)
+  apply (induct_tac x)
+  apply (auto simp add: Pred_def)
+  done
+
+lemma DEF_ONE_ONE:
+  "inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
+  by (simp add: inj_on_def)
+
+definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
+
+lemma DEF_ODD:
+  "odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> ODD n)))"
+  apply (rule some_equality[symmetric])
+  apply simp
+  unfolding fun_eq_iff
+  apply (intro allI)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+definition [hol4rew, simp]: "NUMERAL (x :: nat) = x"
+
+lemma DEF_MOD:
+  "op mod = (SOME r. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
+     r m n = m else m = m div n * n + r m n \<and> r m n < n)"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (case_tac "xa = 0")
+  apply auto
+  apply (drule_tac x="x" in spec)
+  apply (drule_tac x="xa" in spec)
+  apply auto
+  by (metis mod_less mod_mult_self2 nat_add_commute nat_mult_commute)
+
+definition "MEASURE = (%u x y. (u x :: nat) < u y)"
+
+lemma [hol4rew]:
+  "MEASURE u = (%a b. (a, b) \<in> measure u)"
+  unfolding MEASURE_def measure_def
+  by simp
+
+definition
+  "LET f s = f s"
+
+lemma [hol4rew]:
+  "LET f s = Let s f"
+  by (simp add: LET_def Let_def)
+
+lemma DEF_INTERS:
+  "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
+  by auto
+
+lemma DEF_INTER:
+  "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
+  by auto
+
+lemma DEF_INSERT:
+  "insert = (\<lambda>u ua. {y. y \<in> ua | y = u})"
+  by auto
+
+lemma DEF_IMAGE:
+  "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
+  by (simp add: fun_eq_iff image_def Bex_def)
+
+lemma DEF_GEQ:
+  "(op =) = (op =)"
+  by simp
+
+lemma DEF_GABS:
+  "Eps = Eps"
+  by simp
+
+lemma DEF_FST:
+  "fst = (%p. SOME x. EX y. p = (x, y))"
+  unfolding fun_eq_iff
+  by (rule someI2) (auto intro: fst_conv[symmetric] someI2)
+
+lemma DEF_FINITE:
+  "finite = (\<lambda>a. \<forall>FP. (\<forall>a. a = {} \<or> (\<exists>x s. a = insert x s \<and> FP s) \<longrightarrow> FP a) \<longrightarrow> FP a)"
+  unfolding fun_eq_iff
+  apply (intro allI iffI impI)
+  apply (erule finite_induct)
+  apply auto[2]
+  apply (drule_tac x="finite" in spec)
+  by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
+
+lemma DEF_FACT:
+  "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
+  apply (rule some_equality[symmetric])
+  apply (simp_all)
+  unfolding fun_eq_iff
+  apply (intro allI)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma DEF_EXP:
+  "power = (SOME EXP. (\<forall>m. EXP m 0 = 1) \<and> (\<forall>m n. EXP m (Suc n) = m * EXP m n))"
+  apply (rule some_equality[symmetric])
+  apply (simp_all)
+  unfolding fun_eq_iff
+  apply (intro allI)
+  apply (induct_tac xa)
+  apply simp_all
+  done
+
+lemma DEF_EVEN:
+  "even = (SOME EVEN. EVEN 0 = True \<and> (\<forall>n. EVEN (Suc n) = (\<not> EVEN n)))"
+  apply (rule some_equality[symmetric])
+  apply simp
+  unfolding fun_eq_iff
+  apply (intro allI)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma DEF_EMPTY: "bot = (%x. False)"
+  by (rule ext) auto
+  
+lemma DEF_DIV:
+  "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
+     else m = q m n * n + r m n \<and> r m n < n)"
+  apply (rule some_equality[symmetric])
+  apply (rule_tac x="op mod" in exI)
+  apply (auto simp add: fun_eq_iff)
+  apply (case_tac "xa = 0")
+  apply auto
+  apply (drule_tac x="x" in spec)
+  apply (drule_tac x="xa" in spec)
+  apply auto
+  by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less
+      nat_add_commute nat_mult_commute plus_nat.add_0)
+
+definition [hol4rew]: "DISJOINT a b \<longleftrightarrow> a \<inter> b = {}"
+
+lemma DEF_DISJOINT:
+  "DISJOINT = (%u ua. u \<inter> ua = {})"
+  by (auto simp add: DISJOINT_def_raw)
+
+lemma DEF_DIFF:
+  "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
+  by (metis set_diff_eq)
+
+definition [hol4rew]: "DELETE s e = s - {e}"
+
+lemma DEF_DELETE:
+  "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
+  by (auto simp add: DELETE_def_raw)
+
+lemma COND_DEF:
+  "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
+  by auto
+
+definition [simp]: "NUMERAL_BIT1 n = n + (n + Suc 0)"
+
+lemma BIT1_DEF:
+  "NUMERAL_BIT1 = (%u. Suc (2 * u))"
+  by (auto)
+
+definition [simp]: "NUMERAL_BIT0 (n :: nat) = n + n"
+
+lemma BIT0_DEF:
+  "NUMERAL_BIT0 = (SOME BIT0. BIT0 0 = 0 \<and> (\<forall>n. BIT0 (Suc n) = Suc (Suc (BIT0 n))))"
+  apply (rule some_equality[symmetric])
+  apply auto
+  apply (rule ext)
+  apply (induct_tac x)
+  apply auto
+  done
+
+lemma [hol4rew]:
+  "NUMERAL_BIT0 n = 2 * n"
+  "NUMERAL_BIT1 n = 2 * n + 1"
+  "2 * 0 = (0 :: nat)"
+  "2 * 1 = (2 :: nat)"
+  "0 + 1 = (1 :: nat)"
+  by simp_all
+
+lemma DEF_MINUS: "op - = (SOME sub. (\<forall>m. sub m 0 = m) & (\<forall>m n. sub m (Suc n) = sub m n - Suc 0))"
+  apply (rule some_equality[symmetric])
+  apply auto
+  apply (rule ext)+
+  apply (induct_tac xa)
+  apply auto
+  done
+
+lemma DEF_PLUS: "op + = (SOME add. (\<forall>n. add 0 n = n) & (\<forall>m n. add (Suc m) n = Suc (add m n)))"
+  apply (rule some_equality[symmetric])
+  apply auto
+  apply (rule ext)+
+  apply (induct_tac x)
+  apply auto
+  done
+
+lemmas [hol4rew] = id_apply
+
+lemma DEF_CHOICE: "Eps = (%u. SOME x. u x)"
+  by simp
+
+definition dotdot :: "nat => nat => nat set"
+  where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
+
+lemma [hol4rew]: "dotdot a b = {a..b}"
+  unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
+  by (simp add: Collect_conj_eq)
+
+definition [hol4rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
+
+lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
+  by (simp add: INFINITE_def_raw)
+
 end
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOL_Light/HOLLightInt.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Sat Mar 03 21:51:38 2012 +0100
@@ -0,0 +1,208 @@
+(*  Title:      HOL/Import/HOLLightInt.thy
+    Author:     Cezary Kaliszyk
+*)
+
+header {* Compatibility theorems for HOL Light integers *}
+
+theory HOLLightInt imports Main Real GCD begin
+
+fun int_coprime where "int_coprime ((a :: int), (b :: int)) = coprime a b"
+
+lemma DEF_int_coprime:
+  "int_coprime = (\<lambda>u. \<exists>x y. ((fst u) * x) + ((snd u) * y) = int 1)"
+  apply (auto simp add: fun_eq_iff)
+  apply (metis bezout_int mult_commute)
+  by (metis coprime_divisors_nat dvd_triv_left gcd_1_int gcd_add2_int)
+
+lemma INT_FORALL_POS:
+  "(\<forall>n. P (int n)) = (\<forall>i\<ge>(int 0). P i)"
+  by (auto, drule_tac x="nat i" in spec) simp
+
+lemma INT_LT_DISCRETE:
+  "(x < y) = (x + int 1 \<le> y)"
+  by auto
+
+lemma INT_ABS_MUL_1:
+  "(abs (x * y) = int 1) = (abs x = int 1 \<and> abs y = int 1)"
+  by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult mult_1_right)
+
+lemma dest_int_rep:
+  "\<exists>(n :: nat). real (i :: int) = real n \<or> real i = - real n"
+  by (metis (full_types) of_int_of_nat real_eq_of_int real_of_nat_def)
+
+lemma DEF_int_add:
+  "op + = (\<lambda>u ua. floor (real u + real ua))"
+  by simp
+
+lemma DEF_int_sub:
+  "op - = (\<lambda>u ua. floor (real u - real ua))"
+  by simp
+
+lemma DEF_int_mul:
+  "op * = (\<lambda>u ua. floor (real u * real ua))"
+  by (metis floor_number_of number_of_is_id number_of_real_def real_eq_of_int real_of_int_mult)
+
+lemma DEF_int_abs:
+  "abs = (\<lambda>u. floor (abs (real u)))"
+  by (metis floor_real_of_int real_of_int_abs)
+
+lemma DEF_int_sgn:
+  "sgn = (\<lambda>u. floor (sgn (real u)))"
+  by (simp add: sgn_if fun_eq_iff)
+
+lemma int_sgn_th:
+  "real (sgn (x :: int)) = sgn (real x)"
+  by (simp add: sgn_if)
+
+lemma DEF_int_max:
+  "max = (\<lambda>u ua. floor (max (real u) (real ua)))"
+  by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max linorder_linear)
+
+lemma int_max_th:
+  "real (max (x :: int) y) = max (real x) (real y)"
+  by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff linorder_linear)
+
+lemma DEF_int_min:
+  "min = (\<lambda>u ua. floor (min (real u) (real ua)))"
+  by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
+
+lemma int_min_th:
+  "real (min (x :: int) y) = min (real x) (real y)"
+  by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
+
+lemma INT_IMAGE:
+  "(\<exists>n. x = int n) \<or> (\<exists>n. x = - int n)"
+  by (metis number_of_eq number_of_is_id of_int_of_nat)
+
+lemma DEF_int_pow:
+  "op ^ = (\<lambda>u ua. floor (real u ^ ua))"
+  by (simp add: floor_power)
+
+lemma DEF_int_divides:
+  "op dvd = (\<lambda>(u :: int) ua. \<exists>x. ua = u * x)"
+  by (metis dvdE dvdI)
+
+lemma DEF_int_divides':
+  "(a :: int) dvd b = (\<exists>x. b = a * x)"
+  by (metis dvdE dvdI)
+
+definition "int_mod (u :: int) ua ub = (u dvd (ua - ub))"
+
+lemma int_mod_def':
+  "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
+  by (simp add: int_mod_def_raw)
+
+lemma int_congruent:
+  "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
+  unfolding int_mod_def'
+  by (auto simp add: DEF_int_divides')
+
+lemma int_congruent':
+  "\<forall>(x :: int) y n. (n dvd x - y) = (\<exists>d. x - y = n * d)"
+  using int_congruent[unfolded int_mod_def] .
+
+fun int_gcd where
+  "int_gcd ((a :: int), (b :: int)) = gcd a b"
+
+definition "hl_mod (k\<Colon>int) (l\<Colon>int) = (if 0 \<le> l then k mod l else k mod - l)"
+
+lemma hl_mod_nonneg:
+  "b \<noteq> 0 \<Longrightarrow> hl_mod a b \<ge> 0"
+  by (simp add: hl_mod_def)
+
+lemma hl_mod_lt_abs:
+  "b \<noteq> 0 \<Longrightarrow> hl_mod a b < abs b"
+  by (simp add: hl_mod_def)
+
+definition "hl_div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
+
+lemma hl_mod_div:
+  "n \<noteq> (0\<Colon>int) \<Longrightarrow> m = hl_div m n * n + hl_mod m n"
+  unfolding hl_div_def hl_mod_def
+  by auto (metis zmod_zdiv_equality mult_commute mult_minus_left)
+
+lemma sth:
+  "(\<forall>(x :: int) y z. x + (y + z) = x + y + z) \<and>
+   (\<forall>(x :: int) y. x + y = y + x) \<and>
+   (\<forall>(x :: int). int 0 + x = x) \<and>
+   (\<forall>(x :: int) y z. x * (y * z) = x * y * z) \<and>
+   (\<forall>(x :: int) y. x * y = y * x) \<and>
+   (\<forall>(x :: int). int 1 * x = x) \<and>
+   (\<forall>(x :: int). int 0 * x = int 0) \<and>
+   (\<forall>(x :: int) y z. x * (y + z) = x * y + x * z) \<and>
+   (\<forall>(x :: int). x ^ 0 = int 1) \<and> (\<forall>(x :: int) n. x ^ Suc n = x * x ^ n)"
+  by (simp_all add: right_distrib)
+
+lemma INT_DIVISION:
+  "n ~= int 0 \<Longrightarrow> m = hl_div m n * n + hl_mod m n \<and> int 0 \<le> hl_mod m n \<and> hl_mod m n < abs n"
+  by (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+
+lemma INT_DIVMOD_EXIST_0:
+  "\<exists>q r. if n = int 0 then q = int 0 \<and> r = m
+         else int 0 \<le> r \<and> r < abs n \<and> m = q * n + r"
+  apply (rule_tac x="hl_div m n" in exI)
+  apply (rule_tac x="hl_mod m n" in exI)
+  apply (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+  unfolding hl_div_def hl_mod_def
+  by auto
+
+lemma DEF_div:
+  "hl_div = (SOME q. \<exists>r. \<forall>m n. if n = int 0 then q m n = int 0 \<and> r m n = m
+     else (int 0) \<le> (r m n) \<and> (r m n) < (abs n) \<and> m = ((q m n) * n) + (r m n))"
+  apply (rule some_equality[symmetric])
+  apply (rule_tac x="hl_mod" in exI)
+  apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+  apply (simp add: hl_div_def)
+  apply (simp add: hl_mod_def)
+  apply (drule_tac x="x" in spec)
+  apply (drule_tac x="xa" in spec)
+  apply (case_tac "0 = xa")
+  apply (simp add: hl_mod_def hl_div_def)
+  apply (case_tac "xa > 0")
+  apply (simp add: hl_mod_def hl_div_def)
+  apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le add_0 zdiv_eq_0_iff mult_commute)
+  apply (simp add: hl_mod_def hl_div_def)
+  by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2)
+
+lemma DEF_rem:
+  "hl_mod = (SOME r. \<forall>m n. if n = int 0 then
+     (if 0 \<le> n then m div n else - (m div - n)) = int 0 \<and> r m n = m
+     else int 0 \<le> r m n \<and> r m n < abs n \<and>
+            m = (if 0 \<le> n then m div n else - (m div - n)) * n + r m n)"
+  apply (rule some_equality[symmetric])
+  apply (fold hl_div_def)
+  apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+  apply (simp add: hl_div_def)
+  apply (simp add: hl_mod_def)
+  apply (drule_tac x="x" in spec)
+  apply (drule_tac x="xa" in spec)
+  apply (case_tac "0 = xa")
+  apply (simp add: hl_mod_def hl_div_def)
+  apply (case_tac "xa > 0")
+  apply (simp add: hl_mod_def hl_div_def)
+  apply (metis add_left_cancel mod_div_equality)
+  apply (simp add: hl_mod_def hl_div_def)
+  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
+
+lemma DEF_int_gcd:
+  "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
+       (d (a, b)) dvd b \<and> (\<exists>x y. d (a, b) = (a * x) + (b * y)))"
+  apply (rule some_equality[symmetric])
+  apply auto
+  apply (metis bezout_int mult_commute)
+  apply (auto simp add: fun_eq_iff)
+  apply (drule_tac x="a" in spec)
+  apply (drule_tac x="b" in spec)
+  using gcd_greatest_int zdvd_antisym_nonneg
+  by auto
+
+definition "eqeq x y (r :: 'a \<Rightarrow> 'b \<Rightarrow> bool) = r x y"
+
+lemma INT_INTEGRAL:
+  "(\<forall>x. int 0 * x = int 0) \<and>
+   (\<forall>(x :: int) y z. (x + y = x + z) = (y = z)) \<and>
+   (\<forall>(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \<or> y = z))"
+  by (auto simp add: crossproduct_eq)
+
+end
+
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOL_Light/HOLLightList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightList.thy	Sat Mar 03 21:51:38 2012 +0100
@@ -0,0 +1,340 @@
+(*  Title:      HOL/Import/HOLLightList.thy
+    Author:     Cezary Kaliszyk
+*)
+
+header {* Compatibility theorems for HOL Light lists *}
+
+theory HOLLightList
+imports List
+begin
+
+lemma FINITE_SET_OF_LIST:
+  "finite (set l)"
+  by simp
+
+lemma AND_ALL2:
+  "(list_all2 P l m \<and> list_all2 Q l m) = list_all2 (\<lambda>x y. P x y \<and> Q x y) l m"
+  by (induct l m rule: list_induct2') auto
+
+lemma MEM_EXISTS_EL:
+  "(x \<in> set l) = (\<exists>i<length l. x = l ! i)"
+  by (auto simp add: in_set_conv_nth)
+
+lemma INJECTIVE_MAP:
+  "(\<forall>l m. map f l = map f m --> l = m) = (\<forall>x y. f x = f y --> x = y)"
+proof (intro iffI allI impI)
+  fix x y
+  assume "\<forall>l m. map f l = map f m \<longrightarrow> l = m" "f x = f y"
+  then show "x = y"
+    by (drule_tac x="[x]" in spec) (drule_tac x="[y]" in spec, simp)
+next
+  fix l m
+  assume a: "\<forall>x y. f x = f y \<longrightarrow> x = y"
+  assume "map f l = map f m"
+  then show "l = m"
+    by (induct l m rule: list_induct2') (simp_all add: a)
+qed
+
+lemma SURJECTIVE_MAP:
+  "(\<forall>m. EX l. map f l = m) = (\<forall>y. EX x. f x = y)"
+  apply (intro iffI allI)
+  apply (drule_tac x="[y]" in spec)
+  apply (elim exE)
+  apply (case_tac l)
+  apply simp
+  apply (rule_tac x="a" in exI)
+  apply simp
+  apply (induct_tac m)
+  apply simp
+  apply (drule_tac x="a" in spec)
+  apply (elim exE)
+  apply (rule_tac x="x # l" in exI)
+  apply simp
+  done
+
+lemma LENGTH_TL:
+  "l \<noteq> [] \<longrightarrow> length (tl l) = length l - 1"
+  by simp
+
+lemma DEF_APPEND:
+  "op @ = (SOME APPEND. (\<forall>l. APPEND [] l = l) \<and> (\<forall>h t l. APPEND (h # t) l = h # APPEND t l))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma DEF_REVERSE:
+  "rev = (SOME REVERSE. REVERSE [] = [] \<and> (\<forall>l x. REVERSE (x # l) = (REVERSE l) @ [x]))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma DEF_LENGTH:
+  "length = (SOME LENGTH. LENGTH [] = 0 \<and> (\<forall>h t. LENGTH (h # t) = Suc (LENGTH t)))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma DEF_MAP:
+  "map = (SOME MAP. (\<forall>f. MAP f [] = []) \<and> (\<forall>f h t. MAP f (h # t) = f h # MAP f t))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac xa)
+  apply simp_all
+  done
+
+lemma DEF_REPLICATE:
+  "replicate =
+    (SOME REPLICATE. (\<forall>x. REPLICATE 0 x = []) \<and> (\<forall>n x. REPLICATE (Suc n) x = x # REPLICATE n x))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma DEF_ITLIST:
+  "foldr = (SOME ITLIST. (\<forall>f b. ITLIST f [] b = b) \<and> (\<forall>h f t b. ITLIST f (h # t) b = f h (ITLIST f t b)))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac xa)
+  apply simp_all
+  done
+
+lemma DEF_ALL2: "list_all2 =
+  (SOME ALL2.
+    (\<forall>P l2. ALL2 P [] l2 = (l2 = [])) \<and>
+    (\<forall>h1 P t1 l2.
+      ALL2 P (h1 # t1) l2 = (if l2 = [] then False else P h1 (hd l2) \<and> ALL2 P t1 (tl l2))))"
+  apply (rule some_equality[symmetric])
+  apply (auto)
+  apply (case_tac l2, simp_all)
+  apply (case_tac l2, simp_all)
+  apply (case_tac l2, simp_all)
+  apply (simp add: fun_eq_iff)
+  apply (intro allI)
+  apply (induct_tac xa xb rule: list_induct2')
+  apply simp_all
+  done
+
+lemma ALL2:
+ "list_all2 P [] [] = True \<and>
+  list_all2 P (h1 # t1) [] = False \<and>
+  list_all2 P [] (h2 # t2) = False \<and>
+  list_all2 P (h1 # t1) (h2 # t2) = (P h1 h2 \<and> list_all2 P t1 t2)"
+  by simp
+
+lemma DEF_FILTER:
+  "filter = (SOME FILTER. (\<forall>P. FILTER P [] = []) \<and>
+     (\<forall>h P t. FILTER P (h # t) = (if P h then h # FILTER P t else FILTER P t)))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac xa)
+  apply simp_all
+  done
+
+fun map2 where
+  "map2 f [] [] = []"
+| "map2 f (h1 # t1) (h2 # t2) = (f h1 h2) # (map2 f t1 t2)"
+
+lemma MAP2:
+  "map2 f [] [] = [] \<and> map2 f (h1 # t1) (h2 # t2) = f h1 h2 # map2 f t1 t2"
+  by simp
+
+fun fold2 where
+  "fold2 f [] [] b = b"
+| "fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
+
+lemma ITLIST2:
+  "fold2 f [] [] b = b \<and> fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
+  by simp
+
+definition [simp]: "list_el x xs = nth xs x"
+
+lemma ZIP:
+  "zip [] [] = [] \<and> zip (h1 # t1) (h2 # t2) = (h1, h2) # (zip t1 t2)"
+  by simp
+
+lemma LAST_CLAUSES:
+  "last [h] = h \<and> last (h # k # t) = last (k # t)"
+  by simp
+
+lemma DEF_NULL:
+  "List.null = (SOME NULL. NULL [] = True \<and> (\<forall>h t. NULL (h # t) = False))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: fun_eq_iff null_def)
+  apply (case_tac x)
+  apply simp_all
+  done
+
+lemma DEF_ALL:
+  "list_all = (SOME u. (\<forall>P. u P [] = True) \<and> (\<forall>h P t. u P (h # t) = (P h \<and> u P t)))"
+  apply (rule some_equality[symmetric])
+  apply auto[1]
+  apply (simp add: fun_eq_iff)
+  apply (intro allI)
+  apply (induct_tac xa)
+  apply simp_all
+  done
+
+lemma MAP_EQ:
+  "list_all (\<lambda>x. f x = g x) l \<longrightarrow> map f l = map g l"
+  by (induct l) auto
+
+definition [simp]: "list_mem x xs = List.member xs x"
+
+lemma DEF_MEM:
+  "list_mem = (SOME MEM. (\<forall>x. MEM x [] = False) \<and> (\<forall>h x t. MEM x (h # t) = (x = h \<or> MEM x t)))"
+  apply (rule some_equality[symmetric])
+  apply (auto simp add: member_def)[1]
+  apply (simp add: fun_eq_iff)
+  apply (intro allI)
+  apply (induct_tac xa)
+  apply (simp_all add: member_def)
+  done
+
+lemma DEF_EX:
+  "list_ex = (SOME u. (\<forall>P. u P [] = False) \<and> (\<forall>h P t. u P (h # t) = (P h \<or> u P t)))"
+  apply (rule some_equality[symmetric])
+  apply (auto)
+  apply (simp add: fun_eq_iff)
+  apply (intro allI)
+  apply (induct_tac xa)
+  apply (simp_all)
+  done
+
+lemma ALL_IMP:
+  "(\<forall>x. x \<in> set l \<and> P x \<longrightarrow> Q x) \<and> list_all P l \<longrightarrow> list_all Q l"
+  by (simp add: list_all_iff)
+
+lemma NOT_EX: "(\<not> list_ex P l) = list_all (\<lambda>x. \<not> P x) l"
+  by (simp add: list_all_iff list_ex_iff)
+
+lemma NOT_ALL: "(\<not> list_all P l) = list_ex (\<lambda>x. \<not> P x) l"
+  by (simp add: list_all_iff list_ex_iff)
+
+lemma ALL_MAP: "list_all P (map f l) = list_all (P o f) l"
+  by (simp add: list_all_iff)
+
+lemma ALL_T: "list_all (\<lambda>x. True) l"
+  by (simp add: list_all_iff)
+
+lemma MAP_EQ_ALL2: "list_all2 (\<lambda>x y. f x = f y) l m \<longrightarrow> map f l = map f m"
+  by (induct l m rule: list_induct2') simp_all
+
+lemma ALL2_MAP: "list_all2 P (map f l) l = list_all (\<lambda>a. P (f a) a) l"
+  by (induct l) simp_all
+
+lemma MAP_EQ_DEGEN: "list_all (\<lambda>x. f x = x) l --> map f l = l"
+  by (induct l) simp_all
+
+lemma ALL2_AND_RIGHT:
+   "list_all2 (\<lambda>x y. P x \<and> Q x y) l m = (list_all P l \<and> list_all2 Q l m)"
+  by (induct l m rule: list_induct2') auto
+
+lemma ITLIST_EXTRA:
+  "foldr f (l @ [a]) b = foldr f l (f a b)"
+  by simp
+
+lemma ALL_MP:
+  "list_all (\<lambda>x. P x \<longrightarrow> Q x) l \<and> list_all P l \<longrightarrow> list_all Q l"
+  by (simp add: list_all_iff)
+
+lemma AND_ALL:
+  "(list_all P l \<and> list_all Q l) = list_all (\<lambda>x. P x \<and> Q x) l"
+  by (auto simp add: list_all_iff)
+
+lemma EX_IMP:
+  "(\<forall>x. x\<in>set l \<and> P x \<longrightarrow> Q x) \<and> list_ex P l \<longrightarrow> list_ex Q l"
+  by (auto simp add: list_ex_iff)
+
+lemma ALL_MEM:
+  "(\<forall>x. x\<in>set l \<longrightarrow> P x) = list_all P l"
+  by (auto simp add: list_all_iff)
+
+lemma EX_MAP:
+  "ALL P f l. list_ex P (map f l) = list_ex (P o f) l"
+  by (simp add: list_ex_iff)
+
+lemma EXISTS_EX:
+  "\<forall>P l. (EX x. list_ex (P x) l) = list_ex (\<lambda>s. EX x. P x s) l"
+  by (auto simp add: list_ex_iff)
+
+lemma FORALL_ALL:
+  "\<forall>P l. (\<forall>x. list_all (P x) l) = list_all (\<lambda>s. \<forall>x. P x s) l"
+  by (auto simp add: list_all_iff)
+
+lemma MEM_APPEND: "\<forall>x l1 l2. (x\<in>set (l1 @ l2)) = (x\<in>set l1 \<or> x\<in>set l2)"
+  by simp
+
+lemma MEM_MAP: "\<forall>f y l. (y\<in>set (map f l)) = (EX x. x\<in>set l \<and> y = f x)"
+  by auto
+
+lemma MEM_FILTER: "\<forall>P l x. (x\<in>set (filter P l)) = (P x \<and> x\<in>set l)"
+  by auto
+
+lemma EX_MEM: "(EX x. P x \<and> x\<in>set l) = list_ex P l"
+  by (auto simp add: list_ex_iff)
+
+lemma ALL2_MAP2:
+  "list_all2 P (map f l) (map g m) = list_all2 (\<lambda>x y. P (f x) (g y)) l m"
+  by (simp add: list_all2_map1 list_all2_map2)
+
+lemma ALL2_ALL:
+  "list_all2 P l l = list_all (\<lambda>x. P x x) l"
+  by (induct l) simp_all
+
+lemma LENGTH_MAP2:
+  "length l = length m \<longrightarrow> length (map2 f l m) = length m"
+  by (induct l m rule: list_induct2') simp_all
+
+lemma DEF_set_of_list:
+  "set = (SOME sol. sol [] = {} \<and> (\<forall>h t. sol (h # t) = insert h (sol t)))"
+  apply (rule some_equality[symmetric])
+  apply (simp_all)
+  apply (rule ext)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
+lemma IN_SET_OF_LIST:
+  "(x : set l) = (x : set l)"
+  by simp
+
+lemma DEF_BUTLAST:
+  "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))"
+  apply (rule some_equality[symmetric])
+  apply auto
+  apply (rule ext)
+  apply (induct_tac x)
+  apply auto
+  done
+
+lemma MONO_ALL:
+  "(ALL x. P x \<longrightarrow> Q x) \<longrightarrow> list_all P l \<longrightarrow> list_all Q l"
+  by (simp add: list_all_iff)
+
+lemma EL_TL: "l \<noteq> [] \<Longrightarrow> tl l ! x = l ! (x + 1)"
+  by (induct l) (simp_all)
+
+(* Assume the same behaviour outside of the usual domain.
+   For HD, LAST, EL it follows from "undefined = SOME _. False".
+
+   The definitions of TL and ZIP are different for empty lists.
+ *)
+axiomatization where
+  DEF_HD: "hd = (SOME HD. \<forall>t h. HD (h # t) = h)"
+
+axiomatization where
+  DEF_LAST: "last =
+    (SOME LAST. \<forall>h t. LAST (h # t) = (if t = [] then h else LAST t))"
+
+axiomatization where
+  DEF_EL: "list_el =
+    (SOME EL. (\<forall>l. EL 0 l = hd l) \<and> (\<forall>n l. EL (Suc n) l = EL n (tl l)))"
+
+end
diff -r 150f37dad503 -r f0285e69d704 src/HOL/Import/HOL_Light/HOLLightReal.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightReal.thy	Sat Mar 03 21:51:38 2012 +0100
@@ -0,0 +1,329 @@
+(*  Title:      HOL/Import/HOLLightReal.thy
+    Author:     Cezary Kaliszyk
+*)
+
+header {* Compatibility theorems for HOL Light reals *}
+
+theory HOLLightReal imports Real begin
+
+lemma REAL_OF_NUM_MAX:
+  "max (real (m :: nat)) (real n) = real (max m n)"
+  by simp
+
+lemma REAL_OF_NUM_MIN:
+  "min (real (m :: nat)) (real n) = real (min m n)"
+  by simp
+
+lemma REAL_POLY_NEG_CLAUSES:
+  "(\<forall>(x :: real). - x = - 1 * x) \<and> (\<forall>(x :: real) y. x - y = x + - 1 * y)"
+  by simp
+
+lemma REAL_MUL_AC:
+  "(m :: real) * n = n * m \<and> m * n * p = m * (n * p) \<and> m * (n * p) = n * (m * p)"
+  by simp
+
+lemma REAL_EQ_ADD_LCANCEL_0:
+  "((x :: real) + y = x) = (y = 0)"
+  by simp
+
+lemma REAL_EQ_ADD_RCANCEL_0:
+  "((x :: real) + y = y) = (x = 0)"
+  by simp
+
+lemma REAL_LT_ANTISYM:
+  "\<not> ((x :: real) < y \<and> y < x)"
+  by simp
+
+lemma REAL_LET_ANTISYM:
+  "\<not> ((x :: real) \<le> y \<and> y < x)"
+  by simp
+
+lemma REAL_LT_NEGTOTAL:
+  "(x :: real) = 0 \<or> 0 < x \<or> 0 < - x"
+  by auto
+
+lemma REAL_LT_ADDNEG:
+  "((y :: real) < x + - z) = (y + z < x)"
+  by auto
+
+lemma REAL_LT_ADDNEG2:
+  "((x :: real) + - y < z) = (x < z + y)"
+  by auto
+
+lemma REAL_LT_ADD1:
+  "(x :: real) \<le> y \<longrightarrow> x < y + 1"
+  by simp
+
+lemma REAL_SUB_ADD2:
+  "(y :: real) + (x - y) = x"
+  by simp
+
+lemma REAL_ADD_SUB:
+  "(x :: real) + y - x = y"
+  by simp
+
+lemma REAL_NEG_EQ:
+  "(- (x :: real) = y) = (x = - y)"
+  by auto
+
+lemma REAL_LE_ADDR:
+  "((x :: real) \<le> x + y) = (0 \<le> y)"
+  by simp
+
+lemma REAL_LE_ADDL:
+  "((y :: real) \<le> x + y) = (0 \<le> x)"
+  by simp
+
+lemma REAL_LT_ADDR:
+  "((x :: real) < x + y) = (0 < y)"
+  by simp
+
+lemma REAL_LT_ADDL:
+  "((y :: real) < x + y) = (0 < x)"
+  by simp
+
+lemma REAL_SUB_SUB:
+  "(x :: real) - y - x = - y"
+  by simp
+
+lemma REAL_SUB_LNEG:
+  "- (x :: real) - y = - (x + y)"
+  by simp
+
+lemma REAL_SUB_NEG2:
+  "- (x :: real) - - y = y - x"
+  by simp
+
+lemma REAL_SUB_TRIANGLE:
+  "(a :: real) - b + (b - c) = a - c"
+  by simp
+
+lemma REAL_SUB_SUB2:
+  "(x :: real) - (x - y) = y"
+  by simp
+
+lemma REAL_ADD_SUB2:
+  "(x :: real) - (x + y) = - y"
+  by simp
+
+lemma REAL_POS_NZ:
+  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
+  by simp
+
+lemma REAL_DIFFSQ:
+  "((x :: real) + y) * (x - y) = x * x - y * y"
+  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
+
+lemma REAL_ABS_TRIANGLE_LE:
+  "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
+  by auto
+
+lemma REAL_ABS_TRIANGLE_LT:
+  "abs (x :: real) + abs (y - x) < z \<longrightarrow> abs y < z"
+  by auto
+
+lemma REAL_ABS_REFL:
+  "(abs (x :: real) = x) = (0 \<le> x)"
+  by auto
+
+lemma REAL_ABS_BETWEEN:
+  "(0 < (d :: real) \<and> x - d < y \<and> y < x + d) = (abs (y - x) < d)"
+  by auto
+
+lemma REAL_ABS_BOUND:
+  "abs ((x :: real) - y) < d \<longrightarrow> y < x + d"
+  by auto
+
+lemma REAL_ABS_STILLNZ:
+  "abs ((x :: real) - y) < abs y \<longrightarrow> x \<noteq> 0"
+  by auto
+
+lemma REAL_ABS_CASES:
+  "(x :: real) = 0 \<or> 0 < abs x"
+  by simp
+
+lemma REAL_ABS_BETWEEN1:
+  "(x :: real) < z \<and> abs (y - x) < z - x \<longrightarrow> y < z"
+  by auto
+
+lemma REAL_ABS_SIGN:
+  "abs ((x :: real) - y) < y \<longrightarrow> 0 < x"
+  by auto
+
+lemma REAL_ABS_SIGN2:
+  "abs ((x :: real) - y) < - y \<longrightarrow> x < 0"
+  by auto
+
+lemma REAL_ABS_CIRCLE:
+  "abs (h :: real) < abs y - abs x \<longrightarrow> abs (x + h) < abs y"
+  by auto
+
+lemma REAL_BOUNDS_LT:
+  "(- (k :: real) < x \<and> x < k) = (abs x < k)"
+  by auto
+
+lemma REAL_MIN_MAX:
+  "min (x :: real) y = - max (- x) (- y)"
+  by auto
+
+lemma REAL_MAX_MIN:
+  "max (x :: real) y = - min (- x) (- y)"
+  by auto
+
+lemma REAL_MAX_MAX:
+  "(x :: real) \<le> max x y \<and> y \<le> max x y"
+  by simp
+
+lemma REAL_MIN_MIN:
+  "min (x :: real) y \<le> x \<and> min x y \<le> y"
+  by simp
+
+lemma REAL_MAX_ACI:
+  "max (x :: real) y = max y x \<and>
+   max (max x y) z = max x (max y z) \<and>
+   max x (max y z) = max y (max x z) \<and> max x x = x \<and> max x (max x y) = max x y"
+  by auto
+
+
+lemma REAL_MIN_ACI:
+  "min (x :: real) y = min y x \<and>
+   min (min x y) z = min x (min y z) \<and>
+   min x (min y z) = min y (min x z) \<and> min x x = x \<and> min x (min x y) = min x y"
+  by auto
+
+lemma REAL_EQ_MUL_RCANCEL:
+  "((x :: real) * z = y * z) = (x = y \<or> z = 0)"
+  by auto
+
+lemma REAL_MUL_LINV_UNIQ:
+  "(x :: real) * y = 1 \<longrightarrow> inverse y = x"
+  by (metis inverse_inverse_eq inverse_unique)
+
+lemma REAL_DIV_RMUL:
+  "(y :: real) \<noteq> 0 \<longrightarrow> x / y * y = x"
+  by simp
+
+lemma REAL_DIV_LMUL:
+  "(y :: real) \<noteq> 0 \<longrightarrow> y * (x / y) = x"
+  by simp
+
+lemma REAL_LT_IMP_NZ:
+  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
+  by simp
+
+lemma REAL_LT_LCANCEL_IMP:
+  "0 < (x :: real) \<and> x * y < x * z \<longrightarrow> y < z"
+  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
+
+lemma REAL_LT_RCANCEL_IMP:
+  "0 < (z :: real) \<and> x * z < y * z \<longrightarrow> x < y"
+  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
+
+lemma REAL_MUL_POS_LE:
+  "(0 \<le> (x :: real) * y) = (x = 0 \<or> y = 0 \<or> 0 < x \<and> 0 < y \<or> x < 0 \<and> y < 0)"
+  by (metis less_eq_real_def mult_eq_0_iff zero_le_mult_iff)
+
+lemma REAL_EQ_RDIV_EQ:
+  "0 < (z :: real) \<longrightarrow> (x = y / z) = (x * z = y)"
+  by auto
+
+lemma REAL_EQ_LDIV_EQ:
+  "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)"
+  by auto
+
+lemma REAL_SUB_INV:
+  "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
+  by (simp add: division_ring_inverse_diff divide_real_def)
+
+lemma REAL_DOWN:
+  "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
+  by (intro impI exI[of _ "d / 2"]) simp
+
+lemma REAL_POW_MONO_LT:
+  "1 < (x :: real) \<and> m < n \<longrightarrow> x ^ m < x ^ n"
+  by simp
+
+lemma REAL_POW_MONO:
+  "1 \<le> (x :: real) \<and> m \<le> n \<longrightarrow> x ^ m \<le> x ^ n"
+  by (cases "m < n", cases "x = 1") auto
+
+lemma REAL_EQ_LCANCEL_IMP:
+  "(z :: real) \<noteq> 0 \<and> z * x = z * y \<longrightarrow> x = y"
+  by auto
+
+lemma REAL_LE_DIV:
+  "0 \<le> (x :: real) \<and> 0 \<le> y \<longrightarrow> 0 \<le> x / y"
+  by (simp add: zero_le_divide_iff)
+
+lemma REAL_10: "(1::real) \<noteq> 0"
+  by simp
+
+lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
+  by simp
+
+lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
+  by simp
+
+lemma REAL_ADD_LINV:  "-x + x = (0::real)"
+  by simp
+
+lemma REAL_MUL_LINV: "x \<noteq> (0::real) \<Longrightarrow> inverse x * x = 1"
+  by simp
+
+lemma REAL_LT_TOTAL: "((x::real) = y) \<or> x < y \<or> y < x"
+  by auto
+
+lemma real_lte: "((x::real) \<le> y) = (\<not>(y < x))"
+  by auto
+
+lemma real_of_num: "((0::real) = 0) \<and> (!n. real (Suc n) = real n + 1)"
+  by (simp add: real_of_nat_Suc)
+
+lemma abs: "abs (x::real) = (if 0 \<le> x then x else -x)"
+  by (simp add: abs_if)
+
+lemma pow: "(!x::real. x ^ 0 = 1) \<and> (!x::real. \<forall>n. x ^ (Suc n) = x * x ^ n)"
+  by simp
+
+lemma REAL_POLY_CLAUSES:
+  "(\<forall>(x :: real) y z. x + (y + z) = x + y + z) \<and>
+   (\<forall>(x :: real) y. x + y = y + x) \<and>
+   (\<forall>(x :: real). 0 + x = x) \<and>
+   (\<forall>(x :: real) y z. x * (y * z) = x * y * z) \<and>
+   (\<forall>(x :: real) y. x * y = y * x) \<and>
+   (\<forall>(x :: real). 1 * x = x) \<and>
+   (\<forall>(x :: real). 0 * x = 0) \<and>
+   (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
+   (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
+  by (auto simp add: right_distrib)
+
+lemma REAL_COMPLETE:
+  "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
+   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
+          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
+  using complete_real[unfolded Ball_def, of "Collect P"] by auto
+
+lemma REAL_COMPLETE_SOMEPOS:
+  "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
+   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
+          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
+  using REAL_COMPLETE by auto
+
+lemma REAL_ADD_AC:
+  "(m :: real) + n = n + m \<and> m + n + p = m + (n + p) \<and> m + (n + p) = n + (m + p)"
+  by simp
+
+lemma REAL_LE_RNEG:
+  "((x :: real) \<le> - y) = (x + y \<le> 0)"
+  by auto
+
+lemma REAL_LE_NEGTOTAL:
+  "0 \<le> (x :: real) \<or> 0 \<le> - x"
+  by auto
+
+lemma DEF_real_sgn:
+  "sgn = (\<lambda>u. if (0 :: real) < u then 1 else if u < 0 then - 1 else 0)"
+  by (simp add: ext)
+
+end
+