Isabelle proving with translation issue

I had defined a few translations like this:

consts
  "time" :: "i"
  "sig" :: "i ⇒ i"
  "BaseChTy" :: "i"

syntax
  "time" :: "i"
  "sig" :: "i ⇒ i"
translations
  "time" ⇌ "CONST int"
  "sig(A)" ⇌ "CONST int → A"

Then, I want to prove a theorem like this:

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"

It should be a very simple theorem, and should be proved with theorem Pi_mono in a single step:

thm Pi_mono
?B ⊆ ?C ⟹ ?A → ?B ⊆ ?A → ?C

So I did it like this:

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"

apply(drule Pi_mono[of _ _ "time"])
(*Output:
goal (1 subgoal):
 1. sig(A) ⊆ sig(B) ⟹ sig(A) ⊆ sig(B)
*)

apply(simp)
(*Output:
Failed ...
*)

Since the premise has become the same as the goal, it should be proved immediately, but it didn't. May I know have I done anything wrong in the translation definition? I tried to change the theorem to:

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ (time → A) ⊆ (time → B)"
(*Output:
goal (1 subgoal):
 1. A ⊆ B ⟹ sig(A) ⊆ sig(B)
*)

apply(drule Pi_mono[of _ _ "time"])
(*Output:
goal (1 subgoal):
 1. sig(A) ⊆ sig(B) ⟹ sig(A) ⊆ sig(B)
*)

apply(simp)
(*Output:
Success ...
*)

Then it works immediately, but shouldn't the translation will make them to be the same thing?

Update: Thanks for Mathias Fleury reply, I tried to do a simplify trace, and it shows something like this:

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"
using [[show_sorts]] apply(drule Pi_mono[of _ _ "time"])
using [[simp_trace]] apply(simp)
oops

(*
Output:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
sig(A::i) ⊆ sig(B::i) ⟹ sig(A) ⊆ sig(B) 
[1]Adding rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
*)

while the time -> A version shows:

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ time → A ⊆ time → B"
using [[show_sorts]] apply(drule Pi_mono[of _ _ "time"])
using [[simp_trace]] apply(simp)
oops

(*
Output:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
sig(A::i) ⊆ sig(B::i) ⟹ sig(A) ⊆ sig(B) 
[1]Adding rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
[1]Applying instance of rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
[1]Rewriting:
sig(A::i) ⊆ sig(B::i) ≡ True
*)

Why can this time version can apply the instance of rewrite rule to continue to the proof, but the original one does not?

Solution

Thanks to the imports you mentioned in you comment (thanks), I could reproduce the problem. The issue is the translation, you need to do something like

syntax
  "sig" :: "i ⇒ i" (‹sig(_)›)
translations
  "sig(A)" == "CONST int → A"

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"
  apply(rule Pi_mono)
  apply assumption
  done

Just to expand on my comment and explain how I found that the problem is the translation. I looked at the unification failure:

theorem ⟦ A ⊆ B ⟧ ⟹ time → A ⊆ time → B
  supply[[unify_trace_failure]]
   apply (rule PI_mono)

The error message tells that sig and Pi are not unifiable. This is already strange. To be certain that the problem comes from the translation, I looked at the underlying term:

ML ‹@{print}@{term ‹sig(A)›}›

It shows the underlying term and we can see that the translation is not working and I looked at other translations in the library to fix issue.