# HG changeset patch # User paulson # Date 1075282909 -3600 # Node ID 2763da611ad9e04819d3d7b1686b456fd60971bf # Parent 0b1447d371616d200fb8f46b9917cd13b68b321d converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic. diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Wed Jan 28 01:19:34 2004 +0100 +++ b/src/HOL/Integ/int_arith1.ML Wed Jan 28 10:41:49 2004 +0100 @@ -516,7 +516,7 @@ val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ [int_numeral_0_eq_0, int_numeral_1_eq_1, - zminus_0, zadd_0, zadd_0_right, zdiff_def, + zminus_0, zdiff_def, zadd_zminus_inverse, zadd_zminus_inverse2, zmult_0, zmult_0_right, zmult_1, zmult_1_right, @@ -528,21 +528,11 @@ Int_Numeral_Simprocs.cancel_numerals @ Bin_Simprocs.eval_numerals; -val add_mono_thms_int = - map (fn s => prove_goal (the_context ()) s - (fn prems => [cut_facts_tac prems 1, - asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) - ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", - "(i = j) & (k <= l) ==> i + k <= j + (l::int)", - "(i <= j) & (k = l) ==> i + k <= j + (l::int)", - "(i = j) & (k = l) ==> i + k = j + (l::int)" - ]; - in val int_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => - {add_mono_thms = add_mono_thms @ add_mono_thms_int, + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms, lessD = lessD @ [zless_imp_add1_zle], diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jan 28 01:19:34 2004 +0100 +++ b/src/HOL/IsaMakefile Wed Jan 28 10:41:49 2004 +0100 @@ -138,8 +138,7 @@ $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML\ Library/Zorn.thy\ - Real/Complex_Numbers.thy \ - Real/Lubs.ML Real/Lubs.thy Real/rat_arith.ML Real/RatArith.thy\ + Real/Complex_Numbers.thy Real/Lubs.thy Real/rat_arith.ML Real/RatArith.thy\ Real/Rational.thy Real/PReal.thy Real/RComplete.thy \ Real/ROOT.ML Real/Real.thy \ Real/RealArith.thy Real/real_arith.ML Real/RealDef.thy \ diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/Real/Lubs.ML --- a/src/HOL/Real/Lubs.ML Wed Jan 28 01:19:34 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -(* Title : Lubs.ML - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Completeness of the reals. A few of the - definitions suggested by James Margetson -*) - -(*------------------------------------------------------------------------ - Rules for *<= and <=* - ------------------------------------------------------------------------*) -Goalw [setle_def] "ALL y: S. y <= x ==> S *<= x"; -by (assume_tac 1); -qed "setleI"; - -Goalw [setle_def] "[| S *<= x; y: S |] ==> y <= x"; -by (Fast_tac 1); -qed "setleD"; - -Goalw [setge_def] "ALL y: S. x<= y ==> x <=* S"; -by (assume_tac 1); -qed "setgeI"; - -Goalw [setge_def] "[| x <=* S; y: S |] ==> x <= y"; -by (Fast_tac 1); -qed "setgeD"; - -(*------------------------------------------------------------------------ - Rules about leastP, ub and lub - ------------------------------------------------------------------------*) -Goalw [leastP_def] "leastP P x ==> P x"; -by (Step_tac 1); -qed "leastPD1"; - -Goalw [leastP_def] "leastP P x ==> x <=* Collect P"; -by (Step_tac 1); -qed "leastPD2"; - -Goal "[| leastP P x; y: Collect P |] ==> x <= y"; -by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1); -qed "leastPD3"; - -Goalw [isLub_def,isUb_def,leastP_def] - "isLub R S x ==> S *<= x"; -by (Step_tac 1); -qed "isLubD1"; - -Goalw [isLub_def,isUb_def,leastP_def] - "isLub R S x ==> x: R"; -by (Step_tac 1); -qed "isLubD1a"; - -Goalw [isUb_def] "isLub R S x ==> isUb R S x"; -by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1); -qed "isLub_isUb"; - -Goal "[| isLub R S x; y : S |] ==> y <= x"; -by (blast_tac (claset() addSDs [isLubD1,setleD]) 1); -qed "isLubD2"; - -Goalw [isLub_def] "isLub R S x ==> leastP(isUb R S) x"; -by (assume_tac 1); -qed "isLubD3"; - -Goalw [isLub_def] "leastP(isUb R S) x ==> isLub R S x"; -by (assume_tac 1); -qed "isLubI1"; - -Goalw [isLub_def,leastP_def] - "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"; -by (Step_tac 1); -qed "isLubI2"; - -Goalw [isUb_def] "[| isUb R S x; y : S |] ==> y <= x"; -by (fast_tac (claset() addDs [setleD]) 1); -qed "isUbD"; - -Goalw [isUb_def] "isUb R S x ==> S *<= x"; -by (Step_tac 1); -qed "isUbD2"; - -Goalw [isUb_def] "isUb R S x ==> x: R"; -by (Step_tac 1); -qed "isUbD2a"; - -Goalw [isUb_def] "[| S *<= x; x: R |] ==> isUb R S x"; -by (Step_tac 1); -qed "isUbI"; - -Goalw [isLub_def] "[| isLub R S x; isUb R S y |] ==> x <= y"; -by (blast_tac (claset() addSIs [leastPD3]) 1); -qed "isLub_le_isUb"; - -Goalw [ubs_def,isLub_def] "isLub R S x ==> x <=* ubs R S"; -by (etac leastPD2 1); -qed "isLub_ubs"; - - - - diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/Real/Lubs.thy --- a/src/HOL/Real/Lubs.thy Wed Jan 28 01:19:34 2004 +0100 +++ b/src/HOL/Real/Lubs.thy Wed Jan 28 10:41:49 2004 +0100 @@ -2,38 +2,137 @@ ID : $Id$ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge - Description : Upper bounds, lubs definitions - suggested by James Margetson -*) +*) +header{*Definitions of Upper Bounds and Least Upper Bounds*} -Lubs = Main + +theory Lubs = Main: -consts - - "*<=" :: ['a set, 'a::ord] => bool (infixl 70) - "<=*" :: ['a::ord, 'a set] => bool (infixl 70) +text{*Thanks to suggestions by James Margetson*} constdefs - leastP :: ['a =>bool,'a::ord] => bool + + setle :: "['a set, 'a::ord] => bool" (infixl "*<=" 70) + "S *<= x == (ALL y: S. y <= x)" + + setge :: "['a::ord, 'a set] => bool" (infixl "<=*" 70) + "x <=* S == (ALL y: S. x <= y)" + + leastP :: "['a =>bool,'a::ord] => bool" "leastP P x == (P x & x <=* Collect P)" - isLub :: ['a set, 'a set, 'a::ord] => bool + isLub :: "['a set, 'a set, 'a::ord] => bool" "isLub R S x == leastP (isUb R S) x" - isUb :: ['a set, 'a set, 'a::ord] => bool + isUb :: "['a set, 'a set, 'a::ord] => bool" "isUb R S x == S *<= x & x: R" - ubs :: ['a set, 'a::ord set] => 'a set + ubs :: "['a set, 'a::ord set] => 'a set" "ubs R S == Collect (isUb R S)" -defs - setle_def - "S *<= x == (ALL y: S. y <= x)" + + +subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*} + +lemma setleI: "ALL y: S. y <= x ==> S *<= x" +by (simp add: setle_def) + +lemma setleD: "[| S *<= x; y: S |] ==> y <= x" +by (simp add: setle_def) + +lemma setgeI: "ALL y: S. x<= y ==> x <=* S" +by (simp add: setge_def) + +lemma setgeD: "[| x <=* S; y: S |] ==> x <= y" +by (simp add: setge_def) + + +subsection{*Rules about the Operators @{term leastP}, @{term ub} + and @{term lub}*} + +lemma leastPD1: "leastP P x ==> P x" +by (simp add: leastP_def) + +lemma leastPD2: "leastP P x ==> x <=* Collect P" +by (simp add: leastP_def) + +lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y" +by (blast dest!: leastPD2 setgeD) + +lemma isLubD1: "isLub R S x ==> S *<= x" +by (simp add: isLub_def isUb_def leastP_def) + +lemma isLubD1a: "isLub R S x ==> x: R" +by (simp add: isLub_def isUb_def leastP_def) + +lemma isLub_isUb: "isLub R S x ==> isUb R S x" +apply (simp add: isUb_def) +apply (blast dest: isLubD1 isLubD1a) +done + +lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x" +by (blast dest!: isLubD1 setleD) + +lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x" +by (simp add: isLub_def) + +lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x" +by (simp add: isLub_def) + +lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x" +by (simp add: isLub_def leastP_def) - setge_def - "x <=* S == (ALL y: S. x <= y)" +lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x" +by (simp add: isUb_def setle_def) + +lemma isUbD2: "isUb R S x ==> S *<= x" +by (simp add: isUb_def) + +lemma isUbD2a: "isUb R S x ==> x: R" +by (simp add: isUb_def) + +lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x" +by (simp add: isUb_def) + +lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y" +apply (simp add: isLub_def) +apply (blast intro!: leastPD3) +done + +lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S" +apply (simp add: ubs_def isLub_def) +apply (erule leastPD2) +done -end +ML +{* +val setle_def = thm "setle_def"; +val setge_def = thm "setge_def"; +val leastP_def = thm "leastP_def"; +val isLub_def = thm "isLub_def"; +val isUb_def = thm "isUb_def"; +val ubs_def = thm "ubs_def"; - +val setleI = thm "setleI"; +val setleD = thm "setleD"; +val setgeI = thm "setgeI"; +val setgeD = thm "setgeD"; +val leastPD1 = thm "leastPD1"; +val leastPD2 = thm "leastPD2"; +val leastPD3 = thm "leastPD3"; +val isLubD1 = thm "isLubD1"; +val isLubD1a = thm "isLubD1a"; +val isLub_isUb = thm "isLub_isUb"; +val isLubD2 = thm "isLubD2"; +val isLubD3 = thm "isLubD3"; +val isLubI1 = thm "isLubI1"; +val isLubI2 = thm "isLubI2"; +val isUbD = thm "isUbD"; +val isUbD2 = thm "isUbD2"; +val isUbD2a = thm "isUbD2a"; +val isUbI = thm "isUbI"; +val isLub_le_isUb = thm "isLub_le_isUb"; +val isLub_ubs = thm "isLub_ubs"; +*} + +end diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/Real/rat_arith.ML --- a/src/HOL/Real/rat_arith.ML Wed Jan 28 01:19:34 2004 +0100 +++ b/src/HOL/Real/rat_arith.ML Wed Jan 28 10:41:49 2004 +0100 @@ -577,9 +577,6 @@ (****Instantiation of the generic linear arithmetic package****) -val add_zero_left = thm"Ring_and_Field.add_0"; -val add_zero_right = thm"Ring_and_Field.add_0_right"; - local @@ -591,7 +588,7 @@ mult_rat_number_of, eq_rat_number_of, less_rat_number_of, le_number_of_eq_not_less, diff_minus, minus_add_distrib, minus_minus, mult_assoc, minus_zero, - add_zero_left, add_zero_right, left_minus, right_minus, + left_minus, right_minus, mult_zero_left, mult_zero_right, mult_1, mult_1_right, minus_mult_left RS sym, minus_mult_right RS sym]; @@ -603,18 +600,14 @@ val mono_ss = simpset() addsimps [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono]; -val add_mono_thms_rat = +val add_mono_thms_ordered_field = map (fn s => prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) - ["(i <= j) & (k <= l) ==> i + k <= j + (l::rat)", - "(i = j) & (k <= l) ==> i + k <= j + (l::rat)", - "(i <= j) & (k = l) ==> i + k <= j + (l::rat)", - "(i = j) & (k = l) ==> i + k = j + (l::rat)", - "(i < j) & (k = l) ==> i + k < j + (l::rat)", - "(i = j) & (k < l) ==> i + k < j + (l::rat)", - "(i < j) & (k <= l) ==> i + k < j + (l::rat)", - "(i <= j) & (k < l) ==> i + k < j + (l::rat)", - "(i < j) & (k < l) ==> i + k < j + (l::rat)"]; + ["(i < j) & (k = l) ==> i + k < j + (l::'a::ordered_field)", + "(i = j) & (k < l) ==> i + k < j + (l::'a::ordered_field)", + "(i < j) & (k <= l) ==> i + k < j + (l::'a::ordered_field)", + "(i <= j) & (k < l) ==> i + k < j + (l::'a::ordered_field)", + "(i < j) & (k < l) ==> i + k < j + (l::'a::ordered_field)"]; fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; @@ -643,7 +636,7 @@ val rat_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => - {add_mono_thms = add_mono_thms @ add_mono_thms_rat, + {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_field, mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms, inj_thms = (***int_inj_thms @*???**) inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*) diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Wed Jan 28 01:19:34 2004 +0100 +++ b/src/HOL/Real/real_arith.ML Wed Jan 28 10:41:49 2004 +0100 @@ -591,9 +591,6 @@ (****Instantiation of the generic linear arithmetic package****) -val add_zero_left = thm"Ring_and_Field.add_0"; -val add_zero_right = thm"Ring_and_Field.add_0_right"; - local (* reduce contradictory <= to False *) @@ -604,7 +601,7 @@ mult_real_number_of, eq_real_number_of, less_real_number_of, le_number_of_eq_not_less, diff_minus, minus_add_distrib, minus_minus, mult_assoc, minus_zero, - add_zero_left, add_zero_right, left_minus, right_minus, + left_minus, right_minus, mult_zero_left, mult_zero_right, mult_1, mult_1_right, minus_mult_left RS sym, minus_mult_right RS sym]; @@ -613,22 +610,6 @@ Real_Numeral_Simprocs.cancel_numerals @ Real_Numeral_Simprocs.eval_numerals; -val mono_ss = simpset() addsimps - [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono]; - -val add_mono_thms_real = - map (fn s => prove_goal (the_context ()) s - (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) - ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)", - "(i = j) & (k <= l) ==> i + k <= j + (l::real)", - "(i <= j) & (k = l) ==> i + k <= j + (l::real)", - "(i = j) & (k = l) ==> i + k = j + (l::real)", - "(i < j) & (k = l) ==> i + k < j + (l::real)", - "(i = j) & (k < l) ==> i + k < j + (l::real)", - "(i < j) & (k <= l) ==> i + k < j + (l::real)", - "(i <= j) & (k < l) ==> i + k < j + (l::real)", - "(i < j) & (k < l) ==> i + k < j + (l::real)"]; - fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; val real_mult_mono_thms = @@ -660,7 +641,7 @@ val real_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => - {add_mono_thms = add_mono_thms @ add_mono_thms_real, + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms @ real_mult_mono_thms, inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*) diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Wed Jan 28 01:19:34 2004 +0100 +++ b/src/HOL/Ring_and_Field.thy Wed Jan 28 10:41:49 2004 +0100 @@ -1625,8 +1625,12 @@ val divide_inverse = thm"divide_inverse"; val inverse_zero = thm"inverse_zero"; val divide_zero = thm"divide_zero"; + val add_0 = thm"add_0"; val add_0_right = thm"add_0_right"; +val add_zero_left = thm"add_0"; +val add_zero_right = thm"add_0_right"; + val add_left_commute = thm"add_left_commute"; val left_minus = thm"left_minus"; val right_minus = thm"right_minus"; diff -r 0b1447d37161 -r 2763da611ad9 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Wed Jan 28 01:19:34 2004 +0100 +++ b/src/HOL/arith_data.ML Wed Jan 28 10:41:49 2004 +0100 @@ -379,16 +379,16 @@ Most of the work is done by the cancel tactics. *) val add_rules = - [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, + [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, One_nat_def,isolateSuc]; -val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s +val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1, - blast_tac (claset() addIs [add_le_mono]) 1])) -["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)", - "(i = j) & (k <= l) ==> i + k <= j + (l::nat)", - "(i <= j) & (k = l) ==> i + k <= j + (l::nat)", - "(i = j) & (k = l) ==> i + k = j + (l::nat)" + blast_tac (claset() addIs [add_mono]) 1])) +["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)", + "(i = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)", + "(i <= j) & (k = l) ==> i + k <= j + (l::'a::ordered_semiring)", + "(i = j) & (k = l) ==> i + k = j + (l::'a::ordered_semiring)" ]; in @@ -396,7 +396,7 @@ val init_lin_arith_data = Fast_Arith.setup @ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset = _} => - {add_mono_thms = add_mono_thms @ add_mono_thms_nat, + {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_semiring, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, lessD = lessD @ [Suc_leI],