# HG changeset patch
# User wenzelm
# Date 1006617250 -3600
# Node ID 3bd113b8f7a6de1b5a124856e2190dfb86757dd9
# Parent  fc7e3f01bc40d933d372b1b2d8c0117fb2156332
converted simp lemmas;

diff -r fc7e3f01bc40 -r 3bd113b8f7a6 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Nov 24 16:53:31 2001 +0100
+++ b/src/HOL/HOL.thy	Sat Nov 24 16:54:10 2001 +0100
@@ -265,6 +265,198 @@
 
 subsubsection {* Simplifier setup *}
 
+lemma meta_eq_to_obj_eq: "x == y ==> x = y"
+proof -
+  assume r: "x == y"
+  show "x = y" by (unfold r) (rule refl)
+qed
+
+lemma eta_contract_eq: "(%s. f s) = f" ..
+
+lemma simp_thms:
+  (not_not: "(~ ~ P) = P" and
+    "(x = x) = True"
+    "(~True) = False"  "(~False) = True"
+    "(~P) ~= P"  "P ~= (~P)"  "(P ~= Q) = (P = (~Q))"
+    "(True=P) = P"  "(P=True) = P"  "(False=P) = (~P)"  "(P=False) = (~P)"
+    "(True --> P) = P"  "(False --> P) = True"
+    "(P --> True) = True"  "(P --> P) = True"
+    "(P --> False) = (~P)"  "(P --> ~P) = (~P)"
+    "(P & True) = P"  "(True & P) = P"
+    "(P & False) = False"  "(False & P) = False"
+    "(P & P) = P"  "(P & (P & Q)) = (P & Q)"
+    "(P & ~P) = False"    "(~P & P) = False"
+    "(P | True) = True"  "(True | P) = True"
+    "(P | False) = P"  "(False | P) = P"
+    "(P | P) = P"  "(P | (P | Q)) = (P | Q)"
+    "(P | ~P) = True"    "(~P | P) = True"
+    "((~P) = (~Q)) = (P=Q)" and
+    "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
+    -- {* needed for the one-point-rule quantifier simplification procs *}
+    -- {* essential for termination!! *} and
+    "!!P. (EX x. x=t & P(x)) = P(t)"
+    "!!P. (EX x. t=x & P(x)) = P(t)"
+    "!!P. (ALL x. x=t --> P(x)) = P(t)"
+    "!!P. (ALL x. t=x --> P(x)) = P(t)")
+  by blast+
+
+lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
+  by blast
+
+lemma ex_simps:
+  "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
+  "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
+  "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"
+  "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"
+  "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
+  "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
+  -- {* Miniscoping: pushing in existential quantifiers. *}
+  by blast+
+
+lemma all_simps:
+  "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
+  "!!P Q. (ALL x. P & Q x)   = (P & (ALL x. Q x))"
+  "!!P Q. (ALL x. P x | Q)   = ((ALL x. P x) | Q)"
+  "!!P Q. (ALL x. P | Q x)   = (P | (ALL x. Q x))"
+  "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
+  "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
+  -- {* Miniscoping: pushing in universal quantifiers. *}
+  by blast+
+
+lemma eq_ac:
+ (eq_commute: "(a=b) = (b=a)" and
+  eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" and
+  eq_assoc: "((P=Q)=R) = (P=(Q=R))") by blast+
+lemma neq_commute: "(a~=b) = (b~=a)" by blast
+
+lemma conj_comms:
+ (conj_commute: "(P&Q) = (Q&P)" and
+  conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by blast+
+lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by blast
+
+lemma disj_comms:
+ (disj_commute: "(P|Q) = (Q|P)" and
+  disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by blast+
+lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by blast
+
+lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by blast
+lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by blast
+
+lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by blast
+lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by blast
+
+lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by blast
+lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by blast
+lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by blast
+
+text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
+lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
+lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast
+
+lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
+lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
+
+lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by blast
+lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
+lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
+lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
+lemma disj_not1: "(~P | Q) = (P --> Q)" by blast
+lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- {* changes orientation :-( *}
+  by blast
+lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
+
+lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by blast
+
+
+lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
+  -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *}
+  -- {* cases boil down to the same thing. *}
+  by blast
+
+lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
+lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
+lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by blast
+lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by blast
+
+lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by blast
+lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by blast
+
+text {*
+  \medskip The @{text "&"} congruence rule: not included by default!
+  May slow rewrite proofs down by as much as 50\% *}
+
+lemma conj_cong:
+    "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
+  by blast
+
+lemma rev_conj_cong:
+    "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
+  by blast
+
+text {* The @{text "|"} congruence rule: not included by default! *}
+
+lemma disj_cong:
+    "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
+  by blast
+
+lemma eq_sym_conv: "(x = y) = (y = x)"
+  by blast
+
+
+text {* \medskip if-then-else rules *}
+
+lemma if_True: "(if True then x else y) = x"
+  by (unfold if_def) blast
+
+lemma if_False: "(if False then x else y) = y"
+  by (unfold if_def) blast
+
+lemma if_P: "P ==> (if P then x else y) = x"
+  by (unfold if_def) blast
+
+lemma if_not_P: "~P ==> (if P then x else y) = y"
+  by (unfold if_def) blast
+
+lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
+  apply (rule case_split [of Q])
+   apply (subst if_P)
+    prefer 3 apply (subst if_not_P)
+     apply blast+
+  done
+
+lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
+  apply (subst split_if)
+  apply blast
+  done
+
+lemmas if_splits = split_if split_if_asm
+
+lemma if_def2: "(if Q then x else y) = ((Q --> x) & (~ Q --> y))"
+  by (rule split_if)
+
+lemma if_cancel: "(if c then x else x) = x"
+  apply (subst split_if)
+  apply blast
+  done
+
+lemma if_eq_cancel: "(if x = y then y else x) = x"
+  apply (subst split_if)
+  apply blast
+  done
+
+lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
+  -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
+  by (rule split_if)
+
+lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
+  -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
+  apply (subst split_if)
+  apply blast
+  done
+
+lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) blast
+lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) blast
+
 use "simpdata.ML"
 setup Simplifier.setup
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
@@ -496,14 +688,14 @@
   "[| P (x::'a::order);
       !!y. P y ==> x <= y;
       !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
