I am trying to solve a rather simple proof goal with a ML tactic. My goal has the form:

```
⋀x f1 f2 g1 g2. (⋀z1. z1 ∈ set1_sum2 x ⟹ f1 z1 = g1 z1) ⟹ (⋀z2. z2 ∈ set2_sum2 x ⟹ f2 z2 = g2 z2) ⟹ map_sum2 f1 f2 x = map_sum2 g1 g2 x
```

and I have a theorem of the form

```
(⋀z1. z1 ∈ set1_sum2 ?x ⟹ ?f1.0 z1 = ?g1.0 z1) ⟹ (⋀z2. z2 ∈ set2_sum2 ?x ⟹ ?f2.0 z2 = ?g2.0 z2) ⟹ map_sum2 ?f1.0 ?f2.0 ?x = map_sum2 ?g1.0 ?g2.0 ?x
```

So I need to instanciate the schematic variables of the theorem with the forall bound variables of the goal. I can get the bound variables with `Subgoal.SUBPROOF`

, but I have no idea what the ML equivalent of the lowercase `of`

is

In this case, just resolving (resolve_tac) with the theorem should instantiate the schematic variables correctly.

After the resolution step, Goal.assume_rule_tac (which is different from assume_tac in that it follows ==> recursively) should be able to solve the remaining subgoals.

To answer you actual question: `infer_instantiate`

is an equivalent of `where`

and `infer_instantiate'`

of `of`

.

Indeed, this works:

```
apply (tactic ‹resolve_tac @{context} [BNF_Def.map_cong0_of_bnf a] 1
THEN REPEAT (Goal.assume_rule_tac @{context} 1)›)
```

Jan van Brügge has marked this topic as resolved.

Last updated: Nov 11 2024 at 04:22 UTC