900 "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" |
900 "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" |
901 "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" |
901 "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" |
902 "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" |
902 "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" |
903 by auto |
903 by auto |
904 |
904 |
905 lemma xt2: |
905 lemma xt2 [no_atp]: |
906 "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" |
906 "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" |
907 by (subgoal_tac "f b >= f c", force, force) |
907 by (subgoal_tac "f b >= f c", force, force) |
908 |
908 |
909 lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> |
909 lemma xt3 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> |
910 (!!x y. x >= y ==> f x >= f y) ==> f a >= c" |
910 (!!x y. x >= y ==> f x >= f y) ==> f a >= c" |
911 by (subgoal_tac "f a >= f b", force, force) |
911 by (subgoal_tac "f a >= f b", force, force) |
912 |
912 |
913 lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> |
913 lemma xt4 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> |
914 (!!x y. x >= y ==> f x >= f y) ==> a > f c" |
914 (!!x y. x >= y ==> f x >= f y) ==> a > f c" |
915 by (subgoal_tac "f b >= f c", force, force) |
915 by (subgoal_tac "f b >= f c", force, force) |
916 |
916 |
917 lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==> |
917 lemma xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==> |
918 (!!x y. x > y ==> f x > f y) ==> f a > c" |
918 (!!x y. x > y ==> f x > f y) ==> f a > c" |
919 by (subgoal_tac "f a > f b", force, force) |
919 by (subgoal_tac "f a > f b", force, force) |
920 |
920 |
921 lemma xt6: "(a::'a::order) >= f b ==> b > c ==> |
921 lemma xt6 [no_atp]: "(a::'a::order) >= f b ==> b > c ==> |
922 (!!x y. x > y ==> f x > f y) ==> a > f c" |
922 (!!x y. x > y ==> f x > f y) ==> a > f c" |
923 by (subgoal_tac "f b > f c", force, force) |
923 by (subgoal_tac "f b > f c", force, force) |
924 |
924 |
925 lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> |
925 lemma xt7 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> |
926 (!!x y. x >= y ==> f x >= f y) ==> f a > c" |
926 (!!x y. x >= y ==> f x >= f y) ==> f a > c" |
927 by (subgoal_tac "f a >= f b", force, force) |
927 by (subgoal_tac "f a >= f b", force, force) |
928 |
928 |
929 lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==> |
929 lemma xt8 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) > c ==> |
930 (!!x y. x > y ==> f x > f y) ==> a > f c" |
930 (!!x y. x > y ==> f x > f y) ==> a > f c" |
931 by (subgoal_tac "f b > f c", force, force) |
931 by (subgoal_tac "f b > f c", force, force) |
932 |
932 |
933 lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==> |
933 lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==> |
934 (!!x y. x > y ==> f x > f y) ==> f a > c" |
934 (!!x y. x > y ==> f x > f y) ==> f a > c" |
935 by (subgoal_tac "f a > f b", force, force) |
935 by (subgoal_tac "f a > f b", force, force) |
936 |
936 |
937 lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 |
937 lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp] |
938 |
938 |
939 (* |
939 (* |
940 Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands |
940 Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands |
941 for the wrong thing in an Isar proof. |
941 for the wrong thing in an Isar proof. |
942 |
942 |