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.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"
```