Isabelle proving with translation issue

Question

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?

It would be easier if your example would type or if you could give the imports you are using… What does the arrow in sig mean? — Mathias Fleury
Some suggestions: i) check with supply [[show_types]] that the types are really the same; ii) check with supply [[unify_trace_failure]] apply assumption why no unification happens; iii) check with supply [[show_sorts]] that the sorts are really the same — Mathias Fleury
The imports are: imports Nlist IntExt Hilbert ZF.Univ, where Nlist IntExt Hilbert are written on my own, but all of them does not have any definition related to time or time -> A, they only contains theorem about int, the arrow means that it is a function from time (in here it is int) to set A. I would have a look on the supply command, thank you very much. — kaiboy05
The problem is that the translation does not work for some reason... — Mathias Fleury

Mathias Fleury Mathias Fleury · Accepted Answer · 2020-08-04T17:12:03

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.

Isabelle proving with translation issue

1 Answers