src/HOL/HOL.thy
changeset 12281 3bd113b8f7a6
parent 12256 26243ebf2831
child 12338 de0f4a63baa5
     1.1 --- a/src/HOL/HOL.thy	Sat Nov 24 16:53:31 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Nov 24 16:54:10 2001 +0100
     1.3 @@ -265,6 +265,198 @@
     1.4  
     1.5  subsubsection {* Simplifier setup *}
     1.6  
     1.7 +lemma meta_eq_to_obj_eq: "x == y ==> x = y"
     1.8 +proof -
     1.9 +  assume r: "x == y"
    1.10 +  show "x = y" by (unfold r) (rule refl)
    1.11 +qed
    1.12 +
    1.13 +lemma eta_contract_eq: "(%s. f s) = f" ..
    1.14 +
    1.15 +lemma simp_thms:
    1.16 +  (not_not: "(~ ~ P) = P" and
    1.17 +    "(x = x) = True"
    1.18 +    "(~True) = False"  "(~False) = True"
    1.19 +    "(~P) ~= P"  "P ~= (~P)"  "(P ~= Q) = (P = (~Q))"
    1.20 +    "(True=P) = P"  "(P=True) = P"  "(False=P) = (~P)"  "(P=False) = (~P)"
    1.21 +    "(True --> P) = P"  "(False --> P) = True"
    1.22 +    "(P --> True) = True"  "(P --> P) = True"
    1.23 +    "(P --> False) = (~P)"  "(P --> ~P) = (~P)"
    1.24 +    "(P & True) = P"  "(True & P) = P"
    1.25 +    "(P & False) = False"  "(False & P) = False"
    1.26 +    "(P & P) = P"  "(P & (P & Q)) = (P & Q)"
    1.27 +    "(P & ~P) = False"    "(~P & P) = False"
    1.28 +    "(P | True) = True"  "(True | P) = True"
    1.29 +    "(P | False) = P"  "(False | P) = P"
    1.30 +    "(P | P) = P"  "(P | (P | Q)) = (P | Q)"
    1.31 +    "(P | ~P) = True"    "(~P | P) = True"
    1.32 +    "((~P) = (~Q)) = (P=Q)" and
    1.33 +    "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
    1.34 +    -- {* needed for the one-point-rule quantifier simplification procs *}
    1.35 +    -- {* essential for termination!! *} and
    1.36 +    "!!P. (EX x. x=t & P(x)) = P(t)"
    1.37 +    "!!P. (EX x. t=x & P(x)) = P(t)"
    1.38 +    "!!P. (ALL x. x=t --> P(x)) = P(t)"
    1.39 +    "!!P. (ALL x. t=x --> P(x)) = P(t)")
    1.40 +  by blast+
    1.41 +
    1.42 +lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
    1.43 +  by blast
    1.44 +
    1.45 +lemma ex_simps:
    1.46 +  "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
    1.47 +  "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
    1.48 +  "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"
    1.49 +  "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"
    1.50 +  "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
    1.51 +  "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
    1.52 +  -- {* Miniscoping: pushing in existential quantifiers. *}
    1.53 +  by blast+
    1.54 +
    1.55 +lemma all_simps:
    1.56 +  "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
    1.57 +  "!!P Q. (ALL x. P & Q x)   = (P & (ALL x. Q x))"
    1.58 +  "!!P Q. (ALL x. P x | Q)   = ((ALL x. P x) | Q)"
    1.59 +  "!!P Q. (ALL x. P | Q x)   = (P | (ALL x. Q x))"
    1.60 +  "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
    1.61 +  "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
    1.62 +  -- {* Miniscoping: pushing in universal quantifiers. *}
    1.63 +  by blast+
    1.64 +
    1.65 +lemma eq_ac:
    1.66 + (eq_commute: "(a=b) = (b=a)" and
    1.67 +  eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" and
    1.68 +  eq_assoc: "((P=Q)=R) = (P=(Q=R))") by blast+
    1.69 +lemma neq_commute: "(a~=b) = (b~=a)" by blast
    1.70 +
    1.71 +lemma conj_comms:
    1.72 + (conj_commute: "(P&Q) = (Q&P)" and
    1.73 +  conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by blast+
    1.74 +lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by blast
    1.75 +
    1.76 +lemma disj_comms:
    1.77 + (disj_commute: "(P|Q) = (Q|P)" and
    1.78 +  disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by blast+
    1.79 +lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by blast
    1.80 +
    1.81 +lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by blast
    1.82 +lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by blast
    1.83 +
    1.84 +lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by blast
    1.85 +lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by blast
    1.86 +
    1.87 +lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by blast
    1.88 +lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by blast
    1.89 +lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by blast
    1.90 +
    1.91 +text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
    1.92 +lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
    1.93 +lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast
    1.94 +
    1.95 +lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
    1.96 +lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
    1.97 +
    1.98 +lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by blast
    1.99 +lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
   1.100 +lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
   1.101 +lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
   1.102 +lemma disj_not1: "(~P | Q) = (P --> Q)" by blast
   1.103 +lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- {* changes orientation :-( *}
   1.104 +  by blast
   1.105 +lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
   1.106 +
   1.107 +lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by blast
   1.108 +
   1.109 +
   1.110 +lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
   1.111 +  -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *}
   1.112 +  -- {* cases boil down to the same thing. *}
   1.113 +  by blast
   1.114 +
   1.115 +lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
   1.116 +lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
   1.117 +lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by blast
   1.118 +lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by blast
   1.119 +
   1.120 +lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by blast
   1.121 +lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by blast
   1.122 +
   1.123 +text {*
   1.124 +  \medskip The @{text "&"} congruence rule: not included by default!
   1.125 +  May slow rewrite proofs down by as much as 50\% *}
   1.126 +
   1.127 +lemma conj_cong:
   1.128 +    "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
   1.129 +  by blast
   1.130 +
   1.131 +lemma rev_conj_cong:
   1.132 +    "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
   1.133 +  by blast
   1.134 +
   1.135 +text {* The @{text "|"} congruence rule: not included by default! *}
   1.136 +
   1.137 +lemma disj_cong:
   1.138 +    "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
   1.139 +  by blast
   1.140 +
   1.141 +lemma eq_sym_conv: "(x = y) = (y = x)"
   1.142 +  by blast
   1.143 +
   1.144 +
   1.145 +text {* \medskip if-then-else rules *}
   1.146 +
   1.147 +lemma if_True: "(if True then x else y) = x"
   1.148 +  by (unfold if_def) blast
   1.149 +
   1.150 +lemma if_False: "(if False then x else y) = y"
   1.151 +  by (unfold if_def) blast
   1.152 +
   1.153 +lemma if_P: "P ==> (if P then x else y) = x"
   1.154 +  by (unfold if_def) blast
   1.155 +
   1.156 +lemma if_not_P: "~P ==> (if P then x else y) = y"
   1.157 +  by (unfold if_def) blast
   1.158 +
   1.159 +lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
   1.160 +  apply (rule case_split [of Q])
   1.161 +   apply (subst if_P)
   1.162 +    prefer 3 apply (subst if_not_P)
   1.163 +     apply blast+
   1.164 +  done
   1.165 +
   1.166 +lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
   1.167 +  apply (subst split_if)
   1.168 +  apply blast
   1.169 +  done
   1.170 +
   1.171 +lemmas if_splits = split_if split_if_asm
   1.172 +
   1.173 +lemma if_def2: "(if Q then x else y) = ((Q --> x) & (~ Q --> y))"
   1.174 +  by (rule split_if)
   1.175 +
   1.176 +lemma if_cancel: "(if c then x else x) = x"
   1.177 +  apply (subst split_if)
   1.178 +  apply blast
   1.179 +  done
   1.180 +
   1.181 +lemma if_eq_cancel: "(if x = y then y else x) = x"
   1.182 +  apply (subst split_if)
   1.183 +  apply blast
   1.184 +  done
   1.185 +
   1.186 +lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   1.187 +  -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
   1.188 +  by (rule split_if)
   1.189 +
   1.190 +lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
   1.191 +  -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
   1.192 +  apply (subst split_if)
   1.193 +  apply blast
   1.194 +  done
   1.195 +
   1.196 +lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) blast
   1.197 +lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) blast
   1.198 +
   1.199  use "simpdata.ML"
   1.200  setup Simplifier.setup
   1.201  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
   1.202 @@ -496,14 +688,14 @@
   1.203    "[| P (x::'a::order);
   1.204        !!y. P y ==> x <= y;
   1.205        !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   1.206 -   ==> Q (Least P)";
   1.207 +   ==> Q (Least P)"
   1.208    apply (unfold Least_def)
   1.209    apply (rule theI2)
   1.210      apply (blast intro: order_antisym)+
   1.211    done
   1.212  
   1.213  lemma Least_equality:
   1.214 -    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
   1.215 +    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   1.216    apply (simp add: Least_def)
   1.217    apply (rule the_equality)
   1.218    apply (auto intro!: order_antisym)