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. `rule`

.

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 `and`

.

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.

But `induct`

/`induction`

normally work without consuming all the facts as well, right?

section ‹Abelian Groups›

context abelian_group

begin

definition minus:: "'a ⇒ 'a ⇒ 'a" (infixl "‐" 70)

where "x ‐ y ≡ x ⋅ inverse y "

lemma vsdf:"x ⋅ y = 𝟭 ⟹ x = inverse y"

proof(unfold_locales,auto)

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)

qed

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 `assume`

d something that isn't part of the goal

you shouldn't need `unfold_locales`

unless you're proving a statement with the shape `locale_name some_object`

fundamentally, the issue is that your `xg`

and `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`

= `hence`

; `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 `'a`

). However, `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 `1`

s the type `'a`

with a sort constraint `'a::{plus, and_probably_something_else_I_forget}`

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 `A`

with `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, `by simp`

Last updated: Sep 25 2022 at 23:25 UTC