CODEWITHSUNDEEP
isabelle
kaiboy05
kaiboy05

Reputation: 47

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?

Upvotes: 1

Views: 82

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

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.

Upvotes: 2

Related Questions