# HG changeset patch # User skalberg # Date 1112374757 -7200 # Node ID b1f486a9c56b94433c124cccd2db1d8df5c30323 # Parent b45393fb38c0accd2e8e960c304df78b9fb7818e Updated import configuration. diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Apr 01 18:59:17 2005 +0200 @@ -3,13 +3,13 @@ Author: Sebastian Skalberg (TU Muenchen) *) -theory GenHOL4Base = HOL4Compat + HOL4Syntax:; +theory GenHOL4Base = "../HOL4Compat" + "../HOL4Syntax":; import_segment "hol4"; setup_dump "../HOL" "HOL4Base"; -append_dump "theory HOL4Base = HOL4Compat + HOL4Syntax:"; +append_dump {*theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":*}; import_theory bool; @@ -50,8 +50,8 @@ sum > "+"; const_maps - INL > Inl - INR > Inr + INL > Sum_Type.Inl + INR > Sum_Type.Inr ISL > HOL4Compat.ISL ISR > HOL4Compat.ISR OUTL > HOL4Compat.OUTL @@ -166,7 +166,7 @@ import_theory prim_rec; const_maps - "<" > "op <" :: "[nat,nat]\bool"; + "<" > "op <" :: "[nat,nat]=>bool"; end_import; @@ -181,15 +181,15 @@ ">" > HOL4Compat.nat_gt ">=" > HOL4Compat.nat_ge FUNPOW > HOL4Compat.FUNPOW - "<=" > "op <=" :: "[nat,nat]\bool" - "+" > "op +" :: "[nat,nat]\nat" - "*" > "op *" :: "[nat,nat]\nat" - "-" > "op -" :: "[nat,nat]\nat" - MIN > HOL.min :: "[nat,nat]\nat" - MAX > HOL.max :: "[nat,nat]\nat" - DIV > "Divides.op div" :: "[nat,nat]\nat" - MOD > "Divides.op mod" :: "[nat,nat]\nat" - EXP > Nat.power :: "[nat,nat]\nat"; + "<=" > "op <=" :: "[nat,nat]=>bool" + "+" > "op +" :: "[nat,nat]=>nat" + "*" > "op *" :: "[nat,nat]=>nat" + "-" > "op -" :: "[nat,nat]=>nat" + MIN > Orderings.min :: "[nat,nat]=>nat" + MAX > Orderings.max :: "[nat,nat]=>nat" + DIV > "Divides.op div" :: "[nat,nat]=>nat" + MOD > "Divides.op mod" :: "[nat,nat]=>nat" + EXP > Nat.power :: "[nat,nat]=>nat"; end_import; @@ -208,7 +208,7 @@ import_theory divides; const_maps - divides > "Divides.op dvd" :: "[nat,nat]\bool"; + divides > "Divides.op dvd" :: "[nat,nat]=>bool"; end_import; diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Apr 01 18:59:17 2005 +0200 @@ -19,11 +19,11 @@ const_maps real_0 > 0 :: real real_1 > 1 :: real - real_neg > uminus :: "real \ real" - inv > HOL.inverse :: "real \ real" - real_add > "op +" :: "[real,real] \ real" - real_mul > "op *" :: "[real,real] \ real" - real_lt > "op <" :: "[real,real] \ bool"; + real_neg > uminus :: "real => real" + inv > HOL.inverse :: "real => real" + real_add > "op +" :: "[real,real] => real" + real_mul > "op *" :: "[real,real] => real" + real_lt > "op <" :: "[real,real] => bool"; ignore_thms real_TY_DEF @@ -51,12 +51,12 @@ const_maps real_gt > HOL4Compat.real_gt real_ge > HOL4Compat.real_ge - real_lte > "op <=" :: "[real,real] \ bool" - real_sub > "op -" :: "[real,real] \ real" - "/" > HOL.divide :: "[real,real] \ real" - pow > Nat.power :: "[real,nat] \ real" - abs > HOL.abs :: "real \ real" - real_of_num > RealDef.real :: "nat \ real"; + real_lte > "op <=" :: "[real,real] => bool" + real_sub > "op -" :: "[real,real] => real" + "/" > HOL.divide :: "[real,real] => real" + pow > Nat.power :: "[real,nat] => real" + abs > HOL.abs :: "real => real" + real_of_num > RealDef.real :: "nat => real"; end_import; diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/Generate-HOL/ROOT.ML --- a/src/HOL/Import/Generate-HOL/ROOT.ML Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/Generate-HOL/ROOT.ML Fri Apr 01 18:59:17 2005 +0200 @@ -3,8 +3,6 @@ Author: Sebastian Skalberg (TU Muenchen) *) -with_path ".." use_thy "HOL4Compat"; -with_path ".." use_thy "HOL4Syntax"; use_thy "GenHOL4Prob"; use_thy "GenHOL4Vec"; use_thy "GenHOL4Word32"; diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/HOL4Base.thy --- a/src/HOL/Import/HOL/HOL4Base.thy Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/HOL4Base.thy Fri Apr 01 18:59:17 2005 +0200 @@ -1,4 +1,6 @@ -theory HOL4Base = HOL4Compat + HOL4Syntax: +(* AUTOMATICALLY GENERATED, DO NOT EDIT! *) + +theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax": ;setup_theory bool @@ -755,7 +757,11 @@ lemma CURRY_ONE_ONE_THM: "(curry f = curry g) = (f = g)" by (import pair CURRY_ONE_ONE_THM) -lemma UNCURRY_ONE_ONE_THM: "(split f = split g) = (f = g)" +lemma UNCURRY_ONE_ONE_THM: "(op =::bool => bool => bool) + ((op =::('a * 'b => 'c) => ('a * 'b => 'c) => bool) + ((split::('a => 'b => 'c) => 'a * 'b => 'c) (f::'a => 'b => 'c)) + ((split::('a => 'b => 'c) => 'a * 'b => 'c) (g::'a => 'b => 'c))) + ((op =::('a => 'b => 'c) => ('a => 'b => 'c) => bool) f g)" by (import pair UNCURRY_ONE_ONE_THM) lemma pair_Axiom: "ALL f. EX x. ALL xa y. x (xa, y) = f xa y" @@ -772,18 +778,53 @@ lemma ELIM_PFORALL: "(ALL p. P (fst p) (snd p)) = (ALL p1. All (P p1))" by (import pair ELIM_PFORALL) -lemma PFORALL_THM: "ALL x. (ALL xa. All (x xa)) = All (split x)" +lemma PFORALL_THM: "(All::(('a => 'b => bool) => bool) => bool) + (%x::'a => 'b => bool. + (op =::bool => bool => bool) + ((All::('a => bool) => bool) + (%xa::'a. (All::('b => bool) => bool) (x xa))) + ((All::('a * 'b => bool) => bool) + ((split::('a => 'b => bool) => 'a * 'b => bool) x)))" by (import pair PFORALL_THM) -lemma PEXISTS_THM: "ALL x. (EX xa. Ex (x xa)) = Ex (split x)" +lemma PEXISTS_THM: "(All::(('a => 'b => bool) => bool) => bool) + (%x::'a => 'b => bool. + (op =::bool => bool => bool) + ((Ex::('a => bool) => bool) + (%xa::'a. (Ex::('b => bool) => bool) (x xa))) + ((Ex::('a * 'b => bool) => bool) + ((split::('a => 'b => bool) => 'a * 'b => bool) x)))" by (import pair PEXISTS_THM) -lemma LET2_RAND: "ALL (x::'c => 'd) (xa::'a * 'b) xb::'a => 'b => 'c. - x (Let xa (split xb)) = (let (xa::'a, y::'b) = xa in x (xb xa y))" +lemma LET2_RAND: "(All::(('c => 'd) => bool) => bool) + (%x::'c => 'd. + (All::('a * 'b => bool) => bool) + (%xa::'a * 'b. + (All::(('a => 'b => 'c) => bool) => bool) + (%xb::'a => 'b => 'c. + (op =::'d => 'd => bool) + (x ((Let::'a * 'b => ('a * 'b => 'c) => 'c) xa + ((split::('a => 'b => 'c) => 'a * 'b => 'c) xb))) + ((Let::'a * 'b => ('a * 'b => 'd) => 'd) xa + ((split::('a => 'b => 'd) => 'a * 'b => 'd) + (%(xa::'a) y::'b. x (xb xa y)))))))" by (import pair LET2_RAND) -lemma LET2_RATOR: "ALL (x::'a1 * 'a2) (xa::'a1 => 'a2 => 'b => 'c) xb::'b. - Let x (split xa) xb = (let (x::'a1, y::'a2) = x in xa x y xb)" +lemma LET2_RATOR: "(All::('a1 * 'a2 => bool) => bool) + (%x::'a1 * 'a2. + (All::(('a1 => 'a2 => 'b => 'c) => bool) => bool) + (%xa::'a1 => 'a2 => 'b => 'c. + (All::('b => bool) => bool) + (%xb::'b. + (op =::'c => 'c => bool) + ((Let::'a1 * 'a2 => ('a1 * 'a2 => 'b => 'c) => 'b => 'c) x + ((split::('a1 => 'a2 => 'b => 'c) + => 'a1 * 'a2 => 'b => 'c) + xa) + xb) + ((Let::'a1 * 'a2 => ('a1 * 'a2 => 'c) => 'c) x + ((split::('a1 => 'a2 => 'c) => 'a1 * 'a2 => 'c) + (%(x::'a1) y::'a2. xa x y xb))))))" by (import pair LET2_RATOR) lemma pair_case_cong: "ALL x xa xb. @@ -1116,10 +1157,10 @@ ((Not::bool => bool) (P m)))))))" by (import arithmetic WOP) -lemma INV_PRE_LESS: "ALL m. 0 < m --> (ALL n. (PRE m < PRE n) = (m < n))" +lemma INV_PRE_LESS: "ALL m>0. ALL n. (PRE m < PRE n) = (m < n)" by (import arithmetic INV_PRE_LESS) -lemma INV_PRE_LESS_EQ: "ALL n. 0 < n --> (ALL m. (PRE m <= PRE n) = (m <= n))" +lemma INV_PRE_LESS_EQ: "ALL n>0. ALL m. (PRE m <= PRE n) = (m <= n)" by (import arithmetic INV_PRE_LESS_EQ) lemma SUB_EQ_EQ_0: "ALL (m::nat) n::nat. (m - n = m) = (m = (0::nat) | n = (0::nat))" @@ -1282,7 +1323,7 @@ (0::nat) < n --> (EX (x::nat) q::nat. k = q * n + x & x < n)" by (import arithmetic DA) -lemma DIV_LESS_EQ: "ALL n::nat. (0::nat) < n --> (ALL k::nat. k div n <= k)" +lemma DIV_LESS_EQ: "ALL n>0::nat. ALL k::nat. k div n <= k" by (import arithmetic DIV_LESS_EQ) lemma DIV_UNIQUE: "ALL (n::nat) (k::nat) q::nat. @@ -1296,33 +1337,28 @@ lemma DIV_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) div n = q)" by (import arithmetic DIV_MULT) -lemma MOD_EQ_0: "ALL n::nat. (0::nat) < n --> (ALL k::nat. k * n mod n = (0::nat))" +lemma MOD_EQ_0: "ALL n>0::nat. ALL k::nat. k * n mod n = (0::nat)" by (import arithmetic MOD_EQ_0) -lemma ZERO_MOD: "ALL n::nat. (0::nat) < n --> (0::nat) mod n = (0::nat)" +lemma ZERO_MOD: "ALL n>0::nat. (0::nat) mod n = (0::nat)" by (import arithmetic ZERO_MOD) -lemma ZERO_DIV: "ALL n::nat. (0::nat) < n --> (0::nat) div n = (0::nat)" +lemma ZERO_DIV: "ALL n>0::nat. (0::nat) div n = (0::nat)" by (import arithmetic ZERO_DIV) lemma MOD_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) mod n = r)" by (import arithmetic MOD_MULT) -lemma MOD_TIMES: "ALL n::nat. - (0::nat) < n --> (ALL (q::nat) r::nat. (q * n + r) mod n = r mod n)" +lemma MOD_TIMES: "ALL n>0::nat. ALL (q::nat) r::nat. (q * n + r) mod n = r mod n" by (import arithmetic MOD_TIMES) -lemma MOD_PLUS: "ALL n::nat. - (0::nat) < n --> - (ALL (j::nat) k::nat. (j mod n + k mod n) mod n = (j + k) mod n)" +lemma MOD_PLUS: "ALL n>0::nat. ALL (j::nat) k::nat. (j mod n + k mod n) mod n = (j + k) mod n" by (import arithmetic MOD_PLUS) -lemma MOD_MOD: "ALL n::nat. (0::nat) < n --> (ALL k::nat. k mod n mod n = k mod n)" +lemma MOD_MOD: "ALL n>0::nat. ALL k::nat. k mod n mod n = k mod n" by (import arithmetic MOD_MOD) -lemma ADD_DIV_ADD_DIV: "ALL x::nat. - (0::nat) < x --> - (ALL (xa::nat) r::nat. (xa * x + r) div x = xa + r div x)" +lemma ADD_DIV_ADD_DIV: "ALL x>0::nat. ALL (xa::nat) r::nat. (xa * x + r) div x = xa + r div x" by (import arithmetic ADD_DIV_ADD_DIV) lemma MOD_MULT_MOD: "ALL (m::nat) n::nat. @@ -1330,7 +1366,7 @@ (ALL x::nat. x mod (n * m) mod n = x mod n)" by (import arithmetic MOD_MULT_MOD) -lemma DIVMOD_ID: "ALL n::nat. (0::nat) < n --> n div n = (1::nat) & n mod n = (0::nat)" +lemma DIVMOD_ID: "ALL n>0::nat. n div n = (1::nat) & n mod n = (0::nat)" by (import arithmetic DIVMOD_ID) lemma DIV_DIV_DIV_MULT: "ALL (x::nat) xa::nat. @@ -1348,9 +1384,7 @@ P (p mod q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P r)" by (import arithmetic MOD_P) -lemma MOD_TIMES2: "ALL n::nat. - (0::nat) < n --> - (ALL (j::nat) k::nat. j mod n * (k mod n) mod n = j * k mod n)" +lemma MOD_TIMES2: "ALL n>0::nat. ALL (j::nat) k::nat. j mod n * (k mod n) mod n = j * k mod n" by (import arithmetic MOD_TIMES2) lemma MOD_COMMON_FACTOR: "ALL (n::nat) (p::nat) q::nat. @@ -1362,7 +1396,7 @@ nat_case b f M = nat_case b' f' M'" by (import arithmetic num_case_cong) -lemma SUC_ELIM_THM: "ALL P. (ALL n. P (Suc n) n) = (ALL n. 0 < n --> P n (n - 1))" +lemma SUC_ELIM_THM: "ALL P. (ALL n. P (Suc n) n) = (ALL n>0. P n (n - 1))" by (import arithmetic SUC_ELIM_THM) lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat) - (b::nat)) = @@ -1375,7 +1409,7 @@ lemma MULT_INCREASES: "ALL m n. 1 < m & 0 < n --> Suc n <= m * n" by (import arithmetic MULT_INCREASES) -lemma EXP_ALWAYS_BIG_ENOUGH: "ALL b::nat. (1::nat) < b --> (ALL n::nat. EX m::nat. n <= b ^ m)" +lemma EXP_ALWAYS_BIG_ENOUGH: "ALL b>1::nat. ALL n::nat. EX m::nat. n <= b ^ m" by (import arithmetic EXP_ALWAYS_BIG_ENOUGH) lemma EXP_EQ_0: "ALL (n::nat) m::nat. (n ^ m = (0::nat)) = (n = (0::nat) & (0::nat) < m)" @@ -2449,7 +2483,7 @@ lemma NOT_LT_DIV: "ALL (a::nat) b::nat. (0::nat) < b & b < a --> ~ a dvd b" by (import divides NOT_LT_DIV) -lemma DIVIDES_FACT: "ALL b. 0 < b --> b dvd FACT b" +lemma DIVIDES_FACT: "ALL b>0. b dvd FACT b" by (import divides DIVIDES_FACT) lemma DIVIDES_MULT_LEFT: "ALL (x::nat) xa::nat. (x * xa dvd xa) = (xa = (0::nat) | x = (1::nat))" @@ -2661,9 +2695,21 @@ EL n (zip l1 l2) = (EL n l1, EL n l2)" by (import list EL_ZIP) -lemma MAP2_ZIP: "ALL l1 l2. - length l1 = length l2 --> - (ALL f. map2 f l1 l2 = map (split f) (zip l1 l2))" +lemma MAP2_ZIP: "(All::('a list => bool) => bool) + (%l1::'a list. + (All::('b list => bool) => bool) + (%l2::'b list. + (op -->::bool => bool => bool) + ((op =::nat => nat => bool) ((size::'a list => nat) l1) + ((size::'b list => nat) l2)) + ((All::(('a => 'b => 'c) => bool) => bool) + (%f::'a => 'b => 'c. + (op =::'c list => 'c list => bool) + ((map2::('a => 'b => 'c) => 'a list => 'b list => 'c list) + f l1 l2) + ((map::('a * 'b => 'c) => ('a * 'b) list => 'c list) + ((split::('a => 'b => 'c) => 'a * 'b => 'c) f) + ((zip::'a list => 'b list => ('a * 'b) list) l1 l2))))))" by (import list MAP2_ZIP) lemma MEM_EL: "(All::('a list => bool) => bool) @@ -4260,9 +4306,6 @@ lemma NULL_FOLDL: "ALL l. null l = foldl (%x l'. False) True l" by (import rich_list NULL_FOLDL) -lemma FILTER_REVERSE: "ALL P l. filter P (rev l) = rev (filter P l)" - by (import rich_list FILTER_REVERSE) - lemma SEG_LENGTH_ID: "ALL l. SEG (length l) 0 l = l" by (import rich_list SEG_LENGTH_ID) @@ -4539,7 +4582,7 @@ lemma ELL_0_SNOC: "ALL l x. ELL 0 (SNOC x l) = x" by (import rich_list ELL_0_SNOC) -lemma ELL_SNOC: "ALL n. 0 < n --> (ALL x l. ELL n (SNOC x l) = ELL (PRE n) l)" +lemma ELL_SNOC: "ALL n>0. ALL x l. ELL n (SNOC x l) = ELL (PRE n) l" by (import rich_list ELL_SNOC) lemma ELL_SUC_SNOC: "ALL n x xa. ELL (Suc n) (SNOC x xa) = ELL n xa" @@ -4615,9 +4658,6 @@ lemma FLAT_FLAT: "ALL l. concat (concat l) = concat (map concat l)" by (import rich_list FLAT_FLAT) -lemma ALL_EL_REVERSE: "ALL P l. list_all P (rev l) = list_all P l" - by (import rich_list ALL_EL_REVERSE) - lemma SOME_EL_REVERSE: "ALL P l. list_exists P (rev l) = list_exists P l" by (import rich_list SOME_EL_REVERSE) @@ -4735,7 +4775,7 @@ lemma EL_MAP: "ALL n l. n < length l --> (ALL f. EL n (map f l) = f (EL n l))" by (import rich_list EL_MAP) -lemma EL_CONS: "ALL n. 0 < n --> (ALL x l. EL n (x # l) = EL (PRE n) l)" +lemma EL_CONS: "ALL n>0. ALL x l. EL n (x # l) = EL (PRE n) l" by (import rich_list EL_CONS) lemma EL_SEG: "ALL n l. n < length l --> EL n l = hd (SEG 1 n l)" @@ -4805,7 +4845,7 @@ lemma LENGTH_REPLICATE: "ALL n x. length (REPLICATE n x) = n" by (import rich_list LENGTH_REPLICATE) -lemma IS_EL_REPLICATE: "ALL n. 0 < n --> (ALL x. x mem REPLICATE n x)" +lemma IS_EL_REPLICATE: "ALL n>0. ALL x. x mem REPLICATE n x" by (import rich_list IS_EL_REPLICATE) lemma ALL_EL_REPLICATE: "ALL x n. list_all (op = x) (REPLICATE n x)" @@ -4837,9 +4877,24 @@ constdefs BIND :: "('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a" - "BIND == %g f. split f o g" - -lemma BIND_DEF: "ALL g f. BIND g f = split f o g" + "(op ==::(('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a) + => (('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a) + => prop) + (BIND::('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a) + (%(g::'a => 'b * 'a) f::'b => 'a => 'c * 'a. + (op o::('b * 'a => 'c * 'a) => ('a => 'b * 'a) => 'a => 'c * 'a) + ((split::('b => 'a => 'c * 'a) => 'b * 'a => 'c * 'a) f) g)" + +lemma BIND_DEF: "(All::(('a => 'b * 'a) => bool) => bool) + (%g::'a => 'b * 'a. + (All::(('b => 'a => 'c * 'a) => bool) => bool) + (%f::'b => 'a => 'c * 'a. + (op =::('a => 'c * 'a) => ('a => 'c * 'a) => bool) + ((BIND::('a => 'b * 'a) + => ('b => 'a => 'c * 'a) => 'a => 'c * 'a) + g f) + ((op o::('b * 'a => 'c * 'a) => ('a => 'b * 'a) => 'a => 'c * 'a) + ((split::('b => 'a => 'c * 'a) => 'b * 'a => 'c * 'a) f) g)))" by (import state_transformer BIND_DEF) constdefs diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/HOL4Prob.thy --- a/src/HOL/Import/HOL/HOL4Prob.thy Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/HOL4Prob.thy Fri Apr 01 18:59:17 2005 +0200 @@ -1,3 +1,5 @@ +(* AUTOMATICALLY GENERATED, DO NOT EDIT! *) + theory HOL4Prob = HOL4Real: ;setup_theory prob_extra @@ -26,10 +28,10 @@ ((op +::nat => nat => nat) ((op *::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))) q) r)) ((op |::bool => bool => bool) @@ -39,17 +41,17 @@ ((op =::nat => nat => bool) q ((op div::nat => nat => nat) n ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((op =::nat => nat => bool) r ((op mod::nat => nat => nat) n ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))))))" by (import prob_extra DIV_TWO_UNIQUE) lemma DIVISION_TWO: "ALL n::nat. @@ -75,16 +77,16 @@ ((op <::nat => nat => bool) ((op div::nat => nat => nat) m ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) ((op div::nat => nat => nat) n ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((op <::nat => nat => bool) m n)))" by (import prob_extra DIV_TWO_MONO) @@ -97,16 +99,16 @@ ((op <::nat => nat => bool) ((op div::nat => nat => nat) m ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) ((op div::nat => nat => nat) n ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((op <::nat => nat => bool) m n))))" by (import prob_extra DIV_TWO_MONO_EVEN) @@ -203,18 +205,18 @@ ((op ^::real => nat => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) n) ((op ^::real => nat => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) m))))" by (import prob_extra POW_HALF_MONO) @@ -2527,10 +2529,10 @@ ((op *::real => real => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) ((prob::((nat => bool) => bool) => real) p)))))" by (import prob PROB_INTER_SHD) @@ -3155,10 +3157,10 @@ ((op ^::real => nat => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) - (Numeral.Pls::bin) (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) + (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit)))) ((size::bool list => nat) x)) ((prob::((nat => bool) => bool) => real) q))))))))" by (import prob_indep INDEP_INDEP_SET_LEMMA) @@ -3381,10 +3383,10 @@ (op -->::bool => bool => bool) (P ((op div::nat => nat => nat) ((Suc::nat => nat) v) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) (P ((Suc::nat => nat) v))))) ((All::(nat => bool) => bool) P))" by (import prob_uniform unif_bound_ind) @@ -3435,10 +3437,10 @@ (op -->::bool => bool => bool) (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) - (Numeral.Pls::bin) (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) s) (P ((Suc::nat => nat) v2) s))))) ((All::(nat => bool) => bool) @@ -3715,15 +3717,15 @@ ((op <=::nat => nat => bool) ((op ^::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))) ((unif_bound::nat => nat) n)) ((op *::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))) n)))" by (import prob_uniform UNIF_BOUND_UPPER) @@ -3770,10 +3772,10 @@ ((op <=::nat => nat => bool) k ((op ^::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))) ((unif_bound::nat => nat) n))) ((op =::real => real => bool) ((prob::((nat => bool) => bool) => real) @@ -3787,10 +3789,10 @@ ((op ^::real => nat => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) ((unif_bound::nat => nat) n))))))" by (import prob_uniform PROB_UNIF_BOUND) @@ -3906,10 +3908,10 @@ ((op ^::real => nat => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) - (Numeral.Pls::bin) (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) + (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit)))) t))))))" by (import prob_uniform PROB_UNIFORM_PAIR_SUC) @@ -3937,10 +3939,10 @@ ((op ^::real => nat => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) t)))))" by (import prob_uniform PROB_UNIFORM_SUC) @@ -3968,10 +3970,10 @@ ((op ^::real => nat => real) ((op /::real => real => real) (1::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) t)))))" by (import prob_uniform PROB_UNIFORM) diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/HOL4Real.thy --- a/src/HOL/Import/HOL/HOL4Real.thy Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/HOL4Real.thy Fri Apr 01 18:59:17 2005 +0200 @@ -1,3 +1,5 @@ +(* AUTOMATICALLY GENERATED, DO NOT EDIT! *) + theory HOL4Real = HOL4Base: ;setup_theory realax @@ -254,9 +256,6 @@ lemma REAL_LT_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y < x)" by (import real REAL_LT_ANTISYM) -lemma REAL_LET_TOTAL: "ALL (x::real) y::real. x <= y | y < x" - by (import real REAL_LET_TOTAL) - lemma REAL_LTE_TOTAL: "ALL (x::real) y::real. x < y | y <= x" by (import real REAL_LTE_TOTAL) @@ -284,6 +283,12 @@ lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x" by (import real REAL_SUB_ADD2) +lemma REAL_SUB_LT: "ALL (x::real) y::real. ((0::real) < x - y) = (y < x)" + by (import real REAL_SUB_LT) + +lemma REAL_SUB_LE: "ALL (x::real) y::real. ((0::real) <= x - y) = (y <= x)" + by (import real REAL_SUB_LE) + lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y" by (import real REAL_ADD_SUB) @@ -307,7 +312,7 @@ lemma REAL_LINV_UNIQ: "ALL (x::real) y::real. x * y = (1::real) --> x = inverse y" by (import real REAL_LINV_UNIQ) -lemma REAL_LE_INV: "ALL x::real. (0::real) <= x --> (0::real) <= inverse x" +lemma REAL_LE_INV: "ALL x>=0::real. (0::real) <= inverse x" by (import real REAL_LE_INV) lemma REAL_LE_ADDR: "ALL (x::real) y::real. (x <= x + y) = ((0::real) <= y)" @@ -355,7 +360,7 @@ lemma REAL_DIV_RMUL: "ALL (x::real) y::real. y ~= (0::real) --> x / y * y = x" by (import real REAL_DIV_RMUL) -lemma REAL_DOWN: "ALL x::real. (0::real) < x --> (EX xa::real. (0::real) < xa & xa < x)" +lemma REAL_DOWN: "ALL x>0::real. EX xa>0::real. xa < x" by (import real REAL_DOWN) lemma REAL_SUB_SUB: "ALL (x::real) y::real. x - y - x = - y" @@ -417,7 +422,7 @@ lemma REAL_LT_1: "ALL (x::real) y::real. (0::real) <= x & x < y --> x / y < (1::real)" by (import real REAL_LT_1) -lemma REAL_POS_NZ: "ALL x::real. (0::real) < x --> x ~= (0::real)" +lemma REAL_POS_NZ: "ALL x>0::real. x ~= (0::real)" by (import real REAL_POS_NZ) lemma REAL_EQ_LMUL_IMP: "ALL (x::real) (xa::real) xb::real. @@ -447,9 +452,6 @@ abs w < y & abs x < z --> abs (w * x) < y * z" by (import real ABS_LT_MUL2) -lemma ABS_SUB: "ALL (x::real) y::real. abs (x - y) = abs (y - x)" - by (import real ABS_SUB) - lemma ABS_REFL: "ALL x::real. (abs x = x) = ((0::real) <= x)" by (import real ABS_REFL) @@ -492,16 +494,16 @@ x < y" by (import real ABS_BETWEEN2) -lemma POW_PLUS1: "ALL e. 0 < e --> (ALL n. 1 + real n * e <= (1 + e) ^ n)" +lemma POW_PLUS1: "ALL e>0. ALL n. 1 + real n * e <= (1 + e) ^ n" by (import real POW_PLUS1) lemma POW_M1: "ALL n::nat. abs ((- (1::real)) ^ n) = (1::real)" by (import real POW_M1) -lemma REAL_LE1_POW2: "ALL x::real. (1::real) <= x --> (1::real) <= x ^ 2" +lemma REAL_LE1_POW2: "ALL x>=1::real. (1::real) <= x ^ 2" by (import real REAL_LE1_POW2) -lemma REAL_LT1_POW2: "ALL x::real. (1::real) < x --> (1::real) < x ^ 2" +lemma REAL_LT1_POW2: "ALL x>1::real. (1::real) < x ^ 2" by (import real REAL_LT1_POW2) lemma POW_POS_LT: "ALL (x::real) n::nat. (0::real) < x --> (0::real) < x ^ Suc n" @@ -571,9 +573,7 @@ lemma REAL_SUP_UBOUND_LE: "ALL P. Ex P & (EX z. ALL x. P x --> x <= z) --> (ALL y. P y --> y <= sup P)" by (import real REAL_SUP_UBOUND_LE) -lemma REAL_ARCH_LEAST: "ALL y. - 0 < y --> - (ALL x. 0 <= x --> (EX n. real n * y <= x & x < real (Suc n) * y))" +lemma REAL_ARCH_LEAST: "ALL y>0. ALL x>=0. EX n. real n * y <= x & x < real (Suc n) * y" by (import real REAL_ARCH_LEAST) consts @@ -587,7 +587,12 @@ sum :: "nat * nat => (nat => real) => real" defs - sum_def: "real.sum == split sumc" + sum_def: "(op ==::(nat * nat => (nat => real) => real) + => (nat * nat => (nat => real) => real) => prop) + (real.sum::nat * nat => (nat => real) => real) + ((split::(nat => nat => (nat => real) => real) + => nat * nat => (nat => real) => real) + (sumc::nat => nat => (nat => real) => real))" lemma SUM_DEF: "ALL m n f. real.sum (m, n) f = sumc m n f" by (import real SUM_DEF) @@ -913,25 +918,22 @@ mtop :: "'a metric => 'a topology" "mtop == %m. topology - (%S'. ALL x. - S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))" + (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))" lemma mtop: "ALL m. mtop m = topology - (%S'. ALL x. - S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))" + (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))" by (import topology mtop) lemma mtop_istopology: "ALL m. istopology - (%S'. ALL x. - S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))" + (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))" by (import topology mtop_istopology) lemma MTOP_OPEN: "ALL S' x. open (mtop x) S' = - (ALL xa. S' xa --> (EX e. 0 < e & (ALL y. dist x (xa, y) < e --> S' y)))" + (ALL xa. S' xa --> (EX e>0. ALL y. dist x (xa, y) < e --> S' y))" by (import topology MTOP_OPEN) constdefs @@ -948,8 +950,7 @@ by (import topology BALL_NEIGH) lemma MTOP_LIMPT: "ALL m x S'. - limpt (mtop m) x S' = - (ALL e. 0 < e --> (EX y. x ~= y & S' y & dist m (x, y) < e))" + limpt (mtop m) x S' = (ALL e>0. EX y. x ~= y & S' y & dist m (x, y) < e)" by (import topology MTOP_LIMPT) lemma ISMET_R1: "ismet (%(x, y). abs (y - x))" @@ -1054,8 +1055,7 @@ lemma MTOP_TENDS: "ALL d g x x0. tends x x0 (mtop d, g) = - (ALL e. - 0 < e --> (EX n. g n n & (ALL m. g m n --> dist d (x m, x0) < e)))" + (ALL e>0. EX n. g n n & (ALL m. g m n --> dist d (x m, x0) < e))" by (import nets MTOP_TENDS) lemma MTOP_TENDS_UNIQ: "ALL (g::'b => 'b => bool) d::'a metric. @@ -1067,29 +1067,27 @@ lemma SEQ_TENDS: "ALL d x x0. tends x x0 (mtop d, nat_ge) = - (ALL xa. 0 < xa --> (EX xb. ALL xc. xb <= xc --> dist d (x xc, x0) < xa))" + (ALL xa>0. EX xb. ALL xc. xb <= xc --> dist d (x xc, x0) < xa)" by (import nets SEQ_TENDS) lemma LIM_TENDS: "ALL m1 m2 f x0 y0. limpt (mtop m1) x0 re_universe --> tends f y0 (mtop m2, tendsto (m1, x0)) = - (ALL e. - 0 < e --> - (EX d. 0 < d & - (ALL x. - 0 < dist m1 (x, x0) & dist m1 (x, x0) <= d --> - dist m2 (f x, y0) < e)))" + (ALL e>0. + EX d>0. + ALL x. + 0 < dist m1 (x, x0) & dist m1 (x, x0) <= d --> + dist m2 (f x, y0) < e)" by (import nets LIM_TENDS) lemma LIM_TENDS2: "ALL m1 m2 f x0 y0. limpt (mtop m1) x0 re_universe --> tends f y0 (mtop m2, tendsto (m1, x0)) = - (ALL e. - 0 < e --> - (EX d. 0 < d & - (ALL x. - 0 < dist m1 (x, x0) & dist m1 (x, x0) < d --> - dist m2 (f x, y0) < e)))" + (ALL e>0. + EX d>0. + ALL x. + 0 < dist m1 (x, x0) & dist m1 (x, x0) < d --> + dist m2 (f x, y0) < e)" by (import nets LIM_TENDS2) lemma MR1_BOUNDED: "ALL g f. @@ -1915,16 +1913,16 @@ ((Pair::nat => nat => nat * nat) ((op *::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))) n) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) f) ((suminf::(nat => real) => real) f)))" by (import seq SER_PAIR) @@ -1956,19 +1954,19 @@ (f ((op +::nat => nat => nat) n ((op *::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) - (Numeral.Pls::bin) (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) + (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))) d))) (f ((op +::nat => nat => nat) n ((op +::nat => nat => nat) ((op *::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) - (Numeral.Pls::bin) (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) + (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))) d) (1::nat)))))))) ((op <::real => real => bool) @@ -2824,10 +2822,10 @@ ((uminus::real => real) ((op ^::real => nat => real) ((inverse::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x))" by (import lim DIFF_XM1) @@ -2848,10 +2846,10 @@ ((op /::real => real => real) l ((op ^::real => nat => real) (f x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) x))))" by (import lim DIFF_INV) @@ -2885,10 +2883,10 @@ ((op *::real => real => real) m (f x))) ((op ^::real => nat => real) (g x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) -(Numeral.Pls::bin) (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) +(Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))))) x))))))" by (import lim DIFF_DIV) @@ -3869,9 +3867,9 @@ ((op -::nat => nat => nat) ((op -::nat => nat => nat) n ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit)))) p) q)))))))))))" by (import powser TERMDIFF_LEMMA2) @@ -3916,10 +3914,10 @@ ((op ^::real => nat => real) k' ((op -::nat => nat => nat) n ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) - (Numeral.Pls::bin) (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) + (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))))) ((abs::real => real) h)))))))))" by (import powser TERMDIFF_LEMMA3) @@ -4112,10 +4110,10 @@ ((op /::real => real => real) l ((op ^::real => nat => real) (f x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) x)) ((op &::bool => bool => bool) ((op -->::bool => bool => bool) @@ -4134,10 +4132,10 @@ ((op *::real => real => real) m (f x))) ((op ^::real => nat => real) (g x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x)) ((op &::bool => bool => bool) ((op -->::bool => bool => bool) @@ -4212,19 +4210,10 @@ lemma EXP_0: "exp 0 = 1" by (import transc EXP_0) -lemma EXP_LE_X: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op <=::real => real => bool) - ((op +::real => real => real) (1::real) x) ((exp::real => real) x)))" +lemma EXP_LE_X: "ALL x>=0. 1 + x <= exp x" by (import transc EXP_LE_X) -lemma EXP_LT_1: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <::real => real => bool) (0::real) x) - ((op <::real => real => bool) (1::real) ((exp::real => real) x)))" +lemma EXP_LT_1: "ALL x>0. 1 < exp x" by (import transc EXP_LT_1) lemma EXP_ADD_MUL: "ALL x y. exp (x + y) * exp (- x) = exp y" @@ -4275,26 +4264,10 @@ lemma EXP_INJ: "ALL x y. (exp x = exp y) = (x = y)" by (import transc EXP_INJ) -lemma EXP_TOTAL_LEMMA: "(All::(real => bool) => bool) - (%y::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (1::real) y) - ((Ex::(real => bool) => bool) - (%x::real. - (op &::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op &::bool => bool => bool) - ((op <=::real => real => bool) x - ((op -::real => real => real) y (1::real))) - ((op =::real => real => bool) ((exp::real => real) x) y)))))" +lemma EXP_TOTAL_LEMMA: "ALL y>=1. EX x>=0. x <= y - 1 & exp x = y" by (import transc EXP_TOTAL_LEMMA) -lemma EXP_TOTAL: "(All::(real => bool) => bool) - (%y::real. - (op -->::bool => bool => bool) - ((op <::real => real => bool) (0::real) y) - ((Ex::(real => bool) => bool) - (%x::real. (op =::real => real => bool) ((exp::real => real) x) y)))" +lemma EXP_TOTAL: "ALL y>0. EX x. exp x = y" by (import transc EXP_TOTAL) constdefs @@ -4341,13 +4314,7 @@ lemma LN_1: "ln 1 = 0" by (import transc LN_1) -lemma LN_INV: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <::real => real => bool) (0::real) x) - ((op =::real => real => bool) - ((ln::real => real) ((inverse::real => real) x)) - ((uminus::real => real) ((ln::real => real) x))))" +lemma LN_INV: "ALL x>0. ln (inverse x) = - ln x" by (import transc LN_INV) lemma LN_DIV: "(All::(real => bool) => bool) @@ -4404,26 +4371,13 @@ ((ln::real => real) x)))))" by (import transc LN_POW) -lemma LN_LE: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op <=::real => real => bool) - ((ln::real => real) ((op +::real => real => real) (1::real) x)) x))" +lemma LN_LE: "ALL x>=0. ln (1 + x) <= x" by (import transc LN_LE) -lemma LN_LT_X: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <::real => real => bool) (0::real) x) - ((op <::real => real => bool) ((ln::real => real) x) x))" +lemma LN_LT_X: "ALL x>0. ln x < x" by (import transc LN_LT_X) -lemma LN_POS: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (1::real) x) - ((op <=::real => real => bool) (0::real) ((ln::real => real) x)))" +lemma LN_POS: "ALL x>=1. 0 <= ln x" by (import transc LN_POS) constdefs @@ -4630,34 +4584,16 @@ lemma SQRT_1: "sqrt 1 = 1" by (import transc SQRT_1) -lemma SQRT_POS_LT: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <::real => real => bool) (0::real) x) - ((op <::real => real => bool) (0::real) ((sqrt::real => real) x)))" +lemma SQRT_POS_LT: "ALL x>0. 0 < sqrt x" by (import transc SQRT_POS_LT) -lemma SQRT_POS_LE: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op <=::real => real => bool) (0::real) ((sqrt::real => real) x)))" +lemma SQRT_POS_LE: "ALL x>=0. 0 <= sqrt x" by (import transc SQRT_POS_LE) lemma SQRT_POW2: "ALL x. (sqrt x ^ 2 = x) = (0 <= x)" by (import transc SQRT_POW2) -lemma SQRT_POW_2: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op =::real => real => bool) - ((op ^::real => nat => real) ((sqrt::real => real) x) - ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool)))) - x))" +lemma SQRT_POW_2: "ALL x>=0. sqrt x ^ 2 = x" by (import transc SQRT_POW_2) lemma POW_2_SQRT: "(op -->::bool => bool => bool) @@ -4666,9 +4602,9 @@ ((sqrt::real => real) ((op ^::real => nat => real) x ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))))) x)" by (import transc POW_2_SQRT) @@ -4684,10 +4620,10 @@ ((op =::real => real => bool) ((op ^::real => nat => real) xa ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) x))) ((op =::real => real => bool) ((sqrt::real => real) x) xa)))" by (import transc SQRT_POS_UNIQ) @@ -4706,13 +4642,7 @@ ((sqrt::real => real) xa)))))" by (import transc SQRT_MUL) -lemma SQRT_INV: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op =::real => real => bool) - ((sqrt::real => real) ((inverse::real => real) x)) - ((inverse::real => real) ((sqrt::real => real) x))))" +lemma SQRT_INV: "ALL x>=0. sqrt (inverse x) = inverse (sqrt x)" by (import transc SQRT_INV) lemma SQRT_DIV: "(All::(real => bool) => bool) @@ -4748,31 +4678,25 @@ ((sqrt::real => real) ((op ^::real => nat => real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))) n)) ((op ^::real => nat => real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))) ((op div::nat => nat => nat) n ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))))" by (import transc SQRT_EVEN_POW2) -lemma REAL_DIV_SQRT: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op =::real => real => bool) - ((op /::real => real => real) x ((sqrt::real => real) x)) - ((sqrt::real => real) x)))" +lemma REAL_DIV_SQRT: "ALL x>=0. x / sqrt x = sqrt x" by (import transc REAL_DIV_SQRT) lemma SQRT_EQ: "(All::(real => bool) => bool) @@ -4784,10 +4708,10 @@ ((op =::real => real => bool) ((op ^::real => nat => real) x ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))) y) ((op <=::real => real => bool) (0::real) x)) ((op =::real => real => bool) x ((sqrt::real => real) y))))" @@ -4852,9 +4776,9 @@ ((op <::real => real => bool) (0::real) x) ((op <::real => real => bool) x ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))))) ((op <::real => real => bool) (0::real) ((sin::real => real) x)))" by (import transc SIN_POS) @@ -4927,10 +4851,10 @@ ((op <::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op <::real => real => bool) (0::real) ((sin::real => real) x)))" by (import transc SIN_POS_PI2) @@ -4942,10 +4866,10 @@ ((op <::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op <::real => real => bool) (0::real) ((cos::real => real) x)))" by (import transc COS_POS_PI2) @@ -4957,18 +4881,18 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x) ((op <::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op <::real => real => bool) (0::real) ((cos::real => real) x)))" by (import transc COS_POS_PI) @@ -4989,10 +4913,10 @@ ((op <=::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))" by (import transc COS_POS_PI2_LE) @@ -5004,18 +4928,18 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x) ((op <=::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))" by (import transc COS_POS_PI_LE) @@ -5027,10 +4951,10 @@ ((op <=::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op <=::real => real => bool) (0::real) ((sin::real => real) x)))" by (import transc SIN_POS_PI2_LE) @@ -5071,19 +4995,19 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x) ((op &::bool => bool => bool) ((op <=::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((op =::real => real => bool) ((sin::real => real) x) y)))))" by (import transc SIN_TOTAL) @@ -5101,10 +5025,10 @@ ((op *::real => real => real) ((real::nat => real) n) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))))))" by (import transc COS_ZERO_LEMMA) lemma SIN_ZERO_LEMMA: "(All::(real => bool) => bool) @@ -5120,10 +5044,10 @@ ((op *::real => real => real) ((real::nat => real) n) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))))))" by (import transc SIN_ZERO_LEMMA) lemma COS_ZERO: "ALL x. @@ -5198,36 +5122,36 @@ ((cos::real => real) ((op *::real => real => real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))) x)) (0::real)))) ((op =::real => real => bool) ((tan::real => real) ((op *::real => real => real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))) x)) ((op /::real => real => real) ((op *::real => real => real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))) ((tan::real => real) x)) ((op -::real => real => real) (1::real) ((op ^::real => nat => real) ((tan::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))))))" by (import transc TAN_DOUBLE) lemma TAN_POS_PI2: "(All::(real => bool) => bool) @@ -5238,10 +5162,10 @@ ((op <::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op <::real => real => bool) (0::real) ((tan::real => real) x)))" by (import transc TAN_POS_PI2) @@ -5254,49 +5178,17 @@ ((inverse::real => real) ((op ^::real => nat => real) ((cos::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x))" by (import transc DIFF_TAN) -lemma TAN_TOTAL_LEMMA: "(All::(real => bool) => bool) - (%y::real. - (op -->::bool => bool => bool) - ((op <::real => real => bool) (0::real) y) - ((Ex::(real => bool) => bool) - (%x::real. - (op &::bool => bool => bool) - ((op <::real => real => bool) (0::real) x) - ((op &::bool => bool => bool) - ((op <::real => real => bool) x - ((op /::real => real => real) (pi::real) - ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) - ((op <::real => real => bool) y ((tan::real => real) x))))))" +lemma TAN_TOTAL_LEMMA: "ALL y>0. EX x>0. x < pi / 2 & y < tan x" by (import transc TAN_TOTAL_LEMMA) -lemma TAN_TOTAL_POS: "(All::(real => bool) => bool) - (%y::real. - (op -->::bool => bool => bool) - ((op <=::real => real => bool) (0::real) y) - ((Ex::(real => bool) => bool) - (%x::real. - (op &::bool => bool => bool) - ((op <=::real => real => bool) (0::real) x) - ((op &::bool => bool => bool) - ((op <::real => real => bool) x - ((op /::real => real => real) (pi::real) - ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) - ((op =::real => real => bool) ((tan::real => real) x) y)))))" +lemma TAN_TOTAL_POS: "ALL y>=0. EX x>=0. x < pi / 2 & tan x = y" by (import transc TAN_TOTAL_POS) lemma TAN_TOTAL: "ALL y. EX! x. - (pi / 2) < x & x < pi / 2 & tan x = y" @@ -5334,19 +5226,19 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((asn::real => real) y)) ((op &::bool => bool => bool) ((op <=::real => real => bool) ((asn::real => real) y) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((op =::real => real => bool) ((sin::real => real) ((asn::real => real) y)) y))))" by (import transc ASN) @@ -5372,18 +5264,18 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((asn::real => real) y)) ((op <=::real => real => bool) ((asn::real => real) y) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))))" by (import transc ASN_BOUNDS) lemma ASN_BOUNDS_LT: "(All::(real => bool) => bool) @@ -5397,18 +5289,18 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((asn::real => real) y)) ((op <::real => real => bool) ((asn::real => real) y) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))))" by (import transc ASN_BOUNDS_LT) lemma SIN_ASN: "(All::(real => bool) => bool) @@ -5419,18 +5311,18 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x) ((op <=::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op =::real => real => bool) ((asn::real => real) ((sin::real => real) x)) x))" by (import transc SIN_ASN) @@ -5508,18 +5400,18 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x) ((op <::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op =::real => real => bool) ((atn::real => real) ((tan::real => real) x)) x))" by (import transc TAN_ATN) @@ -5533,16 +5425,16 @@ ((op +::real => real => real) (1::real) ((op ^::real => nat => real) ((tan::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) ((op ^::real => nat => real) ((inverse::real => real) ((cos::real => real) x)) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))))))" by (import transc TAN_SEC) lemma SIN_COS_SQ: "(All::(real => bool) => bool) @@ -5556,10 +5448,10 @@ ((op -::real => real => real) (1::real) ((op ^::real => nat => real) ((cos::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))))))" by (import transc SIN_COS_SQ) lemma COS_SIN_SQ: "(All::(real => bool) => bool) @@ -5570,27 +5462,27 @@ ((uminus::real => real) ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))) x) ((op <=::real => real => bool) x ((op /::real => real => real) (pi::real) ((number_of::bin => real) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))) ((op =::real => real => bool) ((cos::real => real) x) ((sqrt::real => real) ((op -::real => real => real) (1::real) ((op ^::real => nat => real) ((sin::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))))))" by (import transc COS_SIN_SQ) lemma COS_ATN_NZ: "ALL x. cos (atn x) ~= 0" @@ -5627,10 +5519,10 @@ ((op -::real => real => real) (1::real) ((op ^::real => nat => real) ((sin::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))))))" by (import transc COS_SIN_SQRT) lemma SIN_COS_SQRT: "(All::(real => bool) => bool) @@ -5642,18 +5534,13 @@ ((op -::real => real => real) (1::real) ((op ^::real => nat => real) ((cos::real => real) x) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))))))" + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))))))" by (import transc SIN_COS_SQRT) -lemma DIFF_LN: "(All::(real => bool) => bool) - (%x::real. - (op -->::bool => bool => bool) - ((op <::real => real => bool) (0::real) x) - ((diffl::(real => real) => real => real => bool) (ln::real => real) - ((inverse::real => real) x) x))" +lemma DIFF_LN: "ALL x>0. diffl ln (inverse x) x" by (import transc DIFF_LN) lemma DIFF_ASN_LEMMA: "(All::(real => bool) => bool) @@ -5680,10 +5567,10 @@ ((op -::real => real => real) (1::real) ((op ^::real => nat => real) x ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool))))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit))))))) x))" by (import transc DIFF_ASN) @@ -5713,10 +5600,10 @@ ((op -::real => real => real) (1::real) ((op ^::real => nat => real) x ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) - (True::bool)) - (False::bool)))))))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) + (bit.B1::bit)) + (bit.B0::bit)))))))) x))" by (import transc DIFF_ACS) diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/HOL4Vec.thy --- a/src/HOL/Import/HOL/HOL4Vec.thy Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/HOL4Vec.thy Fri Apr 01 18:59:17 2005 +0200 @@ -1,3 +1,5 @@ +(* AUTOMATICALLY GENERATED, DO NOT EDIT! *) + theory HOL4Vec = HOL4Base: ;setup_theory res_quan @@ -1102,9 +1104,9 @@ (op -->::bool => bool => bool) ((op <::nat => nat => bool) x ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) - (False::bool)))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit)))) ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x)) x))" by (import bword_num BV_VB) @@ -1157,8 +1159,7 @@ lemma NBWORD_SUC_WSEG: "ALL n. RES_FORALL (PWORDLEN (Suc n)) (%w. NBWORD n (BNVAL w) = WSEG n 0 w)" by (import bword_num NBWORD_SUC_WSEG) -lemma DOUBL_EQ_SHL: "ALL x. - 0 < x --> +lemma DOUBL_EQ_SHL: "ALL x>0. RES_FORALL (PWORDLEN x) (%xa. ALL xb. NBWORD x (BNVAL xa + BNVAL xa + BV xb) = snd (SHL False xa xb))" @@ -1297,10 +1298,10 @@ ((BV::bool => nat) cin)) ((op ^::nat => nat => nat) ((number_of::bin => nat) - ((op BIT::bin => bool => bin) - ((op BIT::bin => bool => bin) - (Numeral.Pls::bin) (True::bool)) - (False::bool))) + ((op BIT::bin => bit => bin) + ((op BIT::bin => bit => bin) + (Numeral.Pls::bin) (bit.B1::bit)) + (bit.B0::bit))) k)))))))" by (import bword_arith ACARRY_EQ_ADD_DIV) diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/HOL4Word32.thy --- a/src/HOL/Import/HOL/HOL4Word32.thy Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/HOL4Word32.thy Fri Apr 01 18:59:17 2005 +0200 @@ -1,3 +1,5 @@ +(* AUTOMATICALLY GENERATED, DO NOT EDIT! *) + theory HOL4Word32 = HOL4Base: ;setup_theory bits @@ -293,22 +295,17 @@ ~ oper (bit x a) (bit x b) --> BITWISE n oper a b div 2 ^ x mod 2 = 0" by (import bits BITWISE_NOT_COR) -lemma MOD_PLUS_RIGHT: "ALL n::nat. - (0::nat) < n --> - (ALL (j::nat) k::nat. (j + k mod n) mod n = (j + k) mod n)" +lemma MOD_PLUS_RIGHT: "ALL n>0::nat. ALL (j::nat) k::nat. (j + k mod n) mod n = (j + k) mod n" by (import bits MOD_PLUS_RIGHT) -lemma MOD_PLUS_1: "ALL n::nat. - (0::nat) < n --> - (ALL x::nat. - ((x + (1::nat)) mod n = (0::nat)) = (x mod n + (1::nat) = n))" +lemma MOD_PLUS_1: "ALL n>0::nat. + ALL x::nat. ((x + (1::nat)) mod n = (0::nat)) = (x mod n + (1::nat) = n)" by (import bits MOD_PLUS_1) -lemma MOD_ADD_1: "ALL n::nat. - (0::nat) < n --> - (ALL x::nat. - (x + (1::nat)) mod n ~= (0::nat) --> - (x + (1::nat)) mod n = x mod n + (1::nat))" +lemma MOD_ADD_1: "ALL n>0::nat. + ALL x::nat. + (x + (1::nat)) mod n ~= (0::nat) --> + (x + (1::nat)) mod n = x mod n + (1::nat)" by (import bits MOD_ADD_1) ;end_setup diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/ROOT.ML --- a/src/HOL/Import/HOL/ROOT.ML Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/ROOT.ML Fri Apr 01 18:59:17 2005 +0200 @@ -3,7 +3,5 @@ Author: Sebastian Skalberg (TU Muenchen) *) -with_path ".." use_thy "HOL4Compat"; -with_path ".." use_thy "HOL4Syntax"; setmp quick_and_dirty true use_thy "HOL4Prob"; setmp quick_and_dirty true use_thy "HOL4"; diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/arithmetic.imp --- a/src/HOL/Import/HOL/arithmetic.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/arithmetic.imp Fri Apr 01 18:59:17 2005 +0200 @@ -15,8 +15,8 @@ "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1" "NUMERAL" > "HOL4Compat.NUMERAL" "MOD" > "Divides.op mod" :: "nat => nat => nat" - "MIN" > "HOL.min" :: "nat => nat => nat" - "MAX" > "HOL.max" :: "nat => nat => nat" + "MIN" > "Orderings.min" :: "nat => nat => nat" + "MAX" > "Orderings.max" :: "nat => nat => nat" "FUNPOW" > "HOL4Compat.FUNPOW" "EXP" > "Nat.power" :: "nat => nat => nat" "DIV" > "Divides.op div" :: "nat => nat => nat" @@ -141,17 +141,17 @@ "MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ" "MIN_LT" > "HOL4Base.arithmetic.MIN_LT" "MIN_LE" > "HOL4Base.arithmetic.MIN_LE" - "MIN_IDEM" > "HOL.min_same" + "MIN_IDEM" > "Orderings.min_same" "MIN_DEF" > "HOL4Compat.MIN_DEF" - "MIN_COMM" > "HOL.min_ac_2" - "MIN_ASSOC" > "HOL.min_ac_1" + "MIN_COMM" > "Orderings.min_ac_2" + "MIN_ASSOC" > "Orderings.min_ac_1" "MIN_0" > "HOL4Base.arithmetic.MIN_0" "MAX_LT" > "HOL4Base.arithmetic.MAX_LT" "MAX_LE" > "HOL4Base.arithmetic.MAX_LE" - "MAX_IDEM" > "HOL.max_same" + "MAX_IDEM" > "Orderings.max_same" "MAX_DEF" > "HOL4Compat.MAX_DEF" - "MAX_COMM" > "HOL.max_ac_2" - "MAX_ASSOC" > "HOL.max_ac_1" + "MAX_COMM" > "Orderings.max_ac_2" + "MAX_ASSOC" > "Orderings.max_ac_1" "MAX_0" > "HOL4Base.arithmetic.MAX_0" "LESS_TRANS" > "Nat.less_trans" "LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT" @@ -235,7 +235,7 @@ "EVEN" > "HOL4Base.arithmetic.EVEN" "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj" "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel" - "EQ_LESS_EQ" > "HOL.order_eq_iff" + "EQ_LESS_EQ" > "Orderings.order_eq_iff" "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel" "EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel" "DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/bool.imp --- a/src/HOL/Import/HOL/bool.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/bool.imp Fri Apr 01 18:59:17 2005 +0200 @@ -37,7 +37,7 @@ "bool_case_thm" > "HOL4Base.bool.bool_case_thm" "bool_case_ID" > "HOL4Base.bool.bool_case_ID" "bool_case_DEF" > "HOL4Compat.bool_case_DEF" - "bool_INDUCT" > "Set.bool_induct" + "bool_INDUCT" > "Datatype.bool.induct" "boolAxiom" > "HOL4Base.bool.boolAxiom" "UNWIND_THM2" > "HOL.simp_thms_39" "UNWIND_THM1" > "HOL.simp_thms_40" @@ -78,7 +78,7 @@ "OR_INTRO_THM2" > "HOL.disjI2" "OR_INTRO_THM1" > "HOL.disjI1" "OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM" - "OR_ELIM_THM" > "Recdef.tfl_disjE" + "OR_ELIM_THM" > "HOL.disjE" "OR_DEF" > "HOL.or_def" "OR_CONG" > "HOL4Base.bool.OR_CONG" "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES" @@ -93,10 +93,10 @@ "NOT_DEF" > "HOL.simp_thms_19" "NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES" "NOT_AND" > "HOL4Base.bool.NOT_AND" - "MONO_OR" > "Inductive.basic_monos_3" + "MONO_OR" > "Sum_Type.basic_monos_3" "MONO_NOT" > "HOL.rev_contrapos" "MONO_IMP" > "Set.imp_mono" - "MONO_EXISTS" > "Inductive.basic_monos_5" + "MONO_EXISTS" > "Sum_Type.basic_monos_5" "MONO_COND" > "HOL4Base.bool.MONO_COND" "MONO_AND" > "Hilbert_Choice.conj_forward" "MONO_ALL" > "Inductive.basic_monos_6" @@ -139,12 +139,12 @@ "EXISTS_OR_THM" > "HOL.ex_disj_distrib" "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF" "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE" - "ETA_THM" > "Presburger.fm_modd_pinf" - "ETA_AX" > "Presburger.fm_modd_pinf" + "ETA_THM" > "HOL.eta_contract_eq" + "ETA_AX" > "HOL.eta_contract_eq" "EQ_TRANS" > "Set.basic_trans_rules_31" "EQ_SYM_EQ" > "HOL.eq_sym_conv" "EQ_SYM" > "HOL.meta_eq_to_obj_eq" - "EQ_REFL" > "Presburger.fm_modd_pinf" + "EQ_REFL" > "HOL.refl" "EQ_IMP_THM" > "HOL.iff_conv_conj_imp" "EQ_EXT" > "HOL.meta_eq_to_obj_eq" "EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND" @@ -152,7 +152,7 @@ "DISJ_SYM" > "HOL.disj_comms_1" "DISJ_IMP_THM" > "HOL.imp_disjL" "DISJ_COMM" > "HOL.disj_comms_1" - "DISJ_ASSOC" > "Recdef.tfl_disj_assoc" + "DISJ_ASSOC" > "HOL.disj_assoc" "DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM" "CONJ_SYM" > "HOL.conj_comms_1" "CONJ_COMM" > "HOL.conj_comms_1" @@ -172,8 +172,8 @@ "BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT" "BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM" "BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT" - "BOOL_CASES_AX" > "HOL.True_or_False" - "BETA_THM" > "Presburger.fm_modd_pinf" + "BOOL_CASES_AX" > "Datatype.bool.nchotomy" + "BETA_THM" > "HOL.eta_contract_eq" "ARB_def" > "HOL4Base.bool.ARB_def" "ARB_DEF" > "HOL4Base.bool.ARB_DEF" "AND_INTRO_THM" > "HOL.conjI" @@ -183,7 +183,7 @@ "AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES" "AND2_THM" > "HOL.conjunct2" "AND1_THM" > "HOL.conjunct1" - "ABS_SIMP" > "Presburger.fm_modd_pinf" + "ABS_SIMP" > "HOL.refl" "ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM" ignore_thms diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/num.imp --- a/src/HOL/Import/HOL/num.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/num.imp Fri Apr 01 18:59:17 2005 +0200 @@ -12,7 +12,7 @@ thm_maps "NOT_SUC" > "Nat.nat.simps_1" "INV_SUC" > "Nat.Suc_inject" - "INDUCTION" > "List.lexn.induct" + "INDUCTION" > "NatArith.of_nat.induct" ignore_thms "num_TY_DEF" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/pair.imp --- a/src/HOL/Import/HOL/pair.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/pair.imp Fri Apr 01 18:59:17 2005 +0200 @@ -21,7 +21,7 @@ "##" > "prod_fun" thm_maps - "pair_induction" > "Product_Type.prod_induct" + "pair_induction" > "Datatype.prod.induct" "pair_case_thm" > "Product_Type.split" "pair_case_def" > "HOL4Compat.pair_case_def" "pair_case_cong" > "HOL4Base.pair.pair_case_cong" @@ -41,7 +41,7 @@ "PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM" "PAIR_MAP_THM" > "Product_Type.prod_fun" "PAIR_MAP" > "HOL4Compat.PAIR_MAP" - "PAIR_EQ" > "Product_Type.Pair_eq" + "PAIR_EQ" > "Datatype.prod.simps_1" "PAIR" > "HOL4Compat.PAIR" "LEX_def" > "HOL4Base.pair.LEX_def" "LEX_DEF" > "HOL4Base.pair.LEX_DEF" @@ -57,8 +57,8 @@ "CURRY_UNCURRY_THM" > "Product_Type.curry_split" "CURRY_ONE_ONE_THM" > "HOL4Base.pair.CURRY_ONE_ONE_THM" "CURRY_DEF" > "Product_Type.curry_conv" - "CLOSED_PAIR_EQ" > "Product_Type.Pair_eq" - "ABS_PAIR_THM" > "Product_Type.surj_pair" + "CLOSED_PAIR_EQ" > "Datatype.prod.simps_1" + "ABS_PAIR_THM" > "Datatype.prod.nchotomy" ignore_thms "prod_TY_DEF" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/prob_extra.imp --- a/src/HOL/Import/HOL/prob_extra.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/prob_extra.imp Fri Apr 01 18:59:17 2005 +0200 @@ -39,7 +39,7 @@ "MEM_FILTER" > "HOL4Prob.prob_extra.MEM_FILTER" "MAP_MEM" > "HOL4Prob.prob_extra.MAP_MEM" "MAP_ID" > "List.map_ident" - "LENGTH_FILTER" > "List.length_filter" + "LENGTH_FILTER" > "List.length_filter_le" "LAST_MEM" > "HOL4Prob.prob_extra.LAST_MEM" "LAST_MAP_CONS" > "HOL4Prob.prob_extra.LAST_MAP_CONS" "IS_PREFIX_TRANS" > "HOL4Prob.prob_extra.IS_PREFIX_TRANS" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/real.imp Fri Apr 01 18:59:17 2005 +0200 @@ -28,7 +28,7 @@ "real_sub" > "OrderedGroup.diff_def" "real_of_num" > "HOL4Compat.real_of_num" "real_lte" > "HOL4Compat.real_lte" - "real_lt" > "HOL.linorder_not_le" + "real_lt" > "Orderings.linorder_not_le" "real_gt" > "HOL4Compat.real_gt" "real_ge" > "HOL4Compat.real_ge" "real_div" > "Ring_and_Field.field.divide_inverse" @@ -77,21 +77,21 @@ "REAL_SUB_RZERO" > "OrderedGroup.diff_0_right" "REAL_SUB_RNEG" > "OrderedGroup.diff_minus_eq_add" "REAL_SUB_REFL" > "OrderedGroup.diff_self" - "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_6" + "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_3" "REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2" "REAL_SUB_LZERO" > "OrderedGroup.diff_0" - "REAL_SUB_LT" > "RealDef.real_0_less_diff_iff" + "REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT" "REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG" - "REAL_SUB_LE" > "RealDef.real_0_le_diff_iff" - "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_7" + "REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE" + "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_4" "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2" "REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2" "REAL_SUB_ADD" > "OrderedGroup.diff_add_cancel" "REAL_SUB_ABS" > "HOL4Real.real.REAL_SUB_ABS" "REAL_SUB_0" > "OrderedGroup.eq_iff_diff_eq_0" "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff" - "REAL_RINV_UNIQ" > "RealDef.real_inverse_unique" - "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4" + "REAL_RINV_UNIQ" > "Ring_and_Field.inverse_unique" + "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1" "REAL_POW_POW" > "Power.power_mult" "REAL_POW_MONO_LT" > "Power.power_strict_increasing" "REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2" @@ -112,7 +112,7 @@ "REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add" "REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT" "REAL_NOT_LT" > "HOL4Compat.real_lte" - "REAL_NOT_LE" > "HOL.linorder_not_le" + "REAL_NOT_LE" > "Orderings.linorder_not_le" "REAL_NEG_SUB" > "OrderedGroup.minus_diff_eq" "REAL_NEG_RMUL" > "Ring_and_Field.minus_mult_right" "REAL_NEG_NEG" > "OrderedGroup.minus_minus" @@ -129,7 +129,7 @@ "REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib" "REAL_NEG_0" > "OrderedGroup.minus_zero" "REAL_NEGNEG" > "OrderedGroup.minus_minus" - "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2" + "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_6" "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right" "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right" "REAL_MUL_RINV" > "Ring_and_Field.right_inverse" @@ -150,7 +150,7 @@ "REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict.mult_strict_right_mono" "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" - "REAL_LT_REFL" > "HOL.order_less_irrefl" + "REAL_LT_REFL" > "Orderings.order_less_irrefl" "REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq" "REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0" "REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV" @@ -164,17 +164,17 @@ "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono" "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" - "REAL_LT_LE" > "HOL.order.order_less_le" + "REAL_LT_LE" > "Orderings.order.order_less_le" "REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq" "REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left" "REAL_LT_INV_EQ" > "Ring_and_Field.inverse_positive_iff_positive" "REAL_LT_INV" > "Ring_and_Field.less_imp_inverse_less" - "REAL_LT_IMP_NE" > "HOL.less_imp_neq" - "REAL_LT_IMP_LE" > "HOL.order_less_imp_le" + "REAL_LT_IMP_NE" > "Orderings.less_imp_neq" + "REAL_LT_IMP_LE" > "Orderings.order_less_imp_le" "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" "REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2" "REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff" - "REAL_LT_GT" > "HOL.order_less_not_sym" + "REAL_LT_GT" > "Orderings.order_less_not_sym" "REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0" "REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION" "REAL_LT_DIV" > "HOL4Real.real.REAL_LT_DIV" @@ -199,18 +199,18 @@ "REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ" "REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ" "REAL_LE_TRANS" > "Set.basic_trans_rules_25" - "REAL_LE_TOTAL" > "HOL.linorder.linorder_linear" + "REAL_LE_TOTAL" > "Orderings.linorder.linorder_linear" "REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8" "REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9" "REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square" "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg" "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring.mult_right_mono" "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" - "REAL_LE_REFL" > "HOL.order.order_refl" + "REAL_LE_REFL" > "Orderings.order.order_refl" "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq" "REAL_LE_RDIV" > "HOL4Real.real.REAL_LE_RDIV" "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right" - "REAL_LE_POW2" > "NatBin.zero_le_power2" + "REAL_LE_POW2" > "NatBin.zero_compare_simps_12" "REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL" "REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff" "REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff" @@ -218,7 +218,7 @@ "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le" "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2" "REAL_LE_MUL" > "Ring_and_Field.mult_pos_le" - "REAL_LE_LT" > "HOL.order_le_less" + "REAL_LE_LT" > "Orderings.order_le_less" "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono" "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" @@ -230,20 +230,20 @@ "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" "REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add" "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV" - "REAL_LE_ANTISYM" > "HOL.order_eq_iff" + "REAL_LE_ANTISYM" > "Orderings.order_eq_iff" "REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR" "REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL" "REAL_LE_ADD2" > "OrderedGroup.add_mono" "REAL_LE_ADD" > "RealDef.real_le_add_order" "REAL_LE_01" > "Ring_and_Field.zero_le_one" "REAL_LET_TRANS" > "Set.basic_trans_rules_23" - "REAL_LET_TOTAL" > "HOL4Real.real.REAL_LET_TOTAL" + "REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear" "REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM" "REAL_LET_ADD2" > "OrderedGroup.add_le_less_mono" "REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD" "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2" "REAL_LE" > "RealDef.real_of_nat_le_iff" - "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" + "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" "REAL_INV_POS" > "Ring_and_Field.positive_imp_inverse_positive" "REAL_INV_NZ" > "Ring_and_Field.nonzero_imp_inverse_nonzero" "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL" @@ -270,7 +270,7 @@ "REAL_EQ_LMUL" > "Ring_and_Field.field_mult_cancel_left" "REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ" "REAL_EQ_LADD" > "OrderedGroup.add_left_cancel" - "REAL_EQ_IMP_LE" > "HOL.order_eq_refl" + "REAL_EQ_IMP_LE" > "Orderings.order_eq_refl" "REAL_ENTIRE" > "Ring_and_Field.field_mult_eq_0_iff" "REAL_DOWN2" > "RealDef.real_lbound_gt_zero" "REAL_DOWN" > "HOL4Real.real.REAL_DOWN" @@ -289,11 +289,11 @@ "REAL_ADD_RINV" > "OrderedGroup.right_minus" "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ" "REAL_ADD_RID" > "OrderedGroup.add_0_right" - "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4" + "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1" "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ" "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0" - "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" + "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2" "REAL_ADD" > "RealDef.real_of_nat_add" @@ -330,7 +330,7 @@ "ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq" "ABS_SUM" > "HOL4Real.real.ABS_SUM" "ABS_SUB_ABS" > "HOL4Real.real.ABS_SUB_ABS" - "ABS_SUB" > "HOL4Real.real.ABS_SUB" + "ABS_SUB" > "OrderedGroup.abs_minus_commute" "ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ" "ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2" "ABS_SIGN" > "HOL4Real.real.ABS_SIGN" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/realax.imp Fri Apr 01 18:59:17 2005 +0200 @@ -91,16 +91,16 @@ "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" "TREAL_10" > "HOL4Real.realax.TREAL_10" "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" - "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2" + "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_6" "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1" "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" "REAL_LT_TRANS" > "Set.basic_trans_rules_21" "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" - "REAL_LT_REFL" > "HOL.order_less_irrefl" + "REAL_LT_REFL" > "Orderings.order_less_irrefl" "REAL_LT_MUL" > "Ring_and_Field.mult_pos" "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" - "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" + "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/rich_list.imp --- a/src/HOL/Import/HOL/rich_list.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/rich_list.imp Fri Apr 01 18:59:17 2005 +0200 @@ -253,7 +253,7 @@ "FIRSTN_APPEND1" > "HOL4Base.rich_list.FIRSTN_APPEND1" "FIRSTN" > "HOL4Base.rich_list.FIRSTN" "FILTER_SNOC" > "HOL4Base.rich_list.FILTER_SNOC" - "FILTER_REVERSE" > "HOL4Base.rich_list.FILTER_REVERSE" + "FILTER_REVERSE" > "List.rev_filter" "FILTER_MAP" > "HOL4Base.rich_list.FILTER_MAP" "FILTER_IDEM" > "HOL4Base.rich_list.FILTER_IDEM" "FILTER_FOLDR" > "HOL4Base.rich_list.FILTER_FOLDR" @@ -357,7 +357,7 @@ "AND_EL_DEF" > "HOL4Base.rich_list.AND_EL_DEF" "ALL_EL_SNOC" > "HOL4Base.rich_list.ALL_EL_SNOC" "ALL_EL_SEG" > "HOL4Base.rich_list.ALL_EL_SEG" - "ALL_EL_REVERSE" > "HOL4Base.rich_list.ALL_EL_REVERSE" + "ALL_EL_REVERSE" > "List.list_all_rev" "ALL_EL_REPLICATE" > "HOL4Base.rich_list.ALL_EL_REPLICATE" "ALL_EL_MAP" > "HOL4Base.rich_list.ALL_EL_MAP" "ALL_EL_LASTN" > "HOL4Base.rich_list.ALL_EL_LASTN" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/HOL/sum.imp --- a/src/HOL/Import/HOL/sum.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/sum.imp Fri Apr 01 18:59:17 2005 +0200 @@ -11,12 +11,12 @@ "OUTL" > "HOL4Compat.OUTL" "ISR" > "HOL4Compat.ISR" "ISL" > "HOL4Compat.ISL" - "INR" > "Inr" - "INL" > "Inl" + "INR" > "Sum_Type.Inr" + "INL" > "Sum_Type.Inl" thm_maps - "sum_distinct1" > "Sum_Type.Inr_not_Inl" - "sum_distinct" > "Sum_Type.Inl_not_Inr" + "sum_distinct1" > "Datatype.sum.simps_2" + "sum_distinct" > "Datatype.sum.simps_1" "sum_case_def" > "HOL4Compat.sum_case_def" "sum_case_cong" > "HOL4Base.sum.sum_case_cong" "sum_INDUCT" > "HOL4Compat.OUTR.induct" @@ -26,7 +26,7 @@ "ISR" > "HOL4Compat.ISR" "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR" "ISL" > "HOL4Compat.ISL" - "INR_neq_INL" > "Sum_Type.Inr_not_Inl" + "INR_neq_INL" > "Datatype.sum.simps_2" "INR_INL_11" > "HOL4Compat.INR_INL_11" "INR" > "HOL4Base.sum.INR" "INL" > "HOL4Base.sum.INL" diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/hol4rews.ML Fri Apr 01 18:59:17 2005 +0200 @@ -496,7 +496,7 @@ end; fun setup_dump (dir,thyname) thy = - HOL4Dump.put (dir,thyname,[]) thy + HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy fun add_dump str thy = let diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/proof_kernel.ML Fri Apr 01 18:59:17 2005 +0200 @@ -203,7 +203,7 @@ then F true n else F false (n+1) in - transform_error (Library.setmp Syntax.ambiguity_is_error true (F false)) 0 + transform_error (Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true (F false))) 0 end handle ERROR_MESSAGE mesg => (writeln "Exception in smart_string_of_cterm!"; @@ -1217,6 +1217,7 @@ fun get_isabelle_thm thyname thmname hol4conc thy = let + val _ = message "get_isabelle_thm called..." val sg = sign_of thy val (info,hol4conc') = disamb_term hol4conc @@ -1257,7 +1258,7 @@ if_debug prin isaconc) val cs = non_trivial_term_consts isaconc val _ = (message "Looking for consts:"; - message (String.concat cs)) + message (commas cs)) val pot_thms = Shuffler.find_potential thy isaconc val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems") in @@ -1273,16 +1274,16 @@ | NONE => (thy,NONE) end end - handle _ => (thy,NONE) + handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE)) fun get_thm thyname thmname thy = case get_hol4_thm thyname thmname thy of SOME hth => (thy,SOME hth) | NONE => ((case fst (import_proof thyname thmname thy) of SOME f => get_isabelle_thm thyname thmname (f thy) thy - | NONE => (thy,NONE)) - handle e as IO.Io _ => (thy,NONE) - | e as PK _ => (thy,NONE)) + | NONE => (message "No conclusion"; (thy,NONE))) + handle e as IO.Io _ => (message "IO exception"; (thy,NONE)) + | e as PK _ => (message "PK exception"; (thy,NONE))) fun rename_const thyname thy name = case get_hol4_const_renaming thyname name thy of diff -r b45393fb38c0 -r b1f486a9c56b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/IsaMakefile Fri Apr 01 18:59:17 2005 +0200 @@ -6,7 +6,7 @@ default: HOL generate: HOL-Complex-Generate-HOL -images: HOL HOL-Algebra HOL-Complex TLA ####lcp temporary####HOL4 +images: HOL HOL-Algebra HOL-Complex TLA HOL4 #Note: keep targets sorted (except for HOL-Library) test: \