# HG changeset patch # User obua # Date 1125327099 -7200 # Node ID a26a4fc323ed506fc413aa0974a9394da2fa1538 # Parent 45bee2f6e61f8be107fa82bf9595761521926afb Updated import. diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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 diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/HOL4Base.thy --- 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) diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/HOL4Prob.thy --- 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 diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/HOL4Real.thy --- 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) --> diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/HOL4Vec.thy --- 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)" diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/HOL4Word32.thy --- 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 diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/arithmetic.imp --- 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" diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/bool.imp --- 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 diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/divides.imp --- 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" diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/num.imp --- 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" diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/real.imp --- 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 diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/realax.imp --- 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" diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL/rich_list.imp --- 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" diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/HOL4Compat.thy --- 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" diff -r 45bee2f6e61f -r a26a4fc323ed src/HOL/Import/shuffler.ML --- 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