src/HOL/Orderings.thy
changeset 45221 3eadb9b6a055
parent 44921 58eef4843641
child 45231 d85a2fdc586c
     1.1 --- a/src/HOL/Orderings.thy	Thu Oct 20 22:02:49 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Oct 20 22:26:02 2011 +0200
     1.3 @@ -883,7 +883,7 @@
     1.4  text {* These support proving chains of decreasing inequalities
     1.5      a >= b >= c ... in Isar proofs. *}
     1.6  
     1.7 -lemma xt1:
     1.8 +lemma xt1 [no_atp]:
     1.9    "a = b ==> b > c ==> a > c"
    1.10    "a > b ==> b = c ==> a > c"
    1.11    "a = b ==> b >= c ==> a >= c"
    1.12 @@ -902,39 +902,39 @@
    1.13    "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
    1.14    by auto
    1.15  
    1.16 -lemma xt2:
    1.17 +lemma xt2 [no_atp]:
    1.18    "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
    1.19  by (subgoal_tac "f b >= f c", force, force)
    1.20  
    1.21 -lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> 
    1.22 +lemma xt3 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
    1.23      (!!x y. x >= y ==> f x >= f y) ==> f a >= c"
    1.24  by (subgoal_tac "f a >= f b", force, force)
    1.25  
    1.26 -lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
    1.27 +lemma xt4 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
    1.28    (!!x y. x >= y ==> f x >= f y) ==> a > f c"
    1.29  by (subgoal_tac "f b >= f c", force, force)
    1.30  
    1.31 -lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
    1.32 +lemma xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
    1.33      (!!x y. x > y ==> f x > f y) ==> f a > c"
    1.34  by (subgoal_tac "f a > f b", force, force)
    1.35  
    1.36 -lemma xt6: "(a::'a::order) >= f b ==> b > c ==>
    1.37 +lemma xt6 [no_atp]: "(a::'a::order) >= f b ==> b > c ==>
    1.38      (!!x y. x > y ==> f x > f y) ==> a > f c"
    1.39  by (subgoal_tac "f b > f c", force, force)
    1.40  
    1.41 -lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
    1.42 +lemma xt7 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
    1.43      (!!x y. x >= y ==> f x >= f y) ==> f a > c"
    1.44  by (subgoal_tac "f a >= f b", force, force)
    1.45  
    1.46 -lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
    1.47 +lemma xt8 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
    1.48      (!!x y. x > y ==> f x > f y) ==> a > f c"
    1.49  by (subgoal_tac "f b > f c", force, force)
    1.50  
    1.51 -lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
    1.52 +lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
    1.53      (!!x y. x > y ==> f x > f y) ==> f a > c"
    1.54  by (subgoal_tac "f a > f b", force, force)
    1.55  
    1.56 -lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
    1.57 +lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp]
    1.58  
    1.59  (* 
    1.60    Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands