src/HOL/simpdata.ML
changeset 3913 96e28b16861c
parent 3904 c0d56e4c823e
child 3919 c036caebfc75
equal deleted inserted replaced
3912:4ed64ad7fb42 3913:96e28b16861c
   101    "(P --> True) = True", "(P --> P) = True",
   101    "(P --> True) = True", "(P --> P) = True",
   102    "(P --> False) = (~P)", "(P --> ~P) = (~P)",
   102    "(P --> False) = (~P)", "(P --> ~P) = (~P)",
   103    "(P & True) = P", "(True & P) = P", 
   103    "(P & True) = P", "(True & P) = P", 
   104    "(P & False) = False", "(False & P) = False",
   104    "(P & False) = False", "(False & P) = False",
   105    "(P & P) = P", "(P & (P & Q)) = (P & Q)",
   105    "(P & P) = P", "(P & (P & Q)) = (P & Q)",
       
   106    "(P & ~P) = False",    "(~P & P) = False",
   106    "(P | True) = True", "(True | P) = True", 
   107    "(P | True) = True", "(True | P) = True", 
   107    "(P | False) = P", "(False | P) = P",
   108    "(P | False) = P", "(False | P) = P",
   108    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
   109    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
       
   110    "(P | ~P) = True",    "(~P | P) = True",
   109    "((~P) = (~Q)) = (P=Q)",
   111    "((~P) = (~Q)) = (P=Q)",
   110    "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", 
   112    "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", 
   111    "(? x. x=t & P(x)) = P(t)",
   113    "(? x. x=t & P(x)) = P(t)",
   112    "(! x. t=x --> P(x)) = P(t)" ];
   114    "(! x. t=x --> P(x)) = P(t)" ];
   113 
   115 
   309          REPEAT(blast_tac HOL_cs 1) ]);
   311          REPEAT(blast_tac HOL_cs 1) ]);
   310 
   312 
   311 qed_goal "if_bool_eq" HOL.thy
   313 qed_goal "if_bool_eq" HOL.thy
   312                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   314                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   313                    (fn _ => [rtac expand_if 1]);
   315                    (fn _ => [rtac expand_if 1]);
       
   316 
       
   317 
       
   318 
       
   319 (** Case splitting **)
   314 
   320 
   315 local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
   321 local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
   316 in
   322 in
   317 fun split_tac splits = mktac (map mk_meta_eq splits)
   323 fun split_tac splits = mktac (map mk_meta_eq splits)
   318 end;
   324 end;