-   ==> Q (Least P)";
+   ==> Q (Least P)"
   apply (unfold Least_def)
   apply (rule theI2)
     apply (blast intro: order_antisym)+
   done
 
 lemma Least_equality:
-    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
+    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   apply (simp add: Least_def)
   apply (rule the_equality)
   apply (auto intro!: order_antisym)
diff -r fc7e3f01bc40 -r 3bd113b8f7a6 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Sat Nov 24 16:53:31 2001 +0100
+++ b/src/HOL/simpdata.ML	Sat Nov 24 16:54:10 2001 +0100
@@ -6,206 +6,73 @@
 Instantiation of the generic simplifier for HOL.
 *)
 
-section "Simplifier";
-
-val [prem] = goal (the_context ()) "x==y ==> x=y";
-by (rewtac prem);
-by (rtac refl 1);
-qed "meta_eq_to_obj_eq";
-
-Goal "(%s. f s) = f";
-br refl 1;
-qed "eta_contract_eq";
-
-
-fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
-
-bind_thm ("not_not", prover "(~ ~ P) = P");
-
-bind_thms ("simp_thms", [not_not] @ map prover
- ["(x=x) = True",
-  "(~True) = False", "(~False) = True",
-  "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
-  "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
-  "(True --> P) = P", "(False --> P) = True",
-  "(P --> True) = True", "(P --> P) = True",
-  "(P --> False) = (~P)", "(P --> ~P) = (~P)",
-  "(P & True) = P", "(True & P) = P",
-  "(P & False) = False", "(False & P) = False",
-  "(P & P) = P", "(P & (P & Q)) = (P & Q)",
-  "(P & ~P) = False",    "(~P & P) = False",
-  "(P | True) = True", "(True | P) = True",
-  "(P | False) = P", "(False | P) = P",
-  "(P | P) = P", "(P | (P | Q)) = (P | Q)",
-  "(P | ~P) = True",    "(~P | P) = True",
-  "((~P) = (~Q)) = (P=Q)",
-  "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
-(* needed for the one-point-rule quantifier simplification procs*)
-(*essential for termination!!*)
-  "(? x. x=t & P(x)) = P(t)",
-  "(? x. t=x & P(x)) = P(t)",
-  "(! x. x=t --> P(x)) = P(t)",
-  "(! x. t=x --> P(x)) = P(t)"]);
-
-bind_thm ("imp_cong", standard (impI RSN
-    (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
-        (fn _=> [(Blast_tac 1)]) RS mp RS mp)));
-
-(*Miniscoping: pushing in existential quantifiers*)
-bind_thms ("ex_simps", map prover
- ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
-  "(EX x. P & Q x)   = (P & (EX x. Q x))",
-  "(EX x. P x | Q)   = ((EX x. P x) | Q)",
-  "(EX x. P | Q x)   = (P | (EX x. Q x))",
-  "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
-  "(EX x. P --> Q x) = (P --> (EX x. Q x))"]);
-
-(*Miniscoping: pushing in universal quantifiers*)
-bind_thms ("all_simps", map prover
- ["(ALL x. P x & Q)   = ((ALL x. P x) & Q)",
-  "(ALL x. P & Q x)   = (P & (ALL x. Q x))",
-  "(ALL x. P x | Q)   = ((ALL x. P x) | Q)",
-  "(ALL x. P | Q x)   = (P | (ALL x. Q x))",
-  "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
-  "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]);
-
-
-fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
-
-prove "eq_commute" "(a=b) = (b=a)";
-prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))";
-prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))";
-bind_thms ("eq_ac", [eq_commute, eq_left_commute, eq_assoc]);
-
-prove "neq_commute" "(a~=b) = (b~=a)";
-
-prove "conj_commute" "(P&Q) = (Q&P)";
-prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
-bind_thms ("conj_comms", [conj_commute, conj_left_commute]);
-prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))";
-
-prove "disj_commute" "(P|Q) = (Q|P)";
-prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))";
-bind_thms ("disj_comms", [disj_commute, disj_left_commute]);
-prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))";
-
-prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
-prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";
-
-prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))";
-prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))";
-
-prove "imp_conjR" "(P --> (Q&R)) = ((P-->Q) & (P-->R))";
-prove "imp_conjL" "((P&Q) -->R)  = (P --> (Q --> R))";
-prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))";
-
-(*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*)
-prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)";
-prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)";
-
-prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
-prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";
+(* legacy ML bindings *)
 
-prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
-prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
-prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
-prove "not_iff" "(P~=Q) = (P = (~Q))";
-prove "disj_not1" "(~P | Q) = (P --> Q)";
-prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
-prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)";
-
-prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))";
-
-
-(*Avoids duplication of subgoals after split_if, when the true and false
-  cases boil down to the same thing.*)
-prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
-
-prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))";
-prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)";
-prove "not_ex"  "(~ (? x. P(x))) = (! x.~P(x))";
-prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)";
-
-prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
-prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
-
-(* '&' congruence rule: not included by default!
-   May slow rewrite proofs down by as much as 50% *)
-
-let val th = prove_goal (the_context ())
-                "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
-                (fn _=> [(Blast_tac 1)])
-in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
-
-let val th = prove_goal (the_context ())
-                "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
-                (fn _=> [(Blast_tac 1)])
-in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
-
-(* '|' congruence rule: not included by default! *)
-
-let val th = prove_goal (the_context ())
-                "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
-                (fn _=> [(Blast_tac 1)])
-in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
-
-prove "eq_sym_conv" "(x=y) = (y=x)";
-
-
-(** if-then-else rules **)
+val Eq_FalseI = thm "Eq_FalseI";
+val Eq_TrueI = thm "Eq_TrueI";
+val all_conj_distrib = thm "all_conj_distrib";
+val all_simps = thms "all_simps";
+val cases_simp = thm "cases_simp";
+val conj_assoc = thm "conj_assoc";
+val conj_comms = thms "conj_comms";
+val conj_commute = thm "conj_commute";
+val conj_cong = thm "conj_cong";
+val conj_disj_distribL = thm "conj_disj_distribL";
+val conj_disj_distribR = thm "conj_disj_distribR";
+val conj_left_commute = thm "conj_left_commute";
+val de_Morgan_conj = thm "de_Morgan_conj";
+val de_Morgan_disj = thm "de_Morgan_disj";
+val disj_assoc = thm "disj_assoc";
+val disj_comms = thms "disj_comms";
+val disj_commute = thm "disj_commute";
+val disj_cong = thm "disj_cong";
+val disj_conj_distribL = thm "disj_conj_distribL";
+val disj_conj_distribR = thm "disj_conj_distribR";
+val disj_left_commute = thm "disj_left_commute";
+val disj_not1 = thm "disj_not1";
+val disj_not2 = thm "disj_not2";
+val eq_ac = thms "eq_ac";
+val eq_assoc = thm "eq_assoc";
+val eq_commute = thm "eq_commute";
+val eq_left_commute = thm "eq_left_commute";
+val eq_sym_conv = thm "eq_sym_conv";
+val eta_contract_eq = thm "eta_contract_eq";
+val ex_disj_distrib = thm "ex_disj_distrib";
+val ex_simps = thms "ex_simps";
+val if_False = thm "if_False";
+val if_P = thm "if_P";
+val if_True = thm "if_True";
+val if_bool_eq_conj = thm "if_bool_eq_conj";
+val if_bool_eq_disj = thm "if_bool_eq_disj";
+val if_cancel = thm "if_cancel";
+val if_def2 = thm "if_def2";
+val if_eq_cancel = thm "if_eq_cancel";
+val if_not_P = thm "if_not_P";
+val if_splits = thms "if_splits";
+val iff_conv_conj_imp = thm "iff_conv_conj_imp";
+val imp_all = thm "imp_all";
+val imp_cong = thm "imp_cong";
+val imp_conjL = thm "imp_conjL";
+val imp_conjR = thm "imp_conjR";
+val imp_conv_disj = thm "imp_conv_disj";
+val imp_disj1 = thm "imp_disj1";
+val imp_disj2 = thm "imp_disj2";
+val imp_disjL = thm "imp_disjL";
+val imp_disj_not1 = thm "imp_disj_not1";
+val imp_disj_not2 = thm "imp_disj_not2";
+val imp_ex = thm "imp_ex";
+val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
+val neq_commute = thm "neq_commute";
+val not_all = thm "not_all";
+val not_ex = thm "not_ex";
+val not_iff = thm "not_iff";
+val not_imp = thm "not_imp";
+val not_not = thm "not_not";
+val rev_conj_cong = thm "rev_conj_cong";
+val simp_thms = thms "simp_thms";
+val split_if = thm "split_if";
+val split_if_asm = thm "split_if_asm";
 
