src/HOL/HOL.thy
changeset 14208 144f45277d5a
parent 14201 7ad7ab89c402
child 14223 0ee05eef881b
     1.1 --- a/src/HOL/HOL.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -489,14 +489,11 @@
     1.4  lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
     1.5    apply (rule case_split [of Q])
     1.6     apply (subst if_P)
     1.7 -    prefer 3 apply (subst if_not_P)
     1.8 -     apply blast+
     1.9 +    prefer 3 apply (subst if_not_P, blast+)
    1.10    done
    1.11  
    1.12  lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
    1.13 -  apply (subst split_if)
    1.14 -  apply blast
    1.15 -  done
    1.16 +by (subst split_if, blast)
    1.17  
    1.18  lemmas if_splits = split_if split_if_asm
    1.19  
    1.20 @@ -504,14 +501,10 @@
    1.21    by (rule split_if)
    1.22  
    1.23  lemma if_cancel: "(if c then x else x) = x"
    1.24 -  apply (subst split_if)
    1.25 -  apply blast
    1.26 -  done
    1.27 +by (subst split_if, blast)
    1.28  
    1.29  lemma if_eq_cancel: "(if x = y then y else x) = x"
    1.30 -  apply (subst split_if)
    1.31 -  apply blast
    1.32 -  done
    1.33 +by (subst split_if, blast)
    1.34  
    1.35  lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.36    -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
    1.37 @@ -519,8 +512,7 @@
    1.38  
    1.39  lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
    1.40    -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
    1.41 -  apply (subst split_if)
    1.42 -  apply blast
    1.43 +  apply (subst split_if, blast)
    1.44    done
    1.45  
    1.46  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
    1.47 @@ -552,8 +544,7 @@
    1.48    apply (erule impE)
    1.49    apply (rule allI)
    1.50    apply (rule_tac P = "xa = x" in case_split_thm)
    1.51 -  apply (drule_tac [3] x = x in fun_cong)
    1.52 -  apply simp_all
    1.53 +  apply (drule_tac [3] x = x in fun_cong, simp_all)
    1.54    done
    1.55  
    1.56  text{*Needs only HOL-lemmas:*}
    1.57 @@ -706,8 +697,7 @@
    1.58  
    1.59  lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
    1.60      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
    1.61 -  apply (simp add: order_less_le)
    1.62 -  apply blast
    1.63 +  apply (simp add: order_less_le, blast)
    1.64    done
    1.65  
    1.66  lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
    1.67 @@ -723,8 +713,7 @@
    1.68  
    1.69  lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
    1.70    apply (drule order_less_not_sym)
    1.71 -  apply (erule contrapos_np)
    1.72 -  apply simp
    1.73 +  apply (erule contrapos_np, simp)
    1.74    done
    1.75  
    1.76  
    1.77 @@ -806,14 +795,12 @@
    1.78  
    1.79  lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
    1.80    apply (simp add: order_less_le)
    1.81 -  apply (insert linorder_linear)
    1.82 -  apply blast
    1.83 +  apply (insert linorder_linear, blast)
    1.84    done
    1.85  
    1.86  lemma linorder_cases [case_names less equal greater]:
    1.87      "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
    1.88 -  apply (insert linorder_less_linear)
    1.89 -  apply blast
    1.90 +  apply (insert linorder_less_linear, blast)
    1.91    done
    1.92  
    1.93  lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
    1.94 @@ -829,14 +816,10 @@
    1.95    done
    1.96  
    1.97  lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
    1.98 -  apply (cut_tac x = x and y = y in linorder_less_linear)
    1.99 -  apply auto
   1.100 -  done
   1.101 +by (cut_tac x = x and y = y in linorder_less_linear, auto)
   1.102  
   1.103  lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
   1.104 -  apply (simp add: linorder_neq_iff)
   1.105 -  apply blast
   1.106 -  done
   1.107 +by (simp add: linorder_neq_iff, blast)
   1.108  
   1.109  
   1.110  subsubsection "Min and max on (linear) orders"