converted Real/Lubs to Isar script. Converting arithmetic setup
files to be polymorphic.
--- 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],
--- 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 \
--- 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";
-
-
-
-
--- 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
--- 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!*)
--- 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!*)
--- 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";
--- 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],