What does "Rule has fewer conclusions than the arguments given" mean exactly? I am trying to mutually induct over a inductive, but somehow I am messing up. I even tried explicity instanciating the goals:
lemma fresh_in_context_term_var: assumes "atom (x::var) ♯ Γ" shows "Γ , Δ ⊢ e : τ ⟶ atom x ♯ e" and "Alts Γ Δ T σs τ1 alts τ ⟶ atom x ♯ alts" using assms proof (induction Γ Δ e τ and Γ Δ T σs τ1 alts τ rule: Tm_Alts.induct[of "λ_ _ e _. atom x ♯ e" "λ_ _ _ _ _ alts _. atom x ♯ alts"])
If possible, please post a full example (including all the relevant definitions, or at least dummies for the constants/notation used) so that people can try it out themselves.
In any case, I think instantiating the induction rule manually like this is only going to confuse the
induction method. If you want to instantiate stuff by hand for debugging purposes, you can try applying the induction rule manually with e.g.
I tried it first without instantiating, but with the same error. I pushed the code and this is the lemma: https://github.com/jvanbruegge/isabelle-lambda-calculus/blob/case-expressions/Typing.thy#L214
It works if I use
proof (rule Tm_Alts.induct, goal_cases), but why not with the induction method?
lemma fresh_in_context_term_var: assumes "atom (x::var) ♯ Γ" shows "Γ , Δ ⊢ e : τ ⟹ atom x ♯ e" and "Alts Γ Δ T σs τ1 alts τ ⟹ atom x ♯ alts" proof - have "(Γ , Δ ⊢ e : τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ e)) ∧ (Alts Γ Δ T σs τ1 alts τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ alts))" proof (rule Tm_Alts.induct, goal_cases) (* ... *) qed then show "Γ , Δ ⊢ e : τ ⟹ atom x ♯ e" and "Alts Γ Δ T σs τ1 alts τ ⟹ atom x ♯ alts" using assms by auto qed
the induction tactic might be having a problem with a goal shaped
shows X and Y
no, it works for other lemmas: https://github.com/jvanbruegge/isabelle-lambda-calculus/blob/case-expressions/Lemmas.thy#L178
do the induction rules in question have the right number of conclusions?
yes, it looks like this:
(?x1.0 , ?x2.0 ⊢ ?x3.0 : ?x4.0 ⟶ ?P1.0 ?x1.0 ?x2.0 ?x3.0 ?x4.0) ∧ (Alts ?x5.0 ?x6.0 ?x7.0 ?x8.0 ?x9.0 ?x10.0 ?x11.0 ⟶ ?P2.0 ?x5.0 ?x6.0 ?x7.0 ?x8.0 ?x9.0 ?x10.0 ?x11.0)
The problem is the
ok, this works, but as soon as I try to add
using assms proof it fails again with "Failed to apply initial proof method"
lemma fresh_in_context_term_var: assumes "atom (x::var) ♯ Γ" shows "(Γ , Δ ⊢ e : τ ⟶ atom x ♯ e) ∧ (Alts Γ Δ T σs τ1 alts τ ⟶ atom x ♯ alts)" proof (induction rule: Tm_Alts.induct)
Because the induction rule probably does not consume/eliminate
"atom (x::var) ♯ Γ"
Yes, but formulating the goal like this is annoying to prove because of the extra implication
"(Γ , Δ ⊢ e : τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ e)) ∧ (Alts Γ Δ T σs τ1 alts τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ alts))"
I guess it can't be helped
You could define a new induction rule that consumes the assumption and puts it into the hypothesis. Doesn't make sense for a one-off though.
induction normally work without consuming all the facts as well, right?
section ‹Abelian Groups›
definition minus:: "'a ⇒ 'a ⇒ 'a" (infixl "‐" 70)
where "x ‐ y ≡ x ⋅ inverse y "
lemma vsdf:"x ⋅ y = 𝟭 ⟹ x = inverse y"
assume xg:"x ∈ G" and yg:"y ∈ G"" x ⋅ y = 𝟭"
from this have "y ⋅ x = 𝟭" by (simp add: commutative)
from this and xg and yg show"x = inverse y" by (simp add:inverse_equality)
end (* abelian_group*)
can someone help me with why it indicates:
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(x ∈ G) ⟹
(y ∈ G) ⟹ (x ⋅ y = 𝟭) ⟹ x = local.inverse y
when I use "show" in the last line but it's ok if "show" is replaced by "have"?
(Note: if you're just interested in the group, you'll want
comm_group instead. The
abelian_group locale talks about the additive group of a ring)
(also, paste your code inside
```isabelle ... ```
to make it look nice and preserve indentation)
okay now that I've loaded up Isabelle with HOL-Algebra it seems that you're defining your own
abelian_group locale. Leaving aside why you'd want to do that, there isn't really a good way to check the code out locally and poke around...
anyway, this error usually means that you
assumed something that isn't part of the goal
you shouldn't need
unfold_locales unless you're proving a statement with the shape
fundamentally, the issue is that your
yg assumptions are unfounded, I think. You might be interested in how
HOL-Algebra solves this problem: https://github.com/NieDzejkob/isabelle-math-contests/blob/master/NOTES.md#the-two-definitions-of-a-group
also, some Isar style tips:
from this have =
from this and xg and yg show =
with xg and yg show or
with xg yg show
I found something very interesting but strange is that: when I add [ x \<in > G; y \<in> G] into the lemma, it works. but why does Isabelle think it reasonable when I state nothing like [ x \<in > G; y \<in> G]? I always think when I state x \<cdot> y, it should indicate [ x \<in > G; y \<in> G].......
why would it automatically assume
x \<in> G?
because \<cdot> should be the type"G -> G -> G" when it was initialized, isabelle should infer x \<in> G
Every expression in Isabelle has some type, and if you don't specify it (for example with
fixes a :: nat and S :: "nat set" in the lemma statement), the most general type will be inferred (in a lemma, based on its statement. For example
a :: 'a and
S :: 'a set, for any type variable
G is not a type here, but a set — simply, a value of type
'something set. The multiplication is defined (like all functions in HOL) on an entire type, not just a set.
ok. I am a bit clear with that. so it's the same reason why we need to clarify the type (1::nat) + 1?
yeah, kinda — inference will give both your
1s the type
'a with a sort constraint
BTW, are you creating your own algebra library because you're unaware of the existing one, or on purpose as practice?
the situation is more closed to practice but I still wanna refer that lemma in another file
what is the difference between unfolding and using
unfolding some_fact where
some_fact is of the form
A = B will replace all occurences of
B in your goal before running the tactic.
using will simply pass on the fact to the tactic. They have quite a similar effect if you're using, for example,
Last updated: Sep 25 2022 at 23:25 UTC