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"
```