src/HOL/HOL.thy
changeset 15481 fc075ae929e4
parent 15423 761a4f8e6ad6
child 15524 2ef571f80a55
     1.1 --- a/src/HOL/HOL.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -8,6 +8,8 @@
     1.4  theory HOL
     1.5  imports CPure
     1.6  files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("antisym_setup.ML")
     1.7 +      ("eqrule_HOL_data.ML")
     1.8 +      ("~~/src/Provers/eqsubst.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Primitive logic *}
    1.12 @@ -898,7 +900,7 @@
    1.13  setup Blast.setup
    1.14  
    1.15  
    1.16 -subsubsection {* Simplifier setup *}
    1.17 +subsection {* Simplifier setup *}
    1.18  
    1.19  lemma meta_eq_to_obj_eq: "x == y ==> x = y"
    1.20  proof -
    1.21 @@ -1068,12 +1070,12 @@
    1.22  
    1.23  lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
    1.24    apply (rule case_split [of Q])
    1.25 -   apply (subst if_P)
    1.26 -    prefer 3 apply (subst if_not_P, blast+)
    1.27 +   apply (simplesubst if_P)
    1.28 +    prefer 3 apply (simplesubst if_not_P, blast+)
    1.29    done
    1.30  
    1.31  lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
    1.32 -by (subst split_if, blast)
    1.33 +by (simplesubst split_if, blast)
    1.34  
    1.35  lemmas if_splits = split_if split_if_asm
    1.36  
    1.37 @@ -1081,10 +1083,10 @@
    1.38    by (rule split_if)
    1.39  
    1.40  lemma if_cancel: "(if c then x else x) = x"
    1.41 -by (subst split_if, blast)
    1.42 +by (simplesubst split_if, blast)
    1.43  
    1.44  lemma if_eq_cancel: "(if x = y then y else x) = x"
    1.45 -by (subst split_if, blast)
    1.46 +by (simplesubst split_if, blast)
    1.47  
    1.48  lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.49    -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
    1.50 @@ -1092,7 +1094,7 @@
    1.51  
    1.52  lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
    1.53    -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
    1.54 -  apply (subst split_if, blast)
    1.55 +  apply (simplesubst split_if, blast)
    1.56    done
    1.57  
    1.58  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
    1.59 @@ -1113,11 +1115,23 @@
    1.60  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    1.61  setup Splitter.setup setup Clasimp.setup
    1.62  
    1.63 +
    1.64 +subsubsection {* Lucas Dixon's eqstep tactic *}
    1.65 +
    1.66 +use "~~/src/Provers/eqsubst.ML";
    1.67 +use "eqrule_HOL_data.ML";
    1.68 +
    1.69 +setup EQSubstTac.setup
    1.70 +
    1.71 +
    1.72 +subsection {* Other simple lemmas *}
    1.73 +
    1.74  declare disj_absorb [simp] conj_absorb [simp]
    1.75  
    1.76  lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
    1.77  by blast+
    1.78  
    1.79 +
    1.80  theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
    1.81    apply (rule iffI)
    1.82    apply (rule_tac a = "%x. THE y. P x y" in ex1I)
    1.83 @@ -1142,7 +1156,7 @@
    1.84  by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]])
    1.85  
    1.86  
    1.87 -subsubsection {* Generic cases and induction *}
    1.88 +subsection {* Generic cases and induction *}
    1.89  
    1.90  constdefs
    1.91    induct_forall :: "('a => bool) => bool"