src/HOL/HOL.thy
changeset 59504 8c6747dba731
parent 59028 df7476e79558
child 59507 b468e0f8da2a
     1.1 --- a/src/HOL/HOL.thy	Tue Feb 10 12:27:30 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Feb 10 16:08:11 2015 +0000
     1.3 @@ -550,63 +550,6 @@
     1.4  done
     1.5  
     1.6  
     1.7 -subsubsection {*THE: definite description operator*}
     1.8 -
     1.9 -lemma the_equality:
    1.10 -  assumes prema: "P a"
    1.11 -      and premx: "!!x. P x ==> x=a"
    1.12 -  shows "(THE x. P x) = a"
    1.13 -apply (rule trans [OF _ the_eq_trivial])
    1.14 -apply (rule_tac f = "The" in arg_cong)
    1.15 -apply (rule ext)
    1.16 -apply (rule iffI)
    1.17 - apply (erule premx)
    1.18 -apply (erule ssubst, rule prema)
    1.19 -done
    1.20 -
    1.21 -lemma theI:
    1.22 -  assumes "P a" and "!!x. P x ==> x=a"
    1.23 -  shows "P (THE x. P x)"
    1.24 -by (iprover intro: assms the_equality [THEN ssubst])
    1.25 -
    1.26 -lemma theI': "EX! x. P x ==> P (THE x. P x)"
    1.27 -apply (erule ex1E)
    1.28 -apply (erule theI)
    1.29 -apply (erule allE)
    1.30 -apply (erule mp)
    1.31 -apply assumption
    1.32 -done
    1.33 -
    1.34 -(*Easier to apply than theI: only one occurrence of P*)
    1.35 -lemma theI2:
    1.36 -  assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
    1.37 -  shows "Q (THE x. P x)"
    1.38 -by (iprover intro: assms theI)
    1.39 -
    1.40 -lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
    1.41 -by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
    1.42 -           elim:allE impE)
    1.43 -
    1.44 -lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
    1.45 -apply (rule the_equality)
    1.46 -apply  assumption
    1.47 -apply (erule ex1E)
    1.48 -apply (erule all_dupE)
    1.49 -apply (drule mp)
    1.50 -apply  assumption
    1.51 -apply (erule ssubst)
    1.52 -apply (erule allE)
    1.53 -apply (erule mp)
    1.54 -apply assumption
    1.55 -done
    1.56 -
    1.57 -lemma the_sym_eq_trivial: "(THE y. x=y) = x"
    1.58 -apply (rule the_equality)
    1.59 -apply (rule refl)
    1.60 -apply (erule sym)
    1.61 -done
    1.62 -
    1.63 -
    1.64  subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
    1.65  
    1.66  lemma disjCI:
    1.67 @@ -876,7 +819,6 @@
    1.68  
    1.69  declare ex_ex1I [intro!]
    1.70    and allI [intro!]
    1.71 -  and the_equality [intro]
    1.72    and exI [intro]
    1.73  
    1.74  declare exE [elim!]
    1.75 @@ -924,6 +866,39 @@
    1.76  *}
    1.77  
    1.78  
    1.79 +subsubsection {*THE: definite description operator*}
    1.80 +
    1.81 +lemma the_equality [intro]:
    1.82 +  assumes "P a"
    1.83 +      and "!!x. P x ==> x=a"
    1.84 +  shows "(THE x. P x) = a"
    1.85 +  by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
    1.86 +
    1.87 +lemma theI:
    1.88 +  assumes "P a" and "!!x. P x ==> x=a"
    1.89 +  shows "P (THE x. P x)"
    1.90 +by (iprover intro: assms the_equality [THEN ssubst])
    1.91 +
    1.92 +lemma theI': "EX! x. P x ==> P (THE x. P x)"
    1.93 +  by (blast intro: theI)
    1.94 +
    1.95 +(*Easier to apply than theI: only one occurrence of P*)
    1.96 +lemma theI2:
    1.97 +  assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
    1.98 +  shows "Q (THE x. P x)"
    1.99 +by (iprover intro: assms theI)
   1.100 +
   1.101 +lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
   1.102 +by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
   1.103 +           elim:allE impE)
   1.104 +
   1.105 +lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
   1.106 +  by blast
   1.107 +
   1.108 +lemma the_sym_eq_trivial: "(THE y. x=y) = x"
   1.109 +  by blast
   1.110 +
   1.111 +
   1.112  subsubsection {* Simplifier *}
   1.113  
   1.114  lemma eta_contract_eq: "(%s. f s) = f" ..
   1.115 @@ -1099,8 +1074,7 @@
   1.116  
   1.117  lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
   1.118    -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
   1.119 -  apply (simplesubst split_if, blast)
   1.120 -  done
   1.121 +  by (simplesubst split_if) blast
   1.122  
   1.123  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
   1.124  lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover