--- 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
--- 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
--- 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
-
--- 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
-
--- 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
--- 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
-
--- 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
--- /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
+
--- /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
--- /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
+