src/HOL/HOL.thy
 changeset 14201 7ad7ab89c402 parent 13764 3e180bf68496 child 14208 144f45277d5a
equal inserted replaced
`   378   "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"`
`   378   "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"`
`   379   "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"`
`   379   "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"`
`   380   -- {* Miniscoping: pushing in universal quantifiers. *}`
`   380   -- {* Miniscoping: pushing in universal quantifiers. *}`
`   381   by (rules | blast)+`
`   381   by (rules | blast)+`
`   382 `
`   382 `
`       `
`   383 lemma disj_absorb: "(A | A) = A"`
`       `
`   384   by blast`
`       `
`   385 `
`       `
`   386 lemma disj_left_absorb: "(A | (A | B)) = (A | B)"`
`       `
`   387   by blast`
`       `
`   388 `
`       `
`   389 lemma conj_absorb: "(A & A) = A"`
`       `
`   390   by blast`
`       `
`   391 `
`       `
`   392 lemma conj_left_absorb: "(A & (A & B)) = (A & B)"`
`       `
`   393   by blast`
`       `
`   394 `
`   383 lemma eq_ac:`
`   395 lemma eq_ac:`
`   384   shows eq_commute: "(a=b) = (b=a)"`
`   396   shows eq_commute: "(a=b) = (b=a)"`
`   385     and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"`
`   397     and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"`
`   386     and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)`
`   398     and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)`
`   387 lemma neq_commute: "(a~=b) = (b~=a)" by rules`
`   399 lemma neq_commute: "(a~=b) = (b~=a)" by rules`
`   512   done`
`   524   done`
`   513 `
`   525 `
`   514 lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules`
`   526 lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules`
`   515 lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules`
`   527 lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules`
`   516 `
`   528 `
`       `
`   529 subsubsection {* Actual Installation of the Simplifier *}`
`       `
`   530 `
`   517 use "simpdata.ML"`
`   531 use "simpdata.ML"`
`   518 setup Simplifier.setup`
`   532 setup Simplifier.setup`
`   519 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup`
`   533 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup`
`   520 setup Splitter.setup setup Clasimp.setup`
`   534 setup Splitter.setup setup Clasimp.setup`
`       `
`   535 `
`       `
`   536 declare disj_absorb [simp] conj_absorb [simp] `
`   521 `
`   537 `
`   522 lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"`
`   538 lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"`
`   523 by blast+`
`   539 by blast+`
`   524 `
`   540 `
`   525 theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"`
`   541 theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"`