Updated import.
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Mon Aug 29 16:51:39 2005 +0200
@@ -22,7 +22,7 @@
"?" > Ex
"?!" > Ex1
"~" > Not
- COND > If
+ COND > HOL.If
bool_case > Datatype.bool.bool_case
ONE_ONE > HOL4Setup.ONE_ONE
ONTO > HOL4Setup.ONTO
--- a/src/HOL/Import/HOL/HOL4Base.thy Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy Mon Aug 29 16:51:39 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
+theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":
;setup_theory bool
@@ -2480,9 +2480,6 @@
lemma DIVIDES_ADD_2: "ALL (a::nat) (b::nat) c::nat. a dvd b & a dvd b + c --> a dvd c"
by (import divides DIVIDES_ADD_2)
-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 dvd FACT b"
by (import divides DIVIDES_FACT)
@@ -4072,10 +4069,6 @@
lemma FILTER_IDEM: "ALL f l. filter f (filter f l) = filter f l"
by (import rich_list FILTER_IDEM)
-lemma FILTER_MAP: "ALL (f1::'b => bool) (f2::'a => 'b) l::'a list.
- filter f1 (map f2 l) = map f2 (filter (f1 o f2) l)"
- by (import rich_list FILTER_MAP)
-
lemma LENGTH_SEG: "ALL n k l. n + k <= length l --> length (SEG n k l) = n"
by (import rich_list LENGTH_SEG)
--- a/src/HOL/Import/HOL/HOL4Prob.thy Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Mon Aug 29 16:51:39 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Prob imports HOL4Real begin
+theory HOL4Prob = HOL4Real:
;setup_theory prob_extra
--- a/src/HOL/Import/HOL/HOL4Real.thy Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy Mon Aug 29 16:51:39 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Real imports HOL4Base begin
+theory HOL4Real = HOL4Base:
;setup_theory realax
@@ -369,12 +369,6 @@
lemma REAL_ADD2_SUB2: "ALL (a::real) (b::real) (c::real) d::real. a + b - (c + d) = a - c + (b - d)"
by (import real REAL_ADD2_SUB2)
-lemma REAL_LET_ADD: "ALL (x::real) y::real. (0::real) <= x & (0::real) < y --> (0::real) < x + y"
- by (import real REAL_LET_ADD)
-
-lemma REAL_LTE_ADD: "ALL (x::real) y::real. (0::real) < x & (0::real) <= y --> (0::real) < x + y"
- by (import real REAL_LTE_ADD)
-
lemma REAL_SUB_LNEG: "ALL (x::real) y::real. - x - y = - (x + y)"
by (import real REAL_SUB_LNEG)
@@ -405,16 +399,6 @@
x1 * y1 <= x2 * y2"
by (import real REAL_LE_MUL2)
-lemma REAL_LE_LDIV: "ALL (x::real) (y::real) z::real. (0::real) < x & y <= z * x --> y / x <= z"
- by (import real REAL_LE_LDIV)
-
-lemma REAL_LE_RDIV: "ALL (x::real) (y::real) z::real. (0::real) < x & y * x <= z --> y <= z / x"
- by (import real REAL_LE_RDIV)
-
-lemma REAL_LT_DIV: "ALL (x::real) xa::real.
- (0::real) < x & (0::real) < xa --> (0::real) < x / xa"
- by (import real REAL_LT_DIV)
-
lemma REAL_LE_DIV: "ALL (x::real) xa::real.
(0::real) <= x & (0::real) <= xa --> (0::real) <= x / xa"
by (import real REAL_LE_DIV)
@@ -442,6 +426,11 @@
(x * x + y * y = (0::real)) = (x = (0::real) & y = (0::real))"
by (import real REAL_SUMSQ)
+lemma REAL_DIV_MUL2: "ALL (x::real) z::real.
+ x ~= (0::real) & z ~= (0::real) -->
+ (ALL y::real. y / z = x * y / (x * z))"
+ by (import real REAL_DIV_MUL2)
+
lemma REAL_MIDDLE1: "ALL (a::real) b::real. a <= b --> a <= (a + b) / (2::real)"
by (import real REAL_MIDDLE1)
@@ -481,12 +470,6 @@
abs h < abs y - abs x --> abs (x + h) < abs y"
by (import real ABS_CIRCLE)
-lemma REAL_SUB_ABS: "ALL (x::real) y::real. abs x - abs y <= abs (x - y)"
- by (import real REAL_SUB_ABS)
-
-lemma ABS_SUB_ABS: "ALL (x::real) y::real. abs (abs x - abs y) <= abs (x - y)"
- by (import real ABS_SUB_ABS)
-
lemma ABS_BETWEEN2: "ALL (x0::real) (x::real) (y0::real) y::real.
x0 < y0 &
abs (x - x0) < (y0 - x0) / (2::real) &
@@ -520,6 +503,9 @@
n ~= (0::nat) & (0::real) <= x & x < y --> x ^ n < y ^ n"
by (import real REAL_POW_LT2)
+lemma REAL_POW_MONO_LT: "ALL (m::nat) (n::nat) x::real. (1::real) < x & m < n --> x ^ m < x ^ n"
+ by (import real REAL_POW_MONO_LT)
+
lemma REAL_SUP_SOMEPOS: "ALL P::real => bool.
(EX x::real. P x & (0::real) < x) &
(EX z::real. ALL x::real. P x --> x < z) -->
--- a/src/HOL/Import/HOL/HOL4Vec.thy Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Mon Aug 29 16:51:39 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Vec imports HOL4Base begin
+theory HOL4Vec = HOL4Base:
;setup_theory res_quan
@@ -32,19 +32,7 @@
lemma RES_FORALL_NULL: "ALL p m. RES_FORALL p (%x. m) = (p = EMPTY | m)"
by (import res_quan RES_FORALL_NULL)
-lemma RES_EXISTS_DISJ_DIST: "(All::(('a => bool) => bool) => bool)
- (%P::'a => bool.
- (All::(('a => bool) => bool) => bool)
- (%Q::'a => bool.
- (All::(('a => bool) => bool) => bool)
- (%R::'a => bool.
- (op =::bool => bool => bool)
- ((RES_EXISTS::('a => bool) => ('a => bool) => bool) P
- (%i::'a. (op |::bool => bool => bool) (Q i) (R i)))
- ((op |::bool => bool => bool)
- ((RES_EXISTS::('a => bool) => ('a => bool) => bool) P Q)
- ((RES_EXISTS::('a => bool) => ('a => bool) => bool) P
- R)))))"
+lemma RES_EXISTS_DISJ_DIST: "ALL P Q R. RES_EXISTS P (%i. Q i | R i) = (RES_EXISTS P Q | RES_EXISTS P R)"
by (import res_quan RES_EXISTS_DISJ_DIST)
lemma RES_DISJ_EXISTS_DIST: "ALL P Q R. RES_EXISTS (%i. P i | Q i) R = (RES_EXISTS P R | RES_EXISTS Q R)"
--- a/src/HOL/Import/HOL/HOL4Word32.thy Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Mon Aug 29 16:51:39 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Word32 imports HOL4Base begin
+theory HOL4Word32 = HOL4Base:
;setup_theory bits
--- a/src/HOL/Import/HOL/arithmetic.imp Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Mon Aug 29 16:51:39 2005 +0200
@@ -102,27 +102,27 @@
"NOT_ODD_EQ_EVEN" > "HOL4Base.arithmetic.NOT_ODD_EQ_EVEN"
"NOT_NUM_EQ" > "HOL4Base.arithmetic.NOT_NUM_EQ"
"NOT_LESS_EQUAL" > "Orderings.linorder_not_le"
- "NOT_LESS" > "Orderings.linorder_not_less"
+ "NOT_LESS" > "Nat.le_def"
"NOT_LEQ" > "HOL4Base.arithmetic.NOT_LEQ"
"NOT_GREATER_EQ" > "HOL4Base.arithmetic.NOT_GREATER_EQ"
- "NOT_GREATER" > "Orderings.linorder_not_less"
+ "NOT_GREATER" > "Nat.le_def"
"NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
"NORM_0" > "HOL4Base.arithmetic.NORM_0"
- "MULT_SYM" > "Nat.nat_mult_commute"
+ "MULT_SYM" > "IntDef.zmult_ac_2"
"MULT_SUC_EQ" > "HOL4Base.arithmetic.MULT_SUC_EQ"
"MULT_SUC" > "Nat.mult_Suc_right"
- "MULT_RIGHT_1" > "Nat.nat_mult_1_right"
+ "MULT_RIGHT_1" > "Finite_Set.AC_mult.f_e.ident"
"MULT_MONO_EQ" > "Nat.Suc_mult_cancel1"
"MULT_LESS_EQ_SUC" > "Nat.Suc_mult_le_cancel1"
- "MULT_LEFT_1" > "Nat.nat_mult_1"
+ "MULT_LEFT_1" > "Finite_Set.AC_mult.f_e.left_ident"
"MULT_INCREASES" > "HOL4Base.arithmetic.MULT_INCREASES"
"MULT_EXP_MONO" > "HOL4Base.arithmetic.MULT_EXP_MONO"
"MULT_EQ_1" > "HOL4Base.arithmetic.MULT_EQ_1"
"MULT_EQ_0" > "Nat.mult_is_0"
"MULT_DIV" > "Divides.div_mult_self_is_m"
- "MULT_COMM" > "Nat.nat_mult_commute"
+ "MULT_COMM" > "IntDef.zmult_ac_2"
"MULT_CLAUSES" > "HOL4Base.arithmetic.MULT_CLAUSES"
- "MULT_ASSOC" > "Nat.nat_mult_assoc"
+ "MULT_ASSOC" > "IntDef.zmult_ac_1"
"MULT_0" > "Nat.mult_0_right"
"MULT" > "HOL4Compat.MULT"
"MOD_UNIQUE" > "HOL4Base.arithmetic.MOD_UNIQUE"
@@ -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" > "Orderings.min_same"
+ "MIN_IDEM" > "Finite_Set.min.f.ACI_4"
"MIN_DEF" > "HOL4Compat.MIN_DEF"
- "MIN_COMM" > "Orderings.min_ac_2"
- "MIN_ASSOC" > "Orderings.min_ac_1"
+ "MIN_COMM" > "Finite_Set.min.f.ACI_2"
+ "MIN_ASSOC" > "Finite_Set.min.f.ACI_1"
"MIN_0" > "HOL4Base.arithmetic.MIN_0"
"MAX_LT" > "HOL4Base.arithmetic.MAX_LT"
"MAX_LE" > "HOL4Base.arithmetic.MAX_LE"
- "MAX_IDEM" > "Orderings.max_same"
+ "MAX_IDEM" > "Finite_Set.max.f.ACI_4"
"MAX_DEF" > "HOL4Compat.MAX_DEF"
- "MAX_COMM" > "Orderings.max_ac_2"
- "MAX_ASSOC" > "Orderings.max_ac_1"
+ "MAX_COMM" > "Finite_Set.max.f.ACI_2"
+ "MAX_ASSOC" > "Finite_Set.max.f.ACI_1"
"MAX_0" > "HOL4Base.arithmetic.MAX_0"
"LESS_TRANS" > "Nat.less_trans"
"LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT"
@@ -179,7 +179,7 @@
"LESS_EQ_TRANS" > "Nat.le_trans"
"LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
"LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
- "LESS_EQ_REFL" > "Nat.le_refl"
+ "LESS_EQ_REFL" > "Finite_Set.max.f_below.below_refl"
"LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
"LESS_EQ_MONO" > "Nat.Suc_le_mono"
"LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
@@ -188,7 +188,7 @@
"LESS_EQ_EXISTS" > "HOL4Base.arithmetic.LESS_EQ_EXISTS"
"LESS_EQ_CASES" > "Nat.nat_le_linear"
"LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
- "LESS_EQ_ADD_SUB" > "Nat.diff_add_assoc"
+ "LESS_EQ_ADD_SUB" > "NatArith.add_diff_assoc"
"LESS_EQ_ADD" > "Nat.le_add1"
"LESS_EQ_0" > "Nat.le_0_eq"
"LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
@@ -251,7 +251,7 @@
"COMPLETE_INDUCTION" > "Nat.less_induct"
"CANCEL_SUB" > "NatArith.eq_diff_iff"
"ALT_ZERO" > "HOL4Compat.ALT_ZERO_def"
- "ADD_SYM" > "Nat.nat_add_commute"
+ "ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
"ADD_SUC" > "Nat.add_Suc_right"
"ADD_SUB" > "Nat.diff_add_inverse2"
"ADD_MONO_LESS_EQ" > "Nat.nat_add_left_cancel_le"
@@ -261,10 +261,10 @@
"ADD_EQ_1" > "HOL4Base.arithmetic.ADD_EQ_1"
"ADD_EQ_0" > "Nat.add_is_0"
"ADD_DIV_ADD_DIV" > "HOL4Base.arithmetic.ADD_DIV_ADD_DIV"
- "ADD_COMM" > "Nat.nat_add_commute"
+ "ADD_COMM" > "Finite_Set.AC_add.f.AC_2"
"ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES"
- "ADD_ASSOC" > "Nat.nat_add_assoc"
- "ADD_0" > "Nat.add_0_right"
+ "ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
+ "ADD_0" > "Finite_Set.AC_add.f_e.ident"
"ADD1" > "Presburger.Suc_plus1"
"ADD" > "HOL4Compat.ADD"
--- a/src/HOL/Import/HOL/bool.imp Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/bool.imp Mon Aug 29 16:51:39 2005 +0200
@@ -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" > "HOL.disjE"
+ "OR_ELIM_THM" > "Recdef.tfl_disjE"
"OR_DEF" > "HOL.or_def"
"OR_CONG" > "HOL4Base.bool.OR_CONG"
"OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
@@ -93,12 +93,12 @@
"NOT_DEF" > "HOL.simp_thms_19"
"NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES"
"NOT_AND" > "HOL4Base.bool.NOT_AND"
- "MONO_OR" > "Sum_Type.basic_monos_3"
+ "MONO_OR" > "Inductive.basic_monos_3"
"MONO_NOT" > "HOL.rev_contrapos"
"MONO_IMP" > "Set.imp_mono"
- "MONO_EXISTS" > "Sum_Type.basic_monos_5"
+ "MONO_EXISTS" > "Inductive.basic_monos_5"
"MONO_COND" > "HOL4Base.bool.MONO_COND"
- "MONO_AND" > "Hilbert_Choice.conj_forward"
+ "MONO_AND" > "Inductive.basic_monos_4"
"MONO_ALL" > "Inductive.basic_monos_6"
"LET_THM" > "HOL.Let_def"
"LET_RATOR" > "HOL4Base.bool.LET_RATOR"
@@ -139,12 +139,12 @@
"EXISTS_OR_THM" > "HOL.ex_disj_distrib"
"EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
"EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
- "ETA_THM" > "HOL.eta_contract_eq"
- "ETA_AX" > "HOL.eta_contract_eq"
+ "ETA_THM" > "Presburger.fm_modd_pinf"
+ "ETA_AX" > "Presburger.fm_modd_pinf"
"EQ_TRANS" > "Set.basic_trans_rules_31"
"EQ_SYM_EQ" > "HOL.eq_sym_conv"
"EQ_SYM" > "HOL.meta_eq_to_obj_eq"
- "EQ_REFL" > "HOL.refl"
+ "EQ_REFL" > "Presburger.fm_modd_pinf"
"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" > "HOL.disj_assoc"
+ "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
"DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM"
"CONJ_SYM" > "HOL.conj_comms_1"
"CONJ_COMM" > "HOL.conj_comms_1"
@@ -173,7 +173,7 @@
"BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM"
"BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT"
"BOOL_CASES_AX" > "Datatype.bool.nchotomy"
- "BETA_THM" > "HOL.eta_contract_eq"
+ "BETA_THM" > "Presburger.fm_modd_pinf"
"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" > "HOL.refl"
+ "ABS_SIMP" > "Presburger.fm_modd_pinf"
"ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM"
ignore_thms
--- a/src/HOL/Import/HOL/divides.imp Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/divides.imp Mon Aug 29 16:51:39 2005 +0200
@@ -8,7 +8,7 @@
thm_maps
"divides_def" > "HOL4Compat.divides_def"
"ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
- "NOT_LT_DIV" > "HOL4Base.divides.NOT_LT_DIV"
+ "NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"
"DIVIDES_TRANS" > "Divides.dvd_trans"
"DIVIDES_SUB" > "Divides.dvd_diff"
"DIVIDES_REFL" > "Divides.dvd_refl"
--- a/src/HOL/Import/HOL/num.imp Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/num.imp Mon Aug 29 16:51:39 2005 +0200
@@ -12,7 +12,7 @@
thm_maps
"NOT_SUC" > "Nat.nat.simps_1"
"INV_SUC" > "Nat.Suc_inject"
- "INDUCTION" > "NatArith.of_nat.induct"
+ "INDUCTION" > "List.lexn.induct"
ignore_thms
"num_TY_DEF"
--- a/src/HOL/Import/HOL/real.imp Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/real.imp Mon Aug 29 16:51:39 2005 +0200
@@ -87,13 +87,13 @@
"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_SUB_ABS" > "OrderedGroup.abs_triangle_ineq2"
+ "REAL_SUB_0" > "OrderedGroup.diff_eq_0_iff_eq"
"REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
"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_MONO_LT" > "HOL4Real.real.REAL_POW_MONO_LT"
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
"REAL_POW_LT" > "Power.zero_less_power"
"REAL_POW_INV" > "Power.power_inverse"
@@ -114,12 +114,12 @@
"REAL_NOT_LT" > "HOL4Compat.real_lte"
"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_RMUL" > "Ring_and_Field.mult_minus_right"
"REAL_NEG_NEG" > "OrderedGroup.minus_minus"
"REAL_NEG_MUL2" > "Ring_and_Field.minus_mult_minus"
"REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1"
"REAL_NEG_LT0" > "OrderedGroup.neg_less_0_iff_less"
- "REAL_NEG_LMUL" > "Ring_and_Field.minus_mult_left"
+ "REAL_NEG_LMUL" > "Ring_and_Field.mult_minus_left"
"REAL_NEG_LE0" > "OrderedGroup.neg_le_0_iff_le"
"REAL_NEG_INV" > "Ring_and_Field.nonzero_inverse_minus_eq"
"REAL_NEG_GT0" > "OrderedGroup.neg_0_less_iff_less"
@@ -129,15 +129,15 @@
"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_6"
+ "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
"REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
- "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right"
+ "REAL_MUL_RNEG" > "Ring_and_Field.mult_minus_right"
"REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
- "REAL_MUL_RID" > "OrderedGroup.monoid_mult.mult_1_right"
+ "REAL_MUL_RID" > "Finite_Set.AC_mult.f_e.ident"
"REAL_MUL_LZERO" > "Ring_and_Field.mult_zero_left"
- "REAL_MUL_LNEG" > "Ring_and_Field.minus_mult_left"
+ "REAL_MUL_LNEG" > "Ring_and_Field.mult_minus_left"
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
- "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1"
+ "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
"REAL_MUL" > "RealDef.real_of_nat_mult"
"REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2"
@@ -177,7 +177,7 @@
"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"
+ "REAL_LT_DIV" > "Ring_and_Field.divide_pos_pos"
"REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM"
"REAL_LT_ADD_SUB" > "OrderedGroup.compare_rls_7"
"REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR"
@@ -186,14 +186,14 @@
"REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL"
"REAL_LT_ADD2" > "OrderedGroup.add_strict_mono"
"REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1"
- "REAL_LT_ADD" > "RealDef.real_add_order"
+ "REAL_LT_ADD" > "OrderedGroup.add_pos_pos"
"REAL_LT_1" > "HOL4Real.real.REAL_LT_1"
"REAL_LT_01" > "Ring_and_Field.ordered_semidom.zero_less_one"
"REAL_LTE_TRANS" > "Set.basic_trans_rules_24"
"REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL"
"REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM"
"REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono"
- "REAL_LTE_ADD" > "HOL4Real.real.REAL_LTE_ADD"
+ "REAL_LTE_ADD" > "OrderedGroup.add_pos_nonneg"
"REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2"
"REAL_LT" > "RealDef.real_of_nat_less_iff"
"REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ"
@@ -206,9 +206,9 @@
"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" > "Orderings.order.order_refl"
+ "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl"
"REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
- "REAL_LE_RDIV" > "HOL4Real.real.REAL_LE_RDIV"
+ "REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos"
"REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"
"REAL_LE_POW2" > "NatBin.zero_compare_simps_12"
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
@@ -223,7 +223,7 @@
"REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono"
"REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
"REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq"
- "REAL_LE_LDIV" > "HOL4Real.real.REAL_LE_LDIV"
+ "REAL_LE_LDIV" > "Ring_and_Field.mult_imp_div_pos_le"
"REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add.add_left_mono"
"REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left"
"REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative"
@@ -234,13 +234,13 @@
"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_ADD" > "OrderedGroup.add_nonneg_nonneg"
"REAL_LE_01" > "Ring_and_Field.zero_le_one"
"REAL_LET_TRANS" > "Set.basic_trans_rules_23"
"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_LET_ADD" > "OrderedGroup.add_nonneg_pos"
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
"REAL_LE" > "RealDef.real_of_nat_le_iff"
"REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
@@ -277,22 +277,22 @@
"REAL_DOUBLE" > "IntArith.mult_2"
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL"
"REAL_DIV_REFL" > "Ring_and_Field.divide_self"
- "REAL_DIV_MUL2" > "Ring_and_Field.nonzero_mult_divide_cancel_left"
+ "REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2"
"REAL_DIV_LZERO" > "Ring_and_Field.divide_zero_left"
"REAL_DIV_LMUL" > "HOL4Real.real.REAL_DIV_LMUL"
"REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ"
"REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST"
"REAL_ARCH" > "RComplete.reals_Archimedean3"
- "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
+ "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
"REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
"REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB"
"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_RID" > "Finite_Set.AC_add.f_e.ident"
"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_LID" > "Finite_Set.AC_add.f_e.left_ident"
"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"
@@ -300,7 +300,7 @@
"REAL_ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
"REAL_ABS_POS" > "OrderedGroup.abs_ge_zero"
"REAL_ABS_MUL" > "Ring_and_Field.abs_mult"
- "REAL_ABS_0" > "OrderedGroup.abs_zero"
+ "REAL_ABS_0" > "Numeral.bin_arith_simps_28"
"REAL_10" > "HOL4Compat.REAL_10"
"REAL_1" > "HOL4Real.real.REAL_1"
"REAL_0" > "HOL4Real.real.REAL_0"
@@ -329,7 +329,7 @@
"ABS_ZERO" > "OrderedGroup.abs_eq_0"
"ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
"ABS_SUM" > "HOL4Real.real.ABS_SUM"
- "ABS_SUB_ABS" > "HOL4Real.real.ABS_SUB_ABS"
+ "ABS_SUB_ABS" > "OrderedGroup.abs_triangle_ineq3"
"ABS_SUB" > "OrderedGroup.abs_minus_commute"
"ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ"
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
@@ -353,7 +353,7 @@
"ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
"ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
"ABS_ABS" > "OrderedGroup.abs_idempotent"
- "ABS_1" > "Ring_and_Field.abs_one"
- "ABS_0" > "OrderedGroup.abs_zero"
+ "ABS_1" > "Numeral.bin_arith_simps_29"
+ "ABS_0" > "Numeral.bin_arith_simps_28"
end
--- a/src/HOL/Import/HOL/realax.imp Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/realax.imp Mon Aug 29 16:51:39 2005 +0200
@@ -91,9 +91,9 @@
"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_6"
+ "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
- "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1"
+ "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
"REAL_LT_TRANS" > "Set.basic_trans_rules_21"
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
@@ -102,9 +102,9 @@
"REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
"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_SYM" > "Finite_Set.AC_add.f.AC_2"
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
- "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0"
+ "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
"REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
"REAL_10" > "HOL4Compat.REAL_10"
"HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB"
--- a/src/HOL/Import/HOL/rich_list.imp Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/rich_list.imp Mon Aug 29 16:51:39 2005 +0200
@@ -254,7 +254,7 @@
"FIRSTN" > "HOL4Base.rich_list.FIRSTN"
"FILTER_SNOC" > "HOL4Base.rich_list.FILTER_SNOC"
"FILTER_REVERSE" > "List.rev_filter"
- "FILTER_MAP" > "HOL4Base.rich_list.FILTER_MAP"
+ "FILTER_MAP" > "List.filter_map"
"FILTER_IDEM" > "HOL4Base.rich_list.FILTER_IDEM"
"FILTER_FOLDR" > "HOL4Base.rich_list.FILTER_FOLDR"
"FILTER_FOLDL" > "HOL4Base.rich_list.FILTER_FOLDL"
--- a/src/HOL/Import/HOL4Compat.thy Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Mon Aug 29 16:51:39 2005 +0200
@@ -26,6 +26,9 @@
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*)
+
consts
ISL :: "'a + 'b => bool"
ISR :: "'a + 'b => bool"
--- a/src/HOL/Import/shuffler.ML Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/shuffler.ML Mon Aug 29 16:51:39 2005 +0200
@@ -350,6 +350,13 @@
fun beta_fun sg assume t =
SOME (beta_conversion true (cterm_of sg t))
+val meta_sym_rew = thm "refl"
+
+fun equals_fun sg assume t =
+ case t of
+ Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
+ | _ => NONE
+
fun eta_expand sg assumes origt =
let
val (typet,Tinst) = freeze_thaw_term origt
@@ -413,6 +420,7 @@
val Q = Var(("Q",0),xT-->yT)
val R = Var(("R",0),xT-->yT)
val S = Var(("S",0),xT)
+val S' = Var(("S'",0),xT)
in
fun beta_simproc sg = Simplifier.simproc_i
sg
@@ -420,6 +428,12 @@
[Abs("x",xT,Q) $ S]
beta_fun
+fun equals_simproc sg = Simplifier.simproc_i
+ sg
+ "Ordered rewriting of meta equalities"
+ [Const("op ==",xT) $ S $ S']
+ equals_fun
+
fun quant_simproc sg = Simplifier.simproc_i
sg
"Ordered rewriting of nested quantifiers"
@@ -584,7 +598,7 @@
val norm_th = varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
val triv_th = trivial rhs
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
- val mod_th = case Seq.pull (bicompose true (false,norm_th,0) 1 triv_th) of
+ val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
SOME(th,_) => SOME th
| NONE => NONE
in