Stream: Beginner Questions

Topic: ✔ Intro rule seems to be ignored?

Bob Rubbens (Aug 07 2026 at 10:18):

Hi everyone,

Why is my intro rule not used automatically here? Is there some technicality with subset_eq? Or am I expecting too much and is there some kind of blind spot in the intro rule automation? Here's a repro file:

(The definitions in the original development are more involved, and the sorries are proved there, so I don't think it's because of a false assumption...)

theory Test
  imports Main
begin

type_synonym pname = nat
type_synonym simple_proc = nat
type_synonym simple_net = "pname ⇒ simple_proc"

definition atomic :: "pname ⇒ simple_proc ⇒ simple_net" where
"atomic p P q = (if p = q then P else 0)"

definition par :: "simple_net ⇒ simple_net ⇒ simple_net" where
"par p q = p" (* bogus definition *)

lemma supp_par [simp]:
"supp (par N M) = supp N ∪ supp M"
  sorry

(* This is the intro rule I'm interested in *)
lemma supp_atomic_subsetI [intro]:
‹p ∈ S ⟹ supp (atomic p P) ⊆ S›
  sorry

lemma ex1:
  shows "supp (par (atomic p P) (atomic q Q)) ⊆ {p, q}"
(* can do it manually: *)
  apply(simp)
  apply(rule conjI)
   apply(intro supp_atomic_subsetI)
   apply(simp)
    (* But would expect something like auto to do it. *)
    (* Force including the lemma also works: *)
    (*  using supp_atomic_subsetI by blast *)

end

Bob Rubbens (Aug 07 2026 at 10:40):

The problem seems to have been related to one of my simp rules. I replaced:

lemma supp_atomic_simps [simp]:
"is_term P ==> supp (p⟨P⟩) = {}"
"~is_term P ==> supp (p⟨P⟩) = {p}"

With:

lemma supp_atomic_simps [simp]:
"supp (p⟨P⟩) = (if is_term P then {} else {p})"

Apparently with the former formulation Isabelle doesn't case split on the assumption, whereas if is_term P occurs as part of an if the simplifier does case split. This extra knowledge allows the simplification to proceed.

Notification Bot (Aug 07 2026 at 10:40):

Bob Rubbens has marked this topic as resolved.

Mathias Fleury (Aug 10 2026 at 20:08):

simp does not use intro rules

Mathias Fleury (Aug 10 2026 at 20:08):

you need auto for that

Ant S. (Aug 10 2026 at 20:10):

Mathias Fleury said:

simp does not use intro rules

why is this the case?

Mathias Fleury (Aug 10 2026 at 20:22):

The simplifier is only using rewriting (and splitting rules, which are still only rewriting).

Mathias Fleury (Aug 10 2026 at 20:23):

The idea is that the simplifier is safe to use (this is also why the rules are supposed to be confluent), while intro/dest/elim rules are not safe

Mathias Fleury (Aug 10 2026 at 20:25):

Once you start adding intro/dest/elim rules you need limits in the search (I loosely remember auto using 4 intro rules and 2 dest/elim rules or something along that lines. If you need 5 intro rules, auto will not prove the goal). In contract force and fastforce are not limited but they can run forever

Mathias Fleury (Aug 10 2026 at 20:25):

Normally simp does not run forever

Last updated: Aug 11 2026 at 20:46 UTC