Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle] Isabelle proving theorem with trans...


view this post on Zulip Email Gateway (Aug 05 2020 at 09:43):

From: "Wong, Yat" <yat.wong18@imperial.ac.uk>
Hi everyone,

I met some problems when I was trying to prove my theorems with my defined translation.


My theory imports theory with:

imports Nlist IntExt Hilbert ZF.Univ
(* Nlist, IntExt, Hilbert are defined on my own, they only contain theorems related to int *)

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?


Thanks for Mathias Fleury’s reply from stack overflow, 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?

Thank you very much,

Best regards,
Chester


Last updated: Jul 15 2022 at 23:21 UTC