src/HOL/simpdata.ML
changeset 2097 076a8d2f972b
parent 2082 8659e3063a30
child 2098 2bfc0675c92f
equal deleted inserted replaced
2096:76ea62f720f1 2097:076a8d2f972b
   178 
   178 
   179 val imp_cong = impI RSN
   179 val imp_cong = impI RSN
   180     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   180     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   181         (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
   181         (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
   182 
   182 
   183 val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
   183 val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
   184  (fn _ => [rtac refl 1]);
   184  (fn _ => [rtac refl 1]);
   185 
   185 
   186 (*Miniscoping: pushing in existential quantifiers*)
   186 (*Miniscoping: pushing in existential quantifiers*)
   187 val ex_simps = map prover 
   187 val ex_simps = map prover 
   188                 ["(EX x. P x & Q)   = ((EX x.P x) & Q)",
   188                 ["(EX x. P x & Q)   = ((EX x.P x) & Q)",
   323 
   323 
   324 qed_goal "if_distrib" HOL.thy
   324 qed_goal "if_distrib" HOL.thy
   325   "f(if c then x else y) = (if c then f x else f y)" 
   325   "f(if c then x else y) = (if c then f x else f y)" 
   326   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
   326   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
   327 
   327 
   328 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = (f o g o h)"
   328 bind_thm ("o_apply", o_apply);
       
   329 
       
   330 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
   329   (fn _=>[rtac ext 1, rtac refl 1]);
   331   (fn _=>[rtac ext 1, rtac refl 1]);
   330 
   332 
   331 
   333 
   332 
   334 
   333 
   335