src/HOL/HOL.thy
changeset 31173 bbe9e29b9672
parent 31172 74d72ba262fb
parent 31166 a90fe83f58ea
child 31299 0c5baf034d0e
equal deleted inserted replaced
31172:74d72ba262fb 31173:bbe9e29b9672
  1048     "(P & ~P) = False"    "(~P & P) = False"
  1048     "(P & ~P) = False"    "(~P & P) = False"
  1049     "(P | True) = True"  "(True | P) = True"
  1049     "(P | True) = True"  "(True | P) = True"
  1050     "(P | False) = P"  "(False | P) = P"
  1050     "(P | False) = P"  "(False | P) = P"
  1051     "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and
  1051     "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and
  1052     "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
  1052     "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
  1053     -- {* needed for the one-point-rule quantifier simplification procs *}
  1053   and
  1054     -- {* essential for termination!! *} and
       
  1055     "!!P. (EX x. x=t & P(x)) = P(t)"
  1054     "!!P. (EX x. x=t & P(x)) = P(t)"
  1056     "!!P. (EX x. t=x & P(x)) = P(t)"
  1055     "!!P. (EX x. t=x & P(x)) = P(t)"
  1057     "!!P. (ALL x. x=t --> P(x)) = P(t)"
  1056     "!!P. (ALL x. x=t --> P(x)) = P(t)"
  1058     "!!P. (ALL x. t=x --> P(x)) = P(t)"
  1057     "!!P. (ALL x. t=x --> P(x)) = P(t)"
  1059   by (blast, blast, blast, blast, blast, iprover+)
  1058   by (blast, blast, blast, blast, blast, iprover+)