2949 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2949 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2950 by (simp_all add: fresh_at_base) |
2950 by (simp_all add: fresh_at_base) |
2951 |
2951 |
2952 |
2952 |
2953 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2953 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2954 case term_of ctrm of @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => |
2954 case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) => |
2955 let |
2955 let |
2956 |
2956 |
2957 fun first_is_neg lhs rhs [] = NONE |
2957 fun first_is_neg lhs rhs [] = NONE |
2958 | first_is_neg lhs rhs (thm::thms) = |
2958 | first_is_neg lhs rhs (thm::thms) = |
2959 (case Thm.prop_of thm of |
2959 (case Thm.prop_of thm of |
2960 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2960 _ $ (@{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ l $ r)) => |
2961 (if l = lhs andalso r = rhs then SOME(thm) |
2961 (if l = lhs andalso r = rhs then SOME(thm) |
2962 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2962 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2963 else first_is_neg lhs rhs thms) |
2963 else first_is_neg lhs rhs thms) |
2964 | _ => first_is_neg lhs rhs thms) |
2964 | _ => first_is_neg lhs rhs thms) |
2965 |
2965 |