# HG changeset patch # User huffman # Date 1159312715 -7200 # Node ID 4358cd94a449b95eb69b86bdf6ecefb7bbb8c6d4 # Parent bf00c59354321f680da67ad7c043ff9bc068bf68 more lemmas about Standard and star_of diff -r bf00c5935432 -r 4358cd94a449 src/HOL/Hyperreal/StarClasses.thy --- a/src/HOL/Hyperreal/StarClasses.thy Wed Sep 27 00:54:10 2006 +0200 +++ b/src/HOL/Hyperreal/StarClasses.thy Wed Sep 27 01:18:35 2006 +0200 @@ -211,6 +211,32 @@ instance star :: (linorder) linorder by (intro_classes, transfer, rule linorder_linear) +lemma star_max_def [transfer_unfold]: "max = *f2* max" +apply (rule ext, rule ext) +apply (unfold max_def, transfer, fold max_def) +apply (rule refl) +done + +lemma star_min_def [transfer_unfold]: "min = *f2* min" +apply (rule ext, rule ext) +apply (unfold min_def, transfer, fold min_def) +apply (rule refl) +done + +lemma Standard_max [simp]: + "\x \ Standard; y \ Standard\ \ max x y \ Standard" +by (simp add: star_max_def) + +lemma Standard_min [simp]: + "\x \ Standard; y \ Standard\ \ min x y \ Standard" +by (simp add: star_min_def) + +lemma star_of_max [simp]: "star_of (max x y) = max (star_of x) (star_of y)" +by transfer (rule refl) + +lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)" +by transfer (rule refl) + subsection {* Lattice ordering classes *} text {* @@ -245,15 +271,29 @@ instance star :: (lorder) lorder .. -lemma star_join_def [transfer_unfold]: "join \ *f2* join" - apply (rule is_join_unique [OF is_join_join, THEN eq_reflection]) - apply (transfer is_join_def, rule is_join_join) +lemma star_meet_def [transfer_unfold]: "meet = *f2* meet" +apply (rule is_meet_unique [OF is_meet_meet]) +apply (transfer is_meet_def, rule is_meet_meet) +done + +lemma star_join_def [transfer_unfold]: "join = *f2* join" +apply (rule is_join_unique [OF is_join_join]) +apply (transfer is_join_def, rule is_join_join) done -lemma star_meet_def [transfer_unfold]: "meet \ *f2* meet" - apply (rule is_meet_unique [OF is_meet_meet, THEN eq_reflection]) - apply (transfer is_meet_def, rule is_meet_meet) -done +lemma Standard_meet [simp]: + "\x \ Standard; y \ Standard\ \ meet x y \ Standard" +by (simp add: star_meet_def) + +lemma Standard_join [simp]: + "\x \ Standard; y \ Standard\ \ join x y \ Standard" +by (simp add: star_join_def) + +lemma star_of_meet [simp]: "star_of (meet x y) = meet (star_of x) (star_of y)" +by transfer (rule refl) + +lemma star_of_join [simp]: "star_of (join x y) = join (star_of x) (star_of y)" +by transfer (rule refl) subsection {* Ordered group classes *} @@ -421,14 +461,20 @@ subsection {* Number classes *} -lemma star_of_nat_def [transfer_unfold]: "of_nat n \ star_of (of_nat n)" -by (rule eq_reflection, induct_tac n, simp_all) +lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)" +by (induct_tac n, simp_all) + +lemma Standard_of_nat [simp]: "of_nat n \ Standard" +by (simp add: star_of_nat_def) lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n" by transfer (rule refl) -lemma star_of_int_def [transfer_unfold]: "of_int z \ star_of (of_int z)" -by (rule eq_reflection, rule_tac z=z in int_diff_cases, simp) +lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)" +by (rule_tac z=z in int_diff_cases, simp) + +lemma Standard_of_int [simp]: "of_int z \ Standard" +by (simp add: star_of_int_def) lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z" by transfer (rule refl)