# Re: [isabelle] Congruence rule for Let

```Hi Andreas,

```
using the function package, I'd like to define a function whose definition contains a number of Let expressions. In the generated induction rule, a term "Let t (%x. y)" yields the induction hypothesis "!!x. x = t ==> P (y x)" However, I would like to get "P (y t)" directly. How do I have to change the congruence rule for Let to achieve this?
```
I tried two alternatives with fundef_cong:
- "[| M = N; f N = g N |] ==> Let M f = Let N g" raises an exception:

*** exception THM 1 raised (line 421 of "drule.ML"): COMP
*** At command "function".

```
- "[| M = N; f M = g N |] ==> Let M f = Let N g" eliminates the quantifier, but produces far to many induction hypotheses.
```
What is the right congruence rule for this?
```
```
```
Actually, I had expected that the first rule works. I need to dig into this again. The rule that should definitely work is the following
```
"f M = g N ==> Let M f = Let N g"

```
It has the same effect on the induction rule as unfolding all lets. Can you try if it works for your function?
```
Jeremy Dawson wrote:
```
```This seems easy enough using the functions in ch 5 of the Reference Manual

val iax = "!!x. x = t ==> P (y x)" : Thm.thm
```
```val ax' = forall_elim_var 0 iax ;
```
```val ax' = "?x = t ==> P (y ?x)" : Thm.thm
```
```refl RS ax' ;
```
val it = "P (y t)" : Thm.thm
The ind.hyp. Andreas is referring to appears nested inside the induction rule, where it cannot be easily manipulated by hand...
```
Alex

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.