-Goalw [if_def] "(if True then x else y) = x";
-by (Blast_tac 1);
-qed "if_True";
-
-Goalw [if_def] "(if False then x else y) = y";
-by (Blast_tac 1);
-qed "if_False";
-
-Goalw [if_def] "P ==> (if P then x else y) = x";
-by (Blast_tac 1);
-qed "if_P";
-
-Goalw [if_def] "~P ==> (if P then x else y) = y";
-by (Blast_tac 1);
-qed "if_not_P";
-
-Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))";
-by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1);
-by (stac if_P 2);
-by (stac if_not_P 1);
-by (ALLGOALS (Blast_tac));
-qed "split_if";
-
-Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))";
-by (stac split_if 1);
-by (Blast_tac 1);
-qed "split_if_asm";
-
-bind_thms ("if_splits", [split_if, split_if_asm]);
-
-bind_thm ("if_def2", read_instantiate [("P","\\<lambda>x. x")] split_if);
-
-Goal "(if c then x else x) = x";
-by (stac split_if 1);
-by (Blast_tac 1);
-qed "if_cancel";
-
-Goal "(if x = y then y else x) = x";
-by (stac split_if 1);
-by (Blast_tac 1);
-qed "if_eq_cancel";
-
-(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
-Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))";
-by (rtac split_if 1);
-qed "if_bool_eq_conj";
-
-(*And this form is useful for expanding IFs on the LEFT*)
-Goal "(if P then Q else R) = ((P&Q) | (~P&R))";
-by (stac split_if 1);
-by (Blast_tac 1);
-qed "if_bool_eq_disj";
 
 local
 val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
@@ -264,9 +131,6 @@
 fun mk_meta_eq r = r RS eq_reflection;
 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
 
-bind_thm ("Eq_TrueI", mk_meta_eq (prover  "P --> (P = True)"  RS mp));
-bind_thm ("Eq_FalseI", mk_meta_eq(prover "~P --> (P = False)" RS mp));
-
 fun mk_eq th = case concl_of th of
         Const("==",_)$_$_       => th
     |   _$(Const("op =",_)$_$_) => mk_meta_eq th