converted simp lemmas;
authorwenzelm
Sat Nov 24 16:54:10 2001 +0100 (2001-11-24)
changeset 122813bd113b8f7a6
parent 12280 fc7e3f01bc40
child 12282 f98beaaa7c4f
converted simp lemmas;
src/HOL/HOL.thy
src/HOL/simpdata.ML
     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)
     2.1 --- a/src/HOL/simpdata.ML	Sat Nov 24 16:53:31 2001 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Sat Nov 24 16:54:10 2001 +0100
     2.3 @@ -6,206 +6,73 @@
     2.4  Instantiation of the generic simplifier for HOL.
     2.5  *)
     2.6  
     2.7 -section "Simplifier";
     2.8 -
     2.9 -val [prem] = goal (the_context ()) "x==y ==> x=y";
    2.10 -by (rewtac prem);
    2.11 -by (rtac refl 1);
    2.12 -qed "meta_eq_to_obj_eq";
    2.13 -
    2.14 -Goal "(%s. f s) = f";
    2.15 -br refl 1;
    2.16 -qed "eta_contract_eq";
    2.17 -
    2.18 -
    2.19 -fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
    2.20 -
    2.21 -bind_thm ("not_not", prover "(~ ~ P) = P");
    2.22 -
    2.23 -bind_thms ("simp_thms", [not_not] @ map prover
    2.24 - ["(x=x) = True",
    2.25 -  "(~True) = False", "(~False) = True",
    2.26 -  "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    2.27 -  "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    2.28 -  "(True --> P) = P", "(False --> P) = True",
    2.29 -  "(P --> True) = True", "(P --> P) = True",
    2.30 -  "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    2.31 -  "(P & True) = P", "(True & P) = P",
    2.32 -  "(P & False) = False", "(False & P) = False",
    2.33 -  "(P & P) = P", "(P & (P & Q)) = (P & Q)",
    2.34 -  "(P & ~P) = False",    "(~P & P) = False",
    2.35 -  "(P | True) = True", "(True | P) = True",
    2.36 -  "(P | False) = P", "(False | P) = P",
    2.37 -  "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    2.38 -  "(P | ~P) = True",    "(~P | P) = True",
    2.39 -  "((~P) = (~Q)) = (P=Q)",
    2.40 -  "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
    2.41 -(* needed for the one-point-rule quantifier simplification procs*)
    2.42 -(*essential for termination!!*)
    2.43 -  "(? x. x=t & P(x)) = P(t)",
    2.44 -  "(? x. t=x & P(x)) = P(t)",
    2.45 -  "(! x. x=t --> P(x)) = P(t)",
    2.46 -  "(! x. t=x --> P(x)) = P(t)"]);
    2.47 -
    2.48 -bind_thm ("imp_cong", standard (impI RSN
    2.49 -    (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    2.50 -        (fn _=> [(Blast_tac 1)]) RS mp RS mp)));
    2.51 -
    2.52 -(*Miniscoping: pushing in existential quantifiers*)
    2.53 -bind_thms ("ex_simps", map prover
    2.54 - ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
    2.55 -  "(EX x. P & Q x)   = (P & (EX x. Q x))",
    2.56 -  "(EX x. P x | Q)   = ((EX x. P x) | Q)",
    2.57 -  "(EX x. P | Q x)   = (P | (EX x. Q x))",
    2.58 -  "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
    2.59 -  "(EX x. P --> Q x) = (P --> (EX x. Q x))"]);
    2.60 -
    2.61 -(*Miniscoping: pushing in universal quantifiers*)
    2.62 -bind_thms ("all_simps", map prover
    2.63 - ["(ALL x. P x & Q)   = ((ALL x. P x) & Q)",
    2.64 -  "(ALL x. P & Q x)   = (P & (ALL x. Q x))",
    2.65 -  "(ALL x. P x | Q)   = ((ALL x. P x) | Q)",
    2.66 -  "(ALL x. P | Q x)   = (P | (ALL x. Q x))",
    2.67 -  "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
    2.68 -  "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]);
    2.69 -
    2.70 -
    2.71 -fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
    2.72 -
    2.73 -prove "eq_commute" "(a=b) = (b=a)";
    2.74 -prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))";
    2.75 -prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))";
    2.76 -bind_thms ("eq_ac", [eq_commute, eq_left_commute, eq_assoc]);
    2.77 -
    2.78 -prove "neq_commute" "(a~=b) = (b~=a)";
    2.79 -
    2.80 -prove "conj_commute" "(P&Q) = (Q&P)";
    2.81 -prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
    2.82 -bind_thms ("conj_comms", [conj_commute, conj_left_commute]);
    2.83 -prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))";
    2.84 -
    2.85 -prove "disj_commute" "(P|Q) = (Q|P)";
    2.86 -prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))";
    2.87 -bind_thms ("disj_comms", [disj_commute, disj_left_commute]);
    2.88 -prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))";
    2.89 -
    2.90 -prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
    2.91 -prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";
    2.92 -
    2.93 -prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))";
    2.94 -prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))";
    2.95 -
    2.96 -prove "imp_conjR" "(P --> (Q&R)) = ((P-->Q) & (P-->R))";
    2.97 -prove "imp_conjL" "((P&Q) -->R)  = (P --> (Q --> R))";
    2.98 -prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))";
    2.99 -
   2.100 -(*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*)
   2.101 -prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)";
   2.102 -prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)";
   2.103 -
   2.104 -prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
   2.105 -prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";
   2.106 +(* legacy ML bindings *)
   2.107  
   2.108 -prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
   2.109 -prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
   2.110 -prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
   2.111 -prove "not_iff" "(P~=Q) = (P = (~Q))";
   2.112 -prove "disj_not1" "(~P | Q) = (P --> Q)";
   2.113 -prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
   2.114 -prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)";
   2.115 -
   2.116 -prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))";
   2.117 -
   2.118 -
   2.119 -(*Avoids duplication of subgoals after split_if, when the true and false
   2.120 -  cases boil down to the same thing.*)
   2.121 -prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
   2.122 -
   2.123 -prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))";
   2.124 -prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)";
   2.125 -prove "not_ex"  "(~ (? x. P(x))) = (! x.~P(x))";
   2.126 -prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)";
   2.127 -
   2.128 -prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
   2.129 -prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
   2.130 -
   2.131 -(* '&' congruence rule: not included by default!
   2.132 -   May slow rewrite proofs down by as much as 50% *)
   2.133 -
   2.134 -let val th = prove_goal (the_context ())
   2.135 -                "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
   2.136 -                (fn _=> [(Blast_tac 1)])
   2.137 -in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   2.138 -
   2.139 -let val th = prove_goal (the_context ())
   2.140 -                "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
   2.141 -                (fn _=> [(Blast_tac 1)])
   2.142 -in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   2.143 -
   2.144 -(* '|' congruence rule: not included by default! *)
   2.145 -
   2.146 -let val th = prove_goal (the_context ())
   2.147 -                "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
   2.148 -                (fn _=> [(Blast_tac 1)])
   2.149 -in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   2.150 -
   2.151 -prove "eq_sym_conv" "(x=y) = (y=x)";
   2.152 -
   2.153 -
   2.154 -(** if-then-else rules **)
   2.155 +val Eq_FalseI = thm "Eq_FalseI";
   2.156 +val Eq_TrueI = thm "Eq_TrueI";
   2.157 +val all_conj_distrib = thm "all_conj_distrib";
   2.158 +val all_simps = thms "all_simps";
   2.159 +val cases_simp = thm "cases_simp";
   2.160 +val conj_assoc = thm "conj_assoc";
   2.161 +val conj_comms = thms "conj_comms";
   2.162 +val conj_commute = thm "conj_commute";
   2.163 +val conj_cong = thm "conj_cong";
   2.164 +val conj_disj_distribL = thm "conj_disj_distribL";
   2.165 +val conj_disj_distribR = thm "conj_disj_distribR";
   2.166 +val conj_left_commute = thm "conj_left_commute";
   2.167 +val de_Morgan_conj = thm "de_Morgan_conj";
   2.168 +val de_Morgan_disj = thm "de_Morgan_disj";
   2.169 +val disj_assoc = thm "disj_assoc";
   2.170 +val disj_comms = thms "disj_comms";
   2.171 +val disj_commute = thm "disj_commute";
   2.172 +val disj_cong = thm "disj_cong";
   2.173 +val disj_conj_distribL = thm "disj_conj_distribL";
   2.174 +val disj_conj_distribR = thm "disj_conj_distribR";
   2.175 +val disj_left_commute = thm "disj_left_commute";
   2.176 +val disj_not1 = thm "disj_not1";
   2.177 +val disj_not2 = thm "disj_not2";
   2.178 +val eq_ac = thms "eq_ac";
   2.179 +val eq_assoc = thm "eq_assoc";
   2.180 +val eq_commute = thm "eq_commute";
   2.181 +val eq_left_commute = thm "eq_left_commute";
   2.182 +val eq_sym_conv = thm "eq_sym_conv";
   2.183 +val eta_contract_eq = thm "eta_contract_eq";
   2.184 +val ex_disj_distrib = thm "ex_disj_distrib";
   2.185 +val ex_simps = thms "ex_simps";
   2.186 +val if_False = thm "if_False";
   2.187 +val if_P = thm "if_P";
   2.188 +val if_True = thm "if_True";
   2.189 +val if_bool_eq_conj = thm "if_bool_eq_conj";
   2.190 +val if_bool_eq_disj = thm "if_bool_eq_disj";
   2.191 +val if_cancel = thm "if_cancel";
   2.192 +val if_def2 = thm "if_def2";
   2.193 +val if_eq_cancel = thm "if_eq_cancel";
   2.194 +val if_not_P = thm "if_not_P";
   2.195 +val if_splits = thms "if_splits";
   2.196 +val iff_conv_conj_imp = thm "iff_conv_conj_imp";
   2.197 +val imp_all = thm "imp_all";
   2.198 +val imp_cong = thm "imp_cong";
   2.199 +val imp_conjL = thm "imp_conjL";
   2.200 +val imp_conjR = thm "imp_conjR";
   2.201 +val imp_conv_disj = thm "imp_conv_disj";
   2.202 +val imp_disj1 = thm "imp_disj1";
   2.203 +val imp_disj2 = thm "imp_disj2";
   2.204 +val imp_disjL = thm "imp_disjL";
   2.205 +val imp_disj_not1 = thm "imp_disj_not1";
   2.206 +val imp_disj_not2 = thm "imp_disj_not2";
   2.207 +val imp_ex = thm "imp_ex";
   2.208 +val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
   2.209 +val neq_commute = thm "neq_commute";
   2.210 +val not_all = thm "not_all";
   2.211 +val not_ex = thm "not_ex";
   2.212 +val not_iff = thm "not_iff";
   2.213 +val not_imp = thm "not_imp";
   2.214 +val not_not = thm "not_not";
   2.215 +val rev_conj_cong = thm "rev_conj_cong";
   2.216 +val simp_thms = thms "simp_thms";
   2.217 +val split_if = thm "split_if";
   2.218 +val split_if_asm = thm "split_if_asm";
   2.219  
   2.220 -Goalw [if_def] "(if True then x else y) = x";
   2.221 -by (Blast_tac 1);
   2.222 -qed "if_True";
   2.223 -
   2.224 -Goalw [if_def] "(if False then x else y) = y";
   2.225 -by (Blast_tac 1);
   2.226 -qed "if_False";
   2.227 -
   2.228 -Goalw [if_def] "P ==> (if P then x else y) = x";
   2.229 -by (Blast_tac 1);
   2.230 -qed "if_P";
   2.231 -
   2.232 -Goalw [if_def] "~P ==> (if P then x else y) = y";
   2.233 -by (Blast_tac 1);
   2.234 -qed "if_not_P";
   2.235 -
   2.236 -Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))";
   2.237 -by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1);
   2.238 -by (stac if_P 2);
   2.239 -by (stac if_not_P 1);
   2.240 -by (ALLGOALS (Blast_tac));
   2.241 -qed "split_if";
   2.242 -
   2.243 -Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))";
   2.244 -by (stac split_if 1);
   2.245 -by (Blast_tac 1);
   2.246 -qed "split_if_asm";
   2.247 -
   2.248 -bind_thms ("if_splits", [split_if, split_if_asm]);
   2.249 -
   2.250 -bind_thm ("if_def2", read_instantiate [("P","\\<lambda>x. x")] split_if);
   2.251 -
   2.252 -Goal "(if c then x else x) = x";
   2.253 -by (stac split_if 1);
   2.254 -by (Blast_tac 1);
   2.255 -qed "if_cancel";
   2.256 -
   2.257 -Goal "(if x = y then y else x) = x";
   2.258 -by (stac split_if 1);
   2.259 -by (Blast_tac 1);
   2.260 -qed "if_eq_cancel";
   2.261 -
   2.262 -(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
   2.263 -Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))";
   2.264 -by (rtac split_if 1);
   2.265 -qed "if_bool_eq_conj";
   2.266 -
   2.267 -(*And this form is useful for expanding IFs on the LEFT*)
   2.268 -Goal "(if P then Q else R) = ((P&Q) | (~P&R))";
   2.269 -by (stac split_if 1);
   2.270 -by (Blast_tac 1);
   2.271 -qed "if_bool_eq_disj";
   2.272  
   2.273  local
   2.274  val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
   2.275 @@ -264,9 +131,6 @@
   2.276  fun mk_meta_eq r = r RS eq_reflection;
   2.277  fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
   2.278  
   2.279 -bind_thm ("Eq_TrueI", mk_meta_eq (prover  "P --> (P = True)"  RS mp));
   2.280 -bind_thm ("Eq_FalseI", mk_meta_eq(prover "~P --> (P = False)" RS mp));
   2.281 -
   2.282  fun mk_eq th = case concl_of th of
   2.283          Const("==",_)$_$_       => th
   2.284      |   _$(Const("op =",_)$_$_) => mk_meta_eq th