CODEWITHSUNDEEP
isabelle
Mathieu
Mathieu

Reputation: 746

How to use single-valued relations to rewrite a goal automatically?

Single valued relations (as defined by single_valued in the Relation theory) allow to deduce equalities from membership relations. I was wondering if there was a way to take advantage of this to rewrite terms in the goal (and then merge these membership relations).

As an example, here is a goal that cannot be solved by auto or force without auxiliary theorems:

lemma
  assumes "single_valued A"
  assumes "(a,b) ∈ A" and "(a,b') ∈ A"
  shows "b = b'"
using assms
by (metis single_valued_def)

Here the equality is directly in the goal, but it would be great to also rewrite in the assumptions.

Also, I talk here about sets of pairs but I have a more complex application with another kind of relation with a similar property, where such kind of assumptions are common, and I am then looking for a way to simplify them.

It seems to me that automatic methods could greatly benefit from such a feature.

I have already written some simprocs before and it seems to me we could use them here if we could access the set of assumptions once the simproc has been triggered on, which I don't know if this is possible. For example, once "(a,b) ∈ A" has triggered the simproc, could we check if any assumption contains "(a,_) ∈ A" ? But it would perhaps be too costly...

Any idea ?

Upvotes: 2

Views: 99

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

Here is a simproc that does what you want:

lemma single_valuedD_eq:
  "⟦ single_valued A; (x, a) ∈ A ⟧ ⟹ (x, b) ∈ A ⟷ b = a"
by(auto dest: single_valuedD)

simproc_setup single_valued ("(x, y) ∈ A") = {*
  (fn phi => fn ctxt => fn redex => case term_of redex of
    Const (@{const_name "Set.member"},
         Type (@{type_name fun},
           [Txy as Type (@{type_name prod}, [Tx, Ty]),
            Type (@{type_name fun}, [TA, _])])) $
      (Const (@{const_name "Pair"}, _) $ tx $ ty) $
      tA =>
    let
      val thy = Proof_Context.theory_of ctxt;
      val prems = Simplifier.prems_of ctxt;

      fun mk_stmt t = t |> HOLogic.mk_Trueprop |> Thm.cterm_of thy |> Goal.init
      fun mk_thm tac t =
        case SINGLE (tac 1) (mk_stmt t) of
          SOME thm => SOME (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_thm thm)) thm)
        | NONE => NONE;

      val svA = Const (@{const_name single_valued}, TA --> @{typ bool}) $ tA
      val [z] = Name.invent (Variable.names_of ctxt) "z" 1
      val xzA = 
        Const (@{const_name Set.member}, Txy --> TA --> @{typ bool})
        $ (Const (@{const_name Pair}, Tx --> Ty --> Txy)
           $ tx $ Var ((z, 0), Ty))
        $ tA
    in
      case mk_thm (resolve_tac prems) svA of NONE => NONE
      | SOME thm_svA => case mk_thm (resolve_tac prems) xzA of NONE => NONE
        | SOME thm_xzA => 
          SOME (@{thm single_valuedD_eq[THEN eq_reflection]} OF [thm_svA, thm_xzA])
    end
  | _ => NONE)
*}

When it triggers on a term of the pattern (_, _) ∈ _, say (x, y) ∈ A, it checks whether there are assumptions single_valued A and (x, ?z) ∈ A in the current goal. If so, it instantiates the theorem single_valuedD_eq with them and rewrites (x, y) ∈ A to y = ?z with ?z being appropriate instantiated.

Here is an example:

lemma
  "⟦ single_valued A; (x, b) ∈ A; (x, c) ∈ A ⟧
  ⟹ map (λy. (x, y) ∈ A) xs = foo"
apply simp

  NEW GOAL:
  1. ⟦single_valued A; b = c; (x, c) ∈ A⟧ ⟹ map (λy. y = c) xs = foo

Note that single_valued A has to be an assumption of the goal. It does not suffice to have single_valued A as a [simp] rule somewhere. This is because the assumptions are looked up with resolve_tac prems rather than a full simplifier invocation.

Upvotes: 3

Related Questions