Maximilian Vollath (Dec 18 2024 at 10:07): Maximilian Vollath (Dec 18 2024 at 10:07):In my project, I often come across lemmas such as this one:
lemma my_lemma: "P (PredDecl p args) ⟷ Q p ∧ R p args"
PredDecl only has one constructor:
datatype predicate_decl = PredDecl
(pred: predicate)
(argTs: "type list")
And I want to easily manipulatel such lemmas into this equivalent form:
"P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
How do I go about this? And is there also a way to do this in the other direction?
Mathias Fleury (Dec 18 2024 at 12:35):what is the question exactly?
Mathias Fleury (Dec 18 2024 at 12:35):Proving the equivalent from is pretty much trivial:
lemma my_lemma': "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
by (cases pd) (rule my_lemma)
So you could use the alternative version
Maximilian Schäffeler (Dec 18 2024 at 14:16):You could do something like this:
lemmas my_lemma' = my_lemma[where p = ‹pred pd› and args = ‹argTs pd› for pd, unfolded predicate_decl.collapse]
lemmas my_lemma'' = my_lemma'[where pd = ‹PredDecl p args› for p args, unfolded predicate_decl.sel]
There may be much simpler solutions to achieve this, though I don't know how to do better.
Maximilian Vollath (Dec 18 2024 at 17:01):Thank you, that's still a little bit tedious but very useful!
David Wang (Dec 18 2024 at 19:49):Maybe this?
datatype predicate_decl = PredDecl
(pred: predicate)
(argTs: "type list")
lemma pred1: assumes "⋀p args. P (PredDecl p args) ⟷ Q p ∧ R p args"
shows "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
using assms [[simp_trace]] by (cases pd) simp
lemma pred2: assumes "⋀pd. P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
shows "P (PredDecl p args) ⟷ Q p ∧ R p args"
using assms [[simp_trace]] by simp
lemma my_lemma: "P (PredDecl p args) ⟷ Q p ∧ R p args"
apply (rule pred1)
sorry
lemma my_lemma': "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
apply (rule pred2)
sorry
I don't know how to make Isabelle favour these when using apply rule. I find this interesting as well.
Kevin Kappelmann (Dec 18 2024 at 20:14):If you use the AFP, you can use Unification Hints:
theory Scratch
imports
Main
ML_Unification.ML_Unification_HOL_Setup
ML_Unification.Unify_Resolve_Tactics
begin
datatype predicate_decl = PredDecl
(pred: nat)
(argTs: int)
consts P :: "predicate_decl ⇒ bool"
consts Q :: "nat ⇒ bool"
consts R :: "nat ⇒ int ⇒ bool"
lemma my_lemma: "P (PredDecl p args) ⟷ Q p ∧ R p args"
sorry
lemma "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
(*quick and dirty*)
supply predicate_decl.collapse[uhint]
by (urule my_lemma)
(* clean version with proper setup *)
lemma PredDecl_eta_uhint[uhint]: "pd = pd' ⟹ PredDecl (pred pd) (argTs pd) = pd'"
by simp
lemma "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
by (urule my_lemma)
Since I didn't clarify that enough, I am not looking for a solution where I have to redefine the lemma manually, but rather an in-line solution that lets me use the transformed variant of these lemmas in proofs.
Your solution seems great, actually, since apply (urule ...) probably does a lot of what I want. I'll look into it once I get it to run. Thank you!
Maximilian Schäffeler (Dec 19 2024 at 10:18):In this case, the rule method also works:
lemma "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
by (rule my_lemma)
Maximilian Schäffeler said:
In this case, the
rulemethod also works:lemma "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)" by (rule my_lemma)
You probably got tricked: If P, Q, R are some fixed constants (which they should be; otherwise my_lemma is unprovable), it doesn't work. If they are free variables, it works due to higher-order unification.
datatype predicate_decl = PredDecl
(pred: nat)
(argTs: int)
lemma my_lemma: "P (PredDecl p args) ⟷ Q p ∧ R p args"
sorry
lemma "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
apply (rule my_lemma)
done
consts P :: "predicate_decl ⇒ bool"
consts Q :: "nat ⇒ bool"
consts R :: "nat ⇒ int ⇒ bool"
lemma my_lemma2: "P (PredDecl p args) ⟷ Q p ∧ R p args"
sorry
lemma "P pd ⟷ Q (pred pd) ∧ R (pred pd) (argTs pd)"
apply (rule my_lemma2)
oops
You are completely right :D
Last updated: Dec 21 2024 at 16:20 UTC