# [isabelle] recdef hint ignored

```The recdef matchE below fails with:

```
*** matchE (a, b) \<and> matchE (b, a) \<and> e = Diff x y \<longrightarrow>
```*** Suc (depthE x + depthE y) < depthE e + (depthE a + depthE b)
```
*** 1. matchE (a, b) \<and> matchE (b, a) \<and> e = Diff x y \<longrightarrow>
```***     Suc (depthE x + depthE y) < depthE e + (depthE a + depthE b)
*** 1 unsolved goals!
*** Proof failed!
*** At command "recdef".

```
despite lemma depth2E_bg_1 being a recdef-hint, stating the truth of this very subgoal. I'm puzzled that the depth2E_bg_1 lemma isn't taken into account in the recdef proof.
```
```
How can I help the system prove the above subgoal, or how do I ensure the hint is effective?
```
Thanks,
- Reto

theory idc = List:

types
element = "nat"
path = "element list"

```
consts inOrEq :: "path \<Rightarrow> path \<Rightarrow> bool" (* (infix "\<subseteq>" 500) *)
```primrec
```
"inOrEq [] q = (case q of [] \<Rightarrow> True (* * in * *) | y#ys \<Rightarrow> False)" (* * in a* *) "inOrEq (x#xs) q = (case q of [] \<Rightarrow> True (* a* in * *) | y#ys \<Rightarrow> (x = y) & (inOrEq xs ys))"
```
types
node = "path \<times> element"

consts path :: "node \<Rightarrow> path"
primrec
"path (p,n) = p"

consts node :: "node \<Rightarrow> element"
primrec
"node (p,n) = n"

constdefs
eqN :: "node \<Rightarrow> node \<Rightarrow> bool"
"eqN a b == a = b"

datatype expr = Empty
| Node node
```
| Descendents path (* a.b.* translates to Descendents [a,b] *)
```              | Children path (* a.b.# translates to Children [a,b] *)
| Sum expr expr
| Diff expr expr

```
consts depthE :: "expr \<Rightarrow> nat" (* helper for termination proof of matchE *)
```primrec
"depthE (Empty)         = 1"
"depthE (Node x)        = 1"
"depthE (Descendents x) = 1"
"depthE (Children x)    = 1"
"depthE (Sum x y)       = (depthE x) + (depthE y)"
"depthE (Diff x y)      = (depthE x) + (depthE y)"

lemma depthE_bg_0: "0 < depthE e"
apply (induct_tac e)
apply simp_all
done

lemma depth2E_bg_1:
"matchE (a,b) \<and> matchE (b,a) \<and> e = Diff x y
```
\<longrightarrow> Suc (depthE x + depthE y) < depthE e + (depthE a + depthE b)"
```  apply (rule impI)
apply simp
apply (induct_tac a)
done

consts matchE :: "expr \<times> expr \<Rightarrow> bool"
recdef matchE "measure (\<lambda>(e1,e2). depthE e1 + depthE e2)"
"matchE (e,(Empty)) = (case e of
Empty         \<Rightarrow> True
| Node x        \<Rightarrow> False
| Descendents x \<Rightarrow> False
| Children x    \<Rightarrow> False
```
| Sum x y \<Rightarrow> matchE (x, Empty)
```                                            & matchE (y, Empty)
| Diff x y      \<Rightarrow>   matchE (y, x)
| matchE (x, Empty))"
"matchE (e,(Node n)) = (case e of
Empty         \<Rightarrow> True
| Node x        \<Rightarrow> eqN n x
| Descendents x \<Rightarrow> False
| Children x    \<Rightarrow> False
```
| Sum x y \<Rightarrow> matchE (x, Node n)
```                                             & matchE (x, Node n)
```
| Diff x y \<Rightarrow> matchE (x, Node n)
```                                             & ~matchE (Node n, y))"
"matchE (e,(Descendents p)) = (case e of
Empty         \<Rightarrow> True
```
| Node (q,m) \<Rightarrow> inOrEq q p
```                                | Descendents x \<Rightarrow> p = x
```
| Children x \<Rightarrow> inOrEq x p | Sum x y \<Rightarrow> matchE (x, Descendents p) & matchE (x, Descendents p) | Diff x y \<Rightarrow> matchE (x, Descendents p) & ~matchE (Descendents p, y))"
```  "matchE (e,(Children p)) = (case e of
Empty          \<Rightarrow> True
| Node (q,m)     \<Rightarrow> p = q
| Descendents x  \<Rightarrow> False
| Children x     \<Rightarrow> p = x
```
| Sum x y \<Rightarrow> matchE (x, Children p) & matchE (x, Children p) | Diff x y \<Rightarrow> matchE (x, Children p) & ~matchE (Children p, y))"
```  "matchE (e,(Sum a b)) = (case e of
Empty         \<Rightarrow> True
```
| Node x \<Rightarrow> (matchE (e,a))|(matchE (e,b)) | Descendents x \<Rightarrow> (matchE (e,a))|(matchE (e,b)) | Children x \<Rightarrow> (matchE (e,a))|(matchE (e,b)) | Sum x y \<Rightarrow> matchE (x, Sum a b)
```                                               & matchE (y, Sum a b)
```
| Diff x y \<Rightarrow> matchE (Diff x y, a) | matchE (Diff x y, b))"
```  "matchE (e,(Diff a b)) = (case e of
Empty         \<Rightarrow> True
```
| Node x \<Rightarrow> (matchE (e,a))&~(matchE (e,b)) | Descendents x \<Rightarrow> (matchE (e,a))&~(matchE (e,b)) | Children x \<Rightarrow> (matchE (e,a))&~(matchE (e,b)) | Sum x y \<Rightarrow> matchE (Sum x y, a)
```                                               & ~matchE (Sum x y, b)
| Diff x y      \<Rightarrow>
(if (matchE (a,b) & matchE (b,a))
then matchE (Diff x y, Empty)
else   matchE (Diff x y, a)
& ~matchE (Diff x y, b)))"
(hints recdef_simp: depth2E_bg_1 depthE_bg_0)

```

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